let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis:
assume Z: 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) ) );
A1: 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 A2: S₁[N] ; :: thesis:
A3: 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
A4: Fk = Fib k and
A5: Fk1 = Fib (k + 1) ; :: thesis:
A6: F . 3 = SubFrom ((dl. 1),(dl. 0)) by Z, L14;
set s0 = Comput (F,s,0);
A7: F . 0 = (dl. 1) >0_goto 2 by Z, L14;
set s1 = Comput (F,s,(0 + 1));
A8: F . 1 = halt SCM by Z, L14;
A9: ( IC s = 3 & s = Comput (F,s,0) ) by COMPOS_1:def 20, EXTPRO_1:3;
then A10: IC (Comput (F,s,(0 + 1))) = 3 + 1 by A6, SCM_1:20
.= 4 ;
set s2 = Comput (F,s,(1 + 1));
A11: F . 2 = (dl. 3) := (dl. 0) by Z, L14;
A12: F . 4 = (dl. 1) =0_goto 1 by Z, L14;
s . (dl. 3) = Fk1 by SCM_1:13;
then (Comput (F,s,(0 + 1))) . (dl. 3) = Fk1 by A6, A9, Lm11, SCM_1:20;
then A13: (Comput (F,s,(1 + 1))) . (dl. 3) = Fk1 by A12, A10, SCM_1:24;
A14: F . 7 = AddTo ((dl. 3),(dl. 4)) by Z, L14;
s . (dl. 2) = Fk by SCM_1:13;
then (Comput (F,s,(0 + 1))) . (dl. 2) = Fk by A6, A9, Lm10, SCM_1:20;
then A15: (Comput (F,s,(1 + 1))) . (dl. 2) = Fk by A12, A10, SCM_1:24;
A16: F . 6 = (dl. 2) := (dl. 3) by Z, L14;
A17: s . (dl. 0) = 1 by SCM_1:13;
then (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A6, A9, Lm7, SCM_1:20;
then A18: (Comput (F,s,(1 + 1))) . (dl. 0) = 1 by A12, A10, SCM_1:24;
s . (dl. 1) = N + 1 by SCM_1:13;
then A19: (Comput (F,s,(0 + 1))) . (dl. 1) = (N + 1) - 1 by A6, A17, A9, SCM_1:20
.= N ;
then A20: (Comput (F,s,(1 + 1))) . (dl. 1) = N by A12, A10, SCM_1:24;
A21: F . 5 = (dl. 4) := (dl. 2) by Z, L14;
A22: F . 8 = SCM-goto 3 by Z, L14;

per cases by A3, XXREAL_0:1;

suppose A23: N = 0 ; :: thesis:

then A24: F . (IC (Comput (F,s,(1 + 1)))) = halt SCM by A8, A12, A19, A10, SCM_1:24;
hence F halts_on s by EXTPRO_1:31; :: thesis:
F . (IC (Comput (F,s,(0 + 1)))) <> halt SCM by A12, A10, SCM_1:26;
hence LifeSpan (F,s) = (6 * (N + 1)) - 4 by A23, A24, EXTPRO_1:33; :: thesis:
take m = k; :: thesis:
thus m = (k + (N + 1)) - 1 by A23; :: thesis:
thus ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A4, A5, A15, A13, A24, EXTPRO_1:32; :: thesis:

end;

suppose A25: N > 0 ; :: thesis:

then A26: (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));
A29: IC (Comput (F,s,(1 + 1))) = 4 + 1 by A12, A19, A10, A25, SCM_1:24;
then A30: IC (Comput (F,s,(2 + 1))) = 5 + 1 by A21, SCM_1:18;
then A31: IC (Comput (F,s,(3 + 1))) = 6 + 1 by A16, SCM_1:18;
then A32: IC (Comput (F,s,(4 + 1))) = 7 + 1 by A14, SCM_1:19;
A33: (Comput (F,s,(2 + 1))) . (dl. 3) = Fib (k + 1) by A5, A21, A13, A29, Lm16, SCM_1:18;
then A34: (Comput (F,s,(3 + 1))) . (dl. 3) = Fib (k + 1) by A16, A30, Lm12, SCM_1:18;
(Comput (F,s,(3 + 1))) . (dl. 2) = Fib (k + 1) by A16, A30, A33, SCM_1:18;
then (Comput (F,s,(4 + 1))) . (dl. 2) = Fib (k + 1) by A14, A31, Lm12, SCM_1:19;
then A35: (Comput (F,s,(5 + 1))) . (dl. 2) = Fib (k + 1) by A22, A32, SCM_1:23;
(Comput (F,s,(2 + 1))) . (dl. 0) = 1 by A21, A18, A29, Lm13, SCM_1:18;
then (Comput (F,s,(3 + 1))) . (dl. 0) = 1 by A16, A30, Lm8, SCM_1:18;
then (Comput (F,s,(4 + 1))) . (dl. 0) = 1 by A14, A31, Lm9, SCM_1:19;
then A36: (Comput (F,s,(5 + 1))) . (dl. 0) = 1 by A22, A32, SCM_1:23;
(Comput (F,s,(2 + 1))) . (dl. 4) = Fib k by A4, A21, A15, A29, SCM_1:18;
then A38: (Comput (F,s,(3 + 1))) . (dl. 4) = Fib k by A16, A30, Lm15, SCM_1:18;
(Comput (F,s,(4 + 1))) . (dl. 3) = ((Comput (F,s,(3 + 1))) . (dl. 4)) + ((Comput (F,s,(3 + 1))) . (dl. 3)) by A14, A31, SCM_1:19
.= Fib ((k + 1) + 1) by A34, A38, PRE_FF:1 ;
then A39: (Comput (F,s,(5 + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A22, A32, SCM_1:23;
(Comput (F,s,(2 + 1))) . (dl. 1) = N by A21, A20, A29, Lm14, SCM_1:18;
then (Comput (F,s,(3 + 1))) . (dl. 1) = N by A16, A30, Lm10, SCM_1:18;
then (Comput (F,s,(4 + 1))) . (dl. 1) = N by A14, A31, Lm11, SCM_1:19;
then A40: (Comput (F,s,(5 + 1))) . (dl. 1) = N by A22, A32, SCM_1:23;
IC (Comput (F,s,(5 + 1))) = 3 by A22, A32, SCM_1:23;
then A43: Comput (F,s,(5 + 1)) is 3 -started State-consisting of 0 ,((<*1*> ^ <*N*>) ^ <*Fk1*>) ^ <*(Fib ((k + 1) + 1))*> by A5, A36, A40, A35, A39, COMPOS_1:def 20, SCM_1:30;
then consider m being Element of NAT such that
A44: 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 A2, A5, A25;
A45: F halts_on Comput (F,s,(5 + 1)) by A2, A5, A25, A43;
hence F halts_on s by EXTPRO_1:22; :: thesis:
LifeSpan (F,(Comput (F,s,(5 + 1)))) = (6 * N) - 4 by A2, A5, A25, A43;
hence LifeSpan (F,s) = 6 + ((6 * N) - 4) by A45, A26, EXTPRO_1:35
.= (6 * (N + 1)) - 4 ;
:: thesis:
take m ; :: thesis:
thus m = (k + (N + 1)) - 1 by A44; :: 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 A2, A5, A25, A43;
hence ( (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) by A44, A45, EXTPRO_1:36; :: thesis:

end;

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