:: by Hisayoshi Kunimune and Yatsuka Nakamura

::

:: Received January 30, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

theorem Th5: :: BINARI_4:5

for n being non zero Nat

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

carry (x,y) = 0* n

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

carry (x,y) = 0* n

proof end;

theorem :: BINARI_4:6

for n being non zero Nat

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

x + y = 0* n

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

x + y = 0* n

proof end;

theorem Th10: :: BINARI_4:10

for n being non zero Nat

for l, m being Nat st l + m <= (2 to_power n) - 1 holds

add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE

for l, m being Nat st l + m <= (2 to_power n) - 1 holds

add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE

proof end;

theorem Th11: :: BINARI_4:11

for n being non zero Nat

for l, m being Nat st l + m <= (2 to_power n) - 1 holds

Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m

for l, m being Nat st l + m <= (2 to_power n) - 1 holds

Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m

proof end;

theorem Th12: :: BINARI_4:12

for n being non zero Nat

for z being Tuple of n, BOOLEAN st z /. n = TRUE holds

Absval z >= 2 to_power (n -' 1)

for z being Tuple of n, BOOLEAN st z /. n = TRUE holds

Absval z >= 2 to_power (n -' 1)

proof end;

theorem Th13: :: BINARI_4:13

for n being non zero Nat

for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds

(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE

for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds

(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE

proof end;

theorem Th14: :: BINARI_4:14

for l, m being Nat

for n being non zero Nat st l + m <= (2 to_power (n -' 1)) - 1 holds

Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m

for n being non zero Nat st l + m <= (2 to_power (n -' 1)) - 1 holds

Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m

proof end;

theorem :: BINARI_4:19

for n being non zero Nat

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

x,y are_summable

for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds

x,y are_summable

proof end;

definition

let m, j be Nat;

ex b_{1} being Nat st

( 2 to_power b_{1} >= j & b_{1} >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= b_{1} ) )

for b_{1}, b_{2} being Nat st 2 to_power b_{1} >= j & b_{1} >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= b_{1} ) & 2 to_power b_{2} >= j & b_{2} >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= b_{2} ) holds

b_{1} = b_{2}

end;
func MajP (m,j) -> Nat means :Def1: :: BINARI_4:def 1

( 2 to_power it >= j & it >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= it ) );

existence ( 2 to_power it >= j & it >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= it ) );

ex b

( 2 to_power b

k >= b

proof end;

uniqueness for b

k >= b

k >= b

b

proof end;

:: deftheorem Def1 defines MajP BINARI_4:def 1 :

for m, j, b_{3} being Nat holds

( b_{3} = MajP (m,j) iff ( 2 to_power b_{3} >= j & b_{3} >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds

k >= b_{3} ) ) );

for m, j, b

( b

k >= b

definition

let m be Nat;

let i be Integer;

coherence

( ( i < 0 implies m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| is Tuple of m, BOOLEAN ) & ( not i < 0 implies m -BinarySequence |.i.| is Tuple of m, BOOLEAN ) );

consistency

for b_{1} being Tuple of m, BOOLEAN holds verum;

;

end;
let i be Integer;

func 2sComplement (m,i) -> Tuple of m, BOOLEAN equals :Def2: :: BINARI_4:def 2

m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| if i < 0

otherwise m -BinarySequence |.i.|;

correctness m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| if i < 0

otherwise m -BinarySequence |.i.|;

coherence

( ( i < 0 implies m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| is Tuple of m, BOOLEAN ) & ( not i < 0 implies m -BinarySequence |.i.| is Tuple of m, BOOLEAN ) );

consistency

for b

;

:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :

for m being Nat

for i being Integer holds

( ( i < 0 implies 2sComplement (m,i) = m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| ) & ( not i < 0 implies 2sComplement (m,i) = m -BinarySequence |.i.| ) );

for m being Nat

for i being Integer holds

( ( i < 0 implies 2sComplement (m,i) = m -BinarySequence |.((2 to_power (MajP (m,|.i.|))) + i).| ) & ( not i < 0 implies 2sComplement (m,i) = m -BinarySequence |.i.| ) );

theorem :: BINARI_4:27

for n being non zero Nat

for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds

Intval (2sComplement (n,i)) = i

for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds

Intval (2sComplement (n,i)) = i

proof end;

Lm1: for n being non zero Nat

for k, l being Nat st k mod n = l mod n & k > l holds

ex s being Integer st k = l + (s * n)

proof end;

Lm2: for n being non zero Nat

for k, l being Nat st k mod n = l mod n holds

ex s being Integer st k = l + (s * n)

proof end;

Lm3: for n being non zero Nat

for k, l, m being Nat st m < n & k mod (2 to_power n) = l mod (2 to_power n) holds

(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2

proof end;

Lm4: for n being non zero Nat

for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds

((2 to_power (MajP (n,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.i.|))) + i) mod (2 to_power n)

proof end;

Lm5: for n being non zero Nat

for h, i being Integer st h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) holds

2sComplement (n,h) = 2sComplement (n,i)

proof end;

Lm6: for n being non zero Nat

for h, i being Integer st h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) holds

2sComplement (n,h) = 2sComplement (n,i)

proof end;

theorem :: BINARI_4:28

theorem :: BINARI_4:29

for n being non zero Nat

for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds

2sComplement (n,h) = 2sComplement (n,i)

for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds

2sComplement (n,h) = 2sComplement (n,i)

proof end;

theorem Th30: :: BINARI_4:30

for n being non zero Nat

for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds

n -BinarySequence l = n -BinarySequence m

for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds

n -BinarySequence l = n -BinarySequence m

proof end;

theorem :: BINARI_4:31

for n being non zero Nat

for l, m being Nat st l,m are_congruent_mod 2 to_power n holds

n -BinarySequence l = n -BinarySequence m

for l, m being Nat st l,m are_congruent_mod 2 to_power n holds

n -BinarySequence l = n -BinarySequence m

proof end;

theorem Th32: :: BINARI_4:32

for n being non zero Nat

for i being Integer

for j being Nat st 1 <= j & j <= n holds

(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j

for i being Integer

for j being Nat st 1 <= j & j <= n holds

(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j

proof end;

theorem Th33: :: BINARI_4:33

for m being Nat

for i being Integer ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>

for i being Integer ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>

proof end;

theorem :: BINARI_4:34

for l, m being Nat ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>

proof end;

theorem Th35: :: BINARI_4:35

for h, i being Integer

for n being non zero Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds

(carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE

for n being non zero Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds

(carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE

proof end;

theorem :: BINARI_4:36

for h, i being Integer

for n being non zero Nat st h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds

Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i

for n being non zero Nat st h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds

Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i

proof end;

theorem :: BINARI_4:37

for h, i being Integer

for n being non zero Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds

Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i

for n being non zero Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds

Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i

proof end;

theorem :: BINARI_4:38

for h, i being Integer

for n being non zero Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds

Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i

for n being non zero Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds

Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i

proof end;