:: A Representation of Integers by Binary Arithmetics and Addition of Integers :: by Hisayoshi Kunimune and Yatsuka Nakamura :: :: Received January 30, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin theorem Th1: :: BINARI_4:1 for m being Nat st m > 0 holds m * 2 >= m + 1 proofend; theorem Th2: :: BINARI_4:2 for m being Nat holds 2 to_power m >= m proofend; theorem :: BINARI_4:3 for m being Nat holds (0* m) + (0* m) = 0* m proofend; theorem Th4: :: BINARI_4:4 for k, m, l being Nat st k <= l & l <= m & not k = l holds ( k + 1 <= l & l <= m ) proofend; theorem Th5: :: BINARI_4:5 for n being non empty Nat for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds carry (x,y) = 0* n proofend; theorem :: BINARI_4:6 for n being non empty Nat for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds x + y = 0* n proofend; theorem :: BINARI_4:7 for n being non empty Nat for F being Tuple of n, BOOLEAN st F = 0* n holds Intval F = 0 proofend; theorem Th8: :: BINARI_4:8 for l, m, k being Nat st l + m <= k - 1 holds ( l < k & m < k ) proofend; theorem Th9: :: BINARI_4:9 for g, h, i being Integer st g <= h + i & h < 0 & i < 0 holds ( g < h & g < i ) proofend; theorem Th10: :: BINARI_4:10 for n being non empty Nat for l, m being Nat st l + m <= (2 to_power n) - 1 holds add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE proofend; theorem Th11: :: BINARI_4:11 for n being non empty Nat for l, m being Nat st l + m <= (2 to_power n) - 1 holds Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m proofend; theorem Th12: :: BINARI_4:12 for n being non empty Nat for z being Tuple of n, BOOLEAN st z /. n = TRUE holds Absval z >= 2 to_power (n -' 1) proofend; theorem Th13: :: BINARI_4:13 for n being non empty 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 proofend; theorem Th14: :: BINARI_4:14 for l, m being Nat for n being non empty Nat st l + m <= (2 to_power (n -' 1)) - 1 holds Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m proofend; theorem Th15: :: BINARI_4:15 for z being Tuple of 1, BOOLEAN st z = <*TRUE*> holds Intval z = - 1 proofend; theorem :: BINARI_4:16 for z being Tuple of 1, BOOLEAN st z = <*FALSE*> holds Intval z = 0 proofend; theorem :: BINARI_4:17 for x being boolean set holds TRUE 'or' x = TRUE ; theorem :: BINARI_4:18 for n being non empty Nat holds ( 0 <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= 0 ) proofend; theorem :: BINARI_4:19 for n being non empty Nat for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds x,y are_summable proofend; theorem Th20: :: BINARI_4:20 for n being non empty Nat for i being Integer holds (i * n) mod n = 0 proofend; begin definition let m, j be Nat; 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 ex b1 being Nat st ( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds k >= b1 ) ) proofend; uniqueness for b1, b2 being Nat st 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds k >= b1 ) & 2 to_power b2 >= j & b2 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds k >= b2 ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines MajP BINARI_4:def_1_:_ for m, j, b3 being Nat holds ( b3 = MajP (m,j) iff ( 2 to_power b3 >= j & b3 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds k >= b3 ) ) ); theorem :: BINARI_4:21 for j, k, m being Nat st j >= k holds MajP (m,j) >= MajP (m,k) proofend; theorem Th22: :: BINARI_4:22 for l, m, j being Nat st l >= m holds MajP (l,j) >= MajP (m,j) proofend; theorem :: BINARI_4:23 for m being Nat st m >= 1 holds MajP (m,1) = m proofend; theorem Th24: :: BINARI_4:24 for j, m being Nat st j <= 2 to_power m holds MajP (m,j) = m proofend; theorem :: BINARI_4:25 for j, m being Nat st j > 2 to_power m holds MajP (m,j) > m proofend; begin definition let m be Nat; let i be Integer; func 2sComplement (m,i) -> Tuple of m, BOOLEAN equals :Def2: :: BINARI_4:def 2 m -BinarySequence (abs ((2 to_power (MajP (m,(abs i)))) + i)) if i < 0 otherwise m -BinarySequence (abs i); correctness coherence ( ( i < 0 implies m -BinarySequence (abs ((2 to_power (MajP (m,(abs i)))) + i)) is Tuple of m, BOOLEAN ) & ( not i < 0 implies m -BinarySequence (abs i) is Tuple of m, BOOLEAN ) ); consistency for b1 being Tuple of m, BOOLEAN holds verum; ; end; :: 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 (abs ((2 to_power (MajP (m,(abs i)))) + i)) ) & ( not i < 0 implies 2sComplement (m,i) = m -BinarySequence (abs i) ) ); theorem :: BINARI_4:26 for m being Nat holds 2sComplement (m,0) = 0* m proofend; theorem :: BINARI_4:27 for n being non empty 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 proofend; Lm1: for n being non empty 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) proofend; Lm2: for n being non empty Nat for k, l being Nat st k mod n = l mod n holds ex s being Integer st k = l + (s * n) proofend; Lm3: for n being non empty 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 proofend; Lm4: for n being non empty 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,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n) proofend; Lm5: for n being non empty 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) proofend; Lm6: for n being non empty 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) proofend; theorem :: BINARI_4:28 for n being non empty Nat for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h mod (2 to_power n) = i mod (2 to_power n) holds 2sComplement (n,h) = 2sComplement (n,i) by Lm5, Lm6; theorem :: BINARI_4:29 for n being non empty 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) proofend; theorem Th30: :: BINARI_4:30 for n being non empty 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 proofend; theorem :: BINARI_4:31 for n being non empty Nat for l, m being Nat st l,m are_congruent_mod 2 to_power n holds n -BinarySequence l = n -BinarySequence m proofend; theorem Th32: :: BINARI_4:32 for n being non empty Nat for i being Integer for j being Nat st 1 <= j & j <= n holds (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j proofend; 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*> proofend; theorem :: BINARI_4:34 for m, l being Nat ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*> proofend; theorem Th35: :: BINARI_4:35 for h, i being Integer for n being non empty 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 proofend; theorem :: BINARI_4:36 for h, i being Integer for n being non empty Nat st h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i proofend; theorem :: BINARI_4:37 for h, i being Integer for n being non empty 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 proofend; theorem :: BINARI_4:38 for h, i being Integer for n being non empty 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 proofend;