let m be Nat; for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L holds
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) )
let L be FinSequence; for v being LTL-formula st L is_Finseq_for v & 1 <= m & m <= len L holds
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) )
let v be LTL-formula; ( L is_Finseq_for v & 1 <= m & m <= len L implies 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) ) )
assume that
A1:
L is_Finseq_for v
and
A2:
1 <= m
and
A3:
m <= len L
; 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) )
A4:
m - 1 <= (len L) - 0
by A3, XREAL_1:13;
set m1 = m - 1;
reconsider m1 = m - 1 as Nat by A2, NAT_1:21;
set L1 = L | (Seg m1);
reconsider L1 = L | (Seg m1) as FinSequence by FINSEQ_1:15;
consider L2 being FinSequence such that
A5:
L = L1 ^ L2
by FINSEQ_1:80;
len L = (len L1) + (len L2)
by A5, FINSEQ_1:22;
then A6: len L2 =
(len L) - (len L1)
.=
(len L) - m1
by A4, FINSEQ_1:17
;
m - m <= (len L) - m
by A3, XREAL_1:9;
then A7:
0 + 1 <= ((len L) - m) + 1
by XREAL_1:6;
then
1 in dom L2
by A6, FINSEQ_3:25;
then A8: L2 . 1 =
L . ((len L1) + 1)
by A5, FINSEQ_1:def 7
.=
L . (m1 + 1)
by A4, FINSEQ_1:17
.=
L . m
;
A9:
len L1 = m1
by A4, FINSEQ_1:17;
for k being Nat st 1 <= k & k < len L2 holds
ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N )
proof
let k be
Nat;
( 1 <= k & k < len L2 implies ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N ) )
assume A10:
( 1
<= k &
k < len L2 )
;
ex N, M being strict LTLnode over v st
( N = L2 . k & M = L2 . (k + 1) & M is_succ_of N )
set k1 =
k + 1;
( 1
<= k + 1 &
k + 1
<= len L2 )
by A10, NAT_1:13;
then A11:
k + 1
in dom L2
by FINSEQ_3:25;
set km1 =
k + m1;
( 1
+ 0 <= k + m1 &
k + m1 < ((len L) - m1) + m1 )
by A6, A10, XREAL_1:6, XREAL_1:7;
then consider N,
M being
strict LTLnode over
v such that A12:
N = L . (k + m1)
and A13:
M = L . ((k + m1) + 1)
and A14:
M is_succ_of N
by A1;
A15:
M =
L . (m1 + (k + 1))
by A13
.=
L2 . (k + 1)
by A9, A5, A11, FINSEQ_1:def 7
;
k in dom L2
by A10, FINSEQ_3:25;
then
N = L2 . k
by A9, A5, A12, FINSEQ_1:def 7;
hence
ex
N,
M being
strict LTLnode over
v st
(
N = L2 . k &
M = L2 . (k + 1) &
M is_succ_of N )
by A14, A15;
verum
end;
then A16:
L2 is_Finseq_for v
;
len L2 in dom L2
by A7, A6, FINSEQ_3:25;
then L2 . (len L2) =
L . ((len L1) + (len L2))
by A5, FINSEQ_1:def 7
.=
L . (len L)
by A5, FINSEQ_1:22
;
hence
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 A7, A5, A6, A8, A16; verum