let v be LTL-formula; :: thesis: for N being strict LTLnode of v ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )
let N be strict LTLnode of v; :: thesis: ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )
defpred S1[ Nat] means for N being strict LTLnode of v st len N <= $1 holds
ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v );
A1:
S1[ 0 ]
A2:
for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be
Nat;
:: thesis: ( S1[l] implies S1[l + 1] )
assume B1:
S1[
l]
;
:: thesis: S1[l + 1]
S1[
l + 1]
proof
let N be
strict LTLnode of
v;
:: thesis: ( len N <= l + 1 implies ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v ) )
(
len N <= l + 1 implies ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v ) )
proof
assume C0:
len N <= l + 1
;
:: thesis: ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
proof
set NewN = the
LTLnew of
N;
now per cases
( len N <= l or len N = l + 1 )
by C0, NAT_1:8;
suppose C2:
len N = l + 1
;
:: thesis: ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )then
the
LTLnew of
N <> {} v
by Thlen19;
then consider x being
set such that D1:
x in the
LTLnew of
N
by XBOOLE_0:def 1;
x in Subformulae v
by D1;
then reconsider x =
x as
LTL-formula by MODELC_2:1;
set M1 =
SuccNode1 x,
N;
SuccNode1 x,
N is_succ1_of N
by D1, Def208;
then D2:
SuccNode1 x,
N is_succ_of N
by Def210;
then
len (SuccNode1 x,N) <= (len N) - 1
by Thlen17;
then consider n being
Nat,
L being
FinSequence,
M being
strict LTLnode of
v such that D3:
( 1
<= n &
len L = n &
L . 1
= SuccNode1 x,
N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
by C2, B1;
set n1 =
n + 1;
D301:
1
< n + 1
by D3, NAT_1:13;
set L1 =
<*N*> ^ L;
D5:
len (<*N*> ^ L) =
(len <*N*>) + (len L)
by FINSEQ_1:35
.=
n + 1
by D3, FINSEQ_1:56
;
D6:
(<*N*> ^ L) . 1
= N
by FINSEQ_1:58;
len <*N*> = 1
by FINSEQ_1:56;
then D7:
(<*N*> ^ L) . (n + 1) =
L . ((n + 1) - 1)
by D301, D5, FINSEQ_1:37
.=
M
by D3
;
<*N*> ^ L is_Finseq_for v
proof
let k be
Nat;
:: according to MODELC_3:def 19 :: thesis: ( 1 <= k & k < len (<*N*> ^ L) implies ex N, M being strict LTLnode of v st
( N = (<*N*> ^ L) . k & M = (<*N*> ^ L) . (k + 1) & M is_succ_of N ) )
assume that E1:
1
<= k
and E2:
k < len (<*N*> ^ L)
;
:: thesis: ex N, M being strict LTLnode of v st
( N = (<*N*> ^ L) . k & M = (<*N*> ^ L) . (k + 1) & M is_succ_of N )
E3:
k + 1
<= len (<*N*> ^ L)
by E2, NAT_1:13;
ex
N1,
N2 being
strict LTLnode of
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
proof
set N1 =
(<*N*> ^ L) . k;
set N2 =
(<*N*> ^ L) . (k + 1);
now per cases
( k <= 1 or 1 < k )
;
suppose
k <= 1
;
:: thesis: ex N1, N2, N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )then E101:
k = 1
by E1, XXREAL_0:1;
reconsider N1 =
(<*N*> ^ L) . k as
strict LTLnode of
v by E101, FINSEQ_1:58;
E104:
len <*N*> = 1
by FINSEQ_1:56;
E105:
(<*N*> ^ L) . (k + 1) =
L . (2 - 1)
by E104, E101, E3, FINSEQ_1:37
.=
SuccNode1 x,
N
by D3
;
then reconsider N2 =
(<*N*> ^ L) . (k + 1) as
strict LTLnode of
v ;
take N1 =
N1;
:: thesis: ex N2, N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )take N2 =
N2;
:: thesis: ex N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )thus
ex
N1,
N2 being
strict LTLnode of
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
by E101, E105, D2, FINSEQ_1:58;
:: thesis: verum end; suppose E200:
1
< k
;
:: thesis: ex N1, N2, N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )then E201:
len <*N*> < k
by FINSEQ_1:56;
k <= k + 1
by NAT_1:11;
then E202:
len <*N*> < k + 1
by E201, XXREAL_0:2;
set km1 =
k - 1;
reconsider km1 =
k - 1 as
Nat by E200, NAT_1:20;
1
< km1 + 1
by E200;
then E203:
1
<= km1
by NAT_1:13;
E204:
km1 < (n + 1) - 1
by E2, D5, XREAL_1:16;
E205:
(<*N*> ^ L) . k =
L . (k - (len <*N*>))
by E2, E201, FINSEQ_1:37
.=
L . km1
by FINSEQ_1:56
;
E206:
(<*N*> ^ L) . (k + 1) =
L . ((k + 1) - (len <*N*>))
by E3, E202, FINSEQ_1:37
.=
L . ((k + 1) - 1)
by FINSEQ_1:56
.=
L . (km1 + 1)
;
consider N10,
N20 being
strict LTLnode of
v such that E207:
(
L . km1 = N10 &
L . (km1 + 1) = N20 &
N20 is_succ_of N10 )
by E203, E204, D3, DefFinseq;
reconsider N1 =
(<*N*> ^ L) . k as
strict LTLnode of
v by E205, E207;
reconsider N2 =
(<*N*> ^ L) . (k + 1) as
strict LTLnode of
v by E206, E207;
take N1 =
N1;
:: thesis: ex N2, N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )take N2 =
N2;
:: thesis: ex N1, N2 being strict LTLnode of v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )thus
ex
N1,
N2 being
strict LTLnode of
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
by E205, E206, E207;
:: thesis: verum end;
hence
ex
N1,
N2 being
strict LTLnode of
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
;
:: thesis: verum
end;
hence
ex
N,
M being
strict LTLnode of
v st
(
N = (<*N*> ^ L) . k &
M = (<*N*> ^ L) . (k + 1) &
M is_succ_of N )
;
:: thesis: verum
end; hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
by D5, D6, D7, D3, NAT_1:11;
:: thesis: verum end;
hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
;
:: thesis: verum
end;
hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
;
:: thesis: verum
end;
hence
(
len N <= l + 1 implies ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode of
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v ) )
;
:: thesis: verum
end;
hence
S1[
l + 1]
;
:: thesis: verum
end;
A3:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
set k = len N;
reconsider k = len N as Nat ;
S1[k]
by A3;
hence
ex n being Nat ex L being FinSequence ex M being strict LTLnode of v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )
; :: thesis: verum