begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
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:
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:
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:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem