defpred S₁[ Element of NAT ] means for k, Fk, Fk1 being Element of NAT
for s being State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*$1*>) ^ <*Fk*>) ^ <*Fk1*> st $1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( ProgramPart s halts_on s & LifeSpan s = (6 * $1) - 4 & ex m being Element of NAT st
( m = (k + $1) - 1 & (Result s) . (dl. 2) = Fib m & (Result 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: ( S₁[N] implies S₁[N + 1] )
assume A2: S₁[N] ; :: thesis: S₁[N + 1]
A3: N >= 0 by NAT_1:2;
let k, Fk, Fk1 be Element of NAT ; :: thesis: for s being State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*(N + 1)*>) ^ <*Fk*>) ^ <*Fk1*> st N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( ProgramPart s halts_on s & LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )
let s be State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*(N + 1)*>) ^ <*Fk*>) ^ <*Fk1*>; :: thesis: ( N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) implies ( ProgramPart s halts_on s & LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) ) )
assume that
N + 1 > 0 and
A4: Fk = Fib k and
A5: Fk1 = Fib (k + 1) ; :: thesis: ( ProgramPart s halts_on s & LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )
A6: s . (il. 3) = SubFrom (dl. 1),(dl. 0 ) by SCM_1:14;
set s0 = Computation s,0 ;
A7: s . (il. 0 ) = (dl. 1) >0_goto (il. 2) by SCM_1:14;
set s1 = Computation s,(0 + 1);
A8: s . (il. 1) = halt SCM by SCM_1:14;
A9: ( IC s = il. 3 & s = Computation s,0 ) by AMI_1:13, SCM_1:def 1;
then A10: IC (Computation s,(0 + 1)) = il. (3 + 1) by A6, SCM_1:20
.= il. 4 ;
set s2 = Computation s,(1 + 1);
A11: s . (il. 2) = (dl. 3) := (dl. 0 ) by SCM_1:14;
A12: s . (il. 4) = (dl. 1) =0_goto (il. 1) by SCM_1:14;
s . (dl. 3) = Fk1 by SCM_1:14;
then (Computation s,(0 + 1)) . (dl. 3) = Fk1 by A6, A9, Lm11, SCM_1:20;
then A13: (Computation s,(1 + 1)) . (dl. 3) = Fk1 by A12, A10, SCM_1:24;
A14: s . (il. 7) = AddTo (dl. 3),(dl. 4) by SCM_1:14;
s . (dl. 2) = Fk by SCM_1:14;
then (Computation s,(0 + 1)) . (dl. 2) = Fk by A6, A9, Lm10, SCM_1:20;
then A15: (Computation s,(1 + 1)) . (dl. 2) = Fk by A12, A10, SCM_1:24;
A16: s . (il. 6) = (dl. 2) := (dl. 3) by SCM_1:14;
A17: s . (dl. 0 ) = 1 by SCM_1:14;
then (Computation s,(0 + 1)) . (dl. 0 ) = 1 by A6, A9, Lm7, SCM_1:20;
then A18: (Computation s,(1 + 1)) . (dl. 0 ) = 1 by A12, A10, SCM_1:24;
s . (dl. 1) = N + 1 by SCM_1:14;
then A19: (Computation s,(0 + 1)) . (dl. 1) = (N + 1) - 1 by A6, A17, A9, SCM_1:20
.= N ;
then A20: (Computation s,(1 + 1)) . (dl. 1) = N by A12, A10, SCM_1:24;
A21: s . (il. 5) = (dl. 4) := (dl. 2) by SCM_1:14;
A22: s . (il. 8) = goto (il. 3) by SCM_1:14;

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

suppose A23: N = 0 ; :: thesis: ( ProgramPart s halts_on s & LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )

then A24: s . (IC (Computation s,(1 + 1))) = halt SCM by A8, A12, A19, A10, SCM_1:24;
hence ProgramPart s halts_on s by SCM_1:3; :: thesis: ( LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )
s . (IC (Computation s,(0 + 1))) <> halt SCM by A12, A10, SCM_1:26;
hence LifeSpan s = (6 * (N + 1)) - 4 by A23, A24, SCM_1:16; :: thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
take m = k; :: thesis: ( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
thus m = (k + (N + 1)) - 1 by A23; :: thesis: ( (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
thus ( (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) by A4, A5, A15, A13, A24, SCM_1:4; :: thesis: verum

end;

suppose A25: N > 0 ; :: thesis: ( ProgramPart s halts_on s & LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )

then A26: (6 * N) - 4 > 0 by Lm6;
set Fk2 = Fib ((k + 1) + 1);
set s6 = Computation s,(5 + 1);
A27: (Computation s,(5 + 1)) . (il. 8) = goto (il. 3) by A22, AMI_1:54;
A28: ( (Computation s,(5 + 1)) . (il. 0 ) = (dl. 1) >0_goto (il. 2) & (Computation s,(5 + 1)) . (il. 1) = halt SCM ) by A7, A8, AMI_1:54;
set s5 = Computation s,(4 + 1);
set s4 = Computation s,(3 + 1);
set s3 = Computation s,(2 + 1);
A29: IC (Computation s,(1 + 1)) = il. (4 + 1) by A12, A19, A10, A25, SCM_1:24;
then A30: IC (Computation s,(2 + 1)) = il. (5 + 1) by A21, SCM_1:18;
then A31: IC (Computation s,(3 + 1)) = il. (6 + 1) by A16, SCM_1:18;
then A32: IC (Computation s,(4 + 1)) = il. (7 + 1) by A14, SCM_1:19;
A33: (Computation s,(2 + 1)) . (dl. 3) = Fib (k + 1) by A5, A21, A13, A29, Lm16, SCM_1:18;
then A34: (Computation s,(3 + 1)) . (dl. 3) = Fib (k + 1) by A16, A30, Lm12, SCM_1:18;
(Computation s,(3 + 1)) . (dl. 2) = Fib (k + 1) by A16, A30, A33, SCM_1:18;
then (Computation s,(4 + 1)) . (dl. 2) = Fib (k + 1) by A14, A31, Lm12, SCM_1:19;
then A35: (Computation s,(5 + 1)) . (dl. 2) = Fib (k + 1) by A22, A32, SCM_1:23;
(Computation s,(2 + 1)) . (dl. 0 ) = 1 by A21, A18, A29, Lm13, SCM_1:18;
then (Computation s,(3 + 1)) . (dl. 0 ) = 1 by A16, A30, Lm8, SCM_1:18;
then (Computation s,(4 + 1)) . (dl. 0 ) = 1 by A14, A31, Lm9, SCM_1:19;
then A36: (Computation s,(5 + 1)) . (dl. 0 ) = 1 by A22, A32, SCM_1:23;
A37: ( (Computation s,(5 + 1)) . (il. 6) = (dl. 2) := (dl. 3) & (Computation s,(5 + 1)) . (il. 7) = AddTo (dl. 3),(dl. 4) ) by A16, A14, AMI_1:54;
(Computation s,(2 + 1)) . (dl. 4) = Fib k by A4, A21, A15, A29, SCM_1:18;
then A38: (Computation s,(3 + 1)) . (dl. 4) = Fib k by A16, A30, Lm15, SCM_1:18;
(Computation s,(4 + 1)) . (dl. 3) = ((Computation s,(3 + 1)) . (dl. 4)) + ((Computation s,(3 + 1)) . (dl. 3)) by A14, A31, SCM_1:19
.= Fib ((k + 1) + 1) by A34, A38, PRE_FF:1 ;
then A39: (Computation s,(5 + 1)) . (dl. 3) = Fib ((k + 1) + 1) by A22, A32, SCM_1:23;
(Computation s,(2 + 1)) . (dl. 1) = N by A21, A20, A29, Lm14, SCM_1:18;
then (Computation s,(3 + 1)) . (dl. 1) = N by A16, A30, Lm10, SCM_1:18;
then (Computation s,(4 + 1)) . (dl. 1) = N by A14, A31, Lm11, SCM_1:19;
then A40: (Computation s,(5 + 1)) . (dl. 1) = N by A22, A32, SCM_1:23;
A41: ( (Computation s,(5 + 1)) . (il. 4) = (dl. 1) =0_goto (il. 1) & (Computation s,(5 + 1)) . (il. 5) = (dl. 4) := (dl. 2) ) by A12, A21, AMI_1:54;
A42: ( (Computation s,(5 + 1)) . (il. 2) = (dl. 3) := (dl. 0 ) & (Computation s,(5 + 1)) . (il. 3) = SubFrom (dl. 1),(dl. 0 ) ) by A11, A6, AMI_1:54;
IC (Computation s,(5 + 1)) = il. 3 by A22, A32, SCM_1:23;
then A43: Computation s,(5 + 1) is State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*N*>) ^ <*Fk1*>) ^ <*(Fib ((k + 1) + 1))*> by A5, A36, A40, A35, A39, A28, A42, A41, A37, A27, SCM_1:30;
then consider m being Element of NAT such that
A44: m = ((k + 1) + N) - 1 and
(Result (Computation s,(5 + 1))) . (dl. 2) = Fib m and
(Result (Computation s,(5 + 1))) . (dl. 3) = Fib (m + 1) by A2, A5, A25;
A45: ProgramPart (Computation s,(5 + 1)) halts_on Computation s,(5 + 1) by A2, A5, A25, A43;
then Y: ProgramPart s halts_on Computation s,(5 + 1) by AMI_1:144;
hence ProgramPart s halts_on s by AMI_1:93; :: thesis: ( LifeSpan s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) )
LifeSpan (Computation s,(5 + 1)) = (6 * N) - 4 by A2, A5, A25, A43;
hence LifeSpan s = 6 + ((6 * N) - 4) by A45, A26, SCM_1:28
.= (6 * (N + 1)) - 4 ;
:: thesis: ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
take m ; :: thesis: ( m = (k + (N + 1)) - 1 & (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
thus m = (k + (N + 1)) - 1 by A44; :: thesis: ( (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) )
X: Result (Computation s,(5 + 1)) = Result s by SCM_1:29, A2, A5, A25, A43, Y;
ex m being Element of NAT st
( m = ((k + 1) + N) - 1 & (Result (Computation s,(5 + 1))) . (dl. 2) = Fib m & (Result (Computation s,(5 + 1))) . (dl. 3) = Fib (m + 1) ) by A2, A5, A25, A43;
hence ( (Result s) . (dl. 2) = Fib m & (Result s) . (dl. 3) = Fib (m + 1) ) by A45, A44, SCM_1:29, X; :: thesis: verum

end;

end;

end;

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