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 LTLnext of s1 holds
( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )
let s2, s1 be strict elementary LTLnode of v; :: thesis: ( s2 is_next_of s1 & H is Release & H in the LTLnext of s1 implies ( the_right_argument_of H in the LTLold of s2 & H in the LTLold 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 LTLnext of s1 ) ; :: thesis: ( the_right_argument_of H in the LTLold of s2 & H in the LTLold 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_right_argument_of H in LTLNew2 H & H in LTLNext H ) by TARSKI:def 1, TARSKI:def 2;
A002: the LTLnext of s1 c= the LTLold of s2 by A1, ThNext01;
then 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;
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),v) c= the LTLold of s2 by A3, A4, A6, ThSucc07;
the_right_argument_of H in the LTLold of s2

proof

now

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

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

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

end;

suppose B1: 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

now

per cases ( ( H in the LTLnew of (CastNode (L . m),v) & CastNode (L . (m + 1)),v = SuccNode1 H,(CastNode (L . m),v) ) or ( H in the LTLnew of (CastNode (L . m),v) & ( 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;

suppose B2: ( H in the LTLnew of (CastNode (L . m),v) & CastNode (L . (m + 1)),v = SuccNode1 H,(CastNode (L . m),v) ) ; :: thesis: the_right_argument_of H in the LTLold of s2

the_right_argument_of H in (LTLNew1 H) \ the LTLold of (CastNode (L . m),v) by B1, 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 B2, Def206;
hence the_right_argument_of H in the LTLold of s2 by A9; :: thesis: verum

end;

suppose B3: ( H in the LTLnew of (CastNode (L . m),v) & ( H is disjunctive or H is Until or H is Release ) & CastNode (L . (m + 1)),v = SuccNode2 H,(CastNode (L . m),v) ) ; :: thesis: the_right_argument_of H in the LTLold of s2

the_right_argument_of H in (LTLNew2 H) \ the LTLold of (CastNode (L . m),v) by B1, A001, XBOOLE_0:def 5;
then the_right_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;
then the_right_argument_of H in the LTLnew of (CastNode (L . (m + 1)),v) by B3, Def207;
hence the_right_argument_of H in the LTLold of s2 by A9; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence ( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 ) by A002, A2; :: thesis: verum