let A be QC-alphabet ; for t, u 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) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds
u < t
let t, u be 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) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds
u < t
let p, q be 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) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds
u < t
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds
u < t
let K be Element of Fin (bound_QC-variables A); ( [q,t,K,f] in SepQuadruples p & x. u in f .: K implies u < t )
defpred S1[ Element of CQC-WFF A, QC-symbol of A, Element of Fin (bound_QC-variables A), Function] means for u being QC-symbol of A st x. u in $4 .: $3 holds
u < $2;
A1:
for q being Element of CQC-WFF A
for v 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),v,K,f] in SepQuadruples p & S1[ 'not' q,v,K,f] holds
S1[q,v,K,f]
;
A2:
now for q, r being Element of CQC-WFF A
for v 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),v,K,f] in SepQuadruples p & S1[q '&' r,v,K,f] holds
( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] )let q,
r be
Element of
CQC-WFF A;
for v 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),v,K,f] in SepQuadruples p & S1[q '&' r,v,K,f] holds
( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] )let v be
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),v,K,f] in SepQuadruples p & S1[q '&' r,v,K,f] holds
( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] )let K be
Element of
Fin (bound_QC-variables A);
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),v,K,f] in SepQuadruples p & S1[q '&' r,v,K,f] holds
( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] )let f be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(q '&' r),v,K,f] in SepQuadruples p & S1[q '&' r,v,K,f] implies ( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] ) )assume
[(q '&' r),v,K,f] in SepQuadruples p
;
( S1[q '&' r,v,K,f] implies ( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] ) )assume A3:
S1[
q '&' r,
v,
K,
f]
;
( S1[q,v,K,f] & S1[r,v + (QuantNbr q),K,f] )hence
S1[
q,
v,
K,
f]
;
S1[r,v + (QuantNbr q),K,f]thus
S1[
r,
v + (QuantNbr q),
K,
f]
verum end;
A5:
now for q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for v 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)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] holds
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]let q be
Element of
CQC-WFF A;
for x being Element of bound_QC-variables A
for v 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)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] holds
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]let x be
Element of
bound_QC-variables A;
for v 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)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] holds
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]let v be
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)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] holds
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]let K be
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)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] holds
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]let f be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(All (x,q)),v,K,f] in SepQuadruples p & S1[ All (x,q),v,K,f] implies S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))] )assume
[(All (x,q)),v,K,f] in SepQuadruples p
;
( S1[ All (x,q),v,K,f] implies S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))] )assume A6:
S1[
All (
x,
q),
v,
K,
f]
;
S1[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]thus
S1[
q,
v ++ ,
K \/ {.x.},
f +* (x .--> (x. v))]
verum end;
A8:
S1[p, index p, {}. (bound_QC-variables A), id (bound_QC-variables A)]
;
for q being Element of CQC-WFF A
for v 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,v,K,f] in SepQuadruples p holds
S1[q,v,K,f]
from CQC_SIM1:sch 6(A8, A1, A2, A5);
hence
( [q,t,K,f] in SepQuadruples p & x. u in f .: K implies u < t )
; verum