let A be QC-alphabet ; for t 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) holds
( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
let t be 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) holds
( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
let p, q be 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) holds
( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); for K being Element of Fin (bound_QC-variables A) holds
( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
let K be Element of Fin (bound_QC-variables A); ( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
assume that
A1:
[q,t,K,f] in SepQuadruples p
and
A2:
[q,t,K,f] <> [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]
and
A3:
not [('not' q),t,K,f] in SepQuadruples p
and
A4:
for r being Element of CQC-WFF A holds not [(q '&' r),t,K,f] in SepQuadruples p
and
A5:
for r being Element of CQC-WFF A
for u being QC-symbol of A holds
( not t = u + (QuantNbr r) or not [(r '&' q),u,K,f] in SepQuadruples p )
and
A6:
for x being Element of bound_QC-variables A
for u being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds
( not u ++ = t or not h +* ({x} --> (x. u)) = f or ( not [(All (x,q)),u,K,h] in SepQuadruples p & not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) )
; contradiction
reconsider Y = (SepQuadruples p) \ {[q,t,K,f]} as Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] ;
A7:
SepQuadruples p is_Sep-closed_on p
by Def13;
A8:
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 Y holds
[q,t,K,f] in Y
proof
let s 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' s),t,K,f] in Y holds
[s,t,K,f] in Ylet u 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' s),u,K,f] in Y holds
[s,u,K,f] in Ylet L be
Element of
Fin (bound_QC-variables A);
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' s),u,L,f] in Y holds
[s,u,L,f] in Ylet h be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [('not' s),u,L,h] in Y implies [s,u,L,h] in Y )
assume A9:
[('not' s),u,L,h] in Y
;
[s,u,L,h] in Y
then
(
s <> q or
u <> t or
L <> K or
f <> h )
by A3, XBOOLE_0:def 5;
then A10:
[s,u,L,h] <> [q,t,K,f]
by XTUPLE_0:5;
[('not' s),u,L,h] in SepQuadruples p
by A9, XBOOLE_0:def 5;
then
[s,u,L,h] in SepQuadruples p
by A7;
hence
[s,u,L,h] in Y
by A10, ZFMISC_1:56;
verum
end;
A11:
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 Y holds
( [q,t,K,f] in Y & [r,(t + (QuantNbr q)),K,f] in Y )
proof
let s,
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 [(s '&' r),t,K,f] in Y holds
( [s,t,K,f] in Y & [r,(t + (QuantNbr s)),K,f] in Y )let u 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 [(s '&' r),u,K,f] in Y holds
( [s,u,K,f] in Y & [r,(u + (QuantNbr s)),K,f] in Y )let L be
Element of
Fin (bound_QC-variables A);
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(s '&' r),u,L,f] in Y holds
( [s,u,L,f] in Y & [r,(u + (QuantNbr s)),L,f] in Y )let h be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(s '&' r),u,L,h] in Y implies ( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y ) )
assume
[(s '&' r),u,L,h] in Y
;
( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y )
then A12:
[(s '&' r),u,L,h] in SepQuadruples p
by XBOOLE_0:def 5;
then
(
s <> q or
u <> t or
L <> K or
f <> h )
by A4;
then A13:
[s,u,L,h] <> [q,t,K,f]
by XTUPLE_0:5;
[s,u,L,h] in SepQuadruples p
by A7, A12;
hence
[s,u,L,h] in Y
by A13, ZFMISC_1:56;
[r,(u + (QuantNbr s)),L,h] in Y
(
r <> q or
L <> K or
f <> h or
u + (QuantNbr s) <> t )
by A5, A12;
then A14:
[r,(u + (QuantNbr s)),L,h] <> [q,t,K,f]
by XTUPLE_0:5;
[r,(u + (QuantNbr s)),L,h] in SepQuadruples p
by A7, A12;
hence
[r,(u + (QuantNbr s)),L,h] in Y
by A14, ZFMISC_1:56;
verum
end;
A15:
Y c= SepQuadruples p
by XBOOLE_1:36;
A16:
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 Y holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y
proof
let s 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,s)),t,K,f] in Y holds
[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Ylet 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,s)),t,K,f] in Y holds
[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Ylet u 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,s)),u,K,f] in Y holds
[s,(u ++),(K \/ {x}),(f +* (x .--> (x. u)))] in Ylet L 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,s)),u,L,f] in Y holds
[s,(u ++),(L \/ {x}),(f +* (x .--> (x. u)))] in Ylet h be
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A));
( [(All (x,s)),u,L,h] in Y implies [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y )
assume A17:
[(All (x,s)),u,L,h] in Y
;
[s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y
now ( not [(All (x,q)),u,K,h] in SepQuadruples p & not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p & s = q implies not L \/ {x} = K )assume that A18:
not
[(All (x,q)),u,K,h] in SepQuadruples p
and A19:
not
[(All (x,q)),u,(K \ {x}),h] in SepQuadruples p
;
( s = q implies not L \/ {x} = K )A20:
(
s <> q or (
L <> K &
L <> K \ {x} ) )
by A17, A18, A19, XBOOLE_0:def 5;
assume A21:
s = q
;
not L \/ {x} = Kassume A22:
L \/ {x} = K
;
contradictionthen
K \ {x} = L \ {x}
by XBOOLE_1:40;
hence
contradiction
by A20, A21, A22, ZFMISC_1:40, ZFMISC_1:57;
verum end;
then
(
s <> q or
u ++ <> t or
L \/ {x} <> K or
f <> h +* ({x} --> (x. u)) )
by A6;
then A23:
[s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] <> [q,t,K,f]
by XTUPLE_0:5;
[(All (x,s)),u,L,h] in SepQuadruples p
by A17, XBOOLE_0:def 5;
then
[s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in SepQuadruples p
by A7;
hence
[s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y
by A23, ZFMISC_1:56;
verum
end;
[p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in SepQuadruples p
by A7;
then
[p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in Y
by A2, ZFMISC_1:56;
then
Y is_Sep-closed_on p
by A8, A11, A16;
then
SepQuadruples p c= Y
by Def13;
then
Y = SepQuadruples p
by A15;
hence
contradiction
by A1, ZFMISC_1:57; verum