let F, v be LTL-formula; :: thesis: for s2, s1 being strict elementary LTLnode of v st s2 is_next_of s1 & F in the LTLold of s2 holds
ex L being FinSequence ex m being Nat st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode (L . (m + 1)),v is_succ_of CastNode (L . m),v,F )
let s2, s1 be strict elementary LTLnode of v; :: thesis: ( s2 is_next_of s1 & F in the LTLold of s2 implies ex L being FinSequence ex m being Nat st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode (L . (m + 1)),v is_succ_of CastNode (L . m),v,F ) )
assume that
A1: s2 is_next_of s1 and
A2: F in the LTLold of s2 ; :: thesis: ex L being FinSequence ex m being Nat st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode (L . (m + 1)),v is_succ_of CastNode (L . m),v,F )
consider L being FinSequence such that
A3: ( 1 <= len L & L is_Finseq_for v ) and
A4: ( L . 1 = 'X' s1 & L . (len L) = s2 ) by Def215, A1;
set N1 = 'X' s1;
set n = len L;
A5: CastNode (L . 1),v = 'X' s1 by defCastNode01, A4;
A6: CastNode (L . (len L)),v = s2 by defCastNode01, A4;
( 1 < len L & len L <= len L ) by A2, A4, A3, XXREAL_0:1;
then consider m being Nat such that
A9: ( 1 <= m & m < len L & not F in the LTLold of (CastNode (L . m),v) & F in the LTLold of (CastNode (L . (m + 1)),v) ) by A3, A5, A6, A2, ThSucc03;
consider N1, N2 being strict LTLnode of v such that
A10: ( N1 = L . m & N2 = L . (m + 1) & N2 is_succ_of N1 ) by A3, A9, DefFinseq;
set m1 = m + 1;
A11: N1 = CastNode (L . m),v by A10, defCastNode01;
N2 = CastNode (L . (m + 1)),v by A10, defCastNode01;
hence ex L being FinSequence ex m being Nat st
( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 & 1 <= m & m < len L & CastNode (L . (m + 1)),v is_succ_of CastNode (L . m),v,F ) by A3, A4, A9, A10, A11, ThSucc04; :: thesis: verum