begin
Lm1:
0 = [\(log 2,1)/]
Lm2:
for nn' being Element of NAT st nn' > 0 holds
( [\(log 2,nn')/] is Element of NAT & (6 * ([\(log 2,nn')/] + 1)) + 1 > 0 )
Lm3:
for nn, nn' being Element of NAT st nn = (2 * nn') + 1 & nn' > 0 holds
6 + ((6 * ([\(log 2,nn')/] + 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, nn' being Element of NAT st nn = 2 * nn' & nn' > 0 holds
6 + ((6 * ([\(log 2,nn')/] + 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
theorem
canceled;
theorem Th5:
theorem