let m be Nat; :: thesis: for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds
the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))
let L be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v holds
the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & 1 <= m & m <= len L & the LTLnew of (CastNode ((L . (len L)),v)) = {} v implies the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v)) )
assume that
A1: ( L is_Finseq_for v & 1 <= m & m <= len L ) and
A2: the LTLnew of (CastNode ((L . (len L)),v)) = {} v ; :: thesis: the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v))
ex L1, L2 being FinSequence st
( L2 is_Finseq_for v & L = L1 ^ L2 & L2 . 1 = L . m & 1 <= len L2 & len L2 = (len L) - (m - 1) & L2 . (len L2) = L . (len L) ) by A1, Lm15;
hence the LTLnew of (CastNode ((L . m),v)) c= the LTLold of (CastNode ((L . (len L)),v)) by A2, Th33; :: thesis: verum