let F be NAT -defined the Instructions 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 0 ,((<*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 Z: Fib_Program c= F ; :: thesis: for N being Element of NAT
for s being 0 -started State-consisting of 0 ,((<*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 0 ,((<*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 0 ,((<*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;
A1: ( IC s = 0 & F . 0 = (dl. 1) >0_goto 2 ) by COMPOS_1:def 20, Z, L14;
set s1 = Comput (F,s,(0 + 1));
set s0 = Comput (F,s,0);
A2: s = Comput (F,s,0) by EXTPRO_1:3;
s . (dl. 0) = 1 by SCM_1:13;
then A3: (Comput (F,s,(0 + 1))) . (dl. 0) = 1 by A1, A2, SCM_1:25;
A4: F . 3 = SubFrom ((dl. 1),(dl. 0)) by Z, L14;
s . (dl. 2) = 0 by SCM_1:13;
then A5: (Comput (F,s,(0 + 1))) . (dl. 2) = 0 by A1, A2, SCM_1:25;
A6: F . 4 = (dl. 1) =0_goto 1 by Z, L14;
s . (dl. 3) = 0 by SCM_1:13;
then A7: (Comput (F,s,(0 + 1))) . (dl. 3) = 0 by A1, A2, SCM_1:25;
A8: F . 6 = (dl. 2) := (dl. 3) by Z, L14;
defpred S1[ Element of 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 ) );
A9: F . 2 = (dl. 3) := (dl. 0) by Z, L14;
A10: F . 7 = AddTo ((dl. 3),(dl. 4)) by Z, L14;
A11: F . 8 = SCM-goto 3 by Z, L14;
A12: F . 5 = (dl. 4) := (dl. 2) by Z, L14;
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 (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
A15: 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));
A16: IC (Comput (F,s,((6 * k) + 3))) = 4 by A14, A15, 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 A17: 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 )
A18: (Comput (F,s,((6 * k) + 3))) . (dl. 1) = (N - 1) - k by A14, A15, NAT_1:13;
then (Comput (F,s,((6 * k) + 3))) . (dl. 1) <> 0 by A15;
then A19: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 4 + 1 by A6, A16, SCM_1:24;
then A20: IC (Comput (F,s,((((6 * k) + 3) + 1) + 1))) = 5 + 1 by A12, SCM_1:18;
then A21: IC (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) = 6 + 1 by A8, SCM_1:18;
then A22: IC (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) = 7 + 1 by A10, SCM_1:19;
then A23: IC (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) = 3 by A11, SCM_1:23;
then A24: IC (Comput (F,s,((((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1) + 1))) = 3 + 1 by A4, SCM_1:20;
(Comput (F,s,((6 * k) + 3))) . (dl. 0) = 1 by A14, A15, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 0) = 1 by A6, A16, SCM_1:24;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 0) = 1 by A12, A19, Lm13, SCM_1:18;
then (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 0) = 1 by A8, A20, Lm8, SCM_1:18;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A10, A21, Lm9, SCM_1:19;
then A25: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 0) = 1 by A11, A22, SCM_1:23;
(Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A14, A15, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) = Fib (k + 1) by A6, A16, SCM_1:24;
then A26: (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A12, A19, Lm16, SCM_1:18;
then A27: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 3) = Fib (k + 1) by A8, A20, Lm12, SCM_1:18;
(Comput (F,s,((6 * k) + 3))) . (dl. 2) = Fib k by A14, A15, NAT_1:13;
then (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 2) = Fib k by A6, A16, SCM_1:24;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 4) = Fib k by A12, A19, SCM_1:18;
then A28: (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 4) = Fib k by A8, A20, Lm15, SCM_1:18;
(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 A10, A21, SCM_1:19
.= Fib ((k + 1) + 1) by A27, A28, PRE_FF:1 ;
then A29: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 3) = Fib ((k + 1) + 1) by A11, A22, SCM_1:23;
(Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A8, A20, A26, SCM_1:18;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A10, A21, Lm12, SCM_1:19;
then A30: (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 2) = Fib (k + 1) by A11, A22, SCM_1:23;
(Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 1) = (N - 1) - k by A6, A18, A16, SCM_1:24;
then (Comput (F,s,((((6 * k) + 3) + 1) + 1))) . (dl. 1) = (N - 1) - k by A12, A19, Lm14, SCM_1:18;
then (Comput (F,s,(((((6 * k) + 3) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A8, A20, Lm10, SCM_1:18;
then (Comput (F,s,((((((6 * k) + 3) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A10, A21, Lm11, SCM_1:19;
then (Comput (F,s,(((((((6 * k) + 3) + 1) + 1) + 1) + 1) + 1))) . (dl. 1) = (N - 1) - k by A11, A22, SCM_1:23;
then (Comput (F,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: F . 1 = halt SCM by Z, L14;
A32: s . (dl. 1) = N by SCM_1:13;
then A33: (Comput (F,s,(0 + 1))) . (dl. 1) = N by A1, A2, SCM_1:25;
A34: 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 A35: IC (Comput (F,s,(0 + 1))) = 2 by A1, A32, A2, SCM_1:25;
then A36: ( (Comput (F,s,(1 + 1))) . (dl. 3) = 1 & (Comput (F,s,(1 + 1))) . (dl. 0) = 1 ) by A9, A3, A7, SCM_1:18;
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 A37: 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 )
A38: ( (Comput (F,s,(1 + 1))) . (dl. 1) = N & (Comput (F,s,(1 + 1))) . (dl. 2) = 0 ) by A9, A33, A5, A35, Lm11, Lm12, SCM_1:18;
A39: IC (Comput (F,s,(1 + 1))) = 2 + 1 by A9, A35, SCM_1:18;
then IC (Comput (F,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: ( 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 A42: F . (IC (Comput (F,s,(0 + 1)))) = halt SCM by A1, A31, A32, A2, SCM_1:25;
hence F halts_on s by EXTPRO_1:31; :: 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:26;
hence LifeSpan (F,s) = 1 by A1, A2, A42, EXTPRO_1:34; :: thesis: verum
end;
thus ( N > 0 implies LifeSpan (F,s) = (6 * N) - 2 ) by A41; :: thesis: (Result (F,s)) . (dl. 3) = Fib N
thus (Result (F,s)) . (dl. 3) = Fib N by A7, A41, A42, EXTPRO_1:32, 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
A43: N = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
set r = Comput (F,s,((6 * k) + 3));
A44: k < N by A43, NAT_1:13;
then A45: IC (Comput (F,s,((6 * k) + 3))) = 4 by A40;
A46: (Comput (F,s,((6 * k) + 3))) . (dl. 3) = Fib (k + 1) by A40, A44;
set t = Comput (F,s,(((6 * k) + 3) + 1));
(Comput (F,s,((6 * k) + 3))) . (dl. 1) = (k + (1 - 1)) - k by A40, A43, A44
.= 0 ;
then A47: IC (Comput (F,s,(((6 * k) + 3) + 1))) = 1 by A6, A45, SCM_1:24;
hence F halts_on s by A31, EXTPRO_1:31; :: 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 A43, NAT_1:5; :: 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 A31, A43, A45, A47, EXTPRO_1:34; :: thesis: (Result (F,s)) . (dl. 3) = Fib N
thus (Result (F,s)) . (dl. 3) = (Comput (F,s,(((6 * k) + 3) + 1))) . (dl. 3) by A31, A47, EXTPRO_1:32
.= Fib N by A6, A43, A46, A45, SCM_1:24 ; :: thesis: verum
end;
end;