Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Binary Arithmetics

by
Takaya Nishiyama, and
Yasuho Mizuhara

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

```environ

vocabulary MONOID_0, FUNCT_1, VECTSP_1, RELAT_1, MIDSP_3, FINSEQ_1, MARGREL1,
ZF_LANG, ORDINAL2, ARYTM_1, CQC_LANG, POWER, SETWISEO, BOOLE, FINSEQ_2,
BINARITH, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, NAT_1, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2,
BINOP_1, MONOID_0, SETWOP_2, SERIES_1, VECTSP_1, CQC_LANG, FINSEQ_1,
FINSEQ_2, FINSEQ_4, MIDSP_3;
constructors REAL_1, NAT_1, MARGREL1, BINOP_1, MONOID_0, SETWISEO, SERIES_1,
CQC_LANG, FINSOP_1, FINSEQ_4, MEMBERED, XBOOLE_0;
clusters INT_1, FUNCT_1, RELSET_1, MARGREL1, NAT_1, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

definition
cluster non empty Nat;
end;

theorem :: BINARITH:1
for i,j being Nat holds addnat.(i,j) = i + j;

theorem :: BINARITH:2
for i,n being Nat,
D being non empty set,
d being Element of D,
z being Tuple of n,D st i in Seg n holds
(z^<*d*>)/.i=z/.i;

theorem :: BINARITH:3
for n being Nat,
D being non empty set,
d being Element of D,
z being Tuple of n,D holds
(z^<*d*>)/.(n+1)=d;

canceled;

theorem :: BINARITH:5
for i,n being Nat holds
i in Seg n implies i is non empty;

definition
let x, y be boolean set;
func x 'or' y equals
:: BINARITH:def 1

'not'('not' x '&' 'not' y);
commutativity;
end;

definition
let x, y be boolean set;
func x 'xor' y equals
:: BINARITH:def 2

('not' x '&' y) 'or' (x '&' 'not' y);
commutativity;
end;

definition
let x, y be boolean set;
cluster x 'or' y -> boolean;
end;

definition
let x, y be boolean set;
cluster x 'xor' y -> boolean;
end;

definition
let x, y be Element of BOOLEAN;
redefine func x 'or' y -> Element of BOOLEAN;
func x 'xor' y -> Element of BOOLEAN;
end;

reserve x,y,z for boolean set;

canceled;

theorem :: BINARITH:7
x 'or' FALSE = x;

canceled;

theorem :: BINARITH:9
'not' (x '&' y) = 'not' x 'or' 'not' y;

theorem :: BINARITH:10
'not' (x 'or' y) = 'not' x '&' 'not' y;

canceled;

theorem :: BINARITH:12
x '&' y = 'not' ('not' x 'or' 'not' y);

theorem :: BINARITH:13
TRUE 'xor' x = 'not' x;

theorem :: BINARITH:14
FALSE 'xor' x = x;

theorem :: BINARITH:15
x 'xor' x = FALSE;

theorem :: BINARITH:16
x '&' x = x;

theorem :: BINARITH:17
x 'xor' 'not' x = TRUE;

theorem :: BINARITH:18
x 'or' 'not' x = TRUE;

theorem :: BINARITH:19
x 'or' TRUE = TRUE;

theorem :: BINARITH:20
(x 'or' y) 'or' z = x 'or' (y 'or' z);

theorem :: BINARITH:21
x 'or' x = x;

theorem :: BINARITH:22
x '&' (y 'or' z) = x '&' y 'or' x '&' z;

theorem :: BINARITH:23
x 'or' y '&' z = (x 'or' y) '&' (x 'or' z);

theorem :: BINARITH:24
x 'or' x '&' y = x;

theorem :: BINARITH:25
x '&' (x 'or' y) = x;

theorem :: BINARITH:26
x 'or' 'not' x '&' y = x 'or' y;

theorem :: BINARITH:27
x '&' ('not' x 'or' y) = x '&' y;

canceled 5;

theorem :: BINARITH:33
TRUE 'xor' FALSE = TRUE;

theorem :: BINARITH:34
(x 'xor' y) 'xor' z = x 'xor' (y 'xor' z);

theorem :: BINARITH:35
x 'xor' 'not' x '&' y = x 'or' y;

theorem :: BINARITH:36
x 'or' (x 'xor' y) = x 'or' y;

theorem :: BINARITH:37
x 'or' ('not' x 'xor' y) = x 'or' 'not' y;

theorem :: BINARITH:38
x '&' (y 'xor' z) = (x '&' y) 'xor' (x '&' z);

definition let i,j be natural number;
func i -' j -> Nat equals
:: BINARITH:def 3
i - j if i - j >= 0 otherwise 0;
end;

theorem :: BINARITH:39
for i,j being natural number holds i + j -' j = i;

reserve i,j,k for Nat;
reserve n for non empty Nat;
reserve x,y,z1,z2 for Tuple of n, BOOLEAN;

definition let n be Nat, x be Tuple of n, BOOLEAN;
func 'not' x -> Tuple of n, BOOLEAN means
:: BINARITH:def 4
for i st i in Seg n holds it/.i = 'not' (x/.i);
end;

definition let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
func carry(x, y) -> Tuple of n, BOOLEAN means
:: BINARITH:def 5

it/.1 = FALSE &
for i st 1 <= i & i < n holds it/.(i+1) = (x/.i) '&' (y/.i) 'or'
(x/.i) '&' (it/.i) 'or' (y/.i) '&' (it/.i);
end;

definition let n be Nat, x be Tuple of n, BOOLEAN;
func Binary(x) -> Tuple of n, NAT means
:: BINARITH:def 6
for i st i in Seg n holds
it/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-'1));
end;

definition let n be Nat, x be Tuple of n, BOOLEAN;
func Absval (x) -> Nat equals
:: BINARITH:def 7
end;

definition let n, x, y;
func x + y -> Tuple of n, BOOLEAN means
:: BINARITH:def 8
for i st i in Seg n holds it/.i =
(x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i);
end;

definition let n,z1,z2;
func add_ovfl(z1,z2) -> Element of BOOLEAN equals
:: BINARITH:def 9
(z1/.n) '&' (z2/.n) 'or'
(z1/.n) '&' (carry(z1,z2)/.n) 'or' (z2/.n) '&' (carry(z1,z2)/.n);
end;

scheme Ind_from_1 { P[Nat] } :
for k being non empty Nat holds P[k]
provided
P[1] and
for k being non empty Nat st P[k] holds P[k + 1];

definition let n,z1,z2;
pred z1,z2 are_summable means
:: BINARITH:def 10
end;

theorem :: BINARITH:40
for z1 being Tuple of 1,BOOLEAN holds
z1= <*FALSE*> or z1=<*TRUE*>;

theorem :: BINARITH:41
for z1 being Tuple of 1,BOOLEAN holds
z1=<*FALSE*> implies Absval(z1) = 0;

theorem :: BINARITH:42
for z1 being Tuple of 1,BOOLEAN holds
z1=<*TRUE*> implies Absval(z1)=1;

definition
let n1 be non empty Nat;
let n2 be Nat;
let D  be non empty set;
let z1 be Tuple of n1,D;
let z2 be Tuple of n2,D;
redefine func z1 ^ z2 -> Tuple of n1+n2,D;
end;

definition
let D be non empty set;
let d be Element of D;
redefine func <* d *> -> Tuple of 1,D;
end;

theorem :: BINARITH:43
for z1,z2 being Tuple of n,BOOLEAN holds
for d1,d2 being Element of BOOLEAN holds
for i being Nat holds
i in Seg n implies
carry(z1^<*d1*>,z2^<*d2*>)/.i = carry(z1,z2)/.i;

theorem :: BINARITH:44
for z1,z2 being Tuple of n,BOOLEAN,
d1,d2 being Element of BOOLEAN holds

theorem :: BINARITH:45
for z1,z2 being Tuple of n,BOOLEAN,
d1,d2 being Element of BOOLEAN holds
z1^<*d1*> + z2^<*d2*> = (z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>;

theorem :: BINARITH:46
for z being Tuple of n,BOOLEAN,
d being Element of BOOLEAN holds
Absval(z^<*d*>) = Absval(z)+IFEQ(d,FALSE,0,2 to_power n);

theorem :: BINARITH:47
for n for z1,z2 being Tuple of n,BOOLEAN holds
Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n)) =
Absval(z1) + Absval(z2);

theorem :: BINARITH:48
for z1,z2 being Tuple of n,BOOLEAN holds
z1,z2 are_summable implies
Absval(z1+z2) = Absval(z1) + Absval(z2);
```