let Al be QC-alphabet ; for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
let CX be Consistent Subset of (CQC-WFF Al); ( Al is countable & still_not-bound_in CX is finite implies ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples ) )
assume A1:
Al is countable
; ( not still_not-bound_in CX is finite or ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples ) )
assume A2:
still_not-bound_in CX is finite
; ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
( not ExCl Al is empty & ExCl Al is countable )
by A1, Th20;
then consider f being Function such that
A3:
dom f = NAT
and
A4:
ExCl Al = rng f
by Lm1;
reconsider f = f as sequence of (CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S1[ Nat, set , set ] means ex K, L being Subset of (bound_QC-variables Al) st
( K = $2 `2 & L = K \/ (still_not-bound_in {(f . ($1 + 1))}) & $3 = [(('not' (f . ($1 + 1))) 'or' ((the_scope_of (f,($1 + 1))) . ((bound_in (f,($1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . ($1 + 1))) 'or' ((the_scope_of (f,($1 + 1))) . ((bound_in (f,($1 + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] );
A5:
for n being Nat
for C being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]
proof
let n be
Nat;
for C being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]let C be
Element of
[:(CQC-WFF Al),(bool (bound_QC-variables Al)):];
ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S1[n,C,D]
set K =
C `2 ;
ex
a,
b being
object st
(
a in CQC-WFF Al &
b in bool (bound_QC-variables Al) &
C = [a,b] )
by ZFMISC_1:def 2;
then reconsider K =
C `2 as
Subset of
(bound_QC-variables Al) ;
set L =
K \/ (still_not-bound_in {(f . (n + 1))});
set D =
[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))];
take
[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))]
;
S1[n,C,[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))]]
thus
S1[
n,
C,
[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))]]
;
verum
end;
reconsider A = [(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in still_not-bound_in (CX \/ {(f . 0)}) } ))))),(still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))}))] as Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ;
consider h being sequence of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] such that
A6:
( h . 0 = A & ( for n being Nat holds S1[n,h . n,h . (n + 1)] ) )
from RECDEF_1:sch 2(A5);
set CY = CX \/ { ((h . n) `1) where n is Nat : verum } ;
then reconsider CY = CX \/ { ((h . n) `1) where n is Nat : verum } as Subset of (CQC-WFF Al) by TARSKI:def 3;
A9:
now for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))let x be
bound_QC-variable of
Al;
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))let p be
Element of
CQC-WFF Al;
ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
Ex (
x,
p)
in ExCl Al
by Def3;
then consider a being
object such that A10:
a in dom f
and A11:
f . a = Ex (
x,
p)
by A4, FUNCT_1:def 3;
reconsider a =
a as
Nat by A10;
reconsider r9 =
f . a as
Element of
CQC-WFF Al ;
A12:
Ex-bound_in r9 = x
by A11, Th22;
A13:
Ex-the_scope_of r9 = p
by A11, Th22;
A14:
bound_in (
f,
a)
= x
by A12, Def6;
A15:
the_scope_of (
f,
a)
= p
by A13, Def7;
A16:
(h . a) `1 in { ((h . n) `1) where n is Nat : verum }
;
A17:
{ ((h . n) `1) where n is Nat : verum } c= CY
by XBOOLE_1:7;
A18:
(
a = 0 implies ex
y being
bound_QC-variable of
Al st
CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) )
by A6, A11, A14, A15, A16, A17, Th21;
now ( a <> 0 implies ex y being Element of bound_QC-variables Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) )assume
a <> 0
;
ex y being Element of bound_QC-variables Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))then consider m being
Nat such that A20:
a = m + 1
by NAT_1:6;
reconsider m =
m as
Nat ;
A21:
ex
K,
L being
Subset of
(bound_QC-variables Al) st
(
K = (h . m) `2 &
L = K \/ (still_not-bound_in {r9}) &
h . a = [(('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] )
by A6, A20;
set K =
(h . m) `2 ;
set L =
(still_not-bound_in {r9}) \/ ((h . m) `2);
take y =
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {r9}) \/ ((h . m) `2) } );
CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
(h . a) `1 = ('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),y))
by A21;
hence
CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
by A11, A14, A15, A16, A17, Th21;
verum end; hence
ex
y being
bound_QC-variable of
Al st
CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
by A18;
verum end;
deffunc H1( set ) -> set = CX \/ { ((h . n) `1) where n is Nat : n in $1 } ;
consider F being Function such that
A22:
( dom F = NAT & ( for a being set st a in NAT holds
F . a = H1(a) ) )
from FUNCT_1:sch 5();
A23:
CY c= union (rng F)
union (rng F) c= CY
then A40:
CY = union (rng F)
by A23;
A41:
for n, m being Nat st m in dom F & n in dom F & n < m holds
F . n c= F . m
rng F c= bool (CQC-WFF Al)
then reconsider F = F as sequence of (bool (CQC-WFF Al)) by A22, FUNCT_2:2;
A54:
for n being Nat holds F . (n + 1) = (F . n) \/ {((h . n) `1)}
defpred S2[ Nat] means ( (h . $1) `2 is finite & (h . $1) `2 is Subset of (bound_QC-variables Al) );
A69:
S2[ 0 ]
A71:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A72:
S2[
k]
;
S2[k + 1]
A73:
ex
K,
L being
Subset of
(bound_QC-variables Al) st
(
K = (h . k) `2 &
L = K \/ (still_not-bound_in {(f . (k + 1))}) &
h . (k + 1) = [(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] )
by A6;
set K =
(h . k) `2 ;
reconsider K =
(h . k) `2 as
Subset of
(bound_QC-variables Al) by A72;
set L =
K \/ (still_not-bound_in {(f . (k + 1))});
set s =
('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))));
still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) is
finite
by CQC_SIM1:19;
hence
S2[
k + 1]
by A72, A73;
verum
end;
A74:
for k being Nat holds S2[k]
from NAT_1:sch 2(A69, A71);
defpred S3[ Nat] means ( still_not-bound_in (F . ($1 + 1)) c= (h . $1) `2 & not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2) } ) in still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}) );
A75:
for k being Nat holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )
proof
A76:
S3[
0 ]
proof
set r =
('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } ))));
set A1 =
{(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))};
reconsider s =
f . 1 as
Element of
CQC-WFF Al ;
A77:
(h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))})
by A6;
reconsider B =
(h . 0) `2 as
Subset of
(bound_QC-variables Al) by A6;
reconsider C =
(still_not-bound_in {s}) \/ B as
Element of
bool (bound_QC-variables Al) ;
still_not-bound_in s is
finite
by CQC_SIM1:19;
then
still_not-bound_in {s} is
finite
by Th26;
then consider x being
bound_QC-variable of
Al such that A78:
not
x in C
by A69, Th28;
consider u being
QC-symbol of
Al such that A79:
x. u = x
by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in C }
by A78, A79;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in C } as non
empty set ;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in C } as non
empty Subset of
(QC-symbols Al) by TARSKI:def 3;
set u =
Al -one_in A;
Al -one_in A = the
Element of
A
by QC_LANG1:def 41;
then
Al -one_in A in A
;
then A80:
ex
t being
QC-symbol of
Al st
(
t = Al -one_in A & not
x. t in C )
;
A81:
F . 0 = CX \/ { ((h . n) `1) where n is Nat : n in 0 }
by A22;
now for b being object holds not b in { ((h . n) `1) where n is Nat : n in 0 } let b be
object ;
not b in { ((h . n) `1) where n is Nat : n in 0 } assume
b in { ((h . n) `1) where n is Nat : n in 0 }
;
contradictionthen
ex
n being
Nat st
(
b = (h . n) `1 &
n in 0 )
;
hence
contradiction
;
verum end;
then A82:
{ ((h . n) `1) where n is Nat : n in 0 } = {}
by XBOOLE_0:def 1;
(h . 0) `1 = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } ))))
by A6;
then
F . (0 + 1) = CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))}
by A54, A81, A82;
hence
S3[
0 ]
by A77, A80, Th27;
verum
end;
A83:
for
k being
Nat st
S3[
k] holds
S3[
k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
assume A84:
S3[
k]
;
S3[k + 1]
reconsider s =
f . (k + 2) as
Element of
CQC-WFF Al ;
A85:
ex
K,
L being
Subset of
(bound_QC-variables Al) st
(
K = (h . k) `2 &
L = K \/ (still_not-bound_in {(f . (k + 1))}) &
h . (k + 1) = [(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] )
by A6;
set K =
(h . k) `2 ;
reconsider K =
(h . k) `2 as
Subset of
(bound_QC-variables Al) by A74;
set L =
K \/ (still_not-bound_in {(f . (k + 1))});
set r =
('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))));
A86:
(h . (k + 1)) `1 = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))
by A85;
A87:
(h . (k + 1)) `2 = K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))))
by A85;
reconsider B =
(h . (k + 1)) `2 as
Subset of
(bound_QC-variables Al) by A85;
reconsider C =
(still_not-bound_in {s}) \/ B as
Element of
bool (bound_QC-variables Al) ;
still_not-bound_in s is
finite
by CQC_SIM1:19;
then A88:
still_not-bound_in {s} is
finite
by Th26;
(h . (k + 1)) `2 is
finite
by A74;
then consider x being
bound_QC-variable of
Al such that A89:
not
x in C
by A88, Th28;
consider u being
QC-symbol of
Al such that A90:
x. u = x
by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B }
by A89, A90;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B } as non
empty set ;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B } as non
empty Subset of
(QC-symbols Al) by TARSKI:def 3;
set u =
Al -one_in A;
Al -one_in A = the
Element of
A
by QC_LANG1:def 41;
then
Al -one_in A in A
;
then A91:
ex
t being
QC-symbol of
Al st
(
t = Al -one_in A & not
x. t in C )
;
then A92:
not
x. (Al -one_in A) in still_not-bound_in {s}
by XBOOLE_0:def 3;
(still_not-bound_in (F . (k + 1))) \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))) c= B
by A84, A87, XBOOLE_1:9;
then
(still_not-bound_in (F . (k + 1))) \/ (still_not-bound_in {(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))}) c= B
by Th26;
then A93:
still_not-bound_in ((F . (k + 1)) \/ {(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))}) c= B
by Th27;
then
still_not-bound_in (F . ((k + 1) + 1)) c= B
by A54, A86;
then
not
x. (Al -one_in A) in still_not-bound_in (F . ((k + 1) + 1))
by A91, XBOOLE_0:def 3;
then
not
x. (Al -one_in A) in (still_not-bound_in (F . ((k + 1) + 1))) \/ (still_not-bound_in {s})
by A92, XBOOLE_0:def 3;
hence
S3[
k + 1]
by A54, A86, A93, Th27;
verum
end;
for
k being
Nat holds
S3[
k]
from NAT_1:sch 2(A76, A83);
hence
for
k being
Nat holds
(
still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )
;
verum
end;
defpred S4[ Nat] means F . $1 is Consistent ;
now for a being object holds not a in { ((h . i) `1) where i is Nat : i in 0 } let a be
object ;
not a in { ((h . i) `1) where i is Nat : i in 0 } assume
a in { ((h . i) `1) where i is Nat : i in 0 }
;
contradictionthen
ex
j being
Nat st
(
a = (h . j) `1 &
j in 0 )
;
hence
contradiction
;
verum end;
then
{ ((h . i) `1) where i is Nat : i in 0 } = {}
by XBOOLE_0:def 1;
then A94:
F . 0 = CX \/ {}
by A22;
then A95:
S4[ 0 ]
;
A96:
for k being Nat st S4[k] holds
S4[k + 1]
proof
let k be
Nat;
( S4[k] implies S4[k + 1] )
assume A97:
S4[
k]
;
S4[k + 1]
ex
c,
d being
object st
(
c in CQC-WFF Al &
d in bool (bound_QC-variables Al) &
h . k = [c,d] )
by ZFMISC_1:def 2;
then reconsider r =
(h . k) `1 as
Element of
CQC-WFF Al ;
now not F . (k + 1) is Inconsistent assume
F . (k + 1) is
Inconsistent
;
contradictionthen
F . (k + 1) |- 'not' (VERUM Al)
by HENMODEL:6;
then
(F . k) \/ {r} |- 'not' (VERUM Al)
by A54;
then consider f1 being
FinSequence of
CQC-WFF Al such that A98:
rng f1 c= F . k
and A99:
|- (f1 ^ <*r*>) ^ <*('not' (VERUM Al))*>
by HENMODEL:8;
A100:
|- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (f . k))*>
by CALCUL_2:21;
A101:
now not k = 0 assume A102:
k = 0
;
contradictionthen A103:
r = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } ))))
by A6;
reconsider s =
(the_scope_of (f,0)) . (
(bound_in (f,0)),
(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } ))) as
Element of
CQC-WFF Al ;
A104:
|- (f1 ^ <*('not' (f . k))*>) ^ <*(('not' (f . k)) 'or' s)*>
by A100, CALCUL_1:51;
0 + 1
<= len (f1 ^ <*r*>)
by CALCUL_1:10;
then
|- (((Ant (f1 ^ <*r*>)) ^ <*('not' (f . k))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by A99, Th25;
then
|- ((f1 ^ <*('not' (f . k))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then
|- ((f1 ^ <*('not' (f . k))*>) ^ <*r*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then A105:
|- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (VERUM Al))*>
by A102, A103, A104, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*>
by CALCUL_2:21;
then A106:
|- (f1 ^ <*s*>) ^ <*(('not' (f . k)) 'or' s)*>
by CALCUL_1:52;
0 + 1
<= len (f1 ^ <*r*>)
by CALCUL_1:10;
then
|- (((Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by A99, Th25;
then
|- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then
|- ((f1 ^ <*s*>) ^ <*r*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then A107:
|- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*>
by A102, A103, A106, CALCUL_2:24;
reconsider r1 =
f . 0 as
Element of
CQC-WFF Al ;
set C =
still_not-bound_in (CX \/ {r1});
still_not-bound_in r1 is
finite
by CQC_SIM1:19;
then
still_not-bound_in {r1} is
finite
by Th26;
then
(still_not-bound_in {r1}) \/ (still_not-bound_in CX) is
finite
by A2;
then
still_not-bound_in (CX \/ {r1}) is
finite
by Th27;
then consider x being
bound_QC-variable of
Al such that A108:
not
x in still_not-bound_in (CX \/ {r1})
by Th28;
consider u being
QC-symbol of
Al such that A109:
x. u = x
by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1}) }
by A108, A109;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1}) } as non
empty set ;
then reconsider A =
{ t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1}) } as non
empty Subset of
(QC-symbols Al) by TARSKI:def 3;
set u =
Al -one_in A;
Al -one_in A = the
Element of
A
by QC_LANG1:def 41;
then
Al -one_in A in A
;
then consider t being
QC-symbol of
Al such that A110:
t = Al -one_in A
and A111:
not
x. t in still_not-bound_in (CX \/ {r1})
;
A112:
not
x. t in (still_not-bound_in CX) \/ (still_not-bound_in {r1})
by A111, Th27;
then A113:
not
x. t in still_not-bound_in {r1}
by XBOOLE_0:def 3;
A114:
F . 0 = CX \/ { ((h . n) `1) where n is Nat : n in 0 }
by A22;
now for b being object holds not b in { ((h . n) `1) where n is Nat : n in 0 } let b be
object ;
not b in { ((h . n) `1) where n is Nat : n in 0 } assume
b in { ((h . n) `1) where n is Nat : n in 0 }
;
contradictionthen
ex
n being
Nat st
(
b = (h . n) `1 &
n in 0 )
;
hence
contradiction
;
verum end; then
{ ((h . n) `1) where n is Nat : n in 0 } = {}
by XBOOLE_0:def 1;
then
still_not-bound_in (rng f1) c= still_not-bound_in CX
by A98, A102, A114, Th29;
then
not
x. t in still_not-bound_in (rng f1)
by A112, XBOOLE_0:def 3;
then A115:
not
x. (Al -one_in A) in still_not-bound_in f1
by A110, Th30;
reconsider r2 =
the_scope_of (
f,
0) as
Element of
CQC-WFF Al ;
reconsider y2 =
bound_in (
f,
0) as
bound_QC-variable of
Al ;
r1 in ExCl Al
by A3, A4, FUNCT_1:3;
then consider y1 being
bound_QC-variable of
Al,
s1 being
Element of
CQC-WFF Al such that A116:
r1 = Ex (
y1,
s1)
by Def3;
A117:
s1 = Ex-the_scope_of r1
by A116, Th22;
A118:
r2 = Ex-the_scope_of r1
by Def7;
A119:
y1 = Ex-bound_in r1
by A116, Th22;
A120:
y2 = Ex-bound_in r1
by Def6;
not
x. (Al -one_in A) in still_not-bound_in r1
by A110, A113, Th26;
then
not
x. (Al -one_in A) in still_not-bound_in <*r1*>
by CALCUL_1:60;
then
not
x. (Al -one_in A) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>)
by A115, XBOOLE_0:def 3;
then A121:
not
x. (Al -one_in A) in still_not-bound_in (f1 ^ <*r1*>)
by CALCUL_1:59;
still_not-bound_in (VERUM Al) = {}
by QC_LANG3:3;
then
not
x. (Al -one_in A) in still_not-bound_in ('not' (VERUM Al))
by QC_LANG3:7;
then
not
x. (Al -one_in A) in still_not-bound_in <*('not' (VERUM Al))*>
by CALCUL_1:60;
then
not
x. (Al -one_in A) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>)
by A121, XBOOLE_0:def 3;
then
not
x. (Al -one_in A) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>)
by CALCUL_1:59;
then
|- (f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>
by A107, A116, A117, A118, A119, A120, CALCUL_1:61;
then
|- f1 ^ <*('not' (VERUM Al))*>
by A102, A105, CALCUL_2:26;
then
F . k |- 'not' (VERUM Al)
by A98, HENMODEL:def 1;
hence
contradiction
by A94, A102, Th24;
verum end; now not k <> 0 assume
k <> 0
;
contradictionthen consider k1 being
Nat such that A122:
k = k1 + 1
by NAT_1:6;
reconsider k1 =
k1 as
Nat ;
A123:
ex
K,
L being
Subset of
(bound_QC-variables Al) st
(
K = (h . k1) `2 &
L = K \/ (still_not-bound_in {(f . (k1 + 1))}) &
h . (k1 + 1) = [(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] )
by A6;
set K =
(h . k1) `2 ;
set r1 =
f . (k1 + 1);
set L =
((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))});
set p1 =
('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))));
A124:
r = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))))
by A122, A123;
reconsider s =
(the_scope_of (f,(k1 + 1))) . (
(bound_in (f,(k1 + 1))),
(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))) as
Element of
CQC-WFF Al ;
A125:
|- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*>
by A100, A122, CALCUL_1:51;
0 + 1
<= len (f1 ^ <*r*>)
by CALCUL_1:10;
then
|- (((Ant (f1 ^ <*r*>)) ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by A99, Th25;
then
|- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then
|- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*r*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then A126:
|- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' (VERUM Al))*>
by A124, A125, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*>
by CALCUL_2:21;
then A127:
|- (f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*>
by CALCUL_1:52;
0 + 1
<= len (f1 ^ <*r*>)
by CALCUL_1:10;
then
|- (((Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by A99, Th25;
then
|- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*>
by CALCUL_1:5;
then
|- ((f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*>) ^ <*('not' (VERUM Al))*>
by A124, CALCUL_1:5;
then A128:
|- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*>
by A127, CALCUL_2:24;
set y =
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } );
set u =
Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ;
reconsider r2 =
the_scope_of (
f,
(k1 + 1)) as
Element of
CQC-WFF Al ;
reconsider y2 =
bound_in (
f,
(k1 + 1)) as
bound_QC-variable of
Al ;
reconsider r1 =
f . (k1 + 1) as
Element of
CQC-WFF Al ;
r1 in ExCl Al
by A3, A4, FUNCT_1:3;
then consider y1 being
bound_QC-variable of
Al,
s1 being
Element of
CQC-WFF Al such that A129:
r1 = Ex (
y1,
s1)
by Def3;
A130:
s1 = Ex-the_scope_of r1
by A129, Th22;
A131:
r2 = Ex-the_scope_of r1
by Def7;
A132:
y1 = Ex-bound_in r1
by A129, Th22;
A133:
y2 = Ex-bound_in r1
by Def6;
reconsider Z =
F . k as
Subset of
(CQC-WFF Al) ;
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (Z \/ {r1})
by A75, A122;
then A134:
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in Z) \/ (still_not-bound_in {r1})
by Th27;
then A135:
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in {r1}
by XBOOLE_0:def 3;
still_not-bound_in (rng f1) c= still_not-bound_in Z
by A98, Th29;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (rng f1)
by A134, XBOOLE_0:def 3;
then A136:
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in f1
by Th30;
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in r1
by A135, Th26;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*r1*>
by CALCUL_1:60;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>)
by A136, XBOOLE_0:def 3;
then A137:
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (f1 ^ <*r1*>)
by CALCUL_1:59;
still_not-bound_in (VERUM Al) = {}
by QC_LANG3:3;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ('not' (VERUM Al))
by QC_LANG3:7;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*('not' (VERUM Al))*>
by CALCUL_1:60;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>)
by A137, XBOOLE_0:def 3;
then
not
x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>)
by CALCUL_1:59;
then
|- (f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>
by A128, A129, A130, A131, A132, A133, CALCUL_1:61;
then
|- f1 ^ <*('not' (VERUM Al))*>
by A126, CALCUL_2:26;
then
F . k |- 'not' (VERUM Al)
by A98, HENMODEL:def 1;
hence
contradiction
by A97, Th24;
verum end; hence
contradiction
by A101;
verum end;
hence
S4[
k + 1]
;
verum
end;
for n being Nat holds S4[n]
from NAT_1:sch 2(A95, A96);
then
for n, m being Nat st m in dom F & n in dom F & n < m holds
( F . n is Consistent & F . n c= F . m )
by A41;
then reconsider CY = CY as Consistent Subset of (CQC-WFF Al) by A40, HENMODEL:11;
take
CY
; ( CX c= CY & CY is with_examples )
thus
( CX c= CY & CY is with_examples )
by A9, XBOOLE_1:7; verum