:: deftheorem Def5 defines ATOMIC CQC_SIM1:def 5 :
for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A
for l being CQC-variable_list of k,A
for b₅ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₅ = ATOMIC (P,l) iff for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b₅ . (t,h) = P ! (h * l) );