let p be Element of CQC-WFF ; for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples p holds
q is_subformula_of p
defpred S1[ Element of CQC-WFF , set , set , set ] means $1 is_subformula_of p;
A1:
now let q be
Element of
CQC-WFF ;
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples p & S1[ 'not' q,k,K,f] holds
S1[q,k,K,f]let k be
Element of
NAT ;
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples p & S1[ 'not' q,k,K,f] holds
S1[q,k,K,f]let K be
Finite_Subset of
bound_QC-variables ;
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples p & S1[ 'not' q,k,K,f] holds
S1[q,k,K,f]let f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
( [('not' q),k,K,f] in SepQuadruples p & S1[ 'not' q,k,K,f] implies S1[q,k,K,f] )assume
[('not' q),k,K,f] in SepQuadruples p
;
( S1[ 'not' q,k,K,f] implies S1[q,k,K,f] )
q is_subformula_of 'not' q
by Th10;
hence
(
S1[
'not' q,
k,
K,
f] implies
S1[
q,
k,
K,
f] )
by QC_LANG2:77;
verum end;
A2:
now let q be
Element of
CQC-WFF ;
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S1[ All x,q,k,K,f] holds
S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))]let x be
Element of
bound_QC-variables ;
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S1[ All x,q,k,K,f] holds
S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))]let k be
Element of
NAT ;
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S1[ All x,q,k,K,f] holds
S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))]let K be
Finite_Subset of
bound_QC-variables ;
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S1[ All x,q,k,K,f] holds
S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))]let f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
( [(All x,q),k,K,f] in SepQuadruples p & S1[ All x,q,k,K,f] implies S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))] )assume
[(All x,q),k,K,f] in SepQuadruples p
;
( S1[ All x,q,k,K,f] implies S1[q,k + 1,K \/ {x},f +* (x .--> (x. k))] )
q is_subformula_of All x,
q
by Th12;
hence
(
S1[
All x,
q,
k,
K,
f] implies
S1[
q,
k + 1,
K \/ {x},
f +* (x .--> (x. k))] )
by QC_LANG2:77;
verum end;
A3:
now let q,
r be
Element of
CQC-WFF ;
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S1[q '&' r,k,K,f] holds
( S1[q,k,K,f] & S1[r,k + (QuantNbr q),K,f] )let k be
Element of
NAT ;
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S1[q '&' r,k,K,f] holds
( S1[q,k,K,f] & S1[r,k + (QuantNbr q),K,f] )let K be
Finite_Subset of
bound_QC-variables ;
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S1[q '&' r,k,K,f] holds
( S1[q,k,K,f] & S1[r,k + (QuantNbr q),K,f] )let f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
( [(q '&' r),k,K,f] in SepQuadruples p & S1[q '&' r,k,K,f] implies ( S1[q,k,K,f] & S1[r,k + (QuantNbr q),K,f] ) )assume
[(q '&' r),k,K,f] in SepQuadruples p
;
( S1[q '&' r,k,K,f] implies ( S1[q,k,K,f] & S1[r,k + (QuantNbr q),K,f] ) )A4:
r is_subformula_of q '&' r
by Th11;
q is_subformula_of q '&' r
by Th11;
hence
(
S1[
q '&' r,
k,
K,
f] implies (
S1[
q,
k,
K,
f] &
S1[
r,
k + (QuantNbr q),
K,
f] ) )
by A4, QC_LANG2:77;
verum end;
A5:
S1[p, index p, {}. bound_QC-variables , id bound_QC-variables ]
;
thus
for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples p holds
S1[q,k,K,f]
from CQC_SIM1:sch 6(A5, A1, A3, A2); verum