let A be QC-alphabet ; 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
q is_subformula_of p
let p be Element of CQC-WFF A; 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
q is_subformula_of p
defpred S1[ Element of CQC-WFF A, set , set , set ] means $1 is_subformula_of p;
A1:
now 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 & S1[ 'not' q,t,K,f] holds
S1[q,t,K,f]let q be
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 & S1[ 'not' q,t,K,f] holds
S1[q,t,K,f]let t 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 [('not' q),t,K,f] in SepQuadruples p & S1[ 'not' q,t,K,f] holds
S1[q,t,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 [('not' q),t,K,f] in SepQuadruples p & S1[ 'not' q,t,K,f] holds
S1[q,t,K,f]let f be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [('not' q),t,K,f] in SepQuadruples p & S1[ 'not' q,t,K,f] implies S1[q,t,K,f] )assume
[('not' q),t,K,f] in SepQuadruples p
;
( S1[ 'not' q,t,K,f] implies S1[q,t,K,f] )
q is_subformula_of 'not' q
by Th10;
hence
(
S1[
'not' q,
t,
K,
f] implies
S1[
q,
t,
K,
f] )
by QC_LANG2:57;
verum end;
A2:
now 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 & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]let q be
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 & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]let x be
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 & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]let t 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)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]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)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] holds
S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]let f be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(All (x,q)),t,K,f] in SepQuadruples p & S1[ All (x,q),t,K,f] implies S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )assume
[(All (x,q)),t,K,f] in SepQuadruples p
;
( S1[ All (x,q),t,K,f] implies S1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )
q is_subformula_of All (
x,
q)
by Th12;
hence
(
S1[
All (
x,
q),
t,
K,
f] implies
S1[
q,
t ++ ,
K \/ {x},
f +* (x .--> (x. t))] )
by QC_LANG2:57;
verum end;
A3:
now 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 & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (QuantNbr q),K,f] )let q,
r be
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 & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (QuantNbr q),K,f] )let t 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),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (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),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] holds
( S1[q,t,K,f] & S1[r,t + (QuantNbr q),K,f] )let f be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(q '&' r),t,K,f] in SepQuadruples p & S1[q '&' r,t,K,f] implies ( S1[q,t,K,f] & S1[r,t + (QuantNbr q),K,f] ) )assume
[(q '&' r),t,K,f] in SepQuadruples p
;
( S1[q '&' r,t,K,f] implies ( S1[q,t,K,f] & S1[r,t + (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,
t,
K,
f] implies (
S1[
q,
t,
K,
f] &
S1[
r,
t + (QuantNbr q),
K,
f] ) )
by A4, QC_LANG2:57;
verum end;
A5:
S1[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
S1[q,t,K,f]
from CQC_SIM1:sch 6(A5, A1, A3, A2); verum