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

per cases ( N = 0 or N > 0 ) by A4, XXREAL_0:1;

suppose A22: 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 A23: F . (IC (Comput (F,s,(1 + 1)))) = halt SCM by A8, A11, A18, A10, 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 A11, A10, SCM_1:12;
hence LifeSpan (F,s) = (6 * (N + 1)) - 4 by A22, A23, 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) )
take m = k; :: 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 A22; :: 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 A5, A6, A14, A12, A23, EXTPRO_1:31; :: thesis: verum

end;

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

end;

end;

end;

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