:: Binary Arithmetics. Addition
:: by Takaya Nishiyama and Yasuho Mizuhara
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: BINARITH:1
canceled;
theorem Th2: :: BINARITH:2
theorem Th3: :: BINARITH:3
theorem :: BINARITH:4
canceled;
theorem :: BINARITH:5
canceled;
theorem :: BINARITH:6
canceled;
theorem :: BINARITH:7
theorem :: BINARITH:8
canceled;
theorem :: BINARITH:9
theorem :: BINARITH:10
theorem :: BINARITH:11
canceled;
theorem :: BINARITH:12
theorem :: BINARITH:13
theorem :: BINARITH:14
theorem :: BINARITH:15
canceled;
theorem :: BINARITH:16
theorem :: BINARITH:17
canceled;
theorem :: BINARITH:18
canceled;
theorem :: BINARITH:19
theorem :: BINARITH:20
theorem :: BINARITH:21
theorem :: BINARITH:22
canceled;
theorem :: BINARITH:23
canceled;
theorem :: BINARITH:24
canceled;
theorem :: BINARITH:25
canceled;
theorem :: BINARITH:26
canceled;
theorem :: BINARITH:27
canceled;
theorem :: BINARITH:28
canceled;
theorem :: BINARITH:29
canceled;
theorem :: BINARITH:30
canceled;
theorem :: BINARITH:31
canceled;
theorem :: BINARITH:32
canceled;
theorem :: BINARITH:33
theorem :: BINARITH:34
canceled;
theorem :: BINARITH:35
canceled;
theorem :: BINARITH:36
canceled;
theorem :: BINARITH:37
canceled;
theorem :: BINARITH:38
canceled;
theorem :: BINARITH:39
canceled;
:: deftheorem BINARITH:def 1 :
canceled;
:: deftheorem BINARITH:def 2 :
canceled;
:: deftheorem BINARITH:def 3 :
canceled;
:: deftheorem defines 'not' BINARITH:def 4 :
:: deftheorem Def5 defines carry BINARITH:def 5 :
definition
let n be
Nat;
let x be
Tuple of
n,
BOOLEAN ;
func Binary x -> Tuple of
n,
NAT means :
Def6:
:: BINARITH:def 6
for
i being
Nat st
i in Seg n holds
it /. i = IFEQ (x /. i),
FALSE ,
0 ,
(2 to_power (i -' 1));
existence
ex b1 being Tuple of n,NAT st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ (x /. i),FALSE ,0 ,(2 to_power (i -' 1))
uniqueness
for b1, b2 being Tuple of n,NAT st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ (x /. i),FALSE ,0 ,(2 to_power (i -' 1)) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ (x /. i),FALSE ,0 ,(2 to_power (i -' 1)) ) holds
b1 = b2
end;
:: deftheorem Def6 defines Binary BINARITH:def 6 :
:: deftheorem defines Absval BINARITH:def 7 :
definition
let n be non
zero Nat;
let x,
y be
Tuple of
n,
BOOLEAN ;
func x + y -> Tuple of
n,
BOOLEAN means :
Def8:
:: BINARITH:def 8
for
i being
Nat st
i in Seg n holds
it /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry x,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' (y /. i)) 'xor' ((carry x,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' (y /. i)) 'xor' ((carry x,y) /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry x,y) /. i) ) holds
b1 = b2
end;
:: deftheorem Def8 defines + BINARITH:def 8 :
:: deftheorem defines add_ovfl BINARITH:def 9 :
:: deftheorem Def10 defines are_summable BINARITH:def 10 :
theorem Th40: :: BINARITH:40
theorem Th41: :: BINARITH:41
theorem Th42: :: BINARITH:42
theorem Th43: :: BINARITH:43
theorem Th44: :: BINARITH:44
theorem Th45: :: BINARITH:45
theorem Th46: :: BINARITH:46
theorem Th47: :: BINARITH:47
theorem :: BINARITH:48