Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### A Representation of Integers by Binary Arithmetics and Addition of Integers

by
Hisayoshi Kunimune, and
Yatsuka Nakamura

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

```environ

vocabulary INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, ABSVALUE,
BINARITH, BINARI_2, BINARI_3, ARYTM_1, NAT_1, BINARI_4, EUCLID, ARYTM_3,
FINSEQ_2, FINSEQ_4, FUNCT_1, BOOLE, RELAT_1, VECTSP_1, ZF_LANG, GROUP_1;
notation INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, BINARITH,
BINARI_2, BINARI_3, GROUP_1, SERIES_1, NUMBERS, XCMPLX_0, XREAL_0,
XBOOLE_0, EUCLID, REAL_1, NAT_1, TARSKI, FINSEQ_4, FUNCT_1, RELAT_1,
VECTSP_1, ZFMISC_1, FINSEQOP, PREPOWER, SUBSET_1;
constructors BINARITH, BINARI_2, BINARI_3, GROUP_1, SERIES_1, REAL_1, EUCLID,
FINSEQ_4, FINSEQOP, SEQ_1, PREPOWER, EULER_2, MEMBERED;
clusters INT_1, BINARITH, MARGREL1, RELSET_1, NAT_1, XREAL_0, MEMBERED;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;

begin :: Preliminaries

reserve n for non empty Nat,
j,k,l,m for Nat,
g,h,i for Integer;

theorem :: BINARI_4:1
m > 0 implies m * 2 >= m + 1;

theorem :: BINARI_4:2
for m being Nat holds 2 to_power m >= m;

theorem :: BINARI_4:3
for m be Nat holds 0*m + 0*m = 0*m;

theorem :: BINARI_4:4
for k be Nat holds
k <= l & l <= m implies k = l or (k + 1 <= l & l <= m);

theorem :: BINARI_4:5
for n be non empty Nat holds
for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n
holds carry(x,y) = 0*n;

theorem :: BINARI_4:6
for n be non empty Nat holds
for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds x + y = 0*n;

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

theorem :: BINARI_4:8
l + m <= k - 1 implies l < k & m < k;

theorem :: BINARI_4:9
g <= h + i & h < 0 & i < 0 implies g < h & g < i;

theorem :: BINARI_4:10
l + m <= 2 to_power n - 1 implies

theorem :: BINARI_4:11
for n be non empty Nat, l,m be Nat st
l + m <= 2 to_power n - 1 holds
Absval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m;

theorem :: BINARI_4:12
for n be non empty Nat holds
(for z be Tuple of n,BOOLEAN st z/.n = TRUE holds
Absval(z) >= 2 to_power (n-'1));

theorem :: BINARI_4:13
l + m <= 2 to_power (n-'1) - 1 implies
carry(n-BinarySequence(l),n-BinarySequence(m))/.n = FALSE;

theorem :: BINARI_4:14
for n be non empty Nat st l + m <= 2 to_power (n-'1) - 1 holds
Intval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m;

theorem :: BINARI_4:15
for z be Tuple of 1,BOOLEAN st z=<*TRUE*> holds
Intval(z) = -1;

theorem :: BINARI_4:16
for z be Tuple of 1,BOOLEAN st z=<*FALSE*> holds
Intval(z) = 0;

theorem :: BINARI_4:17
for x be boolean set holds
TRUE 'or' x = TRUE;

theorem :: BINARI_4:18
for n be non empty Nat holds 0 <= 2 to_power (n-'1) - 1 &
-(2 to_power (n-'1)) <= 0;

theorem :: BINARI_4:19
for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds
x,y are_summable;

theorem :: BINARI_4:20
(i*n) mod n = 0;

begin :: Majorant Power

definition
let m, j be Nat;
func MajP(m, j) -> Nat means
:: BINARI_4:def 1

2 to_power it >= j & it >= m &
for k be Nat st 2 to_power k >= j & k >= m holds
k >= it;
end;

theorem :: BINARI_4:21
j >= k implies MajP(m, j) >= MajP(m, k);

theorem :: BINARI_4:22
l >= m implies MajP(l,j) >= MajP(m,j);

theorem :: BINARI_4:23
m >= 1 implies MajP(m, 1) = m;

theorem :: BINARI_4:24
j <= 2 to_power m implies MajP(m, j) = m;

theorem :: BINARI_4:25
j > 2 to_power m implies MajP(m, j) > m;

begin :: 2's Complement

definition
let m be Nat;
let i be Integer;
func 2sComplement( m, i ) -> Tuple of m, BOOLEAN equals
:: BINARI_4:def 2

m-BinarySequence( abs( (2 to_power MajP(m,abs(i))) + i ) ) if i < 0
otherwise
m-BinarySequence( abs(i) );
end;

theorem :: BINARI_4:26
for m be Nat holds 2sComplement(m,0) = 0*m;

theorem :: BINARI_4:27
for i be Integer st i <= 2 to_power (n-'1) - 1 &
-(2 to_power (n-'1)) <= i holds
Intval( 2sComplement( n, i ) ) = i;

theorem :: BINARI_4:28
for h,i be Integer st ((h >= 0 & i >= 0) or (h < 0 & i < 0)) &
h mod 2 to_power n = i mod 2 to_power n holds
2sComplement(n,h) = 2sComplement(n,i);

theorem :: BINARI_4:29
for h,i be Integer st ((h >= 0 & i >= 0) or (h < 0 & i < 0)) &
h,i are_congruent_mod 2 to_power n holds
2sComplement(n,h) = 2sComplement(n,i);

theorem :: BINARI_4:30
for l,m be Nat st l mod 2 to_power n = m mod 2 to_power n holds
n-BinarySequence(l) = n-BinarySequence(m);

theorem :: BINARI_4:31
for l,m be Nat st l,m are_congruent_mod 2 to_power n holds
n-BinarySequence(l) = n-BinarySequence(m);

theorem :: BINARI_4:32
for j be Nat st 1 <= j & j <= n holds
2sComplement(n+1,i)/.j = 2sComplement(n,i)/.j;

theorem :: BINARI_4:33
ex x be Element of BOOLEAN st
2sComplement(m+1,i) = 2sComplement(m,i)^<*x*>;

theorem :: BINARI_4:34
ex x be Element of BOOLEAN st
(m+1)-BinarySequence(l) = (m-BinarySequence(l))^<*x*>;

theorem :: BINARI_4:35
for n be non empty Nat holds
-2 to_power n <= h+i & h < 0 & i < 0 &
-2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i implies
carry(2sComplement(n+1,h),2sComplement(n+1,i))/.(n+1) = TRUE;

theorem :: BINARI_4:36
for n be non empty Nat st
-(2 to_power (n-'1)) <= h + i & h + i <= 2 to_power (n-'1) - 1 &
h >= 0 & i >= 0 holds
Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i;

theorem :: BINARI_4:37
for n be non empty Nat st
-2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
h < 0 & i < 0 & -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i holds
Intval(2sComplement(n+1,h) + 2sComplement(n+1,i)) = h+i;

theorem :: BINARI_4:38
for n be non empty Nat holds
-(2 to_power (n-'1)) <= h & h <= 2 to_power (n-'1) - 1 &
-(2 to_power (n-'1)) <= i & i <= 2 to_power (n-'1) - 1 &
-(2 to_power (n-'1)) <= h+i & h+i <= 2 to_power (n-'1) - 1 &
((h >= 0 & i < 0) or (h < 0 & i >= 0)) implies
Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i;
```