:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received October 8, 1993

:: Copyright (c) 1993-2016 Association of Mizar Users

Lm1: 0 = [\(log (2,1))/]

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

Lm6: for N being Nat st N <> 0 holds

(6 * N) - 4 > 0

proof end;

Lm7: dl. 0 <> dl. 1

by AMI_3:10;

Lm8: dl. 0 <> dl. 2

by AMI_3:10;

Lm9: dl. 0 <> dl. 3

by AMI_3:10;

Lm10: dl. 1 <> dl. 2

by AMI_3:10;

Lm11: dl. 1 <> dl. 3

by AMI_3:10;

Lm12: dl. 2 <> dl. 3

by AMI_3:10;

Lm13: dl. 0 <> dl. 4

by AMI_3:10;

Lm14: dl. 1 <> dl. 4

by AMI_3:10;

Lm15: dl. 2 <> dl. 4

by AMI_3:10;

Lm16: dl. 3 <> dl. 4

by AMI_3:10;

definition

(((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%> is XFinSequence of the InstructionsF of SCM ;

end;

func Fib_Program -> XFinSequence of the InstructionsF of SCM equals :: FIB_FUSC:def 1

(((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;

coherence (((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;

(((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%> is XFinSequence of the InstructionsF of SCM ;

:: deftheorem defines Fib_Program FIB_FUSC:def 1 :

Fib_Program = (((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;

Fib_Program = (((((((<%((dl. 1) >0_goto 2)%> ^ <%(halt SCM)%>) ^ <%((dl. 3) := (dl. 0))%>) ^ <%(SubFrom ((dl. 1),(dl. 0)))%>) ^ <%((dl. 1) =0_goto 1)%>) ^ <%((dl. 4) := (dl. 2))%>) ^ <%((dl. 2) := (dl. 3))%>) ^ <%(AddTo ((dl. 3),(dl. 4)))%>) ^ <%(SCM-goto 3)%>;

Lm17: for F being NAT -defined the InstructionsF of SCM -valued total Function

for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM st (((((((<%I1%> ^ <%I2%>) ^ <%I3%>) ^ <%I4%>) ^ <%I5%>) ^ <%I6%>) ^ <%I7%>) ^ <%I8%>) ^ <%I9%> c= F holds

( F . 0 = I1 & F . 1 = I2 & F . 2 = I3 & F . 3 = I4 & F . 4 = I5 & F . 5 = I6 & F . 6 = I7 & F . 7 = I8 & F . 8 = I9 )

proof end;

theorem :: FIB_FUSC:1

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fib_Program c= F holds

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 )

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 )

proof end;

:: Fusc

definition

let i be Integer;

ex b_{1} being Element of NAT st

( ex n being Element of NAT st

( i = n & b_{1} = Fusc n ) or ( i is not Element of NAT & b_{1} = 0 ) )

for b_{1}, b_{2} being Element of NAT st ( ex n being Element of NAT st

( i = n & b_{1} = Fusc n ) or ( i is not Element of NAT & b_{1} = 0 ) ) & ( ex n being Element of NAT st

( i = n & b_{2} = Fusc n ) or ( i is not Element of NAT & b_{2} = 0 ) ) holds

b_{1} = b_{2}
;

end;
func Fusc' i -> Element of NAT means :Def2: :: FIB_FUSC:def 2

( ex n being Element of NAT st

( i = n & it = Fusc n ) or ( i is not Element of NAT & it = 0 ) );

existence ( ex n being Element of NAT st

( i = n & it = Fusc n ) or ( i is not Element of NAT & it = 0 ) );

ex b

( ex n being Element of NAT st

( i = n & b

proof end;

uniqueness for b

( i = n & b

( i = n & b

b

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

for i being Integer

for b_{2} being Element of NAT holds

( b_{2} = Fusc' i iff ( ex n being Element of NAT st

( i = n & b_{2} = Fusc n ) or ( i is not Element of NAT & b_{2} = 0 ) ) );

for i being Integer

for b

( b

( i = n & b

definition

(((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%> is XFinSequence of the InstructionsF of SCM ;

end;

func Fusc_Program -> XFinSequence of the InstructionsF of SCM equals :: FIB_FUSC:def 3

(((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;

coherence (((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;

(((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%> is XFinSequence of the InstructionsF of SCM ;

:: deftheorem defines Fusc_Program FIB_FUSC:def 3 :

Fusc_Program = (((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;

Fusc_Program = (((((((<%((dl. 1) =0_goto 8)%> ^ <%((dl. 4) := (dl. 0))%>) ^ <%(Divide ((dl. 1),(dl. 4)))%>) ^ <%((dl. 4) =0_goto 6)%>) ^ <%(AddTo ((dl. 3),(dl. 2)))%>) ^ <%(SCM-goto 0)%>) ^ <%(AddTo ((dl. 2),(dl. 3)))%>) ^ <%(SCM-goto 0)%>) ^ <%(halt SCM)%>;

theorem :: FIB_FUSC:2

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds

for N being Element of NAT st N > 0 holds

for s being 0 -started State-consisting of <%2,N,1,0%> holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 )

for N being Element of NAT st N > 0 holds

for s being 0 -started State-consisting of <%2,N,1,0%> holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 )

proof end;

theorem :: FIB_FUSC:3

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fib_Program c= F holds

for N, k, Fk, Fk1 being Nat

for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds

( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st

( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )

for N, k, Fk, Fk1 being Nat

for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds

( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st

( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )

proof end;

theorem Th4: :: FIB_FUSC:4

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds

for n, N, A, B being Element of NAT

for s being 0 -started State-consisting of <%2,n,A,B%> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( n = 0 implies LifeSpan (F,s) = 1 ) & ( n > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,n))/] + 1)) + 1 ) )

for n, N, A, B being Element of NAT

for s being 0 -started State-consisting of <%2,n,A,B%> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( n = 0 implies LifeSpan (F,s) = 1 ) & ( n > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,n))/] + 1)) + 1 ) )

proof end;

theorem :: FIB_FUSC:5

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds

for N being Element of NAT st N > 0 holds

for s being 0 -started State-consisting of <%2,N,1,0%> holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )

for N being Element of NAT st N > 0 holds

for s being 0 -started State-consisting of <%2,N,1,0%> holds

( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )

proof end;