[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 nat-pair
enrich
   intnat
with
   functions 
       encode : nat × nat → nat;
       . .1 : nat → nat;
      comment: (i ×pos j).1pos = i, i = maxI - j;
       . .2 : nat → nat;
      comment: (i ×pos j).2pos = j, j = (i ×pos j) - maxI;
       maxenc : nat → nat;
      comment: maxI(i) = s ↔ s is biggest nat with s(s+1)/2 ≤ i;
       maxenc : nat × nat → nat;
      comment: computes maxI with counter as first arg.;
   
   variables 
       m : nat;
       n : nat;
   
   
   axioms 
      encode-def: encode(m, n) = ((m + n) * (m + n + 1)) / 2 + n;
      used for: ls;
      
      dec-fst: m.1 = maxenc(m) - m.2;
      
      dec-snd: m.2 = m - (maxenc(m) * (maxenc(m) + 1)) / 2;
      
      maxi-start: maxenc(n) = maxenc(0, n);
      
      maxi-rec: ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = maxenc(m + 1, n);
      
      maxi-found: ¬ ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = m;
   
   
end enrich