let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( Fib_Program c= F implies for N, k, Fk, Fk1 being Nat
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) ) )
assume A1: Fib_Program c= F ; :: thesis: for N, k, Fk, Fk1 being Nat
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
defpred S1[ Nat] means for k, Fk, Fk1 being Nat
for s being 3 -started State-consisting of <%1,$1,Fk,Fk1%> st $1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * $1) - 4 & ex m being Element of NAT st
( m = (k + $1) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) );
A2: for N being Nat st S1[N] holds
S1[N + 1]
proof
set C1 = dl. 0;
set n = dl. 1;
set FP = dl. 2;
set FC = dl. 3;
set AUX = dl. 4;
let N be Nat; :: thesis: ( S1[N] implies S1[N + 1] )
assume A3: S1[N] ; :: thesis: S1[N + 1]
let k, Fk, Fk1 be Nat; :: thesis: for s being 3 -started State-consisting of <%1,(N + 1),Fk,Fk1%> st N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
let s be 3 -started State-consisting of <%1,(N + 1),Fk,Fk1%>; :: thesis: ( N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) implies ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) ) )
assume that
N + 1 > 0 and
A4: Fk = Fib k and
A5: Fk1 = Fib (k + 1) ; :: thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
A6: F . 3 = SubFrom ((dl. 1),(dl. 0)) by A1, Lm17;
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A7: F . 1 = halt SCM by A1, Lm17;
A8: ( IC s = 3 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def 12;
then A9: IC (Comput (F,s,(0 + 1))) = 3 + 1 by A6, SCM_1:6
.= 4 ;
set s2 = Comput (F,s,(1 + 1));
A10: F . 4 = (dl. 1) =0_goto 1 by A1, Lm17;
s . (dl. 3) = Fk1 by SCM_1:1;
then (Comput (F,s,(0 + 1))) . (dl. 3) = Fk1 by A6, A8, Lm11, SCM_1:6;
then A11: (Comput (F,s,(1 + 1))) . (dl. 3) = Fk1 by A10, A9, SCM_1:10;
A12: F . 7 = AddTo ((dl. 3),(dl. 4)) by A1, Lm17;
s . (dl. 2) = Fk by SCM_1:1;
then (Comput (F,s,(0 + 1))) . (dl. 2) = Fk by A6, A8, Lm10, SCM_1:6;
then A13: (Comput (F,s,(1 + 1))) . (dl. 2) = Fk by A10, A9, SCM_1:10;
A14: F . 6 = (dl. 2) := (dl. 3) by A1, Lm17;
A15: s . (dl. 0) = 1 by SCM_1:1;
then (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A6, A8, Lm7, SCM_1:6;
then A16: (Comput (F,s,(1 + 1))) . (dl. 0) = 1 by A10, A9, SCM_1:10;
s . (dl. 1) = N + 1 by SCM_1:1;
then A17: (Comput (F,s,(0 + 1))) . (dl. 1) = (N + 1) - 1 by A6, A15, A8, SCM_1:6
.= N ;
then A18: (Comput (F,s,(1 + 1))) . (dl. 1) = N by A10, A9, SCM_1:10;
A19: F . 5 = (dl. 4) := (dl. 2) by A1, Lm17;
A20: F . 8 = SCM-goto 3 by A1, Lm17;
per cases ( N = 0 or N > 0 ) ;
suppose A21: N = 0 ; :: thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
then A22: F . (IC (Comput (F,s,(1 + 1)))) = halt SCM by A7, A10, A17, A9, SCM_1:10;
hence F halts_on s by EXTPRO_1:30; :: thesis: ( LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
F . (IC (Comput (F,s,(0 + 1)))) <> halt SCM by A10, A9, SCM_1:12;
hence LifeSpan (F,s) = (6 * (N + 1)) - 4 by A21, A22, EXTPRO_1:32; :: thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
reconsider m = k as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: ( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus m = (k + (N + 1)) - 1 by A21; :: thesis: ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A4, A5, A13, A11, A22, EXTPRO_1:7; :: thesis: verum
end;
suppose A23: N > 0 ; :: thesis: ( F halts_on s & LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
then A24: (6 * N) - 4 > 0 by Lm6;
set Fk2 = Fib ((k + 1) + 1);
set s6 = Comput (F,s,(5 + 1));
set s5 = Comput (F,s,(4 + 1));
set s4 = Comput (F,s,(3 + 1));
set s3 = Comput (F,s,(2 + 1));
A25: IC (Comput (F,s,(1 + 1))) = 4 + 1 by A10, A17, A9, A23, SCM_1:10;
then A26: IC (Comput (F,s,(2 + 1))) = 5 + 1 by A19, SCM_1:4;
then A27: IC (Comput (F,s,(3 + 1))) = 6 + 1 by A14, SCM_1:4;
then A28: IC (Comput (F,s,(4 + 1))) = 7 + 1 by A12, SCM_1:5;
A29: (Comput (F,s,(2 + 1))) . (dl. 3) = Fib (k + 1) by A5, A19, A11, A25, Lm16, SCM_1:4;
then A30: (Comput (F,s,(3 + 1))) . (dl. 3) = Fib (k + 1) by A14, A26, Lm12, SCM_1:4;
(Comput (F,s,(3 + 1))) . (dl. 2) = Fib (k + 1) by A14, A26, A29, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 2) = Fib (k + 1) by A12, A27, Lm12, SCM_1:5;
then A31: (Comput (F,s,(5 + 1))) . (dl. 2) = Fib (k + 1) by A20, A28, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 0) = 1 by A19, A16, A25, Lm13, SCM_1:4;
then (Comput (F,s,(3 + 1))) . (dl. 0) = 1 by A14, A26, Lm8, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 1 by A12, A27, Lm9, SCM_1:5;
then A32: (Comput (F,s,(5 + 1))) . (dl. 0) = 1 by A20, A28, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 4) = Fib k by A4, A19, A13, A25, SCM_1:4;
then A33: (Comput (F,s,(3 + 1))) . (dl. 4) = Fib k by A14, A26, Lm15, SCM_1:4;
(Comput (F,s,(4 + 1))) . (dl. 3) = ((Comput (F,s,(3 + 1))) . (dl. 4)) + ((Comput (F,s,(3 + 1))) . (dl. 3)) by A12, A27, SCM_1:5
.= Fib ((k + 1) + 1) by A30, A33, PRE_FF:1 ;
then A34: (Comput (F,s,(5 + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A20, A28, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 1) = N by A19, A18, A25, Lm14, SCM_1:4;
then (Comput (F,s,(3 + 1))) . (dl. 1) = N by A14, A26, Lm10, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 1) = N by A12, A27, Lm11, SCM_1:5;
then A35: (Comput (F,s,(5 + 1))) . (dl. 1) = N by A20, A28, SCM_1:9;
IC (Comput (F,s,(5 + 1))) = 3 by A20, A28, SCM_1:9;
then A36: Comput (F,s,(5 + 1)) is 3 -started State-consisting of <%1,N,Fk1,(Fib ((k + 1) + 1))%> by A5, A32, A35, A31, A34, MEMSTR_0:def 12, SCM_1:13;
then consider m being Element of NAT such that
A37: m = ((k + 1) + N) - 1 and
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 2) = Fib m and
(Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fib (m + 1) by A3, A5, A23;
F halts_on Comput (F,s,(5 + 1)) by A3, A5, A23, A36;
hence F halts_on s by EXTPRO_1:22; :: thesis: ( LifeSpan (F,s) = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )
LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * N) - 4 by A3, A5, A23, A36;
hence LifeSpan (F,s) = 6 + ((6 * N) - 4) by A3, A5, A23, A36, A24, EXTPRO_1:34
.= (6 * (N + 1)) - 4 ;
:: thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
take m ; :: thesis: ( m = (k + (N + 1)) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
thus m = (k + (N + 1)) - 1 by A37; :: thesis: ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) )
ex m being Element of NAT st
( m = ((k + 1) + N) - 1 & (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 2) = Fib m & (Result (F,(Comput (F,s,(5 + 1))))) . (dl. 3) = Fib (m + 1) ) by A3, A5, A23, A36;
hence ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A37, A3, A5, A23, A36, EXTPRO_1:35; :: thesis: verum
end;
end;
end;
A38: S1[ 0 ] ;
thus for N being Nat holds S1[N] from NAT_1:sch 2(A38, A2); :: thesis: verum