Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Two Programs for \bf SCM. Part II - Programs

by
Grzegorz Bancerek, and
Piotr Rudnicki

MML identifier: FIB_FUSC
[ Mizar article, MML identifier index ]

environ

vocabulary AMI_3, INT_1, POWER, ARYTM_1, FINSEQ_1, AMI_1, SCM_1, FUNCT_1,
PRE_FF, GROUP_1, NAT_1, FIB_FUSC;
notation XCMPLX_0, XREAL_0, INT_1, NAT_1, POWER, FINSEQ_1, AMI_1, SCM_1,
AMI_3, PRE_FF, CARD_4;
constructors NAT_1, POWER, SCM_1, PRE_FF, CARD_4, MEMBERED, XBOOLE_0;
clusters INT_1, AMI_1, AMI_3, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;

begin

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 *>^
<* goto il.3 *>;
end;

theorem :: FIB_FUSC:1
for N being Nat,
s being State-consisting of 0, 0, 0,
Fib_Program,
<*1*>^<*N*>^<*0*>^<*0*>
holds s is halting &
(N = 0 implies Complexity s = 1) &
(N > 0 implies Complexity s = 6 * N - 2) &
(Result s).dl.3 = Fib N;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Fusc
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let i be Integer;
func Fusc' i -> Nat means
:: FIB_FUSC:def 2

(ex n being Nat st i = n & it = Fusc n) or i is not Nat & it = 0;
end;

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 *>^
<* goto il.0 *>^
<* goto il.0 *>^
<* halt SCM *>;
end;

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

theorem :: FIB_FUSC:3
for N being Nat, k, Fk, Fk1 being Nat,
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 s is halting &
Complexity s = 6 * N - 4 &
ex m being Nat st m = k+N-1 &
(Result s).dl.2 = Fib m & (Result s).dl.3 = Fib (m+1);

canceled;

theorem :: FIB_FUSC:5
for n being Nat,
N, A, B being Nat,
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 s is halting &
(Result s).dl.3 = Fusc N &
(n = 0 implies Complexity s = 1) &
(n > 0 implies Complexity s = 6 * ([\ log(2, n) /] + 1) + 1);

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