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:57;
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:57;
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:57;
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