let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

let p be Element of CQC-WFF A; :: thesis: for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

deffunc H_{5}( QC-formula of A) -> Element of bool (bound_QC-variables A) = still_not-bound_in $1;

defpred S_{1}[ QC-formula of A, set , set , set ] means H_{5}($1) c= H_{5}(p) \/ $3;

A1: for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in SepQuadruples p & S_{1}[ 'not' q,t,K,f] holds

S_{1}[q,t,K,f]
by QC_LANG3:7;

_{1}[p, index p, {}. (bound_QC-variables A), id (bound_QC-variables A)]
;

thus for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

S_{1}[q,t,K,f]
from CQC_SIM1:sch 6(A8, A1, A2, A6); :: thesis: verum

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

let p be Element of CQC-WFF A; :: thesis: for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

deffunc H

defpred S

A1: for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in SepQuadruples p & S

S

A2: now :: thesis: for q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S_{1}[q '&' r,t,K,f] holds

( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S

( S

let q, r be Element of CQC-WFF A; :: thesis: for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S_{1}[q '&' r,t,K,f] holds

( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )

let t be QC-symbol of A; :: thesis: for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S_{1}[q '&' r,t,K,f] holds

( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )

let K be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S_{1}[q '&' r,t,K,f] holds

( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(q '&' r),t,K,f] in SepQuadruples p & S_{1}[q '&' r,t,K,f] implies ( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] ) )

assume that

[(q '&' r),t,K,f] in SepQuadruples p and

A3: S_{1}[q '&' r,t,K,f]
; :: thesis: ( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )

A4: still_not-bound_in (q '&' r) = (still_not-bound_in q) \/ (still_not-bound_in r) by QC_LANG3:10;

then A5: still_not-bound_in r c= still_not-bound_in (q '&' r) by XBOOLE_1:7;

still_not-bound_in q c= still_not-bound_in (q '&' r) by A4, XBOOLE_1:7;

hence ( S_{1}[q,t,K,f] & S_{1}[r,t + (QuantNbr q),K,f] )
by A3, A5, XBOOLE_1:1; :: thesis: verum

end;for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S

( S

let t be QC-symbol of A; :: thesis: for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S

( S

let K be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S

( S

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(q '&' r),t,K,f] in SepQuadruples p & S

assume that

[(q '&' r),t,K,f] in SepQuadruples p and

A3: S

A4: still_not-bound_in (q '&' r) = (still_not-bound_in q) \/ (still_not-bound_in r) by QC_LANG3:10;

then A5: still_not-bound_in r c= still_not-bound_in (q '&' r) by XBOOLE_1:7;

still_not-bound_in q c= still_not-bound_in (q '&' r) by A4, XBOOLE_1:7;

hence ( S

A6: now :: thesis: for q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] holds

S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

A8:
Sfor x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S

S

let q be Element of CQC-WFF A; :: thesis: for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] holds

S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let x be Element of bound_QC-variables A; :: thesis: for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] holds

S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let t be QC-symbol of A; :: thesis: for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] holds

S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let K be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] holds

S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,q)),t,K,f] in SepQuadruples p & S_{1}[ All (x,q),t,K,f] implies S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )

assume that

[(All (x,q)),t,K,f] in SepQuadruples p and

A7: S_{1}[ All (x,q),t,K,f]
; :: thesis: S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

still_not-bound_in (All (x,q)) = (still_not-bound_in q) \ {x} by QC_LANG3:12;

then still_not-bound_in q c= ((still_not-bound_in p) \/ K) \/ {x} by A7, XBOOLE_1:44;

hence S_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
by XBOOLE_1:4; :: thesis: verum

end;for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S

S

let x be Element of bound_QC-variables A; :: thesis: for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S

S

let t be QC-symbol of A; :: thesis: for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S

S

let K be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p & S

S

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,q)),t,K,f] in SepQuadruples p & S

assume that

[(All (x,q)),t,K,f] in SepQuadruples p and

A7: S

still_not-bound_in (All (x,q)) = (still_not-bound_in q) \ {x} by QC_LANG3:12;

then still_not-bound_in q c= ((still_not-bound_in p) \/ K) \/ {x} by A7, XBOOLE_1:44;

hence S

thus for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

S