:: Two Programs for {\bf SCM}. Part I - Preliminaries :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received October 8, 1993 :: Copyright (c) 1993-2021 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, SUBSET_1, ZFMISC_1, MCART_1, NAT_1, FUNCT_1, CARD_1, ARYTM_3, INT_1, XXREAL_0, ARYTM_1, RELAT_1, POWER, NEWTON, FINSEQ_1, ORDINAL4, PARTFUN1, PRE_FF, REAL_1, FUNCT_7; notations TARSKI, XBOOLE_0, XTUPLE_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, NAT_1, NEWTON, FINSEQ_1, FINSEQ_2; constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, PARTFUN1, NEWTON, POWER, RELSET_1, FINSEQ_2; registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, XCMPLX_0, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Fibonacci sequence :: Definition of fib registration let n,k be Nat; reduce In([n,k],[:NAT,NAT:]) to [n,k]; end; definition func Fib -> sequence of [:NAT, NAT:] means :: PRE_FF:def 1 it.0 = [0,1] & for n being Nat holds it.(n+1) = [ (it.n)`2, (it.n)`1 + (it.n)`2 ]; end; definition let n be Nat; func Fib n -> Element of NAT equals :: PRE_FF:def 2 (Fib.n)`1; 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 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 st a <= b & c >= 1 holds c to_power a <= c to_power b; theorem :: PRE_FF:9 for r, s being Real st r >= s holds [\r/] >= [\s/]; theorem :: PRE_FF:10 for a, b, c being Real 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 ) /]; definition let n be Nat; func Fusc n -> Element of NAT means :: PRE_FF:def 3 it = 0 if n = 0 otherwise ex l being Element of NAT, fusc being sequence of 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: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);