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

### Two Programs for \bf SCM. Part I - Preliminaries

by
Grzegorz Bancerek, and
Piotr Rudnicki

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

environ

vocabulary MCART_1, FUNCT_1, INT_1, NAT_1, ARYTM_3, ARYTM_1, POWER, GROUP_1,
FINSEQ_1, RELAT_1, PRE_FF, FINSEQ_4, ARYTM;
notation XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
INT_1, NAT_1, MCART_1, DOMAIN_1, POWER, FUNCT_1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FINSEQ_4, CARD_4;
constructors INT_1, NAT_1, DOMAIN_1, POWER, FUNCT_2, FINSEQ_4, CARD_4,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, INT_1, RELSET_1, XREAL_0, NAT_1, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Fibonacci sequence

definition let X1, X2 be non empty set;
let Y1 be non empty Subset of X1;
let Y2 be non empty Subset of X2;
let x be Element of [:Y1,Y2:];
redefine func x1 -> Element of Y1;
func x2 -> Element of Y2;
end;

reserve n for Nat;

:: Definition of fib

definition let n;
func Fib (n) -> Nat means
:: PRE_FF:def 1
ex fib being Function of NAT, [:NAT, NAT:] st
it = (fib.n)1 & fib.0 = [0,1] &
for n being Nat holds fib.(n+1) = [ (fib.n)2, (fib.n)1 + (fib.n)2 ];
end;

theorem :: PRE_FF:1
Fib(0) = 0 &
Fib(1) = 1 &
(for n being Nat holds Fib((n+1)+1) = Fib(n) + Fib(n+1));

:: Fusc function auxiliaries

theorem :: PRE_FF:2
for i being Integer holds i div 1 = i;

theorem :: PRE_FF:3
for i, j being Integer st j > 0 & i div j = 0 holds i < j;

theorem :: PRE_FF:4
for i, j being Integer st 0<=i & i<j holds i div j = 0;

theorem :: PRE_FF:5
for i, j, k being Integer st j > 0 & k > 0
holds (i div j) div k = i div (j*k);

theorem :: PRE_FF:6
for i being Integer holds i mod 2 = 0 or i mod 2 = 1;

theorem :: PRE_FF:7
for i being Integer st i is Nat holds i div 2 is Nat;

canceled 2;

theorem :: PRE_FF:10
for a, b, c being real number st a <= b & c > 1
holds c to_power a <= c to_power b;

theorem :: PRE_FF:11
for r, s being real number st r>=s holds [\r/]>=[\s/];

theorem :: PRE_FF:12
for a, b, c being real number st a > 1 & b > 0 & c >= b
holds log (a, c) >= log (a, b);

theorem :: PRE_FF:13
for n being Nat st n > 0 holds
[\ log (2, 2*n) /] +1 <> [\ log (2, 2*n + 1) /];

theorem :: PRE_FF:14
for n being Nat st n > 0 holds
[\ log (2, 2*n) /] +1 >= [\ log (2, 2*n + 1) /];

theorem :: PRE_FF:15
for n being Nat st n > 0 holds
[\ log(2, 2*n) /] = [\ log(2, 2*n + 1) /];

theorem :: PRE_FF:16
for n being Nat st n > 0 holds
[\ log(2, n) /] + 1 = [\ log(2, 2*n + 1) /];

:: Fusc sequence

definition
let f be Function of NAT, NAT*, n be Nat;
redefine func f.n -> FinSequence of NAT;
end;

definition
let n be Nat;
func Fusc n -> Nat means
:: PRE_FF:def 2
it = 0 if n = 0 otherwise
ex l being Nat, fusc  being Function of NAT, NAT* st
l+1 = n & it = (fusc.l)/.n &
fusc.0 = <*1*> &
for n being Nat holds
(for k being Nat st n+2 = 2*k holds
fusc.(n+1) = fusc.n^<*(fusc.n)/.k*>) &
(for k being Nat st n+2 = 2*k+1 holds
fusc.(n+1) = fusc.n^<*((fusc.n)/.k)+((fusc.n)/.(k+1))*>);
end;

theorem :: PRE_FF:17
Fusc 0 = 0 & Fusc 1 = 1 &
for n being Nat holds Fusc (2*n) = Fusc n &
Fusc (2*n+1) = Fusc n + Fusc (n+1);

:: Auxiliary functions specific for Fib and Fusc of little general interest

theorem :: PRE_FF:18
for nn, nn' being Nat st nn <> 0 & nn = 2*nn' holds nn' < nn;

theorem :: PRE_FF:19
for nn, nn' being Nat st nn = 2*nn'+1 holds nn' < nn;

theorem :: PRE_FF:20
for A, B being Nat holds B = A * Fusc 0 + B * Fusc (0+1);

theorem :: PRE_FF:21
for nn, nn', A, B, N being Nat st nn = 2*nn'+1 &
Fusc N = A * Fusc nn + B * Fusc (nn+1) holds
Fusc N = A * Fusc nn' + (B+A) * Fusc (nn'+1);

theorem :: PRE_FF:22
for nn, nn', A, B, N being Nat st nn = 2*nn' &
Fusc N = A * Fusc nn + B * Fusc (nn+1) holds
Fusc N = (A+B) * Fusc nn' + B * Fusc (nn'+1);