The abstract of the Mizar article:

Binary Arithmetics. Binary Sequences

by

Robert Milewski

Received February 24, 1998

MML identifier: BINARI_3

[ Mizar article, MML identifier index ]

environ

 vocabulary MIDSP_3, MARGREL1, BINARITH, POWER, FINSEQ_1, CQC_LANG, FINSEQ_5,
      EUCLID, FINSEQ_2, ZF_LANG, FUNCT_1, ARYTM_1, RELAT_1, BINARI_2, NAT_1,
      ARYTM_3, MATRIX_2, BINARI_3, FINSEQ_4, REALSET1;
 notation SUBSET_1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, POWER, ABIAN, SERIES_1,
      MARGREL1, FUNCT_1, CQC_LANG, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQOP,
      REALSET1, BINARITH, BINARI_2, EUCLID, MIDSP_3;
 constructors REAL_1, ABIAN, SERIES_1, FINSEQ_5, FINSEQOP, BINARITH, BINARI_2,
      EUCLID, FINSEQ_4, REALSET1, MEMBERED;
 clusters RELSET_1, NAT_2, MARGREL1, REALSET1, NAT_1, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Binary Arithmetics

  theorem :: BINARI_3:1
   for n be non empty Nat
   for F be Tuple of n,BOOLEAN holds
    Absval F < 2 to_power n;

  theorem :: BINARI_3:2
   for n be non empty Nat
   for F1,F2 be Tuple of n,BOOLEAN st Absval F1 = Absval F2 holds
    F1 = F2;

  theorem :: BINARI_3:3
     for t1,t2 be FinSequence st Rev t1 = Rev t2 holds t1 = t2;

  theorem :: BINARI_3:4
   for n be Nat holds
    0*(n + 1) = 0*n ^ <* 0 *>;

  theorem :: BINARI_3:5
   for n be Nat holds
    0*n in BOOLEAN*;

  theorem :: BINARI_3:6
   for n be Nat
   for y be Tuple of n,BOOLEAN st y = 0*n holds
    'not' y = n |-> 1;

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

  theorem :: BINARI_3:8
     for n be non empty Nat
   for F be Tuple of n,BOOLEAN st F = 0*n holds
    Absval 'not' F = 2 to_power n - 1;

  theorem :: BINARI_3:9
     for n be Nat holds Rev (0*n) = 0*n;

  theorem :: BINARI_3:10
     for n be Nat
   for y be Tuple of n,BOOLEAN st y = 0*n holds
    Rev 'not' y = 'not' y;

  theorem :: BINARI_3:11
   Bin1 1 = <*TRUE*>;

  theorem :: BINARI_3:12
   for n be non empty Nat holds Absval (Bin1 n) = 1;

  theorem :: BINARI_3:13
   for x,y be Element of BOOLEAN holds
    (x 'or' y = TRUE iff x = TRUE or y = TRUE) &
    (x 'or' y = FALSE iff x = FALSE & y = FALSE);

  theorem :: BINARI_3:14
   for x,y be Element of BOOLEAN holds
    add_ovfl(<*x*>,<*y*>) = TRUE iff x = TRUE & y = TRUE;

  theorem :: BINARI_3:15
   'not' <*FALSE*> = <*TRUE*>;

  theorem :: BINARI_3:16
     'not' <*TRUE*> = <*FALSE*>;

  theorem :: BINARI_3:17
     <*FALSE*> + <*FALSE*> = <*FALSE*>;

  theorem :: BINARI_3:18
   <*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE*>;

  theorem :: BINARI_3:19
     <*TRUE*> + <*TRUE*> = <*FALSE*>;

  theorem :: BINARI_3:20
   for n be non empty Nat
   for x,y be Tuple of n,BOOLEAN st
    x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds
     for k be non empty Nat st k <> 1 & k <= n holds
      x/.k = TRUE & (carry(x,Bin1 n))/.k = TRUE;

  theorem :: BINARI_3:21
   for n be non empty Nat
   for x be Tuple of n,BOOLEAN st
    x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds
     carry(x,Bin1 n) = 'not' Bin1 n;

  theorem :: BINARI_3:22
   for n be non empty Nat
   for x,y be Tuple of n,BOOLEAN st
    y = 0*n & x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds
     x = 'not' y;

  theorem :: BINARI_3:23
   for n be non empty Nat
   for y be Tuple of n,BOOLEAN st y = 0*n holds
    carry('not' y,Bin1 n) = 'not' Bin1 n;

  theorem :: BINARI_3:24
   for n be non empty Nat
   for x,y be Tuple of n,BOOLEAN st y = 0*n holds
    add_ovfl(x,Bin1 n) = TRUE iff x = 'not' y;

  theorem :: BINARI_3:25
   for n be non empty Nat
   for z be Tuple of n,BOOLEAN st z = 0*n holds
    'not' z + Bin1 n = z;

begin :: Binary Sequences

  definition
   let n,k be Nat;
   func n-BinarySequence k -> Tuple of n,BOOLEAN means
:: BINARI_3:def 1
    for i be Nat st i in Seg n holds
     it/.i = IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE);
  end;

  theorem :: BINARI_3:26
   for n be Nat holds n-BinarySequence 0 = 0*n;

  theorem :: BINARI_3:27
   for n,k be Nat st k < 2 to_power n holds
    ((n+1)-BinarySequence k).(n+1) = FALSE;

  theorem :: BINARI_3:28
   for n be non empty Nat
   for k be Nat st k < 2 to_power n holds
    (n+1)-BinarySequence k = (n-BinarySequence k)^<*FALSE*>;

  theorem :: BINARI_3:29
   for n be non empty Nat holds
    (n+1)-BinarySequence 2 to_power n = 0*n^<*TRUE*>;

  theorem :: BINARI_3:30
   for n be non empty Nat
   for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds
    ((n+1)-BinarySequence k).(n+1) = TRUE;

  theorem :: BINARI_3:31
   for n be non empty Nat
   for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds
    (n+1)-BinarySequence k = (n-BinarySequence (k -' 2 to_power n))^<*TRUE*>;

  theorem :: BINARI_3:32
   for n be non empty Nat
   for k be Nat st k < 2 to_power n
   for x be Tuple of n,BOOLEAN st x = 0*n holds
    n-BinarySequence k = 'not' x iff k = 2 to_power n - 1;

  theorem :: BINARI_3:33
   for n be non empty Nat
   for k be Nat st k + 1 < 2 to_power n holds
    add_ovfl(n-BinarySequence k,Bin1 n) = FALSE;

  theorem :: BINARI_3:34
   for n be non empty Nat
   for k be Nat st k + 1 < 2 to_power n holds
    n-BinarySequence (k+1) = n-BinarySequence k + Bin1 n;

  theorem :: BINARI_3:35
     for n,i be Nat holds
    (n+1)-BinarySequence i = <*i mod 2*> ^ (n-BinarySequence (i div 2));

  theorem :: BINARI_3:36
   for n be non empty Nat
   for k be Nat holds k < 2 to_power n implies
   Absval (n-BinarySequence k) = k;

  theorem :: BINARI_3:37
     for n be non empty Nat
   for x be Tuple of n,BOOLEAN holds
    n-BinarySequence (Absval x) = x;