let v be LTL-formula; :: thesis:
let w be Element of Inf_seq AtomicFamily ; :: thesis:
set LN = LTLNodes v;
let f be Function of (LTLNodes v),(LTLNodes v); :: thesis:
assume A0: 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 )

proof

let x be set ; :: thesis:
assume B1: ( x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) ) ; :: thesis:
set len1 = (len (CastNode (f . x),v)) + 1;
0 < 0 + ((len (CastNode (f . x),v)) + 1) ;
then B201: 1 <= (len (CastNode (f . x),v)) + 1 by NAT_1:19;
reconsider len1 = (len (CastNode (f . x),v)) + 1 as Nat ;
deffunc H₁( set ) -> set = (f |** (CastNat $1)) . x;
consider L being FinSequence such that
B2: ( len L = len1 & ( for k being Nat st k in dom L holds
L . k = H₁(k) ) ) from FINSEQ_1:sch 2();
B301: Seg len1 = dom L by B2, FINSEQ_1:def 3;
B3: for k being Nat st 1 <= k & k <= len L holds
L . k = (f |** k) . x

proof

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

end;

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

proof

{ 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 set ; :: according to TARSKI:def 3 :: thesis:
assume y in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) } ; :: thesis:
then consider m being Element of NAT such that
D1: ( y = m & 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) ;
thus y in Seg len1 by D1, FINSEQ_1:3; :: thesis:

end;

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

end;

now

assume B5: { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) } = {} ; :: thesis:
C1: 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:
assume D1: ( 1 <= k & k <= len L ) ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
not k in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) } by B5;
hence not CastNode ((f |** k) . x),v is elementary by D1, B2; :: thesis:

end;

C2: 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:
assume D1: ( 1 <= k & k < len L ) ; :: thesis:
for i being Nat st i <= k holds
not CastNode ((f |** i) . x),v is elementary

proof

let i be Nat; :: thesis:
assume i <= k ; :: thesis:
then E1: i < len L by D1, XXREAL_0:2;

now

per cases by Lem1006;

suppose 1 <= i ; :: thesis:

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

end;

suppose i = 0 ; :: thesis:

then f |** i = id (LTLNodes v) by FUNCT_7:86;
hence not CastNode ((f |** i) . x),v is elementary by B1, FUNCT_1:35; :: thesis:

end;

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

end;

hence CastNode ((f |** (k + 1)) . x),v is_succ_of CastNode ((f |** k) . x),v by A0, B1, ThLTLNodes03; :: thesis:

end;

C3: L is_Finseq_for v

proof

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

proof

let m be Nat; :: thesis:
assume E1: ( 1 <= m & m < len L ) ; :: thesis:
set N = L . m;
E2: L . m = (f |** m) . x by E1, B3;
L . m in LTLNodes v by B1, E2, FUNCT_2:7;
then consider N1 being strict LTLnode of v such that
E3: L . m = N1 by defLTLNodes;
reconsider N = L . m as strict LTLnode of v by E3;
E401: CastNode N,v = N by defCastNode01;
set M = L . (m + 1);
( 1 <= m + 1 & m + 1 <= len L ) by E1, NAT_1:13;
then E4: L . (m + 1) = (f |** (m + 1)) . x by B3;
L . (m + 1) in LTLNodes v by B1, E4, FUNCT_2:7;
then consider M1 being strict LTLnode of v such that
E5: L . (m + 1) = M1 by defLTLNodes;
reconsider M = L . (m + 1) as strict LTLnode of v by E5;
CastNode M,v = M by defCastNode01;
hence ex N, M being strict LTLnode of v st
( N = L . m & M = L . (m + 1) & M is_succ_of N ) by C2, E1, E2, E4, E401; :: thesis:

end;

hence L is_Finseq_for v by DefFinseq; :: thesis:

end;

len (CastNode (L . len1),v) <= ((len (CastNode (L . 1),v)) - len1) + 1 by B201, B2, ThSucc12, C3;
then len (CastNode (L . len1),v) <= ((len (CastNode ((f |** 1) . x),v)) - len1) + 1 by B201, B2, B3;
then len (CastNode (L . len1),v) <= ((len (CastNode (f . x),v)) - len1) + 1 by FUNCT_7:72;
then len (CastNode ((f |** len1) . x),v) <= 0 by B3, B201, B2;
then the LTLnew of (CastNode ((f |** len1) . x),v) = {} v by Thlen18;
then CastNode ((f |** len1) . x),v is elementary by Defelementary;
then len1 in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) } by B201;
hence contradiction by B5; :: thesis:

end;

then consider n being Nat such that
B7: ( 1 <= n & n <= len1 & n in { m where m is Element of NAT : ( 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) } & ( 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 B4, lemExistMin;
B8: CastNode ((f |** n) . x),v is elementary

proof

consider m being Element of NAT such that
C1: ( n = m & 1 <= m & m <= len1 & CastNode ((f |** m) . x),v is elementary ) by B7;
thus CastNode ((f |** n) . x),v is elementary by C1; :: thesis:

end;

for i being Nat st i < n holds
not CastNode ((f |** i) . x),v is elementary

proof

let i be Nat; :: thesis:
assume C1: i < n ; :: thesis:

now

per cases by Lem1006;

suppose i = 0 ; :: thesis:

then f |** i = id (LTLNodes v) by FUNCT_7:86;
hence not CastNode ((f |** i) . x),v is elementary by B1, FUNCT_1:35; :: thesis:

end;

suppose C3: 1 <= i ; :: thesis:

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

now

assume C5: CastNode ((f |** i) . x),v is elementary ; :: thesis:
reconsider i = i as Element of NAT by ORDINAL1:def 13;
i < len1 by C1, B7, XXREAL_0:2;
hence contradiction by C3, C5, C4; :: thesis:

end;

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

end;

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

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 B8; :: thesis:

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: