let v be LTL-formula; for N being strict LTLnode over v ex n being Nat ex L being FinSequence ex M being strict LTLnode over 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 over v; ex n being Nat ex L being FinSequence ex M being strict LTLnode over 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 over v st len N <= $1 holds
ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v );
A1:
for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume A2:
S1[
l]
;
S1[l + 1]
S1[
l + 1]
proof
let N be
strict LTLnode over
v;
( len N <= l + 1 implies ex n being Nat ex L being FinSequence ex M being strict LTLnode over 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 over
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 A3:
len N <= l + 1
;
ex n being Nat ex L being FinSequence ex M being strict LTLnode over 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 over
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 ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )per cases
( len N <= l or len N = l + 1 )
by A3, NAT_1:8;
suppose A4:
len N = l + 1
;
ex n being Nat ex L being FinSequence ex M being strict LTLnode over 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 Th23;
then consider x being
object such that A5:
x in the
LTLnew of
N
by XBOOLE_0:def 1;
x in Subformulae v
by A5;
then reconsider x =
x as
LTL-formula by MODELC_2:1;
set M1 =
SuccNode1 (
x,
N);
SuccNode1 (
x,
N)
is_succ1_of N
by A5;
then A6:
SuccNode1 (
x,
N)
is_succ_of N
;
then
len (SuccNode1 (x,N)) <= (len N) - 1
by Th21;
then consider n being
Nat,
L being
FinSequence,
M being
strict LTLnode over
v such that A7:
1
<= n
and A8:
len L = n
and A9:
L . 1
= SuccNode1 (
x,
N)
and A10:
L . n = M
and A11:
the
LTLnew of
M = {} v
and A12:
L is_Finseq_for v
by A2, A4;
set L1 =
<*N*> ^ L;
set n1 =
n + 1;
A13:
len (<*N*> ^ L) =
(len <*N*>) + (len L)
by FINSEQ_1:22
.=
n + 1
by A8, FINSEQ_1:39
;
A14:
<*N*> ^ L is_Finseq_for v
proof
let k be
Nat;
MODELC_3:def 19 ( 1 <= k & k < len (<*N*> ^ L) implies ex N, M being strict LTLnode over v st
( N = (<*N*> ^ L) . k & M = (<*N*> ^ L) . (k + 1) & M is_succ_of N ) )
assume that A15:
1
<= k
and A16:
k < len (<*N*> ^ L)
;
ex N, M being strict LTLnode over v st
( N = (<*N*> ^ L) . k & M = (<*N*> ^ L) . (k + 1) & M is_succ_of N )
A17:
k + 1
<= len (<*N*> ^ L)
by A16, NAT_1:13;
ex
N1,
N2 being
strict LTLnode over
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
proof
set N2 =
(<*N*> ^ L) . (k + 1);
set N1 =
(<*N*> ^ L) . k;
now ex N1, N2, N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )per cases
( k <= 1 or 1 < k )
;
suppose
k <= 1
;
ex N1, N2, N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )then A18:
k = 1
by A15, XXREAL_0:1;
then reconsider N1 =
(<*N*> ^ L) . k as
strict LTLnode over
v by FINSEQ_1:41;
len <*N*> = 1
by FINSEQ_1:39;
then A19:
(<*N*> ^ L) . (k + 1) =
L . (2 - 1)
by A17, A18, FINSEQ_1:24
.=
SuccNode1 (
x,
N)
by A9
;
then reconsider N2 =
(<*N*> ^ L) . (k + 1) as
strict LTLnode over
v ;
take N1 =
N1;
ex N2, N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )take N2 =
N2;
ex N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )thus
ex
N1,
N2 being
strict LTLnode over
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
by A6, A18, A19, FINSEQ_1:41;
verum end; suppose A20:
1
< k
;
ex N1, N2, N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )set km1 =
k - 1;
reconsider km1 =
k - 1 as
Nat by A20, NAT_1:20;
1
< km1 + 1
by A20;
then A21:
1
<= km1
by NAT_1:13;
A22:
len <*N*> < k
by A20, FINSEQ_1:39;
then A23:
(<*N*> ^ L) . k =
L . (k - (len <*N*>))
by A16, FINSEQ_1:24
.=
L . km1
by FINSEQ_1:39
;
k <= k + 1
by NAT_1:11;
then
len <*N*> < k + 1
by A22, XXREAL_0:2;
then A24:
(<*N*> ^ L) . (k + 1) =
L . ((k + 1) - (len <*N*>))
by A17, FINSEQ_1:24
.=
L . ((k + 1) - 1)
by FINSEQ_1:39
.=
L . (km1 + 1)
;
A25:
km1 < (n + 1) - 1
by A13, A16, XREAL_1:14;
then A26:
ex
N10,
N20 being
strict LTLnode over
v st
(
L . km1 = N10 &
L . (km1 + 1) = N20 &
N20 is_succ_of N10 )
by A8, A12, A21;
then reconsider N1 =
(<*N*> ^ L) . k as
strict LTLnode over
v by A23;
reconsider N2 =
(<*N*> ^ L) . (k + 1) as
strict LTLnode over
v by A24, A26;
take N1 =
N1;
ex N2, N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )take N2 =
N2;
ex N1, N2 being strict LTLnode over v st
( (<*N*> ^ L) . k = N1 & (<*N*> ^ L) . (k + 1) = N2 & N2 is_succ_of N1 )thus
ex
N1,
N2 being
strict LTLnode over
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
by A8, A12, A21, A25, A23, A24;
verum end; end; end;
hence
ex
N1,
N2 being
strict LTLnode over
v st
(
(<*N*> ^ L) . k = N1 &
(<*N*> ^ L) . (k + 1) = N2 &
N2 is_succ_of N1 )
;
verum
end;
hence
ex
N,
M being
strict LTLnode over
v st
(
N = (<*N*> ^ L) . k &
M = (<*N*> ^ L) . (k + 1) &
M is_succ_of N )
;
verum
end; A27:
len <*N*> = 1
by FINSEQ_1:39;
A28:
(<*N*> ^ L) . 1
= N
by FINSEQ_1:41;
1
< n + 1
by A7, NAT_1:13;
then (<*N*> ^ L) . (n + 1) =
L . ((n + 1) - 1)
by A13, A27, FINSEQ_1:24
.=
M
by A10
;
hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode over
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
by A11, A13, A28, A14, NAT_1:11;
verum end; end; end;
hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode over
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
;
verum
end;
hence
ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode over
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v )
;
verum
end;
hence
(
len N <= l + 1 implies ex
n being
Nat ex
L being
FinSequence ex
M being
strict LTLnode over
v st
( 1
<= n &
len L = n &
L . 1
= N &
L . n = M & the
LTLnew of
M = {} v &
L is_Finseq_for v ) )
;
verum
end;
hence
S1[
l + 1]
;
verum
end;
set k = len N;
reconsider k = len N as Nat ;
A29:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A29, A1);
then
S1[k]
;
hence
ex n being Nat ex L being FinSequence ex M being strict LTLnode over v st
( 1 <= n & len L = n & L . 1 = N & L . n = M & the LTLnew of M = {} v & L is_Finseq_for v )
; verum