let w be Element of Inf_seq AtomicFamily ; :: thesis: for v being neg-inner-most LTL-formula
for U being Choice_Function of BOOL (Subformulae v)
for s being strict elementary LTLnode of v st w |= * ('X' s) holds
( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )
let v be neg-inner-most LTL-formula; :: thesis: for U being Choice_Function of BOOL (Subformulae v)
for s being strict elementary LTLnode of v st w |= * ('X' s) holds
( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )
let U be Choice_Function of BOOL (Subformulae v); :: thesis: for s being strict elementary LTLnode of v st w |= * ('X' s) holds
( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )
let s be strict elementary LTLnode of v; :: thesis: ( w |= * ('X' s) implies ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) ) )
set LN = LTLNodes v;
set N = 'X' s;
assume A1: w |= * ('X' s) ; :: thesis: ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )
set n = chosen_succ_end_num w,v,U,('X' s);
set f = choice_succ_func w,v,U;
set nextnode = CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' s))) . ('X' s)),v;
A2: 'X' s in LTLNodes v by Def30;

now

per cases ( not 'X' s is elementary or 'X' s is elementary ) ;

suppose A3: not 'X' s is elementary ; :: thesis: ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )

deffunc H₁( set ) -> strict LTLnode of v = CastNode (((choice_succ_func w,v,U) |** (CastNat ((CastNat $1) - 1))) . ('X' s)),v;
set n1 = (chosen_succ_end_num w,v,U,('X' s)) + 1;
ex L being FinSequence st
( len L = (chosen_succ_end_num w,v,U,('X' s)) + 1 & ( for k being Nat st k in dom L holds
L . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider L being FinSequence such that
A4: len L = (chosen_succ_end_num w,v,U,('X' s)) + 1 and
A5: for k being Nat st k in dom L holds
L . k = H₁(k) ;
A6: Seg ((chosen_succ_end_num w,v,U,('X' s)) + 1) = dom L by A4, FINSEQ_1:def 3;
A7: for k being Nat st 1 <= k & k <= (chosen_succ_end_num w,v,U,('X' s)) + 1 holds
L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat (k - 1))) . ('X' s)),v

proof

let k be Nat; :: thesis: ( 1 <= k & k <= (chosen_succ_end_num w,v,U,('X' s)) + 1 implies L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat (k - 1))) . ('X' s)),v )
assume ( 1 <= k & k <= (chosen_succ_end_num w,v,U,('X' s)) + 1 ) ; :: thesis: L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat (k - 1))) . ('X' s)),v
then k in Seg ((chosen_succ_end_num w,v,U,('X' s)) + 1) by FINSEQ_1:3;
then L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat ((CastNat k) - 1))) . ('X' s)),v by A5, A6;
hence L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat (k - 1))) . ('X' s)),v by MODELC_2:def 1; :: thesis: verum

end;

for k being Nat st 1 <= k & k < len L holds
ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )

proof

let k be Nat; :: thesis: ( 1 <= k & k < len L implies ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) )
assume that
A8: 1 <= k and
A9: k < len L ; :: thesis: ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 )
set k1 = k - 1;
reconsider k1 = k - 1 as Nat by A8, NAT_1:21;
set M1 = CastNode (((choice_succ_func w,v,U) |** (k1 + 1)) . ('X' s)),v;
set kp = k + 1;
( 1 <= k + 1 & k + 1 <= (chosen_succ_end_num w,v,U,('X' s)) + 1 ) by A4, A8, A9, NAT_1:13;
then A10: L . (k + 1) = CastNode (((choice_succ_func w,v,U) |** (CastNat ((k + 1) - 1))) . ('X' s)),v by A7
.= CastNode (((choice_succ_func w,v,U) |** (k1 + 1)) . ('X' s)),v by MODELC_2:def 1 ;
set N1 = CastNode (((choice_succ_func w,v,U) |** k1) . ('X' s)),v;
k - 1 < ((chosen_succ_end_num w,v,U,('X' s)) + 1) - 1 by A4, A9, XREAL_1:16;
then A11: CastNode (((choice_succ_func w,v,U) |** (k1 + 1)) . ('X' s)),v is_succ_of CastNode (((choice_succ_func w,v,U) |** k1) . ('X' s)),v by A1, A3, Def48;
L . k = CastNode (((choice_succ_func w,v,U) |** (CastNat k1)) . ('X' s)),v by A4, A7, A8, A9
.= CastNode (((choice_succ_func w,v,U) |** k1) . ('X' s)),v by MODELC_2:def 1 ;
hence ex N1, M1 being strict LTLnode of v st
( N1 = L . k & M1 = L . (k + 1) & M1 is_succ_of N1 ) by A11, A10; :: thesis: verum

end;

then A12: L is_Finseq_for v by Def19;
A13: 1 <= (chosen_succ_end_num w,v,U,('X' s)) + 1 by NAT_1:11;
then A14: L . (len L) = CastNode (((choice_succ_func w,v,U) |** (CastNat (((chosen_succ_end_num w,v,U,('X' s)) + 1) - 1))) . ('X' s)),v by A4, A7
.= CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' s))) . ('X' s)),v by MODELC_2:def 1 ;
A15: CastNode (((choice_succ_func w,v,U) |** (chosen_succ_end_num w,v,U,('X' s))) . ('X' s)),v = chosen_next w,v,U,s by A1, A3, Def49;
L . 1 = CastNode (((choice_succ_func w,v,U) |** (CastNat (1 - 1))) . ('X' s)),v by A13, A7
.= CastNode (((choice_succ_func w,v,U) |** 0 ) . ('X' s)),v by MODELC_2:def 1
.= CastNode ((id (LTLNodes v)) . ('X' s)),v by FUNCT_7:86
.= CastNode ('X' s),v by A2, FUNCT_1:35
.= 'X' s by Def16 ;
hence ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) ) by A1, A3, A15, A13, A4, A14, A12, Def20, Def48; :: thesis: verum

end;

suppose 'X' s is elementary ; :: thesis: ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) )

then the LTLnew of ('X' s) = the LTLnew of (FinalNode v) by Def11;
then A16: chosen_next w,v,U,s = 'X' s by A1, Def49;
set L = <*('X' s)*>;
A17: Seg 1 = dom <*('X' s)*> by FINSEQ_1:55;
A18: for n being Nat st n in dom <*('X' s)*> holds
<*('X' s)*> . n = 'X' s

proof

let n be Nat; :: thesis: ( n in dom <*('X' s)*> implies <*('X' s)*> . n = 'X' s )
assume n in dom <*('X' s)*> ; :: thesis: <*('X' s)*> . n = 'X' s
then n = 1 by A17, FINSEQ_1:4, TARSKI:def 1;
hence <*('X' s)*> . n = 'X' s by FINSEQ_1:57; :: thesis: verum

end;

for k being Nat st 1 <= k & k < len <*('X' s)*> holds
ex N1, M1 being strict LTLnode of v st
( N1 = <*('X' s)*> . k & M1 = <*('X' s)*> . (k + 1) & M1 is_succ_of N1 ) by FINSEQ_1:56;
then A19: <*('X' s)*> is_Finseq_for v by Def19;
1 in Seg 1 by FINSEQ_1:3;
then ( len <*('X' s)*> = 1 & <*('X' s)*> . 1 = 'X' s ) by A17, A18, FINSEQ_1:56;
hence ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) ) by A1, A16, A19, Def20; :: thesis: verum

end;

end;

end;

hence ( chosen_next w,v,U,s is_next_of s & w |= * (chosen_next w,v,U,s) ) ; :: thesis: verum