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