:: FIB_FUSC semantic presentation

Lemma1: 6 + 1 = (6 * ([\(log 2,1)/] + 1)) + 1

proof end;

Lemma2: for b₁ being Nat st b₁ > 0 holds
( [\(log 2,b₁)/] is Nat & (6 * ([\(log 2,b₁)/] + 1)) + 1 > 0 )

proof end;

Lemma3: for b₁, b₂ being Nat st b₁ = (2 * b₂) + 1 & b₂ > 0 holds
6 + ((6 * ([\(log 2,b₂)/] + 1)) + 1) = (6 * ([\(log 2,b₁)/] + 1)) + 1

proof end;

Lemma4: for b₁ being Nat st b₁ > 0 holds
( log 2,(2 * b₁) = 1 + (log 2,b₁) & log 2,(2 * b₁) = (log 2,b₁) + 1 )

proof end;

Lemma5: for b₁, b₂ being Nat st b₁ = 2 * b₂ & b₂ > 0 holds
6 + ((6 * ([\(log 2,b₂)/] + 1)) + 1) = (6 * ([\(log 2,b₁)/] + 1)) + 1

proof end;

Lemma6: for b₁ being Nat st b₁ <> 0 holds
(6 * b₁) - 4 > 0

proof end;

Lemma7: ( dl. 0 <> dl. 1 & dl. 0 <> dl. 2 & dl. 0 <> dl. 3 & dl. 1 <> dl. 2 & dl. 1 <> dl. 3 & dl. 2 <> dl. 3 )
by AMI_3:52;

Lemma8: ( dl. 0 <> dl. 4 & dl. 1 <> dl. 4 & dl. 2 <> dl. 4 & dl. 3 <> dl. 4 )
by AMI_3:52;

definition

func Fib_Program -> FinSequence of the Instructions of SCM equals :: FIB_FUSC:def 1
(((((((<*((dl. 1) >0_goto (il. 2))*> ^ <*(halt SCM )*>) ^ <*((dl. 3) := (dl. 0))*>) ^ <*(SubFrom (dl. 1),(dl. 0))*>) ^ <*((dl. 1) =0_goto (il. 1))*>) ^ <*((dl. 4) := (dl. 2))*>) ^ <*((dl. 2) := (dl. 3))*>) ^ <*(AddTo (dl. 3),(dl. 4))*>) ^ <*(goto (il. 3))*>;
coherence ;

end;

:: deftheorem Def1 defines Fib_Program FIB_FUSC:def 1 :

theorem Th1: :: FIB_FUSC:1

for b₁ being Nat
for b₂ being State-consisting of 0,0,0, Fib_Program ,((<*1*> ^ <*b₁*>) ^ <*0*>) ^ <*0*> holds
( b₂ is halting & ( b₁ = 0 implies Complexity b₂ = 1 ) & ( b₁ > 0 implies Complexity b₂ = (6 * b₁) - 2 ) & (Result b₂) . (dl. 3) = Fib b₁ )

proof end;

definition

let c₁ be Integer;
func Fusc' c₁ -> Nat means :Def2: :: FIB_FUSC:def 2
( ex b₁ being Nat st
( a₁ = b₁ & a₂ = Fusc b₁ ) or ( a₁ is not Nat & a₂ = 0 ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines Fusc' FIB_FUSC:def 2 :

definition

func Fusc_Program -> FinSequence of the Instructions of SCM equals :: FIB_FUSC:def 3
(((((((<*((dl. 1) =0_goto (il. 8))*> ^ <*((dl. 4) := (dl. 0))*>) ^ <*(Divide (dl. 1),(dl. 4))*>) ^ <*((dl. 4) =0_goto (il. 6))*>) ^ <*(AddTo (dl. 3),(dl. 2))*>) ^ <*(goto (il. 0))*>) ^ <*(AddTo (dl. 2),(dl. 3))*>) ^ <*(goto (il. 0))*>) ^ <*(halt SCM )*>;
coherence ;

end;

:: deftheorem Def3 defines Fusc_Program FIB_FUSC:def 3 :

theorem Th2: :: FIB_FUSC:2

for b₁ being Nat st b₁ > 0 holds
for b₂ being State-consisting of 0,0,0, Fusc_Program ,((<*2*> ^ <*b₁*>) ^ <*1*>) ^ <*0*> holds
( b₂ is halting & (Result b₂) . (dl. 3) = Fusc b₁ & Complexity b₂ = (6 * ([\(log 2,b₁)/] + 1)) + 1 )

proof end;

theorem Th3: :: FIB_FUSC:3

for b₁, b₂, b₃, b₄ being Nat
for b₅ being State-consisting of 3,0,0, Fib_Program ,((<*1*> ^ <*b₁*>) ^ <*b₃*>) ^ <*b₄*> st b₁ > 0 & b₃ = Fib b₂ & b₄ = Fib (b₂ + 1) holds
( b₅ is halting & Complexity b₅ = (6 * b₁) - 4 & ex b₆ being Nat st
( b₆ = (b₂ + b₁) - 1 & (Result b₅) . (dl. 2) = Fib b₆ & (Result b₅) . (dl. 3) = Fib (b₆ + 1) ) )

proof end;

theorem Th4: :: FIB_FUSC:4

canceled;

theorem Th5: :: FIB_FUSC:5

for b₁, b₂, b₃, b₄ being Nat
for b₅ being State-consisting of 0,0,0, Fusc_Program ,((<*2*> ^ <*b₁*>) ^ <*b₃*>) ^ <*b₄*> st b₂ > 0 & Fusc b₂ = (b₃ * (Fusc b₁)) + (b₄ * (Fusc (b₁ + 1))) holds
( b₅ is halting & (Result b₅) . (dl. 3) = Fusc b₂ & ( b₁ = 0 implies Complexity b₅ = 1 ) & ( b₁ > 0 implies Complexity b₅ = (6 * ([\(log 2,b₁)/] + 1)) + 1 ) )

proof end;

theorem Th6: :: FIB_FUSC:6

for b₁ being Nat st b₁ > 0 holds
for b₂ being State-consisting of 0,0,0, Fusc_Program ,((<*2*> ^ <*b₁*>) ^ <*1*>) ^ <*0*> holds
( b₂ is halting & (Result b₂) . (dl. 3) = Fusc b₁ & ( b₁ = 0 implies Complexity b₂ = 1 ) & ( b₁ > 0 implies Complexity b₂ = (6 * ([\(log 2,b₁)/] + 1)) + 1 ) )

proof end;