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 = 6;
set L7 = 7;
set L8 = 8;
set L0 = 0 ;
set L1 = 1;
set L2 = 2;
set L3 = 3;
set L4 = 4;
set L5 = 5;
A1: ( IC s = 0 & s . 0 = (dl. 1) >0_goto 2 ) by SCM_1:14;
set s1 = Comput (ProgramPart s),s,(0 + 1);
set s0 = Comput (ProgramPart s),s,0 ;
A2: s = Comput (ProgramPart s),s,0 by AMI_1:13;
s . (dl. 0 ) = 1 by SCM_1:14;
then A3: (Comput (ProgramPart s),s,(0 + 1)) . (dl. 0 ) = 1 by A1, A2, SCM_1:25;
A4: s . 3 = SubFrom (dl. 1),(dl. 0 ) by SCM_1:14;
s . (dl. 2) = 0 by SCM_1:14;
then A5: (Comput (ProgramPart s),s,(0 + 1)) . (dl. 2) = 0 by A1, A2, SCM_1:25;
A6: s . 4 = (dl. 1) =0_goto 1 by SCM_1:14;
s . (dl. 3) = 0 by SCM_1:14;
then A7: (Comput (ProgramPart s),s,(0 + 1)) . (dl. 3) = 0 by A1, A2, SCM_1:25;
A8: s . 6 = (dl. 2) := (dl. 3) by SCM_1:14;
defpred S1[ Element of NAT ] means ( $1 < N implies for u being State of SCM st u = Comput (ProgramPart s),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 = 4 ) );
A9: s . 2 = (dl. 3) := (dl. 0 ) by SCM_1:14;
A10: s . 7 = AddTo (dl. 3),(dl. 4) by SCM_1:14;
A11: s . 8 = SCM-goto 3 by SCM_1:14;
A12: s . 5 = (dl. 4) := (dl. 2) by SCM_1:14;
A13: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A14: ( k < N implies for u being State of SCM st u = Comput (ProgramPart s),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 = 4 ) ) and
A15: k + 1 < N ; :: thesis: for u being State of SCM st u = Comput (ProgramPart s),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 = 4 )
set b = (6 * k) + 3;
set s5 = Comput (ProgramPart s),s,(((6 * k) + 3) + 1);
set s6 = Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1);
set s7 = Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1);
set s8 = Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1);
set s9 = Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1);
set s10 = Comput (ProgramPart s),s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1);
set s4 = Comput (ProgramPart s),s,((6 * k) + 3);
A16: IC (Comput (ProgramPart s),s,((6 * k) + 3)) = 4 by A14, A15, NAT_1:13;
let t be State of SCM ; :: thesis: ( t = Comput (ProgramPart s),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 = 4 ) )
assume A17: t = Comput (ProgramPart s),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 = 4 )
A18: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) = (N - 1) - k by A14, A15, NAT_1:13;
then (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) <> 0 by A15;
then A19: IC (Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) = 4 + 1 by A6, A16, SCM_1:24;
then A20: IC (Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1)) = 5 + 1 by A12, SCM_1:18;
then A21: IC (Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) = 6 + 1 by A8, SCM_1:18;
then A22: IC (Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) = 7 + 1 by A10, SCM_1:19;
then A23: IC (Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) = 3 by A11, SCM_1:23;
then A24: IC (Comput (ProgramPart s),s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1)) = 3 + 1 by A4, SCM_1:20;
(Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 0 ) = 1 by A14, A15, NAT_1:13;
then (Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) . (dl. 0 ) = 1 by A6, A16, SCM_1:24;
then (Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1)) . (dl. 0 ) = 1 by A12, A19, Lm13, SCM_1:18;
then (Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A8, A20, Lm8, SCM_1:18;
then (Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A10, A21, Lm9, SCM_1:19;
then A25: (Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 0 ) = 1 by A11, A22, SCM_1:23;
(Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 3) = Fib (k + 1) by A14, A15, NAT_1:13;
then (Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) . (dl. 3) = Fib (k + 1) by A6, A16, SCM_1:24;
then A26: (Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1)) . (dl. 3) = Fib (k + 1) by A12, A19, Lm16, SCM_1:18;
then A27: (Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 3) = Fib (k + 1) by A8, A20, Lm12, SCM_1:18;
(Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 2) = Fib k by A14, A15, NAT_1:13;
then (Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) . (dl. 2) = Fib k by A6, A16, SCM_1:24;
then (Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1)) . (dl. 4) = Fib k by A12, A19, SCM_1:18;
then A28: (Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 4) = Fib k by A8, A20, Lm15, SCM_1:18;
(Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 3) = ((Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 4)) + ((Comput (ProgramPart s),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: (Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 3) = Fib ((k + 1) + 1) by A11, A22, SCM_1:23;
(Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A8, A20, A26, SCM_1:18;
then (Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A10, A21, Lm12, SCM_1:19;
then A30: (Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 2) = Fib (k + 1) by A11, A22, SCM_1:23;
(Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) . (dl. 1) = (N - 1) - k by A6, A18, A16, SCM_1:24;
then (Comput (ProgramPart s),s,((((6 * k) + 3) + 1) + 1)) . (dl. 1) = (N - 1) - k by A12, A19, Lm14, SCM_1:18;
then (Comput (ProgramPart s),s,(((((6 * k) + 3) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A8, A20, Lm10, SCM_1:18;
then (Comput (ProgramPart s),s,((((((6 * k) + 3) + 1) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A10, A21, Lm11, SCM_1:19;
then (Comput (ProgramPart s),s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1)) . (dl. 1) = (N - 1) - k by A11, A22, SCM_1:23;
then (Comput (ProgramPart s),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 = 4 ) by A4, A17, A23, A25, A30, A29, A24, Lm7, Lm10, Lm11, SCM_1:20; :: thesis: verum
end;
A31: s . 1 = halt SCM by SCM_1:14;
A32: s . (dl. 1) = N by SCM_1:14;
then A33: (Comput (ProgramPart s),s,(0 + 1)) . (dl. 1) = N by A1, A2, SCM_1:25;
A34: S1[ 0 ]
proof
set s3 = Comput (ProgramPart s),s,(2 + 1);
set s2 = Comput (ProgramPart s),s,(1 + 1);
assume 0 < N ; :: thesis: for u being State of SCM st u = Comput (ProgramPart s),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 = 4 )
then A35: IC (Comput (ProgramPart s),s,(0 + 1)) = 2 by A1, A32, A2, SCM_1:25;
then A36: ( (Comput (ProgramPart s),s,(1 + 1)) . (dl. 3) = 1 & (Comput (ProgramPart s),s,(1 + 1)) . (dl. 0 ) = 1 ) by A9, A3, A7, SCM_1:18;
let t be State of SCM ; :: thesis: ( t = Comput (ProgramPart s),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 = 4 ) )
assume A37: t = Comput (ProgramPart s),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 = 4 )
A38: ( (Comput (ProgramPart s),s,(1 + 1)) . (dl. 1) = N & (Comput (ProgramPart s),s,(1 + 1)) . (dl. 2) = 0 ) by A9, A33, A5, A35, Lm11, Lm12, SCM_1:18;
A39: IC (Comput (ProgramPart s),s,(1 + 1)) = 2 + 1 by A9, A35, SCM_1:18;
then IC (Comput (ProgramPart s),s,(2 + 1)) = 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 = 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 S1[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 (Comput (ProgramPart s),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 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 = Comput (ProgramPart s),s,((6 * k) + 3);
A44: k < N by A43, NAT_1:13;
then A45: IC (Comput (ProgramPart s),s,((6 * k) + 3)) = 4 by A40;
A46: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 3) = Fib (k + 1) by A40, A44;
set t = Comput (ProgramPart s),s,(((6 * k) + 3) + 1);
(Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) = (k + (1 - 1)) - k by A40, A43, A44
.= 0 ;
then A47: IC (Comput (ProgramPart s),s,(((6 * k) + 3) + 1)) = 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 )
thus ( N > 0 implies LifeSpan s = (6 * N) - 2 ) by A31, A43, A45, A47, SCM_1:17; :: thesis: (Result s) . (dl. 3) = Fib N
thus (Result s) . (dl. 3) = (Comput (ProgramPart s),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;