let q, p be Element of CQC-WFF ; :: thesis: for k being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables holds
( not [q,k,K,f] in SepQuadruples p or [q,k,K,f] = [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' q),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF st [(q '&' r),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF ex l being Element of NAT st
( k = l + (QuantNbr r) & [(r '&' q),l,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables ex l being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables st
( l + 1 = k & h +* ({x} --> (x. l)) = f & ( [(All x,q),l,K,h] in SepQuadruples p or [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) ) )
let k be Element of NAT ; :: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables holds
( not [q,k,K,f] in SepQuadruples p or [q,k,K,f] = [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' q),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF st [(q '&' r),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF ex l being Element of NAT st
( k = l + (QuantNbr r) & [(r '&' q),l,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables ex l being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables st
( l + 1 = k & h +* ({x} --> (x. l)) = f & ( [(All x,q),l,K,h] in SepQuadruples p or [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) ) )
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ; :: thesis: for K being Finite_Subset of bound_QC-variables holds
( not [q,k,K,f] in SepQuadruples p or [q,k,K,f] = [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' q),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF st [(q '&' r),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF ex l being Element of NAT st
( k = l + (QuantNbr r) & [(r '&' q),l,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables ex l being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables st
( l + 1 = k & h +* ({x} --> (x. l)) = f & ( [(All x,q),l,K,h] in SepQuadruples p or [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) ) )
let K be Finite_Subset of bound_QC-variables ; :: thesis: ( not [q,k,K,f] in SepQuadruples p or [q,k,K,f] = [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' q),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF st [(q '&' r),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF ex l being Element of NAT st
( k = l + (QuantNbr r) & [(r '&' q),l,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables ex l being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables st
( l + 1 = k & h +* ({x} --> (x. l)) = f & ( [(All x,q),l,K,h] in SepQuadruples p or [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) ) )
assume that
A1:
[q,k,K,f] in SepQuadruples p
and
A2:
[q,k,K,f] <> [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )]
and
A3:
not [('not' q),k,K,f] in SepQuadruples p
and
A4:
for r being Element of CQC-WFF holds not [(q '&' r),k,K,f] in SepQuadruples p
and
A5:
for r being Element of CQC-WFF
for l being Element of NAT holds
( not k = l + (QuantNbr r) or not [(r '&' q),l,K,f] in SepQuadruples p )
and
A6:
for x being Element of bound_QC-variables
for l being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds
( not l + 1 = k or not h +* ({x} --> (x. l)) = f or ( not [(All x,q),l,K,h] in SepQuadruples p & not [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) )
; :: thesis: contradiction
reconsider Y = (SepQuadruples p) \ {[q,k,K,f]} as Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ;
Y is_Sep-closed_on p
proof
A7:
SepQuadruples p is_Sep-closed_on p
by Def13;
then
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples p
by Def12;
hence
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in Y
by A2, ZFMISC_1:64;
:: according to CQC_SIM1:def 12 :: thesis: ( ( 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 [('not' q),k,K,f] in Y holds
[q,k,K,f] in Y ) & ( for q, r 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 '&' r),k,K,f] in Y holds
( [q,k,K,f] in Y & [r,(k + (QuantNbr q)),K,f] in Y ) ) & ( for q being 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 Y holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y ) )
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
[('not' q),k,K,f] in Y holds
[q,k,K,f] in Y
:: thesis: ( ( for q, r 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 '&' r),k,K,f] in Y holds
( [q,k,K,f] in Y & [r,(k + (QuantNbr q)),K,f] in Y ) ) & ( for q being 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 Y holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y ) )proof
let s be
Element of
CQC-WFF ;
:: thesis: 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' s),k,K,f] in Y holds
[s,k,K,f] in Ylet l be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' s),l,K,f] in Y holds
[s,l,K,f] in Ylet L be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' s),l,L,f] in Y holds
[s,l,L,f] in Ylet h be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [('not' s),l,L,h] in Y implies [s,l,L,h] in Y )
assume A8:
[('not' s),l,L,h] in Y
;
:: thesis: [s,l,L,h] in Y
then
[('not' s),l,L,h] in SepQuadruples p
by XBOOLE_0:def 5;
then A9:
[s,l,L,h] in SepQuadruples p
by A7, Def12;
(
s <> q or
l <> k or
L <> K or
f <> h )
by A3, A8, XBOOLE_0:def 5;
then
[s,l,L,h] <> [q,k,K,f]
by MCART_1:33;
hence
[s,l,L,h] in Y
by A9, ZFMISC_1:64;
:: thesis: verum
end;
thus
for
q,
r 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 '&' r),k,K,f] in Y holds
(
[q,k,K,f] in Y &
[r,(k + (QuantNbr q)),K,f] in Y )
:: thesis: for q being 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 Y holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Yproof
let s,
r be
Element of
CQC-WFF ;
:: thesis: 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 [(s '&' r),k,K,f] in Y holds
( [s,k,K,f] in Y & [r,(k + (QuantNbr s)),K,f] in Y )let l be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(s '&' r),l,K,f] in Y holds
( [s,l,K,f] in Y & [r,(l + (QuantNbr s)),K,f] in Y )let L be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(s '&' r),l,L,f] in Y holds
( [s,l,L,f] in Y & [r,(l + (QuantNbr s)),L,f] in Y )let h be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [(s '&' r),l,L,h] in Y implies ( [s,l,L,h] in Y & [r,(l + (QuantNbr s)),L,h] in Y ) )
assume
[(s '&' r),l,L,h] in Y
;
:: thesis: ( [s,l,L,h] in Y & [r,(l + (QuantNbr s)),L,h] in Y )
then A10:
[(s '&' r),l,L,h] in SepQuadruples p
by XBOOLE_0:def 5;
then A11:
(
[s,l,L,h] in SepQuadruples p &
[r,(l + (QuantNbr s)),L,h] in SepQuadruples p )
by A7, Def12;
(
s <> q or
l <> k or
L <> K or
f <> h )
by A4, A10;
then
[s,l,L,h] <> [q,k,K,f]
by MCART_1:33;
hence
[s,l,L,h] in Y
by A11, ZFMISC_1:64;
:: thesis: [r,(l + (QuantNbr s)),L,h] in Y
(
r <> q or
L <> K or
f <> h or
l + (QuantNbr s) <> k )
by A5, A10;
then
[r,(l + (QuantNbr s)),L,h] <> [q,k,K,f]
by MCART_1:33;
hence
[r,(l + (QuantNbr s)),L,h] in Y
by A11, ZFMISC_1:64;
:: thesis: verum
end;
thus
for
q being
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 Y holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y
:: thesis: verumproof
let s be
Element of
CQC-WFF ;
:: thesis: 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,s),k,K,f] in Y holds
[s,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Ylet x be
Element of
bound_QC-variables ;
:: thesis: 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,s),k,K,f] in Y holds
[s,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Ylet l be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,s),l,K,f] in Y holds
[s,(l + 1),(K \/ {x}),(f +* (x .--> (x. l)))] in Ylet L be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,s),l,L,f] in Y holds
[s,(l + 1),(L \/ {x}),(f +* (x .--> (x. l)))] in Ylet h be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [(All x,s),l,L,h] in Y implies [s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in Y )
assume A12:
[(All x,s),l,L,h] in Y
;
:: thesis: [s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in Y
then
[(All x,s),l,L,h] in SepQuadruples p
by XBOOLE_0:def 5;
then A13:
[s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in SepQuadruples p
by A7, Def12;
now assume
( not
[(All x,q),l,K,h] in SepQuadruples p & not
[(All x,q),l,(K \ {x}),h] in SepQuadruples p )
;
:: thesis: ( s = q implies not L \/ {x} = K )then A14:
(
s <> q or (
L <> K &
L <> K \ {x} ) )
by A12, XBOOLE_0:def 5;
assume A15:
s = q
;
:: thesis: not L \/ {x} = Kassume A16:
L \/ {x} = K
;
:: thesis: contradictionthen A17:
K \ {x} = L \ {x}
by XBOOLE_1:40;
(
x in L or not
x in L )
;
hence
contradiction
by A14, A15, A16, A17, ZFMISC_1:46, ZFMISC_1:65;
:: thesis: verum end;
then
(
s <> q or
l + 1
<> k or
L \/ {x} <> K or
f <> h +* ({x} --> (x. l)) )
by A6;
then
[s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] <> [q,k,K,f]
by MCART_1:33;
hence
[s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in Y
by A13, ZFMISC_1:64;
:: thesis: verum
end;
end;
then
( SepQuadruples p c= Y & Y c= SepQuadruples p )
by Def13, XBOOLE_1:36;
then
Y = SepQuadruples p
by XBOOLE_0:def 10;
hence
contradiction
by A1, ZFMISC_1:65; :: thesis: verum