Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Binary Arithmetics, Addition and Subtraction of Integers

by
Yasuho Mizuhara, and
Takaya Nishiyama

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

```environ

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

begin

definition let X be non empty set; let D be non empty Subset of X;
let x,y be set, a,b be Element of D;
redefine func IFEQ(x,y,a,b) -> Element of D;
end;

reserve i,j,n for Nat;
reserve m for non empty Nat;
reserve p,q for Tuple of n, BOOLEAN;
reserve d,d1,d2 for Element of BOOLEAN;

definition let n be Nat;
func Bin1 (n) -> Tuple of n, BOOLEAN means
:: BINARI_2:def 1
for i st i in Seg n holds it/.i = IFEQ(i,1,TRUE,FALSE);
end;

definition let n be non empty Nat, x be Tuple of n, BOOLEAN;
func Neg2 (x) -> Tuple of n,BOOLEAN equals
:: BINARI_2:def 2
'not' x + Bin1 (n);
end;

definition let n be Nat, x be Tuple of n, BOOLEAN;
func Intval (x) -> Integer equals
:: BINARI_2:def 3
Absval (x) if x/.n = FALSE
otherwise Absval (x) - 2 to_power n;
end;

definition let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
func Int_add_ovfl(z1,z2) -> Element of BOOLEAN equals
:: BINARI_2:def 4
'not' (z1/.n) '&' 'not' (z2/.n) '&' (carry(z1,z2)/.n);
end;

definition let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
func Int_add_udfl(z1,z2) -> Element of BOOLEAN equals
:: BINARI_2:def 5
(z1/.n) '&' (z2/.n) '&' 'not' (carry(z1,z2)/.n);
end;

canceled 2;

theorem :: BINARI_2:3
for z1 being Tuple of 2, BOOLEAN holds
z1=<*FALSE*>^<*FALSE*> implies Intval(z1) = 0;

theorem :: BINARI_2:4
for z1 being Tuple of 2, BOOLEAN holds
z1=<*TRUE*>^<*FALSE*> implies Intval(z1) = 1;

theorem :: BINARI_2:5
for z1 being Tuple of 2, BOOLEAN holds
z1=<*FALSE*>^<*TRUE*> implies Intval(z1) = -2;

theorem :: BINARI_2:6
for z1 being Tuple of 2, BOOLEAN holds
z1=<*TRUE*>^<*TRUE*> implies Intval(z1) = -1;

theorem :: BINARI_2:7
for i st i in Seg n & i = 1 holds (Bin1(n))/.i = TRUE;

theorem :: BINARI_2:8
for i st i in Seg n & i <> 1 holds (Bin1(n))/.i = FALSE;

theorem :: BINARI_2:9
Bin1 (m+1) = Bin1 (m)^<*FALSE*>;

theorem :: BINARI_2:10
for m holds Intval (Bin1(m)^<*FALSE*>) = 1;

theorem :: BINARI_2:11
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds
'not' (z^<* d *>) = 'not' z^<* 'not' d *>;

theorem :: BINARI_2:12
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds
Intval(z^<*d*>) = Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat);

theorem :: BINARI_2:13
for z1,z2 being Tuple of m, BOOLEAN
for d1,d2 being Element of BOOLEAN holds
Intval(z1^<*d1*>+z2^<*d2*>)
= Intval(z1^<*d1*>) + Intval(z2^<*d2*>);

theorem :: BINARI_2:14
for z1,z2 being Tuple of m, BOOLEAN
for d1,d2 being Element of BOOLEAN holds
Intval(z1^<*d1*>+z2^<*d2*>)
= Intval(z1^<*d1*>) + Intval(z2^<*d2*>)

theorem :: BINARI_2:15
for m for x being Tuple of m, BOOLEAN holds
Absval('not' x) = - Absval(x) + 2 to_power m - 1;

theorem :: BINARI_2:16
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds
Neg2(z^<*d*>) = Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>;

theorem :: BINARI_2:17
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds
Intval(Neg2(z^<*d*>))
= - Intval(z^<*d*>);

theorem :: BINARI_2:18
for m for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds
Neg2(Neg2(z^<*d*>)) = z^<*d*>;

definition let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
func x - y -> Tuple of n, BOOLEAN means
:: BINARI_2:def 6
for i st i in Seg n holds
it/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
end;

theorem :: BINARI_2:19
for x,y being Tuple of m, BOOLEAN holds x - y = x + Neg2(y);

theorem :: BINARI_2:20
for z1,z2 being Tuple of m, BOOLEAN
for d1,d2 being Element of BOOLEAN holds
z1^<*d1*> - z2^<*d2*>
= (z1 + Neg2(z2))^<*d1 'xor' 'not' d2 'xor' add_ovfl('not'