theorem Th34: :: CQC_SIM1:34

for A being QC-alphabet
for t being QC-symbol of A
for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) holds
( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )