:: 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);