set Y = { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } ;
reconsider X = (SepQuadruples F2()) /\ { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] } as Subset of [:(CQC-WFF F1()),(QC-symbols F1()),(Fin (bound_QC-variables F1())),(Funcs ((bound_QC-variables F1()),(bound_QC-variables F1()))):] ;
A5:
SepQuadruples F2() is_Sep-closed_on F2()
by Def13;
X is_Sep-closed_on F2()
proof
A6:
[F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
by A1;
[F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in SepQuadruples F2()
by Th30;
hence
[F2(),(index F2()),({}. (bound_QC-variables F1())),(id (bound_QC-variables F1()))] in X
by A6, XBOOLE_0:def 4;
CQC_SIM1:def 12 ( ( for q being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) )
thus
for
q being
Element of
CQC-WFF F1()
for
t being
QC-symbol of
F1()
for
K being
Element of
Fin (bound_QC-variables F1()) for
f being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1())) st
[('not' q),t,K,f] in X holds
[q,t,K,f] in X
( ( for q, r being Element of CQC-WFF F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) )proof
let q be
Element of
CQC-WFF F1();
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in Xlet t be
QC-symbol of
F1();
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in Xlet K be
Element of
Fin (bound_QC-variables F1());
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in X holds
[q,t,K,f] in Xlet f be
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()));
( [('not' q),t,K,f] in X implies [q,t,K,f] in X )
assume A7:
[('not' q),t,K,f] in X
;
[q,t,K,f] in X
then A8:
[('not' q),t,K,f] in SepQuadruples F2()
by XBOOLE_0:def 4;
[('not' q),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
by A7, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF F1(),
L being
Element of
Fin (bound_QC-variables F1()),
u being
QC-symbol of
F1(),
h being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()))
such that A9:
[('not' q),t,K,f] = [p,u,L,h]
and A10:
P1[
p,
u,
L,
h]
;
A11:
t = u
by A9, XTUPLE_0:5;
A12:
f = h
by A9, XTUPLE_0:5;
A13:
K = L
by A9, XTUPLE_0:5;
'not' q = p
by A9, XTUPLE_0:5;
then
P1[
q,
t,
K,
f]
by A2, A8, A10, A11, A13, A12;
then A14:
[q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
;
[q,t,K,f] in SepQuadruples F2()
by A5, A8;
hence
[q,t,K,f] in X
by A14, XBOOLE_0:def 4;
verum
end;
thus
for
q,
r being
Element of
CQC-WFF F1()
for
t being
QC-symbol of
F1()
for
K being
Element of
Fin (bound_QC-variables F1()) for
f being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1())) st
[(q '&' r),t,K,f] in X holds
(
[q,t,K,f] in X &
[r,(t + (QuantNbr q)),K,f] in X )
for q being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Xproof
let q,
r be
Element of
CQC-WFF F1();
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )let t be
QC-symbol of
F1();
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )let K be
Element of
Fin (bound_QC-variables F1());
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )let f be
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()));
( [(q '&' r),t,K,f] in X implies ( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) )
assume A15:
[(q '&' r),t,K,f] in X
;
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X )
then A16:
[(q '&' r),t,K,f] in SepQuadruples F2()
by XBOOLE_0:def 4;
then A17:
[r,(t + (QuantNbr q)),K,f] in SepQuadruples F2()
by A5;
[(q '&' r),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
by A15, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF F1(),
L being
Element of
Fin (bound_QC-variables F1()),
u being
QC-symbol of
F1(),
h being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()))
such that A18:
[(q '&' r),t,K,f] = [p,u,L,h]
and A19:
P1[
p,
u,
L,
h]
;
A20:
t = u
by A18, XTUPLE_0:5;
A21:
f = h
by A18, XTUPLE_0:5;
A22:
K = L
by A18, XTUPLE_0:5;
A23:
q '&' r = p
by A18, XTUPLE_0:5;
then
P1[
q,
t,
K,
f]
by A3, A16, A19, A20, A22, A21;
then A24:
[q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
;
P1[
r,
t + (QuantNbr q),
K,
f]
by A3, A16, A19, A23, A20, A22, A21;
then A25:
[r,(t + (QuantNbr q)),K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
;
[q,t,K,f] in SepQuadruples F2()
by A5, A16;
hence
(
[q,t,K,f] in X &
[r,(t + (QuantNbr q)),K,f] in X )
by A24, A25, A17, XBOOLE_0:def 4;
verum
end;
let q be
Element of
CQC-WFF F1();
for x being Element of bound_QC-variables F1()
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Xlet x be
bound_QC-variable of
F1();
for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Xlet t be
QC-symbol of
F1();
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Xlet K be
Element of
Fin (bound_QC-variables F1());
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Xlet f be
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()));
( [(All (x,q)),t,K,f] in X implies [q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X )
assume A26:
[(All (x,q)),t,K,f] in X
;
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
then A27:
[(All (x,q)),t,K,f] in SepQuadruples F2()
by XBOOLE_0:def 4;
f +* (x .--> (x. t)) is
Function of
(bound_QC-variables F1()),
(bound_QC-variables F1())
by Lm1;
then reconsider g =
f +* (x .--> (x. t)) as
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()))
by FUNCT_2:8;
[(All (x,q)),t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
by A26, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF F1(),
L being
Element of
Fin (bound_QC-variables F1()),
u being
QC-symbol of
F1(),
h being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1()))
such that A28:
[(All (x,q)),t,K,f] = [p,u,L,h]
and A29:
P1[
p,
u,
L,
h]
;
A30:
t = u
by A28, XTUPLE_0:5;
A31:
f = h
by A28, XTUPLE_0:5;
A32:
K = L
by A28, XTUPLE_0:5;
All (
x,
q)
= p
by A28, XTUPLE_0:5;
then
P1[
q,
t ++ ,
K \/ {x},
g]
by A4, A27, A29, A30, A32, A31;
then A33:
[q,(t ++),(K \/ {.x.}),(f +* (x .--> (x. t)))] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
;
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in SepQuadruples F2()
by A5, A27;
hence
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X
by A33, XBOOLE_0:def 4;
verum
end;
then A34:
SepQuadruples F2() c= X
by Def13;
let q be Element of CQC-WFF F1(); for t being QC-symbol of F1()
for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let t be QC-symbol of F1(); for K being Element of Fin (bound_QC-variables F1())
for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let K be Element of Fin (bound_QC-variables F1()); for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds
P1[q,t,K,f]
let f be Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())); ( [q,t,K,f] in SepQuadruples F2() implies P1[q,t,K,f] )
assume
[q,t,K,f] in SepQuadruples F2()
; P1[q,t,K,f]
then
[q,t,K,f] in { [s,v,M,g] where s is Element of CQC-WFF F1(), M is Element of Fin (bound_QC-variables F1()), v is QC-symbol of F1(), g is Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) : P1[s,v,M,g] }
by A34, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF F1(), L being Element of Fin (bound_QC-variables F1()), u being QC-symbol of F1(), h being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) such that
A35:
[q,t,K,f] = [p,u,L,h]
and
A36:
P1[p,u,L,h]
;
A37:
t = u
by A35, XTUPLE_0:5;
A38:
K = L
by A35, XTUPLE_0:5;
q = p
by A35, XTUPLE_0:5;
hence
P1[q,t,K,f]
by A35, A36, A37, A38, XTUPLE_0:5; verum