let N be Element of NAT ; :: thesis: for s being State-consisting of 0 , 0 , 0 , Fib_Program ,((<*1*> ^ <*N*>) ^ <*0 *>) ^ <*0 *> holds
( ProgramPart s halts_on s & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )
let s be State-consisting of 0 , 0 , 0 , Fib_Program ,((<*1*> ^ <*N*>) ^ <*0 *>) ^ <*0 *>; :: thesis: ( ProgramPart s halts_on s & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )
set C1 = dl. 0 ;
set n = dl. 1;
set FP = dl. 2;
set FC = dl. 3;
set AUX = dl. 4;
set L6 = il. 6;
set L7 = il. 7;
set L8 = il. 8;
set L0 = il. 0 ;
set L1 = il. 1;
set L2 = il. 2;
set L3 = il. 3;
set L4 = il. 4;
set L5 = il. 5;
A1: ( IC s = il. 0 & s . (il. 0 ) = (dl. 1) >0_goto (il. 2) ) by SCM_1:14, SCM_1:def 1;
set s1 = Computation s,(0 + 1);
set s0 = Computation s,0 ;
A2: s = Computation s,0 by AMI_1:13;
s . (dl. 0 ) = 1 by SCM_1:14;
then A3: (Computation s,(0 + 1)) . (dl. 0 ) = 1 by A1, A2, SCM_1:25;
A4: s . (il. 3) = SubFrom (dl. 1),(dl. 0 ) by SCM_1:14;
s . (dl. 2) = 0 by SCM_1:14;
then A5: (Computation s,(0 + 1)) . (dl. 2) = 0 by A1, A2, SCM_1:25;
A6: s . (il. 4) = (dl. 1) =0_goto (il. 1) by SCM_1:14;
s . (dl. 3) = 0 by SCM_1:14;
then A7: (Computation s,(0 + 1)) . (dl. 3) = 0 by A1, A2, SCM_1:25;
A8: s . (il. 6) = (dl. 2) := (dl. 3) by SCM_1:14;
defpred S₁[ Element of NAT ] means ( $1 < N implies for u being State of st u = Computation s,((6 * $1) + 3) holds
( u . (dl. 0 ) = 1 & u . (dl. 1) = (N - 1) - $1 & u . (dl. 2) = Fib $1 & u . (dl. 3) = Fib ($1 + 1) & IC u = il. 4 ) );
A9: s . (il. 2) = (dl. 3) := (dl. 0 ) by SCM_1:14;
A10: s . (il. 7) = AddTo (dl. 3),(dl. 4) by SCM_1:14;
A11: s . (il. 8) = goto (il. 3) by SCM_1:14;
A12: s . (il. 5) = (dl. 4) := (dl. 2) by SCM_1:14;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A14: ( k < N implies for u being State of st u = Computation s,((6 * k) + 3) holds
( u . (dl. 0 ) = 1 & u . (dl. 1) = (N - 1) - k & u . (dl. 2) = Fib k & u . (dl. 3) = Fib (k + 1) & IC u = il. 4 ) ) and
A15: k + 1 < N ; :: thesis: for u being State of st u = Computation s,((6 * (k + 1)) + 3) holds
( u . (dl. 0 ) = 1 & u . (dl. 1) = (N - 1) - (k + 1) & u . (dl. 2) = Fib (k + 1) & u . (dl. 3) = Fib ((k + 1) + 1) & IC u = il. 4 )
set b = (6 * k) + 3;
set s5 = Computation s,(((6 * k) + 3) + 1);
set s6 = Computation s,((((6 * k) + 3) + 1) + 1);
set s7 = Computation s,(((((6 * k) + 3) + 1) + 1) + 1);
set s8 = Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1);
set s9 = Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1);
set s10 = Computation s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1);
set s4 = Computation s,((6 * k) + 3);
A16: IC (Computation s,((6 * k) + 3)) = il. 4 by A14, A15, NAT_1:13;
let t be State of ; :: thesis: ( t = Computation s,((6 * (k + 1)) + 3) implies ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = il. 4 ) )
assume A17: t = Computation s,((6 * (k + 1)) + 3) ; :: thesis: ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = il. 4 )
A18: (Computation s,((6 * k) + 3)) . (dl. 1) = (N - 1) - k by A14, A15, NAT_1:13;
then (Computation s,((6 * k) + 3)) . (dl. 1) <> 0 by A15;
then A19: IC (Computation s,(((6 * k) + 3) + 1)) = il. (4 + 1) by A6, A16, SCM_1:24;
then A20: IC (Computation s,((((6 * k) + 3) + 1) + 1)) = il. (5 + 1) by A12, SCM_1:18;
then A21: IC (Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) = il. (6 + 1) by A8, SCM_1:18;
then A22: IC (Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) = il. (7 + 1) by A10, SCM_1:19;
then A23: IC (Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) = il. 3 by A11, SCM_1:23;
then A24: IC (Computation s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1)) = il. (3 + 1) by A4, SCM_1:20;
(Computation s,((6 * k) + 3)) . (dl. 0 ) = 1 by A14, A15, NAT_1:13;
then (Computation s,(((6 * k) + 3) + 1)) . (dl. 0 ) = 1 by A6, A16, SCM_1:24;
then (Computation s,((((6 * k) + 3) + 1) + 1)) . (dl. 0 ) = 1 by A12, A19, Lm13, SCM_1:18;
then (Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A8, A20, Lm8, SCM_1:18;
then (Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A10, A21, Lm9, SCM_1:19;
then A25: (Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A11, A22, SCM_1:23;
(Computation s,((6 * k) + 3)) . (dl. 3) = Fib (k + 1) by A14, A15, NAT_1:13;
then (Computation s,(((6 * k) + 3) + 1)) . (dl. 3) = Fib (k + 1) by A6, A16, SCM_1:24;
then A26: (Computation s,((((6 * k) + 3) + 1) + 1)) . (dl. 3) = Fib (k + 1) by A12, A19, Lm16, SCM_1:18;
then A27: (Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 3) = Fib (k + 1) by A8, A20, Lm12, SCM_1:18;
(Computation s,((6 * k) + 3)) . (dl. 2) = Fib k by A14, A15, NAT_1:13;
then (Computation s,(((6 * k) + 3) + 1)) . (dl. 2) = Fib k by A6, A16, SCM_1:24;
then (Computation s,((((6 * k) + 3) + 1) + 1)) . (dl. 4) = Fib k by A12, A19, SCM_1:18;
then A28: (Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 4) = Fib k by A8, A20, Lm15, SCM_1:18;
(Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 3) = ((Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 4)) + ((Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 3)) by A10, A21, SCM_1:19
.= Fib ((k + 1) + 1) by A27, A28, PRE_FF:1 ;
then A29: (Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 3) = Fib ((k + 1) + 1) by A11, A22, SCM_1:23;
(Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A8, A20, A26, SCM_1:18;
then (Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A10, A21, Lm12, SCM_1:19;
then A30: (Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A11, A22, SCM_1:23;
(Computation s,(((6 * k) + 3) + 1)) . (dl. 1) = (N - 1) - k by A6, A18, A16, SCM_1:24;
then (Computation s,((((6 * k) + 3) + 1) + 1)) . (dl. 1) = (N - 1) - k by A12, A19, Lm14, SCM_1:18;
then (Computation s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A8, A20, Lm10, SCM_1:18;
then (Computation s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A10, A21, Lm11, SCM_1:19;
then (Computation s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A11, A22, SCM_1:23;
then (Computation s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1)) . (dl. 1) = ((N - 1) - k) - 1 by A4, A23, A25, SCM_1:20;
hence ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - (k + 1) & t . (dl. 2) = Fib (k + 1) & t . (dl. 3) = Fib ((k + 1) + 1) & IC t = il. 4 ) by A4, A17, A23, A25, A30, A29, A24, Lm7, Lm10, Lm11, SCM_1:20; :: thesis: verum

end;

A31: s . (il. 1) = halt SCM by SCM_1:14;
A32: s . (dl. 1) = N by SCM_1:14;
then A33: (Computation s,(0 + 1)) . (dl. 1) = N by A1, A2, SCM_1:25;
A34: S₁[ 0 ]

proof

set s3 = Computation s,(2 + 1);
set s2 = Computation s,(1 + 1);
assume 0 < N ; :: thesis: for u being State of st u = Computation s,((6 * 0 ) + 3) holds
( u . (dl. 0 ) = 1 & u . (dl. 1) = (N - 1) - 0 & u . (dl. 2) = Fib 0 & u . (dl. 3) = Fib (0 + 1) & IC u = il. 4 )
then A35: IC (Computation s,(0 + 1)) = il. 2 by A1, A32, A2, SCM_1:25;
then A36: ( (Computation s,(1 + 1)) . (dl. 3) = 1 & (Computation s,(1 + 1)) . (dl. 0 ) = 1 ) by A9, A3, A7, SCM_1:18;
let t be State of ; :: thesis: ( t = Computation s,((6 * 0 ) + 3) implies ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = il. 4 ) )
assume A37: t = Computation s,((6 * 0 ) + 3) ; :: thesis: ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = il. 4 )
A38: ( (Computation s,(1 + 1)) . (dl. 1) = N & (Computation s,(1 + 1)) . (dl. 2) = 0 ) by A9, A33, A5, A35, Lm11, Lm12, SCM_1:18;
A39: IC (Computation s,(1 + 1)) = il. (2 + 1) by A9, A35, SCM_1:18;
then IC (Computation s,(2 + 1)) = il. (3 + 1) by A4, SCM_1:20;
hence ( t . (dl. 0 ) = 1 & t . (dl. 1) = (N - 1) - 0 & t . (dl. 2) = Fib 0 & t . (dl. 3) = Fib (0 + 1) & IC t = il. 4 ) by A4, A37, A36, A38, A39, Lm7, Lm10, Lm11, PRE_FF:1, SCM_1:20; :: thesis: verum

end;

A40: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A34, A13);

per cases ( N = 0 or ex k being Nat st N = k + 1 ) by NAT_1:6;

suppose A41: N = 0 ; :: thesis: ( ProgramPart s halts_on s & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

then A42: s . (IC (Computation s,(0 + 1))) = halt SCM by A1, A31, A32, A2, SCM_1:25;
hence ProgramPart s halts_on s by SCM_1:3; :: thesis: ( ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

hereby :: thesis: ( ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

assume N = 0 ; :: thesis: LifeSpan s = 1
halt SCM <> (dl. 1) >0_goto (il. 2) by SCM_1:26;
hence LifeSpan s = 1 by A1, A2, A42, SCM_1:17; :: thesis: verum

end;

thus ( N > 0 implies LifeSpan s = (6 * N) - 2 ) by A41; :: thesis: (Result s) . (dl. 3) = Fib N
thus (Result s) . (dl. 3) = Fib N by A7, A41, A42, PRE_FF:1, SCM_1:4; :: thesis: verum

end;

suppose ex k being Nat st N = k + 1 ; :: thesis: ( ProgramPart s halts_on s & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

then consider k being Nat such that
A43: N = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
set r = Computation s,((6 * k) + 3);
A44: k < N by A43, NAT_1:13;
then A45: IC (Computation s,((6 * k) + 3)) = il. 4 by A40;
A46: (Computation s,((6 * k) + 3)) . (dl. 3) = Fib (k + 1) by A40, A44;
set t = Computation s,(((6 * k) + 3) + 1);
(Computation s,((6 * k) + 3)) . (dl. 1) = (k + (1 - 1)) - k by A40, A43, A44
.= 0 ;
then A47: IC (Computation s,(((6 * k) + 3) + 1)) = il. 1 by A6, A45, SCM_1:24;
hence ProgramPart s halts_on s by A31, SCM_1:3; :: thesis: ( ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )
thus ( N = 0 implies LifeSpan s = 1 ) by A43, NAT_1:5; :: thesis: ( ( N > 0 implies LifeSpan s = (6 * N) - 2 ) & (Result s) . (dl. 3) = Fib N )

hereby :: thesis: (Result s) . (dl. 3) = Fib N

assume N > 0 ; :: thesis: LifeSpan s = (6 * N) - 2
halt SCM <> (dl. 1) =0_goto (il. 1) by SCM_1:26;
hence LifeSpan s = (6 * N) - 2 by A31, A6, A43, A45, A47, SCM_1:17; :: thesis: verum

end;

thus (Result s) . (dl. 3) = (Computation s,(((6 * k) + 3) + 1)) . (dl. 3) by A31, A47, SCM_1:4
.= Fib N by A6, A43, A46, A45, SCM_1:24 ; :: thesis: verum

end;

end;