let m be Nat; :: thesis: for L, L1 being FinSequence
for v being LTL-formula st L is_Finseq_for v & m <= len L & L1 = L | (Seg m) holds
L1 is_Finseq_for v
let L, L1 be FinSequence; :: thesis: for v being LTL-formula st L is_Finseq_for v & m <= len L & L1 = L | (Seg m) holds
L1 is_Finseq_for v
let v be LTL-formula; :: thesis: ( L is_Finseq_for v & m <= len L & L1 = L | (Seg m) implies L1 is_Finseq_for v )
assume that
A1: L is_Finseq_for v and
A2: m <= len L and
A3: L1 = L | (Seg m) ; :: thesis: L1 is_Finseq_for v
reconsider L1 = L1 as FinSequence ;
A4: len L1 = m by A2, A3, FINSEQ_1:17;
A5: dom L1 = Seg m by A2, A3, FINSEQ_1:17;
for k being Nat st 1 <= k & k < len L1 holds
ex N1, N2 being strict LTLnode over v st
( N1 = L1 . k & N2 = L1 . (k + 1) & N2 is_succ_of N1 )

proof

let k be Nat; :: thesis: ( 1 <= k & k < len L1 implies ex N1, N2 being strict LTLnode over v st
( N1 = L1 . k & N2 = L1 . (k + 1) & N2 is_succ_of N1 ) )
assume that
A6: 1 <= k and
A7: k < len L1 ; :: thesis: ex N1, N2 being strict LTLnode over v st
( N1 = L1 . k & N2 = L1 . (k + 1) & N2 is_succ_of N1 )
k in dom L1 by A4, A5, A6, A7, FINSEQ_1:1;
then A8: L1 . k = L . k by A3, FUNCT_1:47;
( 1 <= k + 1 & k + 1 <= m ) by A4, A6, A7, NAT_1:13;
then k + 1 in dom L1 by A5, FINSEQ_1:1;
then A9: L1 . (k + 1) = L . (k + 1) by A3, FUNCT_1:47;
k < len L by A2, A4, A7, XXREAL_0:2;
hence ex N1, N2 being strict LTLnode over v st
( N1 = L1 . k & N2 = L1 . (k + 1) & N2 is_succ_of N1 ) by A1, A6, A8, A9; :: thesis: verum

end;

hence L1 is_Finseq_for v ; :: thesis: verum