let L be FinSequence; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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 ;
:: according to TARSKI:def 3 :: thesis: ( not x in the LTLnew of (CastNode (L . 1),v) or x in the LTLold of (CastNode (L . (len L)),v) )
assume B1:
x in the
LTLnew of
(CastNode (L . 1),v)
;
:: thesis: x in the LTLold of (CastNode (L . (len L)),v)
x in Subformulae v
by B1;
then reconsider x =
x as
LTL-formula by MODELC_2:1;
( 1
< len L &
len L <= len L )
by A3, B1, A2, XXREAL_0:1;
then consider m being
Nat such that B3:
( 1
<= m &
m < len L &
x in the
LTLnew of
(CastNode (L . m),v) & not
x in the
LTLnew of
(CastNode (L . (m + 1)),v) )
by ThSucc05, B1, A1, A3;
consider N1,
N2 being
strict LTLnode of
v such that B301:
(
N1 = L . m &
N2 = L . (m + 1) &
N2 is_succ_of N1 )
by B3, A1, DefFinseq;
set m1 =
m + 1;
B302:
N1 = CastNode (L . m),
v
by B301, defCastNode01;
B303:
N2 = CastNode (L . (m + 1)),
v
by B301, defCastNode01;
then B4:
x in the
LTLold of
N2
by B3, B301, B302, ThSucc06, ThSucc08;
( 1
<= m + 1 &
m + 1
<= len L &
len L <= len L )
by B3, NAT_1:13;
then
the
LTLold of
(CastNode (L . (m + 1)),v) c= the
LTLold of
(CastNode (L . (len L)),v)
by A1, ThSucc07;
hence
x in the
LTLold of
(CastNode (L . (len L)),v)
by B303, B4;
:: thesis: verum
end;
hence
the LTLnew of (CastNode (L . 1),v) c= the LTLold of (CastNode (L . (len L)),v)
; :: thesis: verum