let A be QC-alphabet ; for k being Nat
for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0
let k be Nat; for ll being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0
let ll be CQC-variable_list of k,A; for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0
let P be QC-pred_symbol of k,A; QuantNbr (P ! ll) = 0
deffunc H5( Element of CQC-WFF A) -> Element of NAT = QuantNbr $1;
A1:
for p being Element of CQC-WFF A
for d being Element of NAT holds
( d = H5(p) iff ex F being Function of (CQC-WFF A),NAT st
( d = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( F . (P ! l) = H1(k,P,l) & F . ('not' r) = H2(F . r) & F . (r '&' s) = H3(F . r,F . s) & F . (All (x,r)) = H4(x,F . r) ) ) ) )
by Def6;
thus
H5(P ! ll) = H1(k,P,ll)
from CQC_LANG:sch 6(A1); verum