Specification int-pair

[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
   nat-pair
with
   

   
   
   functions  . × . : int × int → int;
             comment: encode arbitrary pairs of integers (bijective).;
              encode : int → nat;
             comment: encode positive and negative integers (bijective).;
              decode : nat → int;
              encode : nat → int;
             comment: encode nats as all integers (bijective).;
              decode : int → nat;
              . .1 : int → int;
             comment: (i × j).1 = i;
              . .2 : int → int;
             comment: (i × j).2 = j;
   
   
   
   
   

   

   axioms enc-int-pos :  ⊦ 0 ≤ i → encode(i) = 2 * i→n(i);
          used for: ls;
          enc-int-neg :  ⊦ i < 0 → encode(i) = 2 * i→n(i) - 1;
          used for: ls;
          enc-nat-pos :  ⊦ n % 2 = 0 → encode(n) = n→i(n / 2);
          used for: ls;
          enc-nat-neg :  ⊦ n % 2 ≠ 0 → encode(n) = ~ n→i((n + 1) / 2);
          used for: ls;
          encode-pair :  ⊦ i × j = encode(encode(encode(i), encode(j)));
          used for: ls;
          dec-int-pos :  ⊦ n % 2 = 0 → decode(n) = n→i(n / 2);
          used for: ls;
          dec-int-neg :  ⊦ n % 2 ≠ 0 → decode(n) = ~ n→i((n + 1) / 2);
          used for: ls;
          dec-nat-pos :  ⊦ 0 ≤ i → decode(i) = 2 * i→n(i);
          used for: ls;
          dec-nat-neg :  ⊦ i < 0 → decode(i) = 2 * i→n(i) - 1;
          used for: ls;
          dec-fst :  ⊦ i.1 = decode(decode(i).1);
          used for: ls;
          dec-snd :  ⊦ i.2 = decode(decode(i).2);
          used for: ls;

   

   
end enrich