let F be NAT -defined the InstructionsF of SCM -valued total Function; ( 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
; 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 ; 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%>; ( 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;
( 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
;
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;
( 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))
;
( 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;
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
;
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;
( 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))
;
( 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;
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
;
( 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;
( ( 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)
= (6 * N) - 2 )
by A42;
(Result (F,s)) . (dl. 3) = Fib Nthus
(Result (F,s)) . (dl. 3) = Fib N
by A8, A42, A43, EXTPRO_1:7, PRE_FF:1;
verum end; suppose
ex
k being
Nat st
N = k + 1
;
( 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;
( ( 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;
( ( 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;
(Result (F,s)) . (dl. 3) = Fib Nthus (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
;
verum end;