let F, v be LTL-formula; :: thesis: for s1, s2 being strict elementary LTLnode over 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 s1, s2 be strict elementary LTLnode over 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 )
set N1 = 'X' s1;
consider L being FinSequence such that
A3: 1 <= len L and
A4: L is_Finseq_for v and
A5: ( L . 1 = 'X' s1 & L . (len L) = s2 ) by A1;
set n = len L;
A6: ( CastNode ((L . 1),v) = 'X' s1 & CastNode ((L . (len L)),v) = s2 ) by A5, Def16;
1 < len L by A2, A3, A5, XXREAL_0:1;
then consider m being Nat such that
A7: ( 1 <= m & m < len L ) and
A8: ( not F in the LTLold of (CastNode ((L . m),v)) & F in the LTLold of (CastNode ((L . (m + 1)),v)) ) by A2, A4, A6, Th27;
set m1 = m + 1;
consider N1, N2 being strict LTLnode over v such that
A9: ( N1 = L . m & N2 = L . (m + 1) ) and
A10: N2 is_succ_of N1 by A4, A7;
( N1 = CastNode ((L . m),v) & N2 = CastNode ((L . (m + 1)),v) ) by A9, Def16;
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, A5, A7, A8, A10, Th28; :: thesis: verum