set YN = { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } ;
A1: rng T is finite ;
A2: { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } is finite from FRAENKEL:sch 21(A1);
 { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } is finite-membered
proof
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } or x is finite )
assume x in { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } ; :: thesis: x is finite
then consider R being Element of [:(LTLB_WFF **),(LTLB_WFF **):] such that
A3: ( x = rng R & R in rng T ) ;
thus x is finite by A3; :: thesis: verum
end;
then reconsider YN = { (rng R) where R is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : R in rng T } as finite finite-membered set by A2;
now :: thesis: for x being set st x in YN holds
x c= LTLB_WFF
let x be set ; :: thesis: ( x in YN implies x c= LTLB_WFF )
assume x in YN ; :: thesis: x c= LTLB_WFF
then consider R being Element of [:(LTLB_WFF **),(LTLB_WFF **):] such that
A4: ( x = rng R & R in rng T ) ;
thus x c= LTLB_WFF by A4; :: thesis: verum
end;
then reconsider Tforms = union YN as finite Subset of LTLB_WFF by ZFMISC_1:76;
defpred S1[ Element of LTLB_WFF ] means ( P in Tforms & P is s-until );
set uns = { p where p is Element of LTLB_WFF : S1[p] } ;
A5: { p where p is Element of LTLB_WFF : S1[p] } c= LTLB_WFF from FRAENKEL:sch 10();
 { p where p is Element of LTLB_WFF : S1[p] } c= Tforms
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of LTLB_WFF : S1[p] } or x in Tforms )
assume x in { p where p is Element of LTLB_WFF : S1[p] } ; :: thesis: x in Tforms
then ex p being Element of LTLB_WFF st
( p = x & S1[p] ) ;
hence x in Tforms ; :: thesis: verum
end;
then reconsider uns = { p where p is Element of LTLB_WFF : S1[p] } as finite Subset of LTLB_WFF by A5;
reconsider e = 0 as Element of dom T by TREES_1:22;
set f = the Function of NAT,(dom T);
set m = card uns;
consider g being FinSequence such that
A6: rng g = uns and
A7: g is one-to-one by FINSEQ_4:58;
reconsider g = g as one-to-one FinSequence of LTLB_WFF by A6, A7, FINSEQ_1:def 4;
defpred S2[ Nat, Element of dom T, Element of dom T] means ( ( not g . ((P mod (card uns)) + 1) in rng ((T . T) `1) implies c3 in succ T ) & ( g . ((P mod (card uns)) + 1) in rng ((T . T) `1) implies ( T is_a_proper_prefix_of c3 & rarg (g /. ((P mod (card uns)) + 1)) in rng ((T . c3) `1) ) ) );
A8: card g = card uns by A6, PRE_POLY:19;
A9: now :: thesis: for n being Nat
for x being Node of T ex y being Node of T st S2[n,x,y]
let n be Nat; :: thesis: for x being Node of T ex y being Node of T st S2[y,b3,b4]
let x be Node of T; :: thesis: ex y being Node of T st S2[y,b2,b3]
A10: ex t being object st t in succ x by XBOOLE_0:def 1;
set gk = g . ((n mod (card uns)) + 1);
per cases ( not g . ((n mod (card uns)) + 1) in rng ((T . x) `1) or g . ((n mod (card uns)) + 1) in rng ((T . x) `1) ) ;
suppose not g . ((n mod (card uns)) + 1) in rng ((T . x) `1) ; :: thesis: ex y being Node of T st S2[y,b2,b3]
hence ex y being Node of T st S2[n,x,y] by A10; :: thesis: verum
end;
suppose A11: g . ((n mod (card uns)) + 1) in rng ((T . x) `1) ; :: thesis: ex y being Node of T st S2[y,b2,b3]
A12: 1 <= (n mod (card uns)) + 1 by NAT_1:25;
per cases ( uns = {} or uns <> {} ) ;
suppose uns = {} ; :: thesis: ex y being Node of T st S2[y,b2,b3]
then dom g = {} by A6, RELAT_1:42;
then A13: g . ((n mod (card uns)) + 1) = 0 by FUNCT_1:def 2;
len (<*> LTLB_WFF) = 0 ;
hence ex y being Node of T st S2[n,x,y] by HILBERT2:10, A13, A11; :: thesis: verum
end;
suppose uns <> {} ; :: thesis: ex y being Node of T st S2[y,b2,b3]
then (n mod (card uns)) + 1 <= card uns by NAT_D:1, NAT_1:13;
then A14: (n mod (card uns)) + 1 in dom g by A8, FINSEQ_3:25, A12;
then g . ((n mod (card uns)) + 1) in uns by FUNCT_1:3, A6;
then consider puq being Element of LTLB_WFF such that
A15: g . ((n mod (card uns)) + 1) = puq and
puq in Tforms and
A16: puq is s-until ;
consider p, q being Element of LTLB_WFF such that
A17: g . ((n mod (card uns)) + 1) = p 'U' q by A15, A16, HILBERT2:def 6;
consider R being Element of rngr (T | x) such that
A18: q in rng (R `1) by A11, Th32, A17;
R in rngr (T | x) ;
then consider t being Node of (T | x) such that
A19: R = (T | x) . t and
A20: t <> 0 ;
t in dom (T | x) ;
then A21: t in (dom T) | x by TREES_2:def 10;
then reconsider y = x ^ t as Node of T by TREES_1:def 6;
A22: x is_a_proper_prefix_of y by TREES_1:10, A20;
g /. ((n mod (card uns)) + 1) = puq by A15, PARTFUN1:def 6, A14;
then A23: rarg (g /. ((n mod (card uns)) + 1)) = q by Def1, A15, A16, A17;
(T . y) `1 = R `1 by A19, TREES_2:def 10, A21;
hence ex y being Node of T st S2[n,x,y] by A18, A23, A11, A22; :: thesis: verum
end;
end;
end;
end;
end;
consider p being sequence of (dom T) such that
A24: ( p . 0 = e & ( for n being Nat holds S2[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 2(A9);
 defpred S3[ Nat] means P <= len (p . P);
A25: now :: thesis: for k being Nat holds S4[k]
let k be Nat; :: thesis: S4[b1]
defpred S4[ Nat] means ex t being FinSequence st
( (p . P) ^ t = p . (P + 1) & t <> {} );
reconsider pk = p . k, pk1 = p . (k + 1) as Node of T ;
A26: S2[k,pk,pk1] by A24;
per cases ( not g . ((k mod (card uns)) + 1) in rng ((T . pk) `1) or g . ((k mod (card uns)) + 1) in rng ((T . pk) `1) ) ;
suppose not g . ((k mod (card uns)) + 1) in rng ((T . pk) `1) ; :: thesis: S4[b1]
then ex n being Nat st
( pk1 = pk ^ <*n*> & pk ^ <*n*> in dom T ) by A26;
hence S4[k] ; :: thesis: verum
end;
suppose g . ((k mod (card uns)) + 1) in rng ((T . pk) `1) ; :: thesis: S4[b1]
then A27: pk is_a_proper_prefix_of pk1 by A24;
then consider r being FinSequence such that
A28: pk1 = pk ^ r by TREES_1:1;
r <> 0 by FINSEQ_1:34, A27, A28;
hence S4[k] by A28; :: thesis: verum
end;
end;
end;
A29: now :: thesis: for k being Nat st S3[k] holds
S3[k + 1]
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A30: S3[k] ; :: thesis: S3[k + 1]
reconsider pk = p . k, pk1 = p . (k + 1) as Node of T ;
consider t being FinSequence such that
A31: pk1 = pk ^ t and
A32: t <> {} by A25;
len t >= 1 by A32, NAT_1:25;
then (len pk) + (len t) >= k + 1 by A30, XREAL_1:7;
hence S3[k + 1] by A31, FINSEQ_1:22; :: thesis: verum
end;
defpred S4[ Nat] means for i being Nat st i <= P holds
p . i c= p . P;
deffunc H3( Element of NAT ) -> Node of T = (p . P) | P;
consider f being sequence of (dom T) such that
A33: for n being Element of NAT holds f . n = H3(n) from FUNCT_2:sch 4();
A34: now :: thesis: for k being Nat st S4[k] holds
S4[k + 1]
let k be Nat; :: thesis: ( S4[k] implies S4[k + 1] )
reconsider pk = p . k, pk1 = p . (k + 1) as Node of T ;
assume A35: S4[k] ; :: thesis: S4[k + 1]
thus S4[k + 1] :: thesis: verum
proof
let i be Nat; :: thesis: ( i <= k + 1 implies p . i c= p . (k + 1) )
A36: now :: thesis: ( i < k + 1 implies p . i c= p . (k + 1) )
assume i < k + 1 ; :: thesis: p . i c= p . (k + 1)
then i <= k by NAT_1:13;
then A37: p . i c= p . k by A35;
ex t being FinSequence st
( pk ^ t = pk1 & t <> 0 ) by A25;
then pk c= pk1 by FINSEQ_6:10;
hence p . i c= p . (k + 1) by A37; :: thesis: verum
end;
assume i <= k + 1 ; :: thesis: p . i c= p . (k + 1)
hence p . i c= p . (k + 1) by A36, XXREAL_0:1; :: thesis: verum
end;
end;
A38: S3[ 0 ] ;
A39: for n being Nat holds S3[n] from NAT_1:sch 2(A38, A29);
 A40: S4[ 0 ] ;
A41: for j being Nat holds S4[j] from NAT_1:sch 2(A40, A34);
A42: now :: thesis: for k being Nat holds f . (k + 1) in succ (f . k)
let k be Nat; :: thesis: f . (k + 1) in succ (f . k)
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
reconsider fk = f . k, fk1 = f . (k + 1) as Element of dom T ;
reconsider pk = p . k, pk1 = p . (k + 1) as Node of T ;
k + 1 <= len pk1 by A39;
then A43: len (pk1 | (k + 1)) = k + 1 by FINSEQ_1:59;
k1 <= len pk by A39;
then len (pk | k) = k by FINSEQ_1:59;
then A44: len fk = k by A33;
A45: k1 < k1 + 1 by NAT_1:13;
then pk c= pk1 by A41;
then pk | k c= pk1 | (k + 1) by RELAT_1:77, A45, FINSEQ_1:5;
then f . k1 c= pk1 | (k + 1) by A33;
then fk is_a_prefix_of fk1 by A33;
then consider r being FinSequence such that
A46: fk1 = fk ^ r by TREES_1:1;
rng r c= rng fk1 by FINSEQ_1:30, A46;
then reconsider r = r as FinSequence of NAT by XBOOLE_1:1, FINSEQ_1:def 4;
len fk1 = (len fk) + (len r) by FINSEQ_1:22, A46;
then k + 1 = k + (len r) by A43, A33, A44;
then Z: r = <*(r . 1)*> by FINSEQ_5:14;
then 1 <= len r by FINSEQ_1:39;
then 1 in dom r by FINSEQ_3:25;
then r . 1 = r /. 1 by PARTFUN1:def 6;
hence f . (k + 1) in succ (f . k) by A46, Z; :: thesis: verum
end;
f . 0 = H3( 0 ) by A33
.= 0 by A24 ;
then reconsider f = f as path of T by A42, Def13;
A47: now :: thesis: for n being Element of NAT holds H3( len (p . n)) = p . n
let n be Element of NAT ; :: thesis: H3( len (p . n)) = p . n
reconsider pn = p . n as Node of T ;
reconsider pln = p . (len pn) as Node of T ;
pn c= pln by A39, A41;
then ( Seg (len pn) c= dom pn & ex t being FinSequence st pln = pn ^ t ) by FINSEQ_1:def 3, TREES_1:1;
then pln | (len pn) = pn | (len pn) by FINSEQ_6:11
.= pn by FINSEQ_1:58 ;
hence H3( len (p . n)) = p . n ; :: thesis: verum
end;
f is complete
proof
let A be Element of LTLB_WFF ; :: according to LTLAXIO4:def 14 :: thesis: for B being Element of LTLB_WFF
for i being Nat st A 'U' B in rng ((T . (f . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (f . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (f . k)) `1) ) )
let B be Element of LTLB_WFF ; :: thesis: for i being Nat st A 'U' B in rng ((T . (f . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (f . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (f . k)) `1) ) )
let i be Nat; :: thesis: ( A 'U' B in rng ((T . (f . i)) `1) implies ex j being Element of NAT st
( j > i & B in rng ((T . (f . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (f . k)) `1) ) ) )
set aub = A 'U' B;
assume A48: A 'U' B in rng ((T . (f . i)) `1) ; :: thesis: ex j being Element of NAT st
( j > i & B in rng ((T . (f . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (f . k)) `1) ) )
defpred S5[ Nat] means ( P > i implies ( not B in rng ((T . (f . P)) `1) & A 'U' B in rng ((T . (f . P)) `1) & A in rng ((T . (f . P)) `1) ) );
assume A49: for j being Element of NAT holds
( not j > i or not B in rng ((T . (f . j)) `1) or ex k being Element of NAT st
( i < k & k < j & not A in rng ((T . (f . k)) `1) ) ) ; :: thesis: contradiction
A50: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S5[n] ) holds
S5[k]
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S5[n] ) implies S5[k] )
assume A51: for n being Nat st n < k holds
S5[n] ; :: thesis: S5[k]
thus S5[k] :: thesis: verum
proof
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
set fk = T . (f . k1);
assume A52: k > i ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
then k1 >= 1 by NAT_1:25;
then reconsider kk = k1 - 1 as Element of NAT by NAT_1:21;
set fkk = T . (f . kk);
A53: kk + 1 = k ;
then A54: kk >= i by NAT_1:13, A52;
per cases ( kk = i or kk > i ) by A54, XXREAL_0:1;
suppose A55: kk = i ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
per cases ( not B in rng ((T . (f . k1)) `1) or ex m being Element of NAT st
( i < m & m < k1 & not A in rng ((T . (f . m)) `1) ) ) by A49, A52;
suppose A56: not B in rng ((T . (f . k1)) `1) ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
f . k in succ (f . kk) by Def13, A53;
then ex n being Nat st
( f . k = (f . kk) ^ <*n*> & (f . kk) ^ <*n*> in dom T ) ;
then reconsider fk = T . (f . k1) as Element of compn (T . (f . kk)) by Th26;
( B in rng (fk `1) or ( A in rng (fk `1) & A 'U' B in rng (fk `1) ) ) by Th25, A55, A48;
hence ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) ) by A56; :: thesis: verum
end;
suppose ex m being Element of NAT st
( i < m & m < k1 & not A in rng ((T . (f . m)) `1) ) ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
hence ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) ) by NAT_1:13, A55, A53; :: thesis: verum
end;
end;
end;
suppose A57: kk > i ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
per cases ( not B in rng ((T . (f . k1)) `1) or ex m being Element of NAT st
( i < m & m < k1 & not A in rng ((T . (f . m)) `1) ) ) by A49, A52;
suppose A58: not B in rng ((T . (f . k1)) `1) ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
f . k in succ (f . kk) by Def13, A53;
then ex n being Nat st
( f . k = (f . kk) ^ <*n*> & (f . kk) ^ <*n*> in dom T ) ;
then reconsider fk = T . (f . k1) as Element of compn (T . (f . kk)) by Th26;
kk < k by XREAL_1:146;
then A 'U' B in rng ((T . (f . kk)) `1) by A51, A57;
then ( B in rng (fk `1) or ( A in rng (fk `1) & A 'U' B in rng (fk `1) ) ) by Th25;
hence ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) ) by A58; :: thesis: verum
end;
suppose ex m being Element of NAT st
( i < m & m < k1 & not A in rng ((T . (f . m)) `1) ) ; :: thesis: ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) )
hence ( not B in rng ((T . (f . k)) `1) & A 'U' B in rng ((T . (f . k)) `1) & A in rng ((T . (f . k)) `1) ) by A51; :: thesis: verum
end;
end;
end;
end;
end;
end;
A59: for j being Nat holds S5[j] from NAT_1:sch 4(A50);
 T . (f . i) in rng T by FUNCT_1:3;
then ( rng (T . (f . i)) in YN & rng ((T . (f . i)) `1) c= rng (T . (f . i)) ) by XBOOLE_1:7;
then ( A 'U' B is s-until & A 'U' B in Tforms ) by HILBERT2:def 6, A48, TARSKI:def 4;
then A60: A 'U' B in uns ;
then consider n being object such that
A61: n in dom g and
A62: g . n = A 'U' B by A6, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A61;
reconsider k = n - 1 as Element of NAT by A61, FINSEQ_3:25, NAT_1:21;
k + 1 <= len g by FINSEQ_3:25, A61;
then A63: k < card g by NAT_1:13;
set mnk = ((card uns) * (i + 1)) + k;
( i + 1 > i & card uns >= 1 ) by NAT_1:13, A60, NAT_1:25;
then (i + 1) * (card uns) > i * 1 by XREAL_1:97;
then A64: ((card uns) * (i + 1)) + k > i by XREAL_1:40;
then A65: (((card uns) * (i + 1)) + k) + 1 > i by NAT_1:13;
A66: ((((card uns) * (i + 1)) + k) mod (card uns)) + 1 = (k mod (card uns)) + 1 by NAT_D:21
.= k + 1 by NAT_D:24, A63, A8 ;
reconsider t = p . (((card uns) * (i + 1)) + k), t1 = p . ((((card uns) * (i + 1)) + k) + 1) as Node of T ;
((card uns) * (i + 1)) + k <= len t by A39;
then A67: len t > i by A64, XXREAL_0:2;
A68: A 'U' B is s-until by HILBERT2:def 6;
(((card uns) * (i + 1)) + k) + 1 <= len t1 by A39;
then A69: len t1 > i by A65, XXREAL_0:2;
A70: t1 = H3( len t1) by A47
.= f . (len t1) by A33 ;
t = H3( len t) by A47
.= f . (len t) by A33 ;
then g . (k + 1) in rng ((T . t) `1) by A67, A59, A62;
then A71: rarg (g /. (((((card uns) * (i + 1)) + k) mod (card uns)) + 1)) in rng ((T . t1) `1) by A66, A24;
rarg (g /. (((((card uns) * (i + 1)) + k) mod (card uns)) + 1)) = rarg (A 'U' B) by A62, A61, PARTFUN1:def 6, A66
.= B by Def1, A68 ;
hence contradiction by A69, A59, A71, A70; :: thesis: verum
end;
hence ex b1 being path of T st b1 is complete ; :: thesis: verum