:: Binary Arithmetics. Binary Sequences :: by Robert Milewski :: :: Received February 24, 1998 :: Copyright (c) 1998-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, XBOOLE_0, NAT_1, FINSEQ_2, MARGREL1, BINARITH, ARYTM_3, POWER, SUBSET_1, ORDINAL4, FINSEQ_1, FUNCOP_1, XBOOLEAN, CARD_1, RELAT_1, REAL_1, FINSEQ_5, EUCLID, XXREAL_0, FUNCT_1, PARTFUN1, ARYTM_1, BINARI_2, ZFMISC_1, INT_1, ABIAN, BINARI_3, XCMPLX_0; notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_D, POWER, ABIAN, SERIES_1, MARGREL1, FUNCT_1, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_5, ZFMISC_1, FINSEQ_2, BINARITH, BINARI_2, EUCLID; constructors NAT_D, FINSEQOP, SERIES_1, BINARITH, FINSEQ_5, BINARI_2, ABIAN, EUCLID, TREES_3; registrations RELSET_1, XREAL_0, NAT_1, XBOOLEAN, MARGREL1, NAT_2, ORDINAL1, XBOOLE_0, FINSEQ_2, INT_1, FINSEQ_1; requirements REAL, NUMERALS, SUBSET, ARITHM; begin :: Binary Arithmetics theorem :: BINARI_3:1 for n be non zero Nat for F be Tuple of n,BOOLEAN holds Absval F < 2 to_power n; theorem :: BINARI_3:2 for n be non zero Nat for F1,F2 be Tuple of n,BOOLEAN st Absval F1 = Absval F2 holds F1 = F2; theorem :: BINARI_3:3 for t1,t2 be FinSequence st Rev t1 = Rev t2 holds t1 = t2; theorem :: BINARI_3:4 for n be Nat holds 0*n in BOOLEAN*; theorem :: BINARI_3:5 for n be Nat for y be Tuple of n,BOOLEAN st y = 0*n holds 'not' y = n |-> 1; theorem :: BINARI_3:6 for n be non zero Nat for F be Tuple of n,BOOLEAN st F = 0*n holds Absval F = 0; theorem :: BINARI_3:7 for n be non zero Nat for F be Tuple of n,BOOLEAN st F = 0*n holds Absval 'not' F = 2 to_power n - 1; theorem :: BINARI_3:8 for n be Nat holds Rev (0*n) = 0*n; theorem :: BINARI_3:9 for n be Nat for y be Tuple of n,BOOLEAN st y = 0*n holds Rev 'not' y = 'not' y; theorem :: BINARI_3:10 Bin1 1 = <*TRUE*>; theorem :: BINARI_3:11 for n be non zero Nat holds Absval (Bin1 n) = 1; theorem :: BINARI_3:12 for x,y be Element of BOOLEAN holds (x 'or' y = TRUE iff x = TRUE or y = TRUE) & (x 'or' y = FALSE iff x = FALSE & y = FALSE); theorem :: BINARI_3:13 for x,y be Element of BOOLEAN holds add_ovfl(<*x*>,<*y*>) = TRUE iff x = TRUE & y = TRUE; theorem :: BINARI_3:14 'not' <*FALSE*> = <*TRUE*>; theorem :: BINARI_3:15 'not' <*TRUE*> = <*FALSE*>; theorem :: BINARI_3:16 <*FALSE*> + <*FALSE*> = <*FALSE*>; theorem :: BINARI_3:17 <*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE *>; theorem :: BINARI_3:18 <*TRUE*> + <*TRUE*> = <*FALSE*>; theorem :: BINARI_3:19 for n be non zero Nat for x,y be Tuple of n,BOOLEAN st x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds for k be non zero Nat st k <> 1 & k <= n holds x/.k = TRUE & (carry(x,Bin1 n))/.k = TRUE; registration cluster zero -> non positive for Nat; end; theorem :: BINARI_3:20 for n be non zero Nat for x be Tuple of n,BOOLEAN st x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds carry(x,Bin1 n) = 'not' Bin1 n; theorem :: BINARI_3:21 for n be non zero Nat for x,y be Tuple of n,BOOLEAN st y = 0*n & x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds x = 'not' y; theorem :: BINARI_3:22 for n be non zero Nat for y be Tuple of n,BOOLEAN st y = 0*n holds carry('not' y,Bin1 n) = 'not' Bin1 n; theorem :: BINARI_3:23 for n be non zero Nat for x,y be Tuple of n,BOOLEAN st y = 0*n holds add_ovfl(x,Bin1 n) = TRUE iff x = 'not' y; theorem :: BINARI_3:24 for n be non zero Nat for z be Tuple of n,BOOLEAN st z = 0*n holds 'not' z + Bin1 n = z; begin :: Binary Sequences definition let n,k be Nat; func n-BinarySequence k -> Tuple of n,BOOLEAN means :: BINARI_3:def 1 for i be Nat st i in Seg n holds it/.i = IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE); end; theorem :: BINARI_3:25 for n be Nat holds n-BinarySequence 0 = 0*n; theorem :: BINARI_3:26 for n,k be Nat st k < 2 to_power n holds ((n+1)-BinarySequence k ).(n+1) = FALSE; theorem :: BINARI_3:27 for n be non zero Nat for k be Nat st k < 2 to_power n holds (n +1)-BinarySequence k = (n-BinarySequence k)^<*FALSE*>; theorem :: BINARI_3:28 for i being Nat holds (i+1)-BinarySequence 2 to_power i= 0*i^<*1 *>; theorem :: BINARI_3:29 for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds ((n+1)-BinarySequence k).(n+1) = TRUE; theorem :: BINARI_3:30 for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds (n+1)-BinarySequence k = (n-BinarySequence (k -' 2 to_power n))^<*TRUE*>; theorem :: BINARI_3:31 for n be non zero Nat for k be Nat st k < 2 to_power n for x be Tuple of n,BOOLEAN st x = 0*n holds n-BinarySequence k = 'not' x iff k = 2 to_power n - 1; theorem :: BINARI_3:32 for n be non zero Nat for k be Nat st k + 1 < 2 to_power n holds add_ovfl(n-BinarySequence k,Bin1 n) = FALSE; theorem :: BINARI_3:33 for n be non zero Nat for k be Nat st k + 1 < 2 to_power n holds n-BinarySequence (k+1) = n-BinarySequence k + Bin1 n; theorem :: BINARI_3:34 for n,i be Nat holds (n+1)-BinarySequence i = <*i mod 2*> ^ (n -BinarySequence (i div 2)); theorem :: BINARI_3:35 for n be non zero Nat for k be Nat holds k < 2 to_power n implies Absval (n-BinarySequence k) = k; theorem :: BINARI_3:36 for n be non zero Nat for x be Tuple of n,BOOLEAN holds n -BinarySequence (Absval x) = x;