:: deftheorem Def7 defines SepFunc CQC_SIM1:def 7 :
for A being QC-alphabet
for b₂ being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) holds
( b₂ = SepFunc A iff ( b₂ . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds b₂ . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( b₂ . ('not' r) = NEGATIVE (b₂ . r) & b₂ . (r '&' s) = CON ((b₂ . r),(b₂ . s),(QuantNbr r)) & b₂ . (All (x,r)) = UNIVERSAL (x,(b₂ . r)) ) ) ) );