The abstract of the Mizar article:

Two Programs for \bf SCM. Part I - Preliminaries

by

Grzegorz Bancerek, and

Piotr Rudnicki

Received October 8, 1993

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 x`1 -> Element of Y1;
 func x`2 -> 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);