let H, v be LTL-formula; :: thesis: for s1, s2 being strict elementary LTLnode over 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 s1, s2 be strict elementary LTLnode over 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 and
A3: H in the LTLold of s2 and
A4: 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 )
consider L being FinSequence, m being Nat such that
1 <= len L and
A5: L is_Finseq_for v and
L . 1 = 'X' s1 and
A6: L . (len L) = s2 and
A7: ( 1 <= m & m < len L ) and
A8: CastNode ((L . (m + 1)),v) is_succ_of CastNode ((L . m),v),H by A1, A3, Th38;
set m1 = m + 1;
set M2 = CastNode ((L . (m + 1)),v);
set n = len L;
A9: CastNode ((L . (len L)),v) = s2 by A6, Def16;
set M1 = CastNode ((L . m),v);
A10: H in the LTLnew of (CastNode ((L . m),v)) by A8;
A11: ( 1 <= m + 1 & m + 1 <= len L ) by A7, NAT_1:13;
then A12: the LTLnext of (CastNode ((L . (m + 1)),v)) c= the LTLnext of s2 by A5, A9, Th31;
the LTLnew of s2 = {} v by Def11;
then A13: the LTLnew of (CastNode ((L . (m + 1)),v)) c= the LTLold of s2 by A5, A9, A11, Th34;
LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} by A2, Def2;
then A14: the_left_argument_of H in LTLNew2 H by TARSKI:def 2;

A15: now :: thesis: not CastNode ((L . (m + 1)),v) = SuccNode2 (H,(CastNode ((L . m),v)))

the LTLold of (CastNode ((L . m),v)) c= the LTLold of s2 by A5, A7, A9, Th31;
then not the_left_argument_of H in the LTLold of (CastNode ((L . m),v)) by A4;
then the_left_argument_of H in (LTLNew2 H) \ the LTLold of (CastNode ((L . m),v)) by A14, XBOOLE_0:def 5;
then A16: 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;
assume A17: CastNode ((L . (m + 1)),v) = SuccNode2 (H,(CastNode ((L . m),v))) ; :: thesis: contradiction
not the_left_argument_of H in the LTLnew of (CastNode ((L . (m + 1)),v)) by A4, A13;
hence contradiction by A10, A17, A16, Def5; :: thesis: verum

end;

LTLNew1 H = {(the_right_argument_of H)} by A2, Def1;
then A18: the_right_argument_of H in LTLNew1 H by TARSKI:def 1;
A19: ( 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 A8;
A20: the LTLold of (CastNode ((L . (m + 1)),v)) c= the LTLold of s2 by A5, A9, A11, Th31;
A21: the_right_argument_of H in the LTLold of s2

proof

now :: thesis: the_right_argument_of H in the LTLold of s2

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 A18, 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 A10, A19, A15, Def4;
hence the_right_argument_of H in the LTLold of s2 by A13; :: 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 A10, A19, A15, Def4;
hence the_right_argument_of H in the LTLold of s2 by A20; :: thesis: verum

end;

end;

end;

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

end;

LTLNext H = {H} by A2, Def3;
then H in LTLNext H by TARSKI:def 1;
then H in the LTLnext of (CastNode ((L . m),v)) \/ (LTLNext H) by XBOOLE_0:def 3;
then H in the LTLnext of (CastNode ((L . (m + 1)),v)) by A10, A19, A15, Def4;
hence ( the_right_argument_of H in the LTLold of s2 & H in the LTLnext of s2 ) by A12, A21; :: thesis: verum