let CX be Consistent Subset of CQC-WFF ; :: thesis:
assume A1: still_not-bound_in CX is finite ; :: thesis:
consider f being Function such that
A2: ( dom f = NAT & ExCl = rng f ) by Lm1, Th20;
reconsider f = f as Function of NAT ,CQC-WFF by A2, FUNCT_2:4;
defpred S₁[ Element of NAT , set , set ] means ex K, L being Subset of bound_QC-variables 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. (min* { i where i is Element of NAT : not x. i in L } )))),(K \/ (still_not-bound_in (('not' (f . ($1 + 1))) 'or' ((the_scope_of f,($1 + 1)) . (bound_in f,($1 + 1)),(x. (min* { j where j is Element of NAT : not x. j in L } ))))))] );
A3: for n being Element of NAT
for C being Element of [:CQC-WFF ,(bool bound_QC-variables ):] ex D being Element of [:CQC-WFF ,(bool bound_QC-variables ):] st S₁[n,C,D]

proof

let n be Element of NAT ; :: thesis:
let C be Element of [:CQC-WFF ,(bool bound_QC-variables ):]; :: thesis:
set K = C `2 ;
consider a, b being set such that
A4: ( a in CQC-WFF & b in bool bound_QC-variables & C = [a,b] ) by ZFMISC_1:def 2;
reconsider K = C `2 as Subset of bound_QC-variables by A4, MCART_1:7;
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. (min* { i where i is Element of NAT : not x. i 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. (min* { j where j is Element of NAT : not x. j 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. (min* { i where i is Element of NAT : not x. i 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. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))))] ; :: thesis:
thus S₁[n,C,[(('not' (f . (n + 1))) 'or' ((the_scope_of f,(n + 1)) . (bound_in f,(n + 1)),(x. (min* { i where i is Element of NAT : not x. i 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. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))))]] ; :: thesis:

end;

reconsider A = [(('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { i where i is Element of NAT : not x. i 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. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0 )}) } ))))}))] as Element of [:CQC-WFF ,(bool bound_QC-variables ):] ;
consider h being Function of NAT ,[:CQC-WFF ,(bool bound_QC-variables ):] such that
A5: ( h . 0 = A & ( for n being Element of NAT holds S₁[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A3);
set CY = CX \/ { ((h . n) `1 ) where n is Element of NAT : verum } ;

now

let a be set ; :: thesis:
assume A6: a in CX \/ { ((h . n) `1 ) where n is Element of NAT : verum } ; :: thesis:

now

assume not a in CX ; :: thesis:
then a in { ((h . n) `1 ) where n is Element of NAT : verum } by A6, XBOOLE_0:def 3;
then consider n being Element of NAT such that
A7: a = (h . n) `1 ;
consider c, d being set such that
A8: ( c in CQC-WFF & d in bool bound_QC-variables & h . n = [c,d] ) by ZFMISC_1:def 2;
thus a in CQC-WFF by A7, A8, MCART_1:7; :: thesis:

end;

hence a in CQC-WFF ; :: thesis:

end;

then reconsider CY = CX \/ { ((h . n) `1 ) where n is Element of NAT : verum } as Subset of CQC-WFF by TARSKI:def 3;

A9: now

let x be bound_QC-variable; :: thesis:
let p be Element of CQC-WFF ; :: thesis:
Ex x,p in ExCl by Def3;
then consider a being set such that
A10: ( a in dom f & f . a = Ex x,p ) by A2, FUNCT_1:def 5;
reconsider a = a as Element of NAT by A10;
reconsider r' = f . a as Element of CQC-WFF ;
( Ex-bound_in r' = x & Ex-the_scope_of r' = p ) by A10, Th22;
then A11: ( bound_in f,a = x & the_scope_of f,a = p ) by Def6, Def7;
A12: (h . a) `1 in { ((h . n) `1 ) where n is Element of NAT : verum } ;
A13: { ((h . n) `1 ) where n is Element of NAT : verum } c= CY by XBOOLE_1:7;

A14: now

assume A15: a = 0 ; :: thesis:
take y = x. (min* { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r'}) } ); :: thesis:
(h . a) `1 = ('not' r') 'or' ((the_scope_of f,a) . (bound_in f,a),y) by A5, A15, MCART_1:7;
hence CY |- ('not' (Ex x,p)) 'or' (p . x,y) by A10, A11, A12, A13, Th21; :: thesis:

end;

now

assume a <> 0 ; :: thesis:
then consider m being Nat such that
A16: a = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A17: ex K, L being Subset of bound_QC-variables st
( K = (h . m) `2 & L = K \/ (still_not-bound_in {r'}) & h . a = [(('not' r') 'or' ((the_scope_of f,a) . (bound_in f,a),(x. (min* { i where i is Element of NAT : not x. i in L } )))),(K \/ (still_not-bound_in (('not' r') 'or' ((the_scope_of f,a) . (bound_in f,a),(x. (min* { j where j is Element of NAT : not x. j in L } ))))))] ) by A5, A16;
set K = (h . m) `2 ;
set L = (still_not-bound_in {r'}) \/ ((h . m) `2 );
take y = x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {r'}) \/ ((h . m) `2 ) } ); :: thesis:
(h . a) `1 = ('not' r') 'or' ((the_scope_of f,a) . (bound_in f,a),y) by A17, MCART_1:7;
hence CY |- ('not' (Ex x,p)) 'or' (p . x,y) by A10, A11, A12, A13, Th21; :: thesis:

end;

hence ex y being bound_QC-variable st CY |- ('not' (Ex x,p)) 'or' (p . x,y) by A14; :: thesis:

end;

deffunc H₁( set ) -> set = CX \/ { ((h . n) `1 ) where n is Element of NAT : n in $1 } ;
consider F being Function such that
A18: ( dom F = NAT & ( for a being set st a in NAT holds
F . a = H₁(a) ) ) from FUNCT_1:sch 3();
A19: CY = union (rng F)

proof

thus CY c= union (rng F) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A20: a in CY ; :: thesis:

A21: now

assume A22: a in CX ; :: thesis:
A23: F . 0 = CX \/ { ((h . n) `1 ) where n is Element of NAT : n in 0 } by A18;

now

let b be set ; :: thesis:
assume A24: b in { ((h . n) `1 ) where n is Element of NAT : n in 0 } ; :: thesis:
consider n being Element of NAT such that
A25: ( b = (h . n) `1 & n in 0 ) by A24;
thus contradiction by A25; :: thesis:

end;

then A26: { ((h . n) `1 ) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
F . 0 in rng F by A18, FUNCT_1:12;
hence a in union (rng F) by A22, A23, A26, TARSKI:def 4; :: thesis:

end;

now

assume a in { ((h . n) `1 ) where n is Element of NAT : verum } ; :: thesis:
then consider n being Element of NAT such that
A27: a = (h . n) `1 ;
n < n + 1 by NAT_1:13;
then n in n + 1 by NAT_1:45;
then A28: a in { ((h . m) `1 ) where m is Element of NAT : m in n + 1 } by A27;
F . (n + 1) = CX \/ { ((h . m) `1 ) where m is Element of NAT : m in n + 1 } by A18;
then A29: { ((h . m) `1 ) where m is Element of NAT : m in n + 1 } c= F . (n + 1) by XBOOLE_1:7;
F . (n + 1) in rng F by A18, FUNCT_1:12;
hence a in union (rng F) by A28, A29, TARSKI:def 4; :: thesis:

end;

hence a in union (rng F) by A20, A21, XBOOLE_0:def 3; :: thesis:

end;

thus union (rng F) c= CY :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in union (rng F) ; :: thesis:
then consider b being set such that
A30: ( a in b & b in rng F ) by TARSKI:def 4;
consider c being set such that
A31: ( c in dom F & F . c = b ) by A30, FUNCT_1:def 5;
reconsider n = c as Element of NAT by A18, A31;
A32: a in CX \/ { ((h . m) `1 ) where m is Element of NAT : m in n } by A18, A30, A31;

A33: now

assume A34: a in CX ; :: thesis:
CX c= CY by XBOOLE_1:7;
hence a in CY by A34; :: thesis:

end;

now

assume a in { ((h . m) `1 ) where m is Element of NAT : m in n } ; :: thesis:
then consider m being Element of NAT such that
A35: ( a = (h . m) `1 & m in n ) ;
A36: a in { ((h . i) `1 ) where i is Element of NAT : verum } by A35;
{ ((h . i) `1 ) where i is Element of NAT : verum } c= CY by XBOOLE_1:7;
hence a in CY by A36; :: thesis:

end;

hence a in CY by A32, A33, XBOOLE_0:def 3; :: thesis:

end;

A37: for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
F . n c= F . m

proof

let n, m be Element of NAT ; :: thesis:
assume A38: ( m in dom F & n in dom F & n < m ) ; :: thesis:
A39: F . n = CX \/ { ((h . i) `1 ) where i is Element of NAT : i in n } by A18;
A40: F . m = CX \/ { ((h . i) `1 ) where i is Element of NAT : i in m } by A18;

now

let a be set ; :: thesis:
assume A41: a in F . n ; :: thesis:

A42: now

assume A43: a in CX ; :: thesis:
CX c= F . m by A40, XBOOLE_1:7;
hence a in F . m by A43; :: thesis:

end;

now

assume a in { ((h . i) `1 ) where i is Element of NAT : i in n } ; :: thesis:
then consider i being Element of NAT such that
A44: ( (h . i) `1 = a & i in n ) ;
i < n by A44, NAT_1:45;
then i < m by A38, XXREAL_0:2;
then i in m by NAT_1:45;
then A45: a in { ((h . j) `1 ) where j is Element of NAT : j in m } by A44;
{ ((h . j) `1 ) where j is Element of NAT : j in m } c= F . m by A40, XBOOLE_1:7;
hence a in F . m by A45; :: thesis:

end;

hence a in F . m by A39, A41, A42, XBOOLE_0:def 3; :: thesis:

end;

hence F . n c= F . m by TARSKI:def 3; :: thesis:

end;

rng F c= bool CQC-WFF

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A46: a in rng F ; :: thesis:
consider b being set such that
A47: ( b in dom F & F . b = a ) by A46, FUNCT_1:def 5;
reconsider b = b as Element of NAT by A18, A47;
A48: F . b = CX \/ { ((h . i) `1 ) where i is Element of NAT : i in b } by A18;

now

let c be set ; :: thesis:
assume A49: c in { ((h . i) `1 ) where i is Element of NAT : i in b } ; :: thesis:
consider i being Element of NAT such that
A50: ( (h . i) `1 = c & i in b ) by A49;
thus c in CQC-WFF by A50, MCART_1:10; :: thesis:

end;

then { ((h . i) `1 ) where i is Element of NAT : i in b } c= CQC-WFF by TARSKI:def 3;
then F . b c= CQC-WFF by A48, XBOOLE_1:8;
hence a in bool CQC-WFF by A47; :: thesis:

end;

then reconsider F = F as Function of NAT ,(bool CQC-WFF ) by A18, FUNCT_2:4;
A51: for n being Element of NAT holds F . (n + 1) = (F . n) \/ {((h . n) `1 )}

proof

let n be Element of NAT ; :: thesis:

now

let a be set ; :: thesis:
assume a in { ((h . i) `1 ) where i is Element of NAT : i in n + 1 } ; :: thesis:
then consider j being Element of NAT such that
A52: ( a = (h . j) `1 & j in n + 1 ) ;
j < n + 1 by A52, NAT_1:45;
then A53: j + 1 <= n + 1 by NAT_1:13;

A54: now

assume j + 1 = n + 1 ; :: thesis:
then A55: a in {((h . n) `1 )} by A52, TARSKI:def 1;
{((h . n) `1 )} c= { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by XBOOLE_1:7;
hence a in { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by A55; :: thesis:

end;

now

assume j + 1 <= n ; :: thesis:
then j < n by NAT_1:13;
then j in n by NAT_1:45;
then A56: a in { ((h . k) `1 ) where k is Element of NAT : k in n } by A52;
{ ((h . k) `1 ) where k is Element of NAT : k in n } c= { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by XBOOLE_1:7;
hence a in { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by A56; :: thesis:

end;

hence a in { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by A53, A54, NAT_1:8; :: thesis:

end;

then A57: { ((h . k) `1 ) where k is Element of NAT : k in n + 1 } c= { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} by TARSKI:def 3;

now

let a be set ; :: thesis:
assume A58: a in { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} ; :: thesis:

A59: now

assume a in { ((h . i) `1 ) where i is Element of NAT : i in n } ; :: thesis:
then consider j being Element of NAT such that
A60: ( (h . j) `1 = a & j in n ) ;
( n <= n + 1 & j < n ) by A60, NAT_1:11, NAT_1:45;
then j < n + 1 by XXREAL_0:2;
then j in n + 1 by NAT_1:45;
hence a in { ((h . i) `1 ) where i is Element of NAT : i in n + 1 } by A60; :: thesis:

end;

now

assume a in {((h . n) `1 )} ; :: thesis:
then A61: a = (h . n) `1 by TARSKI:def 1;
n < n + 1 by NAT_1:13;
then n in n + 1 by NAT_1:45;
hence a in { ((h . i) `1 ) where i is Element of NAT : i in n + 1 } by A61; :: thesis:

end;

hence a in { ((h . i) `1 ) where i is Element of NAT : i in n + 1 } by A58, A59, XBOOLE_0:def 3; :: thesis:

end;

then { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} c= { ((h . k) `1 ) where k is Element of NAT : k in n + 1 } by TARSKI:def 3;
then { ((h . i) `1 ) where i is Element of NAT : i in n } \/ {((h . n) `1 )} = { ((h . k) `1 ) where k is Element of NAT : k in n + 1 } by A57, XBOOLE_0:def 10;
then F . (n + 1) = CX \/ ({ ((h . k) `1 ) where k is Element of NAT : k in n } \/ {((h . n) `1 )}) by A18;
then F . (n + 1) = (CX \/ { ((h . k) `1 ) where k is Element of NAT : k in n } ) \/ {((h . n) `1 )} by XBOOLE_1:4;
hence F . (n + 1) = (F . n) \/ {((h . n) `1 )} by A18; :: thesis:

end;

defpred S₂[ Element of NAT ] means ( (h . $1) `2 is finite & (h . $1) `2 is Subset of bound_QC-variables );
A62: for k being Element of NAT holds
( (h . k) `2 is finite & (h . k) `2 is Subset of bound_QC-variables )

proof

A63: S₂[ 0 ]

proof

A64: (h . 0 ) `2 = still_not-bound_in (CX \/ {(('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0 )}) } ))))}) by A5, MCART_1:7;
reconsider s = ('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0 )}) } ))) as Element of CQC-WFF ;
still_not-bound_in s is finite by CQC_SIM1:20;
then still_not-bound_in {s} is finite by Th26;
then (still_not-bound_in {s}) \/ (still_not-bound_in CX) is finite by A1;
hence S₂[ 0 ] by A64, Th27; :: thesis:

end;

A65: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A66: S₂[k] ; :: thesis:
A67: ex K, L being Subset of bound_QC-variables 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. (min* { i where i is Element of NAT : not x. i in L } )))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of f,(k + 1)) . (bound_in f,(k + 1)),(x. (min* { j where j is Element of NAT : not x. j in L } ))))))] ) by A5;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of bound_QC-variables by A66;
set L = K \/ (still_not-bound_in {(f . (k + 1))});
A68: (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. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) by A67, MCART_1:7;
set s = ('not' (f . (k + 1))) 'or' ((the_scope_of f,(k + 1)) . (bound_in f,(k + 1)),(x. (min* { j where j is Element of NAT : not x. j 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. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (k + 1))}) } )))) is finite by CQC_SIM1:20;
hence S₂[k + 1] by A66, A68; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A63, A65);
hence for k being Element of NAT holds
( (h . k) `2 is finite & (h . k) `2 is Subset of bound_QC-variables ) ; :: thesis:

end;

defpred S₃[ Element of NAT ] means ( still_not-bound_in (F . ($1 + 1)) c= (h . $1) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2 ) } ) in still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}) );
A69: for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2 ) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )

proof

A70: S₃[ 0 ]

proof

set r = ('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0 )}) } )));
set A1 = {(('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0 )}) } ))))};
reconsider s = f . 1 as Element of CQC-WFF ;
A71: (h . 0 ) `2 = still_not-bound_in (CX \/ {(('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0 )}) } ))))}) by A5, MCART_1:7;
reconsider B = (h . 0 ) `2 as Subset of bound_QC-variables by A5, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool bound_QC-variables ;
still_not-bound_in s is finite by CQC_SIM1:20;
then ( still_not-bound_in {s} is finite & (h . 0 ) `2 is finite ) by A62, Th26;
then C is finite ;
then consider x being bound_QC-variable such that
A72: not x in C by Th28;
consider l being Element of NAT such that
A73: x. l = x by QC_LANG3:36;
l in { i where i is Element of NAT : not x. i in C } by A72, A73;
then reconsider A = { i where i is Element of NAT : not x. i in C } as non empty set ;

now

let a be set ; :: thesis:
assume A74: a in A ; :: thesis:
consider i being Element of NAT such that
A75: ( a = i & not x. i in C ) by A74;
thus a in NAT by A75; :: thesis:

end;

then reconsider A = { i where i is Element of NAT : not x. i in C } as non empty Subset of NAT by TARSKI:def 3;
set j = min* A;
min* A in A by NAT_1:def 1;
then consider i being Element of NAT such that
A76: ( i = min* A & not x. i in C ) ;
A77: F . 0 = CX \/ { ((h . n) `1 ) where n is Element of NAT : n in 0 } by A18;

now

let b be set ; :: thesis:
assume A78: b in { ((h . n) `1 ) where n is Element of NAT : n in 0 } ; :: thesis:
consider n being Element of NAT such that
A79: ( b = (h . n) `1 & n in 0 ) by A78;
thus contradiction by A79; :: thesis:

end;

then A80: { ((h . n) `1 ) where n is Element of 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. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0 )}) } ))) by A5, MCART_1:7;
then A81: F . (0 + 1) = CX \/ {(('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0 )}) } ))))} by A51, A77, A80;
thus S₃[ 0 ] by A71, A76, A81, Th27; :: thesis:

end;

A82: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A83: S₃[k] ; :: thesis:
reconsider s = f . (k + 2) as Element of CQC-WFF ;
A84: ex K, L being Subset of bound_QC-variables 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. (min* { i where i is Element of NAT : not x. i in L } )))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of f,(k + 1)) . (bound_in f,(k + 1)),(x. (min* { j where j is Element of NAT : not x. j in L } ))))))] ) by A5;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of bound_QC-variables by A62;
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. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } )));
A85: ( (h . (k + 1)) `1 = ('not' (f . (k + 1))) 'or' ((the_scope_of f,(k + 1)) . (bound_in f,(k + 1)),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } ))) & (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. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) ) by A84, MCART_1:7;
reconsider B = (h . (k + 1)) `2 as Subset of bound_QC-variables by A84, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool bound_QC-variables ;
still_not-bound_in s is finite by CQC_SIM1:20;
then ( still_not-bound_in {s} is finite & (h . (k + 1)) `2 is finite ) by A62, Th26;
then C is finite ;
then consider x being bound_QC-variable such that
A86: not x in C by Th28;
consider l being Element of NAT such that
A87: x. l = x by QC_LANG3:36;
l in { i where i is Element of NAT : not x. i in (still_not-bound_in {s}) \/ B } by A86, A87;
then reconsider A = { i where i is Element of NAT : not x. i in (still_not-bound_in {s}) \/ B } as non empty set ;

now

let a be set ; :: thesis:
assume A88: a in A ; :: thesis:
consider i being Element of NAT such that
A89: ( a = i & not x. i in C ) by A88;
thus a in NAT by A89; :: thesis:

end;

then reconsider A = { i where i is Element of NAT : not x. i in (still_not-bound_in {s}) \/ B } as non empty Subset of NAT by TARSKI:def 3;
set j = min* A;
min* A in A by NAT_1:def 1;
then consider i being Element of NAT such that
A90: ( i = min* A & not x. i in C ) ;
A91: ( not x. (min* A) in B & not x. (min* A) in still_not-bound_in {s} ) by A90, 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. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) c= B by A83, A85, 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. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))}) c= B by Th26;
then A92: still_not-bound_in ((F . (k + 1)) \/ {(('not' (f . (k + 1))) 'or' ((the_scope_of f,(k + 1)) . (bound_in f,(k + 1)),(x. (min* { i where i is Element of NAT : not x. i 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 A51, A85;
then not x. (min* A) in still_not-bound_in (F . ((k + 1) + 1)) by A90, XBOOLE_0:def 3;
then not x. (min* A) in (still_not-bound_in (F . ((k + 1) + 1))) \/ (still_not-bound_in {s}) by A91, XBOOLE_0:def 3;
hence S₃[k + 1] by A51, A85, A92, Th27; :: thesis:

end;

for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A70, A82);
hence for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2 ) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) ) ; :: thesis:

end;

defpred S₄[ Element of NAT ] means F . $1 is Consistent ;
A93: S₄[ 0 ]

proof

now

let a be set ; :: thesis:
assume A94: a in { ((h . i) `1 ) where i is Element of NAT : i in 0 } ; :: thesis:
consider j being Element of NAT such that
A95: ( a = (h . j) `1 & j in 0 ) by A94;
thus contradiction by A95; :: thesis:

end;

then { ((h . i) `1 ) where i is Element of NAT : i in 0 } = {} by XBOOLE_0:def 1;
then F . 0 = CX \/ {} by A18;
hence S₄[ 0 ] ; :: thesis:

end;

A96: for k being Element of NAT st S₄[k] holds
S₄[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A97: S₄[k] ; :: thesis:
consider c, d being set such that
A98: ( c in CQC-WFF & d in bool bound_QC-variables & h . k = [c,d] ) by ZFMISC_1:def 2;
reconsider r = (h . k) `1 as Element of CQC-WFF by A98, MCART_1:7;

now

assume not F . (k + 1) is Consistent ; :: thesis:
then ( F . (k + 1) |- VERUM & F . (k + 1) |- 'not' VERUM ) by HENMODEL:6;
then (F . k) \/ {r} |- 'not' VERUM by A51;
then consider f1 being FinSequence of CQC-WFF such that
A99: ( rng f1 c= F . k & |- (f1 ^ <*r*>) ^ <*('not' VERUM )*> ) by HENMODEL:8;
A100: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (f . k))*> by CALCUL_2:21;

A101: now

assume A102: k = 0 ; :: thesis:
then A103: r = ('not' (f . 0 )) 'or' ((the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {(f . 0 )}) } ))) by A5, MCART_1:7;
reconsider s = (the_scope_of f,0 ) . (bound_in f,0 ),(x. (min* { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {(f . 0 )}) } )) as Element of CQC-WFF ;
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 )*> by A99, Th25;
then |- ((f1 ^ <*('not' (f . k))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then |- ((f1 ^ <*('not' (f . k))*>) ^ <*r*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then A105: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' VERUM )*> 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 )*> by A99, Th25;
then |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then |- ((f1 ^ <*s*>) ^ <*r*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then A107: |- (f1 ^ <*s*>) ^ <*('not' VERUM )*> by A102, A103, A106, CALCUL_2:24;
reconsider r1 = f . 0 as Element of CQC-WFF ;
set C = still_not-bound_in (CX \/ {r1});
still_not-bound_in r1 is finite by CQC_SIM1:20;
then still_not-bound_in {r1} is finite by Th26;
then (still_not-bound_in {r1}) \/ (still_not-bound_in CX) is finite by A1;
then still_not-bound_in (CX \/ {r1}) is finite by Th27;
then consider x being bound_QC-variable such that
A108: not x in still_not-bound_in (CX \/ {r1}) by Th28;
consider l being Element of NAT such that
A109: x. l = x by QC_LANG3:36;
l in { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r1}) } by A108, A109;
then reconsider A = { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r1}) } as non empty set ;

now

let a be set ; :: thesis:
assume A110: a in A ; :: thesis:
consider i being Element of NAT such that
A111: ( a = i & not x. i in still_not-bound_in (CX \/ {r1}) ) by A110;
thus a in NAT by A111; :: thesis:

end;

then reconsider A = { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r1}) } as non empty Subset of NAT by TARSKI:def 3;
set j = min* A;
min* A in A by NAT_1:def 1;
then consider i being Element of NAT such that
A112: ( i = min* A & not x. i in still_not-bound_in (CX \/ {r1}) ) ;
A113: not x. i in (still_not-bound_in CX) \/ (still_not-bound_in {r1}) by A112, Th27;
then A114: ( not x. i in still_not-bound_in CX & not x. i in still_not-bound_in {r1} ) by XBOOLE_0:def 3;
A115: F . 0 = CX \/ { ((h . n) `1 ) where n is Element of NAT : n in 0 } by A18;

now

let b be set ; :: thesis:
assume A116: b in { ((h . n) `1 ) where n is Element of NAT : n in 0 } ; :: thesis:
consider n being Element of NAT such that
A117: ( b = (h . n) `1 & n in 0 ) by A116;
thus contradiction by A117; :: thesis:

end;

then { ((h . n) `1 ) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
then still_not-bound_in (rng f1) c= still_not-bound_in CX by A99, A102, A115, Th29;
then not x. i in still_not-bound_in (rng f1) by A113, XBOOLE_0:def 3;
then A118: not x. (min* A) in still_not-bound_in f1 by A112, Th30;
reconsider r2 = the_scope_of f,0 as Element of CQC-WFF ;
reconsider y2 = bound_in f,0 as bound_QC-variable ;
r1 in ExCl by A2, FUNCT_1:12;
then consider y1 being bound_QC-variable, s1 being Element of CQC-WFF such that
A119: r1 = Ex y1,s1 by Def3;
A120: ( s1 = Ex-the_scope_of r1 & r2 = Ex-the_scope_of r1 ) by A119, Def7, Th22;
A121: ( y1 = Ex-bound_in r1 & y2 = Ex-bound_in r1 ) by A119, Def6, Th22;
not x. (min* A) in still_not-bound_in r1 by A112, A114, Th26;
then not x. (min* A) in still_not-bound_in <*r1*> by CALCUL_1:60;
then not x. (min* A) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A118, XBOOLE_0:def 3;
then A122: not x. (min* A) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
not x. (min* A) in still_not-bound_in ('not' VERUM ) by QC_LANG3:7, QC_LANG3:11;
then not x. (min* A) in still_not-bound_in <*('not' VERUM )*> by CALCUL_1:60;
then not x. (min* A) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' VERUM )*>) by A122, XBOOLE_0:def 3;
then not x. (min* A) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' VERUM )*>) by CALCUL_1:59;
then |- (f1 ^ <*r1*>) ^ <*('not' VERUM )*> by A107, A119, A120, A121, CALCUL_1:61;
then |- f1 ^ <*('not' VERUM )*> by A102, A105, CALCUL_2:26;
then F . k |- 'not' VERUM by A99, HENMODEL:def 2;
hence contradiction by A93, A102, Th24; :: thesis:

end;

now

assume k <> 0 ; :: thesis:
then consider k1 being Nat such that
A123: k = k1 + 1 by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
A124: ex K, L being Subset of bound_QC-variables 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. (min* { i where i is Element of NAT : not x. i in L } )))),(K \/ (still_not-bound_in (('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { j where j is Element of NAT : not x. j in L } ))))))] ) by A5;
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. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } )));
A125: ( r = ('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))) & (h . (k1 + 1)) `2 = ((h . k1) `2 ) \/ (still_not-bound_in (('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))))) ) by A123, A124, MCART_1:7;
reconsider s = (the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } )) as Element of CQC-WFF ;
A126: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))))*> by A100, A123, 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 )*> by A99, Th25;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*r*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then A127: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' VERUM )*> by A125, A126, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A128: |- (f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i 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 )*> by A99, Th25;
then |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM )*> by CALCUL_1:5;
then |- ((f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of f,(k1 + 1)) . (bound_in f,(k1 + 1)),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))))*>) ^ <*('not' VERUM )*> by A125, CALCUL_1:5;
then A129: |- (f1 ^ <*s*>) ^ <*('not' VERUM )*> by A128, CALCUL_2:24;
set y = x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } );
set j = min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ;
reconsider r2 = the_scope_of f,(k1 + 1) as Element of CQC-WFF ;
reconsider y2 = bound_in f,(k1 + 1) as bound_QC-variable ;
reconsider r1 = f . (k1 + 1) as Element of CQC-WFF ;
r1 in ExCl by A2, FUNCT_1:12;
then consider y1 being bound_QC-variable, s1 being Element of CQC-WFF such that
A130: r1 = Ex y1,s1 by Def3;
A131: ( s1 = Ex-the_scope_of r1 & r2 = Ex-the_scope_of r1 ) by A130, Def7, Th22;
A132: ( y1 = Ex-bound_in r1 & y2 = Ex-bound_in r1 ) by A130, Def6, Th22;
reconsider Z = F . k as Subset of CQC-WFF ;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (Z \/ {r1}) by A69, A123;
then A133: not x. (min* { i where i is Element of NAT : not x. i 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 A134: ( not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in Z & not x. (min* { i where i is Element of NAT : not x. i 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 A99, Th29;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (rng f1) by A133, XBOOLE_0:def 3;
then A135: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in f1 by Th30;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in r1 by A134, Th26;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*r1*> by CALCUL_1:60;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A135, XBOOLE_0:def 3;
then A136: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ('not' VERUM ) by QC_LANG3:7, QC_LANG3:11;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*('not' VERUM )*> by CALCUL_1:60;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' VERUM )*>) by A136, XBOOLE_0:def 3;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2 ) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' VERUM )*>) by CALCUL_1:59;
then |- (f1 ^ <*r1*>) ^ <*('not' VERUM )*> by A129, A130, A131, A132, CALCUL_1:61;
then |- f1 ^ <*('not' VERUM )*> by A127, CALCUL_2:26;
then F . k |- 'not' VERUM by A99, HENMODEL:def 2;
hence contradiction by A97, Th24; :: thesis:

end;

hence contradiction by A101; :: thesis:

end;

hence S₄[k + 1] ; :: thesis:

end;

for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A93, A96);
then for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
( F . n is Consistent & F . n c= F . m ) by A37;
then reconsider CY = CY as Consistent Subset of CQC-WFF by A19, HENMODEL:11;
take CY ; :: thesis:
thus ( CX c= CY & CY is with_examples ) by A9, Def2, XBOOLE_1:7; :: thesis: