let H, v be LTL-formula; 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; ( 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
; ( 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, Def6;
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
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)
;
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;
verum
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, Def6;
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
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; verum