Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### Binary Arithmetics. Binary Sequences

by
Robert Milewski

Received February 24, 1998

MML identifier: BINARI_3
[ Mizar article, MML identifier index ]

```environ

vocabulary MIDSP_3, MARGREL1, BINARITH, POWER, FINSEQ_1, CQC_LANG, FINSEQ_5,
EUCLID, FINSEQ_2, ZF_LANG, FUNCT_1, ARYTM_1, RELAT_1, BINARI_2, NAT_1,
ARYTM_3, MATRIX_2, BINARI_3, FINSEQ_4, REALSET1;
notation SUBSET_1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, POWER, ABIAN, SERIES_1,
MARGREL1, FUNCT_1, CQC_LANG, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQOP,
REALSET1, BINARITH, BINARI_2, EUCLID, MIDSP_3;
constructors REAL_1, ABIAN, SERIES_1, FINSEQ_5, FINSEQOP, BINARITH, BINARI_2,
EUCLID, FINSEQ_4, REALSET1, MEMBERED;
clusters RELSET_1, NAT_2, MARGREL1, REALSET1, NAT_1, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Binary Arithmetics

theorem :: BINARI_3:1
for n be non empty Nat
for F be Tuple of n,BOOLEAN holds
Absval F < 2 to_power n;

theorem :: BINARI_3:2
for n be non empty 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 + 1) = 0*n ^ <* 0 *>;

theorem :: BINARI_3:5
for n be Nat holds
0*n in BOOLEAN*;

theorem :: BINARI_3:6
for n be Nat
for y be Tuple of n,BOOLEAN st y = 0*n holds
'not' y = n |-> 1;

theorem :: BINARI_3:7
for n be non empty Nat
for F be Tuple of n,BOOLEAN st F = 0*n holds Absval F = 0;

theorem :: BINARI_3:8
for n be non empty Nat
for F be Tuple of n,BOOLEAN st F = 0*n holds
Absval 'not' F = 2 to_power n - 1;

theorem :: BINARI_3:9
for n be Nat holds Rev (0*n) = 0*n;

theorem :: BINARI_3:10
for n be Nat
for y be Tuple of n,BOOLEAN st y = 0*n holds
Rev 'not' y = 'not' y;

theorem :: BINARI_3:11
Bin1 1 = <*TRUE*>;

theorem :: BINARI_3:12
for n be non empty Nat holds Absval (Bin1 n) = 1;

theorem :: BINARI_3:13
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:14
for x,y be Element of BOOLEAN holds
add_ovfl(<*x*>,<*y*>) = TRUE iff x = TRUE & y = TRUE;

theorem :: BINARI_3:15
'not' <*FALSE*> = <*TRUE*>;

theorem :: BINARI_3:16
'not' <*TRUE*> = <*FALSE*>;

theorem :: BINARI_3:17
<*FALSE*> + <*FALSE*> = <*FALSE*>;

theorem :: BINARI_3:18
<*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE*>;

theorem :: BINARI_3:19
<*TRUE*> + <*TRUE*> = <*FALSE*>;

theorem :: BINARI_3:20
for n be non empty Nat
for x,y be Tuple of n,BOOLEAN st
x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds
for k be non empty Nat st k <> 1 & k <= n holds
x/.k = TRUE & (carry(x,Bin1 n))/.k = TRUE;

theorem :: BINARI_3:21
for n be non empty 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:22
for n be non empty 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:23
for n be non empty Nat
for y be Tuple of n,BOOLEAN st y = 0*n holds
carry('not' y,Bin1 n) = 'not' Bin1 n;

theorem :: BINARI_3:24
for n be non empty 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:25
for n be non empty 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:26
for n be Nat holds n-BinarySequence 0 = 0*n;

theorem :: BINARI_3:27
for n,k be Nat st k < 2 to_power n holds
((n+1)-BinarySequence k).(n+1) = FALSE;

theorem :: BINARI_3:28
for n be non empty Nat
for k be Nat st k < 2 to_power n holds
(n+1)-BinarySequence k = (n-BinarySequence k)^<*FALSE*>;

theorem :: BINARI_3:29
for n be non empty Nat holds
(n+1)-BinarySequence 2 to_power n = 0*n^<*TRUE*>;

theorem :: BINARI_3:30
for n be non empty 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:31
for n be non empty 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:32
for n be non empty 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:33
for n be non empty Nat
for k be Nat st k + 1 < 2 to_power n holds
add_ovfl(n-BinarySequence k,Bin1 n) = FALSE;

theorem :: BINARI_3:34
for n be non empty 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:35
for n,i be Nat holds
(n+1)-BinarySequence i = <*i mod 2*> ^ (n-BinarySequence (i div 2));

theorem :: BINARI_3:36
for n be non empty Nat
for k be Nat holds k < 2 to_power n implies
Absval (n-BinarySequence k) = k;

theorem :: BINARI_3:37
for n be non empty Nat
for x be Tuple of n,BOOLEAN holds
n-BinarySequence (Absval x) = x;

```

Back to top