[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification int2bits
enrich
   bitopsaux
with
   

   
   
   functions  int2bits : int → bitlist;
             comment: convert int to bits, the list is in correct
                  order, i.e. first is most significant bit. Positive integers have
                  a leading 0 (= false), negative a leading 1 (= true). 0 = (false).
                  Negative integers are represented by two's complement,
                  i.e. bit complement + 1.
                    Legal bitlists for an integer are:
                        0 for 0
                    01... for positive ints
                    10... for negative numbers
                   ;
              uint2bits : int → bitlist;
             comment: positive integer to positive bits (with leading 0);
              bits2int : bitlist → int;
             comment: (nonempty) bitlist to int depending on sign;
              bits2uint : bitlist → int;
             comment: arbitrary (nonempty) bitlist to positive integer;
   
   
   
   
   

   

   axioms int2bits-pos :  ⊦ 0 ≤ i → int2bits(i) = uint2bits(i);
          int2bits-neg :  ⊦ i < 0 → int2bits(i) = sgn(bitsinvert(uint2bits(abs(i))) +1);
          uint2bits-zero :  ⊦ uint2bits(0) = false ';
          used for: s, ls;
          uint2bits-one :  ⊦ uint2bits(1) = false + true;
          used for: s, ls;
          uint2bits-rec :  ⊦ 1 < i → uint2bits(i) = uint2bits(i / 2) + (i % 2 = 1);
          bits2int-base :  ⊦ bits2int([]) = 0;
          used for: s, ls;
          bits2int-pos :  ⊦ bits2int(false ' + bits) = bits2uint(bits);
          used for: s, ls;
          bits2int-neg :  ⊦ bits2int(true ' + bits) = ~ bits2uint(bitsinvert(true + bits) +1);
          used for: s, ls;
          bits2uint-base :  ⊦ bits2uint([]) = 0;
          used for: s, ls;
          bits2uint-zero :  ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2;
          used for: s, ls;
          bits2uint-one :  ⊦ bits2uint(bits + true ') = bits2uint(bits) * 2 + 1;
          used for: s, ls;

   

   
end enrich