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 LTLnext of s1 holds
( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )
let s1, s2 be strict elementary LTLnode over 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 and
A3: H in the LTLnext of s1 ; :: thesis: ( the_right_argument_of H in the LTLold of s2 & H in the LTLold of s2 )
A4: the LTLnext of s1 c= the LTLold of s2 by A1, Th37;
then 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;
A9: the LTLnew of s2 = {} v by Def11;
set M1 = CastNode ((L . m),v);
set m1 = m + 1;
set M2 = CastNode ((L . (m + 1)),v);
set n = len L;
A10: CastNode ((L . (len L)),v) = s2 by A6, Def16;
( 1 <= m + 1 & m + 1 <= len L ) by A7, NAT_1:13;
then A11: the LTLnew of (CastNode ((L . (m + 1)),v)) c= the LTLold of s2 by A5, A10, A9, Th34;
LTLNew2 H = {(the_left_argument_of H),(the_right_argument_of H)} by A2, Def2;
then A12: the_right_argument_of H in LTLNew2 H by TARSKI:def 2;
LTLNew1 H = {(the_right_argument_of H)} by A2, Def1;
then A13: the_right_argument_of H in LTLNew1 H by TARSKI:def 1;
A14: the LTLold of (CastNode ((L . m),v)) c= the LTLold of s2 by A5, A7, A10, Th31;
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 ( 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 A15: 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 :: thesis: the_right_argument_of H in the LTLold of s2
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 A8;
suppose A16: ( 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 A13, A15, 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 A16, Def4;
hence the_right_argument_of H in the LTLold of s2 by A11; :: thesis: verum
end;
suppose A17: ( 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 A12, A15, 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 A17, Def5;
hence the_right_argument_of H in the LTLold of s2 by A11; :: 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 A3, A4; :: thesis: verum