let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis:
assume A1: Fib_Program c= F ; :: thesis:
defpred S₁[ Element of NAT ] means for k, Fk, Fk1 being Element of NAT
for s being 3 -started State-consisting of 0 ,((<*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 Element of NAT st S₁[N] holds
S₁[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 Element of NAT ; :: thesis:
assume A3: S₁[N] ; :: thesis:
A4: N >= 0 by NAT_1:2;
let k, Fk, Fk1 be Element of NAT ; :: thesis:
let s be 3 -started State-consisting of 0 ,((<*1*> ^ <*(N + 1)*>) ^ <*Fk*>) ^ <*Fk1*>; :: thesis:
assume that
N + 1 > 0 and
A5: Fk = Fib k and
A6: Fk1 = Fib (k + 1) ; :: thesis:
A7: F . 3 = SubFrom ((dl. 1),(dl. 0)) by A1, Lm17;
set s0 = Comput (F,s,0);
set s1 = Comput (F,s,(0 + 1));
A9: F . 1 = halt SCM by A1, Lm17;
A10: ( IC s = 3 & s = Comput (F,s,0) ) by EXTPRO_1:2, MEMSTR_0:def 9;
then A11: IC (Comput (F,s,(0 + 1))) = 3 + 1 by A7, SCM_1:6
.= 4 ;
set s2 = Comput (F,s,(1 + 1));
A13: 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 A7, A10, Lm11, SCM_1:6;
then A14: (Comput (F,s,(1 + 1))) . (dl. 3) = Fk1 by A13, A11, SCM_1:10;
A15: 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 A7, A10, Lm10, SCM_1:6;
then A16: (Comput (F,s,(1 + 1))) . (dl. 2) = Fk by A13, A11, SCM_1:10;
A17: F . 6 = (dl. 2) := (dl. 3) by A1, Lm17;
A18: s . (dl. 0) = 1 by SCM_1:1;
then (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A7, A10, Lm7, SCM_1:6;
then A19: (Comput (F,s,(1 + 1))) . (dl. 0) = 1 by A13, A11, SCM_1:10;
s . (dl. 1) = N + 1 by SCM_1:1;
then A20: (Comput (F,s,(0 + 1))) . (dl. 1) = (N + 1) - 1 by A7, A18, A10, SCM_1:6
.= N ;
then A21: (Comput (F,s,(1 + 1))) . (dl. 1) = N by A13, A11, SCM_1:10;
A22: F . 5 = (dl. 4) := (dl. 2) by A1, Lm17;
A23: F . 8 = SCM-goto 3 by A1, Lm17;

per cases by A4, XXREAL_0:1;

suppose A24: N = 0 ; :: thesis:

then A25: F . (IC (Comput (F,s,(1 + 1)))) = halt SCM by A9, A13, A20, A11, SCM_1:10;
hence F halts_on s by EXTPRO_1:30; :: thesis:
F . (IC (Comput (F,s,(0 + 1)))) <> halt SCM by A13, A11, SCM_1:12;
hence LifeSpan (F,s) = (6 * (N + 1)) - 4 by A24, A25, EXTPRO_1:32; :: thesis:
take m = k; :: thesis:
thus m = (k + (N + 1)) - 1 by A24; :: thesis:
thus ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A5, A6, A16, A14, A25, EXTPRO_1:31; :: thesis:

end;

suppose A26: N > 0 ; :: thesis:

then A27: (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));
A28: IC (Comput (F,s,(1 + 1))) = 4 + 1 by A13, A20, A11, A26, SCM_1:10;
then A29: IC (Comput (F,s,(2 + 1))) = 5 + 1 by A22, SCM_1:4;
then A30: IC (Comput (F,s,(3 + 1))) = 6 + 1 by A17, SCM_1:4;
then A31: IC (Comput (F,s,(4 + 1))) = 7 + 1 by A15, SCM_1:5;
A32: (Comput (F,s,(2 + 1))) . (dl. 3) = Fib (k + 1) by A6, A22, A14, A28, Lm16, SCM_1:4;
then A33: (Comput (F,s,(3 + 1))) . (dl. 3) = Fib (k + 1) by A17, A29, Lm12, SCM_1:4;
(Comput (F,s,(3 + 1))) . (dl. 2) = Fib (k + 1) by A17, A29, A32, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 2) = Fib (k + 1) by A15, A30, Lm12, SCM_1:5;
then A34: (Comput (F,s,(5 + 1))) . (dl. 2) = Fib (k + 1) by A23, A31, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 0) = 1 by A22, A19, A28, Lm13, SCM_1:4;
then (Comput (F,s,(3 + 1))) . (dl. 0) = 1 by A17, A29, Lm8, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 1 by A15, A30, Lm9, SCM_1:5;
then A35: (Comput (F,s,(5 + 1))) . (dl. 0) = 1 by A23, A31, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 4) = Fib k by A5, A22, A16, A28, SCM_1:4;
then A36: (Comput (F,s,(3 + 1))) . (dl. 4) = Fib k by A17, A29, 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 A15, A30, SCM_1:5
.= Fib ((k + 1) + 1) by A33, A36, PRE_FF:1 ;
then A37: (Comput (F,s,(5 + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A23, A31, SCM_1:9;
(Comput (F,s,(2 + 1))) . (dl. 1) = N by A22, A21, A28, Lm14, SCM_1:4;
then (Comput (F,s,(3 + 1))) . (dl. 1) = N by A17, A29, Lm10, SCM_1:4;
then (Comput (F,s,(4 + 1))) . (dl. 1) = N by A15, A30, Lm11, SCM_1:5;
then A38: (Comput (F,s,(5 + 1))) . (dl. 1) = N by A23, A31, SCM_1:9;
IC (Comput (F,s,(5 + 1))) = 3 by A23, A31, SCM_1:9;
then A39: Comput (F,s,(5 + 1)) is 3 -started State-consisting of 0 ,((<*1*> ^ <*N*>) ^ <*Fk1*>) ^ <*(Fib ((k + 1) + 1))*> by A6, A35, A38, A34, A37, MEMSTR_0:def 9, SCM_1:13;
then consider m being Element of NAT such that
A40: 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, A6, A26;
A41: F halts_on Comput (F,s,(5 + 1)) by A3, A6, A26, A39;
hence F halts_on s by EXTPRO_1:22; :: thesis:
LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * N) - 4 by A3, A6, A26, A39;
hence LifeSpan (F,s) = 6 + ((6 * N) - 4) by A41, A27, EXTPRO_1:34
.= (6 * (N + 1)) - 4 ;
:: thesis:
take m ; :: thesis:
thus m = (k + (N + 1)) - 1 by A40; :: thesis:
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, A6, A26, A39;
hence ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A40, A41, EXTPRO_1:35; :: thesis:

end;

A42: S₁[ 0 ] ;
thus for N being Element of NAT holds S₁[N] from NAT_1:sch 1(A42, A2); :: thesis: