let A be QC-alphabet ; :: thesis: 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 .: (still_not-bound_in p) holds
u < t
let t, u be QC-symbol of A; :: thesis: 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 .: (still_not-bound_in p) holds
u < t
let p, q be Element of CQC-WFF A; :: thesis: 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 .: (still_not-bound_in p) holds
u < t
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) holds
u < t
let K be Element of Fin (bound_QC-variables A); :: thesis: ( [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) implies u < t )
defpred S₁[ 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 .: (still_not-bound_in p) holds
u < $2;

A1: now :: thesis: 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 & S₁[q '&' r,v,K,f] holds
( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] )

let q, r be Element of CQC-WFF A; :: thesis: 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 & S₁[q '&' r,v,K,f] holds
( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] )
let v 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),v,K,f] in SepQuadruples p & S₁[q '&' r,v,K,f] holds
( S₁[q,v,K,f] & S₁[r,v + (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),v,K,f] in SepQuadruples p & S₁[q '&' r,v,K,f] holds
( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] )
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(q '&' r),v,K,f] in SepQuadruples p & S₁[q '&' r,v,K,f] implies ( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] ) )
assume [(q '&' r),v,K,f] in SepQuadruples p ; :: thesis: ( S₁[q '&' r,v,K,f] implies ( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] ) )
assume A2: S₁[q '&' r,v,K,f] ; :: thesis: ( S₁[q,v,K,f] & S₁[r,v + (QuantNbr q),K,f] )
hence S₁[q,v,K,f] ; :: thesis: S₁[r,v + (QuantNbr q),K,f]
thus S₁[r,v + (QuantNbr q),K,f] :: thesis: verum

proof

let u be QC-symbol of A; :: thesis: ( x. u in f .: (still_not-bound_in p) implies u < v + (QuantNbr q) )
A3: v <= v + (QuantNbr q) by QC_LANG1:31;
assume x. u in f .: (still_not-bound_in p) ; :: thesis: u < v + (QuantNbr q)
hence u < v + (QuantNbr q) by A2, A3, QC_LANG1:30; :: thesis: verum

end;

end;

A4: S₁[p, index p, {}. (bound_QC-variables A), id (bound_QC-variables A)]

proof

let u be QC-symbol of A; :: thesis: ( x. u in (id (bound_QC-variables A)) .: (still_not-bound_in p) implies u < index p )
assume A5: x. u in (id (bound_QC-variables A)) .: (still_not-bound_in p) ; :: thesis: u < index p
(id (bound_QC-variables A)) .: (still_not-bound_in p) = still_not-bound_in p by FUNCT_1:92;
hence u < index p by A5, Th21; :: thesis: verum

end;

A6: now :: thesis: 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 & S₁[ All (x,q),v,K,f] holds
S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]

let q be Element of CQC-WFF A; :: thesis: 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 & S₁[ All (x,q),v,K,f] holds
S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]
let x be Element of bound_QC-variables A; :: thesis: 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 & S₁[ All (x,q),v,K,f] holds
S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]
let v 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)),v,K,f] in SepQuadruples p & S₁[ All (x,q),v,K,f] holds
S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]
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)),v,K,f] in SepQuadruples p & S₁[ All (x,q),v,K,f] holds
S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,q)),v,K,f] in SepQuadruples p & S₁[ All (x,q),v,K,f] implies S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))] )
assume [(All (x,q)),v,K,f] in SepQuadruples p ; :: thesis: ( S₁[ All (x,q),v,K,f] implies S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))] )
assume A7: S₁[ All (x,q),v,K,f] ; :: thesis: S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))]
thus S₁[q,v ++ ,K \/ {.x.},f +* (x .--> (x. v))] :: thesis: verum

proof

let u be QC-symbol of A; :: thesis: ( x. u in (f +* (x .--> (x. v))) .: (still_not-bound_in p) implies u < v ++ )
assume A8: x. u in (f +* (x .--> (x. v))) .: (still_not-bound_in p) ; :: thesis: u < v ++
(f +* (x .--> (x. v))) .: (still_not-bound_in p) c= (f .: (still_not-bound_in p)) \/ {(x. v)} by Th2;
then ( x. u in f .: (still_not-bound_in p) or x. u in {(x. v)} ) by A8, XBOOLE_0:def 3;
then ( u < v or x. u = x. v ) by A7, TARSKI:def 1;
then ( u < v or u = v ) by XTUPLE_0:1;
then ( u <= v & v < v ++ ) by QC_LANG1:22, QC_LANG1:27, QC_LANG1:def 34;
hence u < v ++ by QC_LANG1:29; :: thesis: verum

end;

end;

A9: 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 & S₁[ 'not' q,v,K,f] holds
S₁[q,v,K,f] ;
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
S₁[q,v,K,f] from CQC_SIM1:sch 6(A4, A9, A1, A6);
hence ( [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) implies u < t ) ; :: thesis: verum