[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 bitopsaux
enrich
   int-pot
, 
   bitlista
with
   

   
   
   functions  bitsinvert : bitlist → bitlist;
              . +1 : bitlist → bitlist;
             comment: add one to bitlist;
              sgn : bitlist → bitlist;
             comment: delete leading 0/1s;
              fillsgn : nat × bitlist → bitlist;
             comment: add leading 0/1s;
              fix : nat × bitlist → bitlist;
             comment: make bits exactly n long.;
   
   
   
   
   

   

   axioms invert-base :  ⊦ bitsinvert([]) = [];
          used for: s, ls;
          invert-zero :  ⊦ bitsinvert(false ' + bits) = true + bitsinvert(bits);
          used for: s, ls;
          invert-one :  ⊦ bitsinvert(true ' + bits) = false + bitsinvert(bits);
          used for: s, ls;
          succ-empty :  ⊦ [] +1 = true ';
          used for: s, ls;
          succ-zero :  ⊦ (bits + false ')+1 = bits + true;
          used for: s, ls;
          succ-rec :  ⊦ (bits + true ')+1 = bits +1 + false;
          used for: s, ls;
          sgn-empty :  ⊦ sgn([]) = [];
          used for: s, ls;
          sgn-one :  ⊦ sgn(boolvar ') = boolvar ';
          used for: s, ls;
          sgn-base :  ⊦ sgn(boolvar ' + (¬ boolvar)' + bits) = boolvar ' + (¬ boolvar)' + bits;
          used for: s, ls;
          sgn-rec :  ⊦ sgn(boolvar ' + boolvar ' + bits) = sgn(boolvar ' + bits);
          used for: s, ls;
          fillsgn-longer :  ⊦ n ≤ # bits → fillsgn(n, bits) = bits;
          used for: s, ls;
          fillsgn-empty :  ⊦ fillsgn(n, []) = mklist(false, n);
          used for: s, ls;
          fillsgn-fill :  ⊦ # bits < n → fillsgn(n, boolvar ' + bits) = mklist(boolvar, n - # bits) + bits;
          used for: s, ls;
          fix-longer :  ⊦ n < # bits → fix(n, bits) = lastn(n, bits);
          fix-shorter :  ⊦ ¬ n < # bits → fix(n, bits) = fillsgn(n, bits);
          used for: s, ls;

   

   
end enrich