let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: ( Fib_Program c= F implies for N being Element of NAT
for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N ) )
assume A1: Fib_Program c= F ; :: thesis: for N being Element of NAT
for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
let N be Element of NAT ; :: thesis: for s being 0 -started State-consisting of <%1,N,0,0%> holds
( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
let s be 0 -started State-consisting of <%1,N,0,0%>; :: thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,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;
A2: ( IC s = 0 & F . 0 = (dl. 1) >0_goto 2 ) by A1, Lm17, MEMSTR_0:def 12;
set s1 = Comput (F,s,(0 + 1));
set s0 = Comput (F,s,0);
A3: s = Comput (F,s,0) by EXTPRO_1:2;
s . (dl. 0) = 1 by SCM_1:1;
then A4: (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A2, A3, SCM_1:11;
A5: F . 3 = SubFrom ((dl. 1),(dl. 0)) by A1, Lm17;
s . (dl. 2) = 0 by SCM_1:1;
then A6: (Comput (F,s,(0 + 1))) . (dl. 2) = 0 by A2, A3, SCM_1:11;
A7: F . 4 = (dl. 1) =0_goto 1 by A1, Lm17;
s . (dl. 3) = 0 by SCM_1:1;
then A8: (Comput (F,s,(0 + 1))) . (dl. 3) = 0 by A2, A3, SCM_1:11;
A9: F . 6 = (dl. 2) := (dl. 3) by A1, Lm17;
defpred S1[ Nat] means ( $1 < N implies for u being State of SCM st u = Comput (F,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 ) );
A10: F . 2 = (dl. 3) := (dl. 0) by A1, Lm17;
A11: F . 7 = AddTo ((dl. 3),(dl. 4)) by A1, Lm17;
A12: F . 8 = SCM-goto 3 by A1, Lm17;
A13: F . 5 = (dl. 4) := (dl. 2) by A1, Lm17;
A14: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A15: ( k < N implies for u being State of SCM st u = Comput (F,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
A16: k + 1 < N ; :: thesis: for u being State of SCM st u = Comput (F,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 (F,s,(((6 * k) + 3) + 1));
set s6 = Comput (F,s,((((6 * k) + 3) + 1) + 1));
set s7 = Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1));
set s8 = Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1));
set s9 = Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1));
set s10 = Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1));
set s4 = Comput (F,s,((6 * k) + 3));
A17: IC (Comput (F,s,((6 * k) + 3))) = 4 by A15, A16, NAT_1:13;
let t be State of SCM; :: thesis: ( t = Comput (F,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 A18: t = Comput (F,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 )
A19: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = (N - 1) - k by A15, A16, NAT_1:13;
then (Comput (F,s,((6 * k) + 3))) . (dl. 1) <> 0 by A16;
then A20: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 4 + 1 by A7, A17, SCM_1:10;
then A21: IC (Comput (F,s,((((6 * k) + 3) + 1) + 1))) = 5 + 1 by A13, SCM_1:4;
then A22: IC (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) = 6 + 1 by A9, SCM_1:4;
then A23: IC (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) = 7 + 1 by A11, SCM_1:5;
then A24: IC (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) = 3 by A12, SCM_1:9;
then A25: IC (Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) = 3 + 1 by A5, SCM_1:6;
(Comput (F,s,((6 * k) + 3))) . (dl. 0) = 1 by A15, A16, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 0) = 1 by A7, A17, SCM_1:10;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 0) = 1 by A13, A20, Lm13, SCM_1:4;
then (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 0) = 1 by A9, A21, Lm8, SCM_1:4;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A11, A22, Lm9, SCM_1:5;
then A26: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A12, A23, SCM_1:9;
(Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A15, A16, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) = Fib (k + 1) by A7, A17, SCM_1:10;
then A27: (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A13, A20, Lm16, SCM_1:4;
then A28: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A9, A21, Lm12, SCM_1:4;
(Comput (F,s,((6 * k) + 3))) . (dl. 2) = Fib k by A15, A16, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 2) = Fib k by A7, A17, SCM_1:10;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 4) = Fib k by A13, A20, SCM_1:4;
then A29: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 4) = Fib k by A9, A21, Lm15, SCM_1:4;
(Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 3) = ((Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 4)) + ((Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 3)) by A11, A22, SCM_1:5
.= Fib ((k + 1) + 1) by A28, A29, PRE_FF:1 ;
then A30: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A12, A23, SCM_1:9;
(Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A9, A21, A27, SCM_1:4;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A11, A22, Lm12, SCM_1:5;
then A31: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A12, A23, SCM_1:9;
(Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 1) = (N - 1) - k by A7, A19, A17, SCM_1:10;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 1) = (N - 1) - k by A13, A20, Lm14, SCM_1:4;
then (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A9, A21, Lm10, SCM_1:4;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A11, A22, Lm11, SCM_1:5;
then (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A12, A23, SCM_1:9;
then (Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) = ((N - 1) - k) - 1 by A5, A24, A26, SCM_1:6;
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 A5, A18, A24, A26, A31, A30, A25, Lm7, Lm10, Lm11, SCM_1:6; :: thesis: verum
end;
A32: F . 1 = halt SCM by A1, Lm17;
A33: s . (dl. 1) = N by SCM_1:1;
then A34: (Comput (F,s,(0 + 1))) . (dl. 1) = N by A2, A3, SCM_1:11;
A35: S1[ 0 ]
proof
set s3 = Comput (F,s,(2 + 1));
set s2 = Comput (F,s,(1 + 1));
assume 0 < N ; :: thesis: for u being State of SCM st u = Comput (F,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 A36: IC (Comput (F,s,(0 + 1))) = 2 by A2, A33, A3, SCM_1:11;
then A37: ( (Comput (F,s,(1 + 1))) . (dl. 3) = 1 & (Comput (F,s,(1 + 1))) . (dl. 0) = 1 ) by A10, A4, A8, SCM_1:4;
let t be State of SCM; :: thesis: ( t = Comput (F,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 A38: t = Comput (F,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 )
A39: ( (Comput (F,s,(1 + 1))) . (dl. 1) = N & (Comput (F,s,(1 + 1))) . (dl. 2) = 0 ) by A10, A34, A6, A36, Lm11, Lm12, SCM_1:4;
A40: IC (Comput (F,s,(1 + 1))) = 2 + 1 by A10, A36, SCM_1:4;
then IC (Comput (F,s,(2 + 1))) = 3 + 1 by A5, SCM_1:6;
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 A5, A38, A37, A39, A40, Lm7, Lm10, Lm11, PRE_FF:1, SCM_1:6; :: thesis: verum
end;
A41: for k being Nat holds S1[k] from NAT_1:sch 2(A35, A14);
per cases ( N = 0 or ex k being Nat st N = k + 1 ) by NAT_1:6;
suppose A42: N = 0 ; :: thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
then A43: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A2, A32, A33, A3, SCM_1:11;
hence F halts_on s by EXTPRO_1:30; :: thesis: ( ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
hereby :: thesis: ( ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
assume N = 0 ; :: thesis: LifeSpan (F,s) = 1
halt SCM <> (dl. 1) >0_goto 2 by SCM_1:12;
hence LifeSpan (F,s) = 1 by A2, A3, A43, EXTPRO_1:33; :: thesis: verum
end;
thus ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) by A42; :: thesis: (Result (F,s)) . (dl. 3) = Fib N
thus (Result (F,s)) . (dl. 3) = Fib N by A8, A42, A43, EXTPRO_1:7, PRE_FF:1; :: thesis: verum
end;
suppose ex k being Nat st N = k + 1 ; :: thesis: ( F halts_on s & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
then consider k being Nat such that
A44: N = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set r = Comput (F,s,((6 * k) + 3));
A45: k < N by A44, NAT_1:13;
then A46: IC (Comput (F,s,((6 * k) + 3))) = 4 by A41;
A47: (Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A41, A45;
set t = Comput (F,s,(((6 * k) + 3) + 1));
(Comput (F,s,((6 * k) + 3))) . (dl. 1) = (k + (1 - 1)) - k by A41, A44, A45
.= 0 ;
then A48: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 1 by A7, A46, SCM_1:10;
hence F halts_on s by A32, EXTPRO_1:30; :: thesis: ( ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
thus ( N = 0 implies LifeSpan (F,s) = 1 ) by A44; :: thesis: ( ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) & (Result (F,s)) . (dl. 3) = Fib N )
thus ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) by A32, A44, A46, A48, EXTPRO_1:33; :: thesis: (Result (F,s)) . (dl. 3) = Fib N
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) by A32, A48, EXTPRO_1:7
.= Fib N by A7, A44, A47, A46, SCM_1:10 ; :: thesis: verum
end;
end;