:: Binary Arithmetics. Addition and Subtraction of Integers
:: by Yasuho Mizuhara and Takaya Nishiyama
::
:: Received March 18, 1994
:: Copyright (c) 1994 Association of Mizar Users
Lm1:
for n being Nat
for p, q being Tuple of n,BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
definition
let n be
Nat;
func Bin1 n -> Tuple of
n,
BOOLEAN means :
Def1:
:: BINARI_2:def 1
for
i being
Nat st
i in Seg n holds
it /. i = IFEQ i,1,
TRUE ,
FALSE ;
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ i,1,TRUE ,FALSE
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ i,1,TRUE ,FALSE ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ i,1,TRUE ,FALSE ) holds
b1 = b2
end;
:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :
:: deftheorem defines Neg2 BINARI_2:def 2 :
:: deftheorem Def3 defines Intval BINARI_2:def 3 :
:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :
:: deftheorem defines Int_add_udfl BINARI_2:def 5 :
theorem :: BINARI_2:1
canceled;
theorem :: BINARI_2:2
canceled;
theorem :: BINARI_2:3
theorem Th4: :: BINARI_2:4
theorem :: BINARI_2:5
theorem :: BINARI_2:6
theorem Th7: :: BINARI_2:7
theorem Th8: :: BINARI_2:8
theorem Th9: :: BINARI_2:9
theorem Th10: :: BINARI_2:10
theorem Th11: :: BINARI_2:11
theorem Th12: :: BINARI_2:12
theorem Th13: :: BINARI_2:13
for
m being non
empty Nat for
z1,
z2 being
Tuple of
m,
BOOLEAN for
d1,
d2 being
Element of
BOOLEAN holds
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
theorem Th14: :: BINARI_2:14
for
m being non
empty Nat 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*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))
theorem Th15: :: BINARI_2:15
theorem Th16: :: BINARI_2:16
theorem Th17: :: BINARI_2:17
theorem :: BINARI_2:18
definition
let n be non
empty Nat;
let x,
y be
Tuple of
n,
BOOLEAN ;
func x - y -> Tuple of
n,
BOOLEAN means :
Def6:
:: BINARI_2:def 6
for
i being
Nat st
i in Seg n holds
it /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i);
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i)
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) holds
b1 = b2
end;
:: deftheorem Def6 defines - BINARI_2:def 6 :
theorem Th19: :: BINARI_2:19
theorem :: BINARI_2:20
theorem :: BINARI_2:21
for
m being non
empty Nat for
z1,
z2 being
Tuple of
m,
BOOLEAN for
d1,
d2 being
Element of
BOOLEAN holds
(((Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))