let m be Nat; 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; 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; ( 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)
; 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;
( 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
;
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;
verum
end;
hence
L1 is_Finseq_for v
; verum