let H, v be LTL-formula; :: thesis: for s2, s1 being strict elementary LTLnode of v st s2 is_next_of s1 & H is Release & H in the LTLold of s2 & not the_left_argument_of H in the LTLold of s2 holds
( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 )
let s2, s1 be strict elementary LTLnode of v; :: thesis: ( s2 is_next_of s1 & H is Release & H in the LTLold of s2 & not the_left_argument_of H in the LTLold of s2 implies ( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 ) )
set F = the_left_argument_of H;
set G = the_right_argument_of H;
set N1 = 'X' s1;
assume that
A1: s2 is_next_of s1 and
A2: ( H is Release & H in the LTLold of s2 & not the_left_argument_of H in the LTLold of s2 ) ; :: thesis: ( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 )
( LTLNew1 H = {(the_right_argument_of H)} & LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} & LTLNext H = {H} ) by A2, Def203, Def204, Def205;
then A001: ( the_right_argument_of H in LTLNew1 H & the_left_argument_of H in LTLNew2 H & H in LTLNext H ) by TARSKI:def 1, TARSKI:def 2;
consider L being FinSequence, m being Nat such that
A3: ( 1 <= len L & L is_Finseq_for v & L . 1 = 'X' s1 & L . (len L) = s2 ) and
A4: ( 1 <= m & m < len L & CastNode (L . (m + 1)),v is_succ_of CastNode (L . m),v,H ) by A1, A2, ThNext02;
set n = len L;
A6: CastNode (L . (len L)),v = s2 by defCastNode01, A3;
set m1 = m + 1;
A7: ( 1 <= m + 1 & m + 1 <= len L ) by A4, NAT_1:13;
set M2 = CastNode (L . (m + 1)),v;
set M1 = CastNode (L . m),v;
A8: ( H in the LTLnew of (CastNode (L . m),v) & ( CastNode (L . (m + 1)),v = SuccNode1 H,(CastNode (L . m),v) or ( ( H is disjunctive or H is Until or H is Release ) & CastNode (L . (m + 1)),v = SuccNode2 H,(CastNode (L . m),v) ) ) ) by DefSucc01, A4;
the LTLnew of s2 = {} v by Defelementary;
then A9: the LTLnew of (CastNode (L . (m + 1)),v) c= the LTLold of s2 by A3, A6, A7, ThSucc10;
A10: ( the LTLold of (CastNode (L . (m + 1)),v) c= the LTLold of s2 & the LTLnext of (CastNode (L . (m + 1)),v) c= the LTLnext of s2 ) by A3, A6, A7, ThSucc07;
A11: not CastNode (L . (m + 1)),v = SuccNode2 H,(CastNode (L . m),v)

proof

now

assume B1: CastNode (L . (m + 1)),v = SuccNode2 H,(CastNode (L . m),v) ; :: thesis: contradiction
B2: not the_left_argument_of H in the LTLnew of (CastNode (L . (m + 1)),v) by A2, A9;
the LTLold of (CastNode (L . m),v) c= the LTLold of s2 by A3, A4, A6, ThSucc07;
then not the_left_argument_of H in the LTLold of (CastNode (L . m),v) by A2;
then the_left_argument_of H in (LTLNew2 H) \ the LTLold of (CastNode (L . m),v) by A001, XBOOLE_0:def 5;
then the_left_argument_of H in (the LTLnew of (CastNode (L . m),v) \ {H}) \/ ((LTLNew2 H) \ the LTLold of (CastNode (L . m),v)) by XBOOLE_0:def 3;
hence contradiction by A2, A8, B1, Def207, B2; :: thesis: verum

end;

hence not CastNode (L . (m + 1)),v = SuccNode2 H,(CastNode (L . m),v) ; :: thesis: verum

end;

A12: the_right_argument_of H in the LTLold of s2

proof

now

per cases ( not the_right_argument_of H in the LTLold of (CastNode (L . m),v) or the_right_argument_of H in the LTLold of (CastNode (L . m),v) ) ;

suppose not the_right_argument_of H in the LTLold of (CastNode (L . m),v) ; :: thesis: the_right_argument_of H in the LTLold of s2

then the_right_argument_of H in (LTLNew1 H) \ the LTLold of (CastNode (L . m),v) by A001, XBOOLE_0:def 5;
then the_right_argument_of H in (the LTLnew of (CastNode (L . m),v) \ {H}) \/ ((LTLNew1 H) \ the LTLold of (CastNode (L . m),v)) by XBOOLE_0:def 3;
then the_right_argument_of H in the LTLnew of (CastNode (L . (m + 1)),v) by A11, A8, Def206;
hence the_right_argument_of H in the LTLold of s2 by A9; :: thesis: verum

end;

suppose the_right_argument_of H in the LTLold of (CastNode (L . m),v) ; :: thesis: the_right_argument_of H in the LTLold of s2

then the_right_argument_of H in the LTLold of (CastNode (L . m),v) \/ {H} by XBOOLE_0:def 3;
then the_right_argument_of H in the LTLold of (CastNode (L . (m + 1)),v) by A11, A8, Def206;
hence the_right_argument_of H in the LTLold of s2 by A10; :: thesis: verum

end;

end;

end;

hence the_right_argument_of H in the LTLold of s2 ; :: thesis: verum

end;

H in the LTLnext of (CastNode (L . m),v) \/ (LTLNext H) by A001, XBOOLE_0:def 3;
then H in the LTLnext of (CastNode (L . (m + 1)),v) by A11, A8, Def206;
hence ( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 ) by A10, A12; :: thesis: verum