defpred S1[ Element of NAT ] means for k, Fk, Fk1 being Element of NAT
for s being State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*$1*>) ^ <*Fk*>) ^ <*Fk1*> st $1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * $1) - 4 & ex m being Element of NAT st
( m = (k + $1) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) );
A1:
for N being Element of NAT st S1[N] holds
S1[N + 1]
proof
set C1 =
dl. 0 ;
set n =
dl. 1;
set FP =
dl. 2;
set FC =
dl. 3;
set AUX =
dl. 4;
let N be
Element of
NAT ;
( S1[N] implies S1[N + 1] )
assume A2:
S1[
N]
;
S1[N + 1]
A3:
N >= 0
by NAT_1:2;
let k,
Fk,
Fk1 be
Element of
NAT ;
for s being State-consisting of 3, 0 , 0 , Fib_Program ,((<*1*> ^ <*(N + 1)*>) ^ <*Fk*>) ^ <*Fk1*> st N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )let s be
State-consisting of 3,
0 ,
0 ,
Fib_Program ,
((<*1*> ^ <*(N + 1)*>) ^ <*Fk*>) ^ <*Fk1*>;
( N + 1 > 0 & Fk = Fib k & Fk1 = Fib (k + 1) implies ( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) ) )
assume that
N + 1
> 0
and A4:
Fk = Fib k
and A5:
Fk1 = Fib (k + 1)
;
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )
A6:
s . 3
= SubFrom (dl. 1),
(dl. 0 )
by SCM_1:14;
set s0 =
Comput (ProgramPart s),
s,
0 ;
A7:
s . 0 = (dl. 1) >0_goto 2
by SCM_1:14;
set s1 =
Comput (ProgramPart s),
s,
(0 + 1);
A8:
s . 1
= halt SCM
by SCM_1:14;
A9:
(
IC s = 3 &
s = Comput (ProgramPart s),
s,
0 )
by AMI_1:13, SCM_1:def 1;
then A10:
IC (Comput (ProgramPart s),s,(0 + 1)) =
3
+ 1
by A6, SCM_1:20
.=
4
;
set s2 =
Comput (ProgramPart s),
s,
(1 + 1);
A11:
s . 2
= (dl. 3) := (dl. 0 )
by SCM_1:14;
A12:
s . 4
= (dl. 1) =0_goto 1
by SCM_1:14;
s . (dl. 3) = Fk1
by SCM_1:14;
then
(Comput (ProgramPart s),s,(0 + 1)) . (dl. 3) = Fk1
by A6, A9, Lm11, SCM_1:20;
then A13:
(Comput (ProgramPart s),s,(1 + 1)) . (dl. 3) = Fk1
by A12, A10, SCM_1:24;
A14:
s . 7
= AddTo (dl. 3),
(dl. 4)
by SCM_1:14;
s . (dl. 2) = Fk
by SCM_1:14;
then
(Comput (ProgramPart s),s,(0 + 1)) . (dl. 2) = Fk
by A6, A9, Lm10, SCM_1:20;
then A15:
(Comput (ProgramPart s),s,(1 + 1)) . (dl. 2) = Fk
by A12, A10, SCM_1:24;
A16:
s . 6
= (dl. 2) := (dl. 3)
by SCM_1:14;
A17:
s . (dl. 0 ) = 1
by SCM_1:14;
then
(Comput (ProgramPart s),s,(0 + 1)) . (dl. 0 ) = 1
by A6, A9, Lm7, SCM_1:20;
then A18:
(Comput (ProgramPart s),s,(1 + 1)) . (dl. 0 ) = 1
by A12, A10, SCM_1:24;
s . (dl. 1) = N + 1
by SCM_1:14;
then A19:
(Comput (ProgramPart s),s,(0 + 1)) . (dl. 1) =
(N + 1) - 1
by A6, A17, A9, SCM_1:20
.=
N
;
then A20:
(Comput (ProgramPart s),s,(1 + 1)) . (dl. 1) = N
by A12, A10, SCM_1:24;
A21:
s . 5
= (dl. 4) := (dl. 2)
by SCM_1:14;
A22:
s . 8
= SCM-goto 3
by SCM_1:14;
per cases
( N = 0 or N > 0 )
by A3, XXREAL_0:1;
suppose A23:
N = 0
;
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )then A24:
s . (IC (Comput (ProgramPart s),s,(1 + 1))) = halt SCM
by A8, A12, A19, A10, SCM_1:24;
hence
ProgramPart s halts_on s
by SCM_1:3;
( LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )
s . (IC (Comput (ProgramPart s),s,(0 + 1))) <> halt SCM
by A12, A10, SCM_1:26;
hence
LifeSpan (ProgramPart s),
s = (6 * (N + 1)) - 4
by A23, A24, SCM_1:16;
ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )take m =
k;
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )thus
m = (k + (N + 1)) - 1
by A23;
( (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )thus
(
(Result (ProgramPart s),s) . (dl. 2) = Fib m &
(Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )
by A4, A5, A15, A13, A24, SCM_1:4;
verum end; suppose A25:
N > 0
;
( ProgramPart s halts_on s & LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )then A26:
(6 * N) - 4
> 0
by Lm6;
set Fk2 =
Fib ((k + 1) + 1);
set s6 =
Comput (ProgramPart s),
s,
(5 + 1);
A27:
(Comput (ProgramPart s),s,(5 + 1)) . 8
= SCM-goto 3
by A22, AMI_1:54;
A28:
(
(Comput (ProgramPart s),s,(5 + 1)) . 0 = (dl. 1) >0_goto 2 &
(Comput (ProgramPart s),s,(5 + 1)) . 1
= halt SCM )
by A7, A8, AMI_1:54;
set s5 =
Comput (ProgramPart s),
s,
(4 + 1);
set s4 =
Comput (ProgramPart s),
s,
(3 + 1);
set s3 =
Comput (ProgramPart s),
s,
(2 + 1);
A29:
IC (Comput (ProgramPart s),s,(1 + 1)) = 4
+ 1
by A12, A19, A10, A25, SCM_1:24;
then A30:
IC (Comput (ProgramPart s),s,(2 + 1)) = 5
+ 1
by A21, SCM_1:18;
then A31:
IC (Comput (ProgramPart s),s,(3 + 1)) = 6
+ 1
by A16, SCM_1:18;
then A32:
IC (Comput (ProgramPart s),s,(4 + 1)) = 7
+ 1
by A14, SCM_1:19;
A33:
(Comput (ProgramPart s),s,(2 + 1)) . (dl. 3) = Fib (k + 1)
by A5, A21, A13, A29, Lm16, SCM_1:18;
then A34:
(Comput (ProgramPart s),s,(3 + 1)) . (dl. 3) = Fib (k + 1)
by A16, A30, Lm12, SCM_1:18;
(Comput (ProgramPart s),s,(3 + 1)) . (dl. 2) = Fib (k + 1)
by A16, A30, A33, SCM_1:18;
then
(Comput (ProgramPart s),s,(4 + 1)) . (dl. 2) = Fib (k + 1)
by A14, A31, Lm12, SCM_1:19;
then A35:
(Comput (ProgramPart s),s,(5 + 1)) . (dl. 2) = Fib (k + 1)
by A22, A32, SCM_1:23;
(Comput (ProgramPart s),s,(2 + 1)) . (dl. 0 ) = 1
by A21, A18, A29, Lm13, SCM_1:18;
then
(Comput (ProgramPart s),s,(3 + 1)) . (dl. 0 ) = 1
by A16, A30, Lm8, SCM_1:18;
then
(Comput (ProgramPart s),s,(4 + 1)) . (dl. 0 ) = 1
by A14, A31, Lm9, SCM_1:19;
then A36:
(Comput (ProgramPart s),s,(5 + 1)) . (dl. 0 ) = 1
by A22, A32, SCM_1:23;
A37:
(
(Comput (ProgramPart s),s,(5 + 1)) . 6
= (dl. 2) := (dl. 3) &
(Comput (ProgramPart s),s,(5 + 1)) . 7
= AddTo (dl. 3),
(dl. 4) )
by A16, A14, AMI_1:54;
(Comput (ProgramPart s),s,(2 + 1)) . (dl. 4) = Fib k
by A4, A21, A15, A29, SCM_1:18;
then A38:
(Comput (ProgramPart s),s,(3 + 1)) . (dl. 4) = Fib k
by A16, A30, Lm15, SCM_1:18;
(Comput (ProgramPart s),s,(4 + 1)) . (dl. 3) =
((Comput (ProgramPart s),s,(3 + 1)) . (dl. 4)) + ((Comput (ProgramPart s),s,(3 + 1)) . (dl. 3))
by A14, A31, SCM_1:19
.=
Fib ((k + 1) + 1)
by A34, A38, PRE_FF:1
;
then A39:
(Comput (ProgramPart s),s,(5 + 1)) . (dl. 3) = Fib ((k + 1) + 1)
by A22, A32, SCM_1:23;
(Comput (ProgramPart s),s,(2 + 1)) . (dl. 1) = N
by A21, A20, A29, Lm14, SCM_1:18;
then
(Comput (ProgramPart s),s,(3 + 1)) . (dl. 1) = N
by A16, A30, Lm10, SCM_1:18;
then
(Comput (ProgramPart s),s,(4 + 1)) . (dl. 1) = N
by A14, A31, Lm11, SCM_1:19;
then A40:
(Comput (ProgramPart s),s,(5 + 1)) . (dl. 1) = N
by A22, A32, SCM_1:23;
A41:
(
(Comput (ProgramPart s),s,(5 + 1)) . 4
= (dl. 1) =0_goto 1 &
(Comput (ProgramPart s),s,(5 + 1)) . 5
= (dl. 4) := (dl. 2) )
by A12, A21, AMI_1:54;
A42:
(
(Comput (ProgramPart s),s,(5 + 1)) . 2
= (dl. 3) := (dl. 0 ) &
(Comput (ProgramPart s),s,(5 + 1)) . 3
= SubFrom (dl. 1),
(dl. 0 ) )
by A11, A6, AMI_1:54;
IC (Comput (ProgramPart s),s,(5 + 1)) = 3
by A22, A32, SCM_1:23;
then A43:
Comput (ProgramPart s),
s,
(5 + 1) is
State-consisting of 3,
0 ,
0 ,
Fib_Program ,
((<*1*> ^ <*N*>) ^ <*Fk1*>) ^ <*(Fib ((k + 1) + 1))*>
by A5, A36, A40, A35, A39, A28, A42, A41, A37, A27, SCM_1:30;
then consider m being
Element of
NAT such that A44:
m = ((k + 1) + N) - 1
and
(Result (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),(Comput (ProgramPart s),s,(5 + 1))) . (dl. 2) = Fib m
and
(Result (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),(Comput (ProgramPart s),s,(5 + 1))) . (dl. 3) = Fib (m + 1)
by A2, A5, A25;
A45:
ProgramPart (Comput (ProgramPart s),s,(5 + 1)) halts_on Comput (ProgramPart s),
s,
(5 + 1)
by A2, A5, A25, A43;
then Y:
ProgramPart s halts_on Comput (ProgramPart s),
s,
(5 + 1)
by AMI_1:123;
hence
ProgramPart s halts_on s
by AMI_1:93;
( LifeSpan (ProgramPart s),s = (6 * (N + 1)) - 4 & ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )
LifeSpan (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),
(Comput (ProgramPart s),s,(5 + 1)) = (6 * N) - 4
by A2, A5, A25, A43;
hence LifeSpan (ProgramPart s),
s =
6
+ ((6 * N) - 4)
by A45, A26, SCM_1:28
.=
(6 * (N + 1)) - 4
;
ex m being Element of NAT st
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )take
m
;
( m = (k + (N + 1)) - 1 & (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )thus
m = (k + (N + 1)) - 1
by A44;
( (Result (ProgramPart s),s) . (dl. 2) = Fib m & (Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )X:
Result (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),
(Comput (ProgramPart s),s,(5 + 1)) = Result (ProgramPart s),
s
by Y, SCM_1:29;
ex
m being
Element of
NAT st
(
m = ((k + 1) + N) - 1 &
(Result (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),(Comput (ProgramPart s),s,(5 + 1))) . (dl. 2) = Fib m &
(Result (ProgramPart (Comput (ProgramPart s),s,(5 + 1))),(Comput (ProgramPart s),s,(5 + 1))) . (dl. 3) = Fib (m + 1) )
by A2, A5, A25, A43;
hence
(
(Result (ProgramPart s),s) . (dl. 2) = Fib m &
(Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) )
by A44, X;
verum end;
end;
A46:
S1[ 0 ]
;
thus
for N being Element of NAT holds S1[N]
from NAT_1:sch 1(A46, A1); verum