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
set ;
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 of
v such that A8:
N1 = L . m
and A9:
N2 = L . (m + 1)
and A10:
N2 is_succ_of N1
by A1, A5, Def19;
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