The abstract of the Mizar article:

A Representation of Integers by Binary Arithmetics and Addition of Integers

by

Hisayoshi Kunimune, and

Yatsuka Nakamura

Received January 30, 2003

MML identifier: BINARI_4

[ Mizar article, MML identifier index ]

environ

 vocabulary INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, ABSVALUE,
      BINARITH, BINARI_2, BINARI_3, ARYTM_1, NAT_1, BINARI_4, EUCLID, ARYTM_3,
      FINSEQ_2, FINSEQ_4, FUNCT_1, BOOLE, RELAT_1, VECTSP_1, ZF_LANG, GROUP_1;
 notation INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, BINARITH,
      BINARI_2, BINARI_3, GROUP_1, SERIES_1, NUMBERS, XCMPLX_0, XREAL_0,
      XBOOLE_0, EUCLID, REAL_1, NAT_1, TARSKI, FINSEQ_4, FUNCT_1, RELAT_1,
      VECTSP_1, ZFMISC_1, FINSEQOP, PREPOWER, SUBSET_1;
 constructors BINARITH, BINARI_2, BINARI_3, GROUP_1, SERIES_1, REAL_1, EUCLID,
      FINSEQ_4, FINSEQOP, SEQ_1, PREPOWER, EULER_2, MEMBERED;
 clusters INT_1, BINARITH, MARGREL1, RELSET_1, NAT_1, XREAL_0, MEMBERED;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin :: Preliminaries

reserve n for non empty Nat,
        j,k,l,m for Nat,
        g,h,i for Integer;

theorem :: BINARI_4:1
  m > 0 implies m * 2 >= m + 1;

theorem :: BINARI_4:2
  for m being Nat holds 2 to_power m >= m;

theorem :: BINARI_4:3
    for m be Nat holds 0*m + 0*m = 0*m;

theorem :: BINARI_4:4
  for k be Nat holds
   k <= l & l <= m implies k = l or (k + 1 <= l & l <= m);

theorem :: BINARI_4:5
  for n be non empty Nat holds
   for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n
     holds carry(x,y) = 0*n;

theorem :: BINARI_4:6
    for n be non empty Nat holds
   for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds x + y = 0*n;

theorem :: BINARI_4:7
    for n be non empty Nat
  for F be Tuple of n,BOOLEAN st F = 0*n holds
   Intval F = 0;

theorem :: BINARI_4:8
  l + m <= k - 1 implies l < k & m < k;

theorem :: BINARI_4:9
  g <= h + i & h < 0 & i < 0 implies g < h & g < i;

theorem :: BINARI_4:10
  l + m <= 2 to_power n - 1 implies
   add_ovfl(n-BinarySequence(l),n-BinarySequence(m)) = FALSE;

theorem :: BINARI_4:11
  for n be non empty Nat, l,m be Nat st
  l + m <= 2 to_power n - 1 holds
  Absval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m;

theorem :: BINARI_4:12
  for n be non empty Nat holds
   (for z be Tuple of n,BOOLEAN st z/.n = TRUE holds
    Absval(z) >= 2 to_power (n-'1));

theorem :: BINARI_4:13
  l + m <= 2 to_power (n-'1) - 1 implies
   carry(n-BinarySequence(l),n-BinarySequence(m))/.n = FALSE;

theorem :: BINARI_4:14
  for n be non empty Nat st l + m <= 2 to_power (n-'1) - 1 holds
   Intval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m;

theorem :: BINARI_4:15
  for z be Tuple of 1,BOOLEAN st z=<*TRUE*> holds
   Intval(z) = -1;

theorem :: BINARI_4:16
    for z be Tuple of 1,BOOLEAN st z=<*FALSE*> holds
   Intval(z) = 0;

theorem :: BINARI_4:17
  for x be boolean set holds
   TRUE 'or' x = TRUE;

theorem :: BINARI_4:18
    for n be non empty Nat holds 0 <= 2 to_power (n-'1) - 1 &
      -(2 to_power (n-'1)) <= 0;

theorem :: BINARI_4:19
    for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds
   x,y are_summable;

theorem :: BINARI_4:20
  (i*n) mod n = 0;

begin :: Majorant Power

definition
  let m, j be Nat;
  func MajP(m, j) -> Nat means
:: BINARI_4:def 1

  2 to_power it >= j & it >= m &
    for k be Nat st 2 to_power k >= j & k >= m holds
      k >= it;
end;

theorem :: BINARI_4:21
    j >= k implies MajP(m, j) >= MajP(m, k);

theorem :: BINARI_4:22
  l >= m implies MajP(l,j) >= MajP(m,j);

theorem :: BINARI_4:23
    m >= 1 implies MajP(m, 1) = m;

theorem :: BINARI_4:24
  j <= 2 to_power m implies MajP(m, j) = m;

theorem :: BINARI_4:25
    j > 2 to_power m implies MajP(m, j) > m;

begin :: 2's Complement

definition
  let m be Nat;
  let i be Integer;
  func 2sComplement( m, i ) -> Tuple of m, BOOLEAN equals
:: BINARI_4:def 2

    m-BinarySequence( abs( (2 to_power MajP(m,abs(i))) + i ) ) if i < 0
    otherwise
    m-BinarySequence( abs(i) );
end;

theorem :: BINARI_4:26
    for m be Nat holds 2sComplement(m,0) = 0*m;

theorem :: BINARI_4:27
    for i be Integer st i <= 2 to_power (n-'1) - 1 &
   -(2 to_power (n-'1)) <= i holds
   Intval( 2sComplement( n, i ) ) = i;

theorem :: BINARI_4:28
    for h,i be 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);

theorem :: BINARI_4:29
    for h,i be 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);

theorem :: BINARI_4:30
  for l,m be Nat st l mod 2 to_power n = m mod 2 to_power n holds
    n-BinarySequence(l) = n-BinarySequence(m);

theorem :: BINARI_4:31
    for l,m be Nat st l,m are_congruent_mod 2 to_power n holds
    n-BinarySequence(l) = n-BinarySequence(m);

theorem :: BINARI_4:32
 for j be Nat st 1 <= j & j <= n holds
  2sComplement(n+1,i)/.j = 2sComplement(n,i)/.j;

theorem :: BINARI_4:33
  ex x be Element of BOOLEAN st
   2sComplement(m+1,i) = 2sComplement(m,i)^<*x*>;

theorem :: BINARI_4:34
    ex x be Element of BOOLEAN st
   (m+1)-BinarySequence(l) = (m-BinarySequence(l))^<*x*>;

theorem :: BINARI_4:35
  for n be non empty Nat holds
   -2 to_power n <= h+i & h < 0 & i < 0 &
   -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i implies
   carry(2sComplement(n+1,h),2sComplement(n+1,i))/.(n+1) = TRUE;

theorem :: BINARI_4:36
    for n be non empty Nat st
   -(2 to_power (n-'1)) <= h + i & h + i <= 2 to_power (n-'1) - 1 &
     h >= 0 & i >= 0 holds
      Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i;

theorem :: BINARI_4:37
    for n be non empty Nat st
   -2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
   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;

theorem :: BINARI_4:38
    for n be non empty Nat holds
   -(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)) implies
      Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i;