let v be LTL-formula; :: thesis: for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )
let w be Element of Inf_seq AtomicFamily; :: thesis: for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )
set LN = LTLNodes v;
let f be Function of (LTLNodes v),(LTLNodes v); :: thesis: ( f is_succ_homomorphism v,w implies for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary ) )
assume A1: f is_succ_homomorphism v,w ; :: thesis: for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )

proof

let x be set ; :: thesis: ( x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) implies ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary ) )
assume that
A2: x in LTLNodes v and
A3: not CastNode (x,v) is elementary and
A4: w |= * (CastNode (x,v)) ; :: thesis: ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary )
deffunc H₁( set ) -> set = (f |** (CastNat $1)) . x;
set len1 = (len (CastNode ((f . x),v))) + 1;
0 < 0 + ((len (CastNode ((f . x),v))) + 1) ;
then A5: 1 <= (len (CastNode ((f . x),v))) + 1 by NAT_1:19;
reconsider len1 = (len (CastNode ((f . x),v))) + 1 as Nat ;
consider L being FinSequence such that
A6: ( len L = len1 & ( for k being Nat st k in dom L holds
L . k = H₁(k) ) ) from FINSEQ_1:sch 2();
set X = { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } ;
A7: Seg len1 = dom L by A6, FINSEQ_1:def 3;
A8: for k being Nat st 1 <= k & k <= len L holds
L . k = (f |** k) . x

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len L implies L . k = (f |** k) . x )
assume ( 1 <= k & k <= len L ) ; :: thesis: L . k = (f |** k) . x
then k in Seg len1 by A6, FINSEQ_1:1;
then L . k = (f |** (CastNat k)) . x by A6, A7;
hence L . k = (f |** k) . x by MODELC_2:def 1; :: thesis: verum

end;

A9: now :: thesis: not { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } = {}

assume A10: { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } = {} ; :: thesis: contradiction
A11: for k being Nat st 1 <= k & k <= len L holds
not CastNode (((f |** k) . x),v) is elementary

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len L implies not CastNode (((f |** k) . x),v) is elementary )
assume A12: ( 1 <= k & k <= len L ) ; :: thesis: not CastNode (((f |** k) . x),v) is elementary
reconsider k = k as Element of NAT by ORDINAL1:def 12;
not k in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } by A10;
hence not CastNode (((f |** k) . x),v) is elementary by A6, A12; :: thesis: verum

end;

A13: for k being Nat st 1 <= k & k < len L holds
CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v)

proof

let k be Nat; :: thesis: ( 1 <= k & k < len L implies CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) )
assume that
1 <= k and
A14: k < len L ; :: thesis: CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v)
for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary

proof

let i be Nat; :: thesis: ( i <= k implies not CastNode (((f |** i) . x),v) is elementary )
assume i <= k ; :: thesis: not CastNode (((f |** i) . x),v) is elementary
then A15: i < len L by A14, XXREAL_0:2;

now :: thesis: not CastNode (((f |** i) . x),v) is elementary

per cases ( 1 <= i or i = 0 ) by Lm6;

suppose 1 <= i ; :: thesis: not CastNode (((f |** i) . x),v) is elementary

hence not CastNode (((f |** i) . x),v) is elementary by A11, A15; :: thesis: verum

end;

suppose i = 0 ; :: thesis: not CastNode (((f |** i) . x),v) is elementary

then f |** i = id (LTLNodes v) by FUNCT_7:84;
hence not CastNode (((f |** i) . x),v) is elementary by A2, A3, FUNCT_1:18; :: thesis: verum

end;

end;

end;

hence not CastNode (((f |** i) . x),v) is elementary ; :: thesis: verum

end;

hence CastNode (((f |** (k + 1)) . x),v) is_succ_of CastNode (((f |** k) . x),v) by A1, A2, A3, A4, Th48; :: thesis: verum

end;

for m being Nat st 1 <= m & m < len L holds
ex N, M being strict LTLnode over v st
( N = L . m & M = L . (m + 1) & M is_succ_of N )

proof

let m be Nat; :: thesis: ( 1 <= m & m < len L implies ex N, M being strict LTLnode over v st
( N = L . m & M = L . (m + 1) & M is_succ_of N ) )
assume A16: ( 1 <= m & m < len L ) ; :: thesis: ex N, M being strict LTLnode over v st
( N = L . m & M = L . (m + 1) & M is_succ_of N )
set M = L . (m + 1);
( 1 <= m + 1 & m + 1 <= len L ) by A16, NAT_1:13;
then A17: L . (m + 1) = (f |** (m + 1)) . x by A8;
then L . (m + 1) in LTLNodes v by A2, FUNCT_2:5;
then A18: ex M1 being strict LTLnode over v st L . (m + 1) = M1 by Def30;
set N = L . m;
A19: L . m = (f |** m) . x by A8, A16;
then L . m in LTLNodes v by A2, FUNCT_2:5;
then A20: ex N1 being strict LTLnode over v st L . m = N1 by Def30;
reconsider M = L . (m + 1) as strict LTLnode over v by A18;
reconsider N = L . m as strict LTLnode over v by A20;
( CastNode (N,v) = N & CastNode (M,v) = M ) by Def16;
hence ex N, M being strict LTLnode over v st
( N = L . m & M = L . (m + 1) & M is_succ_of N ) by A13, A16, A19, A17; :: thesis: verum

end;

then L is_Finseq_for v ;
then len (CastNode ((L . len1),v)) <= ((len (CastNode ((L . 1),v))) - len1) + 1 by A5, A6, Th36;
then len (CastNode ((L . len1),v)) <= ((len (CastNode (((f |** 1) . x),v))) - len1) + 1 by A5, A6, A8;
then len (CastNode ((L . len1),v)) <= ((len (CastNode ((f . x),v))) - len1) + 1 by FUNCT_7:70;
then len (CastNode (((f |** len1) . x),v)) <= 0 by A5, A6, A8;
then the LTLnew of (CastNode (((f |** len1) . x),v)) = {} v by Th22;
then CastNode (((f |** len1) . x),v) is elementary ;
then len1 in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } by A5;
hence contradiction by A10; :: thesis: verum

end;

{ m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } c= Seg len1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } or y in Seg len1 )
assume y in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } ; :: thesis: y in Seg len1
then ex m being Element of NAT st
( y = m & 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) ;
hence y in Seg len1 by FINSEQ_1:1; :: thesis: verum

end;

then consider n being Nat such that
1 <= n and
A21: n <= len1 and
A22: n in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } and
A23: for i being Nat st 1 <= i & i < n holds
not i in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } by A9, Lm30;
A24: for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary

proof

let i be Nat; :: thesis: ( i < n implies not CastNode (((f |** i) . x),v) is elementary )
assume A25: i < n ; :: thesis: not CastNode (((f |** i) . x),v) is elementary

now :: thesis: not CastNode (((f |** i) . x),v) is elementary

per cases ( i = 0 or 1 <= i ) by Lm6;

suppose i = 0 ; :: thesis: not CastNode (((f |** i) . x),v) is elementary

then f |** i = id (LTLNodes v) by FUNCT_7:84;
hence not CastNode (((f |** i) . x),v) is elementary by A2, A3, FUNCT_1:18; :: thesis: verum

end;

suppose A26: 1 <= i ; :: thesis: not CastNode (((f |** i) . x),v) is elementary

then A27: not i in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) } by A23, A25;

now :: thesis: not CastNode (((f |** i) . x),v) is elementary

assume A28: CastNode (((f |** i) . x),v) is elementary ; :: thesis: contradiction
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i < len1 by A21, A25, XXREAL_0:2;
hence contradiction by A26, A27, A28; :: thesis: verum

end;

hence not CastNode (((f |** i) . x),v) is elementary ; :: thesis: verum

end;

end;

end;

hence not CastNode (((f |** i) . x),v) is elementary ; :: thesis: verum

end;

CastNode (((f |** n) . x),v) is elementary

proof

ex m being Element of NAT st
( n = m & 1 <= m & m <= len1 & CastNode (((f |** m) . x),v) is elementary ) by A22;
hence CastNode (((f |** n) . x),v) is elementary ; :: thesis: verum

end;

hence ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary ) by A24; :: thesis: verum

end;

hence for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
not CastNode (((f |** i) . x),v) is elementary ) & CastNode (((f |** n) . x),v) is elementary ) ; :: thesis: verum