let v be LTL-formula; for s1, s2 being strict elementary LTLnode over v st s2 is_next_of s1 holds
the LTLnext of s1 c= the LTLold of s2
let s1, s2 be strict elementary LTLnode over v; ( s2 is_next_of s1 implies the LTLnext of s1 c= the LTLold of s2 )
set N1 = 'X' s1;
A1:
the LTLnew of s2 = {} v
by Def11;
assume
s2 is_next_of s1
; the LTLnext of s1 c= the LTLold of s2
then consider L being FinSequence such that
A2:
1 <= len L
and
A3:
L is_Finseq_for v
and
A4:
L . 1 = 'X' s1
and
A5:
L . (len L) = s2
;
set n = len L;
A6:
CastNode ((L . (len L)),v) = s2
by A5, Def16;
A7:
CastNode ((L . 1),v) = 'X' s1
by A4, Def16;
the LTLnext of s1 c= the LTLold of s2
proof
let x be
object ;
TARSKI:def 3 ( not x in the LTLnext of s1 or x in the LTLold of s2 )
assume A8:
x in the
LTLnext of
s1
;
x in the LTLold of s2
then
x in Subformulae v
;
then reconsider x =
x as
LTL-formula by MODELC_2:1;
1
< len L
by A2, A4, A5, A1, A8, XXREAL_0:1;
then consider m being
Nat such that A9:
( 1
<= m &
m < len L )
and A10:
(
x in the
LTLnew of
(CastNode ((L . m),v)) & not
x in the
LTLnew of
(CastNode ((L . (m + 1)),v)) )
by A3, A7, A6, A1, A8, Th29;
set m1 =
m + 1;
consider N1,
N2 being
strict LTLnode over
v such that A11:
N1 = L . m
and A12:
N2 = L . (m + 1)
and A13:
N2 is_succ_of N1
by A3, A9;
A14:
N2 = CastNode (
(L . (m + 1)),
v)
by A12, Def16;
( 1
<= m + 1 &
m + 1
<= len L )
by A9, NAT_1:13;
then A15:
the
LTLold of
N2 c= the
LTLold of
(CastNode ((L . (len L)),v))
by A3, A14, Th31;
N1 = CastNode (
(L . m),
v)
by A11, Def16;
then
x in the
LTLold of
N2
by A10, A13, A14, Th30, Th32;
hence
x in the
LTLold of
s2
by A6, A15;
verum
end;
hence
the LTLnext of s1 c= the LTLold of s2
; verum