:: by Takaya Nishiyama and Yasuho Mizuhara

::

:: Received October 8, 1993

:: Copyright (c) 1993-2019 Association of Mizar Users

theorem Th1: :: BINARITH:1

for i, n being Nat

for D being non empty set

for d being Element of D

for z being Tuple of n,D st i in Seg n holds

(z ^ <*d*>) /. i = z /. i

for D being non empty set

for d being Element of D

for z being Tuple of n,D st i in Seg n holds

(z ^ <*d*>) /. i = z /. i

proof end;

theorem Th2: :: BINARITH:2

for n being Nat

for D being non empty set

for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

for D being non empty set

for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

proof end;

definition

let x, y be Element of BOOLEAN ;

:: original: 'or'

redefine func x 'or' y -> Element of BOOLEAN ;

correctness

coherence

x 'or' y is Element of BOOLEAN ;

redefine func x 'xor' y -> Element of BOOLEAN ;

correctness

coherence

x 'xor' y is Element of BOOLEAN ;

end;
:: original: 'or'

redefine func x 'or' y -> Element of BOOLEAN ;

correctness

coherence

x 'or' y is Element of BOOLEAN ;

proof end;

:: original: 'xor'redefine func x 'xor' y -> Element of BOOLEAN ;

correctness

coherence

x 'xor' y is Element of BOOLEAN ;

proof end;

theorem :: BINARITH:4

theorem :: BINARITH:5

theorem :: BINARITH:6

theorem :: BINARITH:11

definition

let n be Nat;

let x be Tuple of n, BOOLEAN ;

ex b_{1} being Tuple of n, BOOLEAN st

for i being Nat st i in Seg n holds

b_{1} /. i = 'not' (x /. i)

for b_{1}, b_{2} being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds

b_{1} /. i = 'not' (x /. i) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = 'not' (x /. i) ) holds

b_{1} = b_{2}

end;
let x be Tuple of n, BOOLEAN ;

func 'not' x -> Tuple of n, BOOLEAN means :: BINARITH:def 1

for i being Nat st i in Seg n holds

it /. i = 'not' (x /. i);

existence for i being Nat st i in Seg n holds

it /. i = 'not' (x /. i);

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines 'not' BINARITH:def 1 :

for n being Nat

for x, b_{3} being Tuple of n, BOOLEAN holds

( b_{3} = 'not' x iff for i being Nat st i in Seg n holds

b_{3} /. i = 'not' (x /. i) );

for n being Nat

for x, b

( b

b

definition

let n be non zero Nat;

let x, y be Tuple of n, BOOLEAN ;

ex b_{1} being Tuple of n, BOOLEAN st

( b_{1} /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

b_{1} /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b_{1} /. i))) 'or' ((y /. i) '&' (b_{1} /. i)) ) )

for b_{1}, b_{2} being Tuple of n, BOOLEAN st b_{1} /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

b_{1} /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b_{1} /. i))) 'or' ((y /. i) '&' (b_{1} /. i)) ) & b_{2} /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

b_{2} /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b_{2} /. i))) 'or' ((y /. i) '&' (b_{2} /. i)) ) holds

b_{1} = b_{2}

end;
let x, y be Tuple of n, BOOLEAN ;

func carry (x,y) -> Tuple of n, BOOLEAN means :Def2: :: BINARITH:def 2

( it /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

it /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (it /. i))) 'or' ((y /. i) '&' (it /. i)) ) );

existence ( it /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

it /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (it /. i))) 'or' ((y /. i) '&' (it /. i)) ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines carry BINARITH:def 2 :

for n being non zero Nat

for x, y, b_{4} being Tuple of n, BOOLEAN holds

( b_{4} = carry (x,y) iff ( b_{4} /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds

b_{4} /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b_{4} /. i))) 'or' ((y /. i) '&' (b_{4} /. i)) ) ) );

for n being non zero Nat

for x, y, b

( b

b

definition

let n be Nat;

let x be Tuple of n, BOOLEAN ;

ex b_{1} being Tuple of n, NAT st

for i being Nat st i in Seg n holds

b_{1} /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)))

for b_{1}, b_{2} being Tuple of n, NAT st ( for i being Nat st i in Seg n holds

b_{1} /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) holds

b_{1} = b_{2}

end;
let x be Tuple of n, BOOLEAN ;

func Binary x -> Tuple of n, NAT means :Def3: :: BINARITH:def 3

for i being Nat st i in Seg n holds

it /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)));

existence for i being Nat st i in Seg n holds

it /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)));

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Binary BINARITH:def 3 :

for n being Nat

for x being Tuple of n, BOOLEAN

for b_{3} being Tuple of n, NAT holds

( b_{3} = Binary x iff for i being Nat st i in Seg n holds

b_{3} /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) );

for n being Nat

for x being Tuple of n, BOOLEAN

for b

( b

b

definition

let n be Nat;

let x be Tuple of n, BOOLEAN ;

correctness

coherence

addnat $$ (Binary x) is Element of NAT ;

;

end;
let x be Tuple of n, BOOLEAN ;

correctness

coherence

addnat $$ (Binary x) is Element of NAT ;

;

:: deftheorem defines Absval BINARITH:def 4 :

for n being Nat

for x being Tuple of n, BOOLEAN holds Absval x = addnat $$ (Binary x);

for n being Nat

for x being Tuple of n, BOOLEAN holds Absval x = addnat $$ (Binary x);

definition

let n be non zero Nat;

let x, y be Tuple of n, BOOLEAN ;

ex b_{1} being Tuple of n, BOOLEAN st

for i being Nat st i in Seg n holds

b_{1} /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i)

for b_{1}, b_{2} being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds

b_{1} /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) ) holds

b_{1} = b_{2}

end;
let x, y be Tuple of n, BOOLEAN ;

func x + y -> Tuple of n, BOOLEAN means :Def5: :: BINARITH:def 5

for i being Nat st i in Seg n holds

it /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i);

existence for i being Nat st i in Seg n holds

it /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i);

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines + BINARITH:def 5 :

for n being non zero Nat

for x, y, b_{4} being Tuple of n, BOOLEAN holds

( b_{4} = x + y iff for i being Nat st i in Seg n holds

b_{4} /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) );

for n being non zero Nat

for x, y, b

( b

b

definition

let n be non zero Nat;

let z1, z2 be Tuple of n, BOOLEAN ;

coherence

(((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n)) is Element of BOOLEAN ;

;

end;
let z1, z2 be Tuple of n, BOOLEAN ;

func add_ovfl (z1,z2) -> Element of BOOLEAN equals :: BINARITH:def 6

(((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));

correctness (((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));

coherence

(((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n)) is Element of BOOLEAN ;

;

:: deftheorem defines add_ovfl BINARITH:def 6 :

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN holds add_ovfl (z1,z2) = (((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN holds add_ovfl (z1,z2) = (((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));

:: deftheorem defines are_summable BINARITH:def 7 :

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN holds

( z1,z2 are_summable iff add_ovfl (z1,z2) = FALSE );

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN holds

( z1,z2 are_summable iff add_ovfl (z1,z2) = FALSE );

definition

let n1, n2 be Nat;

let D be non empty set ;

let z1 be Tuple of n1,D;

let z2 be Tuple of n2,D;

:: original: ^

redefine func z1 ^ z2 -> Tuple of n1 + n2,D;

coherence

z1 ^ z2 is Tuple of n1 + n2,D by FINSEQ_2:107;

end;
let D be non empty set ;

let z1 be Tuple of n1,D;

let z2 be Tuple of n2,D;

:: original: ^

redefine func z1 ^ z2 -> Tuple of n1 + n2,D;

coherence

z1 ^ z2 is Tuple of n1 + n2,D by FINSEQ_2:107;

definition

let D be non empty set ;

let d be Element of D;

:: original: <*

redefine func <*d*> -> Tuple of 1,D;

coherence

<*d*> is Tuple of 1,D

end;
let d be Element of D;

:: original: <*

redefine func <*d*> -> Tuple of 1,D;

coherence

<*d*> is Tuple of 1,D

proof end;

theorem Th17: :: BINARITH:17

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN

for i being Nat st i in Seg n holds

(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN

for i being Nat st i in Seg n holds

(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i

proof end;

theorem Th18: :: BINARITH:18

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN holds add_ovfl (z1,z2) = (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1)

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN holds add_ovfl (z1,z2) = (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1)

proof end;

theorem Th19: :: BINARITH:19

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>

for z1, z2 being Tuple of n, BOOLEAN

for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>

proof end;

theorem Th20: :: BINARITH:20

for n being non zero Nat

for z being Tuple of n, BOOLEAN

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

for z being Tuple of n, BOOLEAN

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

proof end;

theorem Th21: :: BINARITH:21

for n being non zero Nat

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)

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)

proof end;

theorem :: BINARITH:22

for n being non zero Nat

for z1, z2 being Tuple of n, BOOLEAN st z1,z2 are_summable holds

Absval (z1 + z2) = (Absval z1) + (Absval z2)

for z1, z2 being Tuple of n, BOOLEAN st z1,z2 are_summable holds

Absval (z1 + z2) = (Absval z1) + (Absval z2)

proof end;