:: Two Programs for {\bf SCM}. Part I - Preliminaries
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, ZFMISC_1, MCART_1, NAT_1, FUNCT_1,
      CARD_1, ARYTM_3, INT_1, XXREAL_0, ARYTM_1, RELAT_1, XREAL_0, ORDINAL1,
      POWER, NEWTON, FINSEQ_1, ORDINAL4, PARTFUN1, PRE_FF;
 notations XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
      XREAL_0, INT_1, NAT_D, MCART_1, DOMAIN_1, POWER, FUNCT_1, PARTFUN1,
      FUNCT_2, FINSEQ_1, FINSEQ_2, NAT_1, NEWTON;
 constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, PARTFUN1,
      NEWTON, POWER, SEQ_1, RELSET_1, FINSEQ_2;
 registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, XBOOLE_0, FINSEQ_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Fibonacci sequence

:: Definition of fib

definition
  let n be Nat;
  func Fib (n) -> Element of 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 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 Element of NAT holds i div 2 is Element of NAT;

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

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

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

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

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

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

theorem :: PRE_FF:14
  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 Element of NAT;
  redefine func f.n -> FinSequence of NAT;
end;

definition
  let n be Nat;
  func Fusc n -> Element of NAT means
:: PRE_FF:def 2

  it = 0 if n = 0 otherwise ex l
being Element of 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 qua Element of NAT*)^ <*(fusc.n qua Element of NAT*)
/.k*>) & for k being Nat st n+2 = 2*k+1 holds fusc.(n+1) = (fusc.n qua Element
of NAT*)^<*((fusc.n qua Element of NAT*)/.k)+ ((fusc.n qua Element of NAT*)/.(k
  +1))*>;
end;

theorem :: PRE_FF:15
  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:16
  for n being Nat st n <> 0 holds n < 2*n;

theorem :: PRE_FF:17
  for n being Nat holds n < 2*n+1;

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

theorem :: PRE_FF:19
  for n, A, B, N being Nat st Fusc N = A * Fusc (2*n+1) + B * Fusc (2*n+1+1)
  holds Fusc N = A * Fusc n + (B+A) * Fusc (n+1);

theorem :: PRE_FF:20
  for n, A, B, N being Nat st Fusc N = A * Fusc (2*n) + B * Fusc (2*n+1)
  holds Fusc N = (A+B) * Fusc n + B * Fusc (n+1);