let v be LTL-formula; :: thesis: 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; :: thesis: 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; :: thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; :: thesis: S1[l + 1]
S1[l + 1]
proof
let N be strict LTLnode over v; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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 len N <= l ; :: thesis: 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 )
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 A2; :: thesis: verum
end;
suppose A4: len N = l + 1 ; :: thesis: 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; :: according to MODELC_3:def 19 :: thesis: ( 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) ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
suppose A20: 1 < k ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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 ) ; :: thesis: 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 ) ) ; :: thesis: verum
end;
hence S1[l + 1] ; :: thesis: verum
end;
set k = len N;
reconsider k = len N as Nat ;
A29: S1[ 0 ]
proof
let N be strict LTLnode over v; :: thesis: ( len N <= 0 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 <= 0 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
set n = 1;
set M = N;
assume A30: len N <= 0 ; :: thesis: 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 )
take 1 ; :: thesis: ex L being FinSequence ex M being strict LTLnode over v st
( 1 <= 1 & len L = 1 & L . 1 = N & L . 1 = M & the LTLnew of M = {} v & L is_Finseq_for v )
set L = <*N*>;
take <*N*> ; :: thesis: ex M being strict LTLnode over v st
( 1 <= 1 & len <*N*> = 1 & <*N*> . 1 = N & <*N*> . 1 = M & the LTLnew of M = {} v & <*N*> is_Finseq_for v )
take N ; :: thesis: ( 1 <= 1 & len <*N*> = 1 & <*N*> . 1 = N & <*N*> . 1 = N & the LTLnew of N = {} v & <*N*> is_Finseq_for v )
thus ( 1 <= 1 & len <*N*> = 1 & <*N*> . 1 = N & <*N*> . 1 = N & the LTLnew of N = {} v & <*N*> is_Finseq_for v ) by A30, Th22, FINSEQ_1:40; :: thesis: verum
end;
hence ( len N <= 0 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 ) ) ; :: thesis: verum
end;
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 ) ; :: thesis: verum