:: deftheorem Def6 defines QuantNbr CQC_SIM1:def 6 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for b₃ being Element of NAT holds
( b₃ = QuantNbr p iff ex F being Function of (CQC-WFF A),NAT st
( b₃ = 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) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) );