begin
Lm1:
0 = [\(log 2,1)/]
Lm2:
for nn9 being Element of NAT st nn9 > 0 holds
( [\(log 2,nn9)/] is Element of NAT & (6 * ([\(log 2,nn9)/] + 1)) + 1 > 0 )
Lm3:
for nn, nn9 being Element of NAT st nn = (2 * nn9) + 1 & nn9 > 0 holds
6 + ((6 * ([\(log 2,nn9)/] + 1)) + 1) = (6 * ([\(log 2,nn)/] + 1)) + 1
Lm4:
for n being Element of NAT st n > 0 holds
( log 2,(2 * n) = 1 + (log 2,n) & log 2,(2 * n) = (log 2,n) + 1 )
Lm5:
for nn, nn9 being Element of NAT st nn = 2 * nn9 & nn9 > 0 holds
6 + ((6 * ([\(log 2,nn9)/] + 1)) + 1) = (6 * ([\(log 2,nn)/] + 1)) + 1
Lm6:
for N being Element of NAT st N <> 0 holds
(6 * N) - 4 > 0
Lm7:
dl. 0 <> dl. 1
by AMI_3:52;
Lm8:
dl. 0 <> dl. 2
by AMI_3:52;
Lm9:
dl. 0 <> dl. 3
by AMI_3:52;
Lm10:
dl. 1 <> dl. 2
by AMI_3:52;
Lm11:
dl. 1 <> dl. 3
by AMI_3:52;
Lm12:
dl. 2 <> dl. 3
by AMI_3:52;
Lm13:
dl. 0 <> dl. 4
by AMI_3:52;
Lm14:
dl. 1 <> dl. 4
by AMI_3:52;
Lm15:
dl. 2 <> dl. 4
by AMI_3:52;
Lm16:
dl. 3 <> dl. 4
by AMI_3:52;
:: deftheorem defines Fib_Program FIB_FUSC:def 1 :
theorem
:: deftheorem Def2 defines Fusc' FIB_FUSC:def 2 :
:: deftheorem defines Fusc_Program FIB_FUSC:def 3 :
theorem
theorem
for
N,
k,
Fk,
Fk1 being
Element of
NAT for
s being
State-consisting of 3,
0 ,
0 ,
Fib_Program ,
((<*1*> ^ <*N*>) ^ <*Fk*>) ^ <*Fk1*> st
N > 0 &
Fk = Fib k &
Fk1 = Fib (k + 1) holds
(
ProgramPart s halts_on s &
LifeSpan (ProgramPart s),
s = (6 * N) - 4 & ex
m being
Element of
NAT st
(
m = (k + N) - 1 &
(Result (ProgramPart s),s) . (dl. 2) = Fib m &
(Result (ProgramPart s),s) . (dl. 3) = Fib (m + 1) ) )
theorem
canceled;
theorem Th5:
for
n,
N,
A,
B being
Element of
NAT for
s being
State-consisting of
0 ,
0 ,
0 ,
Fusc_Program ,
((<*2*> ^ <*n*>) ^ <*A*>) ^ <*B*> st
N > 0 &
Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds
(
ProgramPart s halts_on s &
(Result (ProgramPart s),s) . (dl. 3) = Fusc N & (
n = 0 implies
LifeSpan (ProgramPart s),
s = 1 ) & (
n > 0 implies
LifeSpan (ProgramPart s),
s = (6 * ([\(log 2,n)/] + 1)) + 1 ) )
theorem