Specification hexstring

[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,
enrich
   intlista, 
   string-less
, 
   bytes
with
   

   
   
   functions  hexint : intlist → int;
              hex : string → int;
              hexstring : string → intlist;
              hexchar : char → int;
              hexbyte : string → byte;
   
   
   
   
   

   

   axioms hex-def :  ⊦ hex(str) = hexint(hexstring(str));
          hexbyte :  ⊦ hexbyte(str) = i2b(hex(str));
          hexstring-empty :  ⊦ hexstring("") = [];
          used for: s, ls;
          hexstring-rec :  ⊦ hexstring(char + str) = hexchar(char) + hexstring(str);
          used for: s, ls;
          hexint-empty :  ⊦ hexint([]) = 0;
          used for: s, ls;
          hexint-rec :  ⊦ hexint(i ' + ints) = i * 16 ^ n→i(# ints) + hexint(ints);
          used for: s, ls;
          hexchar0 :  ⊦ hexchar('0') = 0;
          used for: s, ls;
          hexchar1 :  ⊦ hexchar('1') = 1;
          used for: s, ls;
          hexchar2 :  ⊦ hexchar('2') = 2;
          used for: s, ls;
          hexchar3 :  ⊦ hexchar('3') = 3;
          used for: s, ls;
          hexchar4 :  ⊦ hexchar('4') = 4;
          used for: s, ls;
          hexchar5 :  ⊦ hexchar('5') = 5;
          used for: s, ls;
          hexchar6 :  ⊦ hexchar('6') = 6;
          used for: s, ls;
          hexchar7 :  ⊦ hexchar('7') = 7;
          used for: s, ls;
          hexchar8 :  ⊦ hexchar('8') = 8;
          used for: s, ls;
          hexchar9 :  ⊦ hexchar('9') = 9;
          used for: s, ls;
          hexchara :  ⊦ hexchar('a') = 10;
          used for: s, ls;
          hexcharb :  ⊦ hexchar('b') = 11;
          used for: s, ls;
          hexcharc :  ⊦ hexchar('c') = 12;
          used for: s, ls;
          hexchard :  ⊦ hexchar('d') = 13;
          used for: s, ls;
          hexchare :  ⊦ hexchar('e') = 14;
          used for: s, ls;
          hexcharf :  ⊦ hexchar('f') = 15;
          used for: s, ls;
          hexcharA :  ⊦ hexchar('A') = 10;
          used for: s, ls;
          hexcharB :  ⊦ hexchar('B') = 11;
          used for: s, ls;
          hexcharC :  ⊦ hexchar('C') = 12;
          used for: s, ls;
          hexcharD :  ⊦ hexchar('D') = 13;
          used for: s, ls;
          hexcharE :  ⊦ hexchar('E') = 14;
          used for: s, ls;
          hexcharF :  ⊦ hexchar('F') = 15;
          used for: s, ls;

   

   
end enrich