theorem Th34:
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 ) ) )