[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 list-last
enrich
   list-dup
with
   

   
   
   functions  . .last : list → elem;
              . .butlast : list → list;
              butlastn : nat × list → list;
             comment: return list except last n elements;
              rev : list → list;
              mklist : elem × nat → list;
             comment: mklist(a, n), return list with n times a.;
              fillfirst : nat × elem × list → list;
   predicates  . ⊑ . : list × list;
              comment: x ⊑ y = x is prefix of y;
               . ⊒ . : list × list;
              comment: x ⊒ y = x is postfix of y;
   
   
   
   

   

   axioms last :  ⊦ x ≠ [] → x.butlast + x.last = x;
          used for: kodkodaxstrong;
          rev-e :  ⊦ rev([]) = [];
          used for: s, ls;
          rev-r :  ⊦ rev(a ' + x) = rev(x) + a;
          used for: s, ls;
          mk-len :  ⊦ # mklist(a, n) = n;
          used for: s, ls, nokodkodax;
          mk-elem :  ⊦ a ∈ mklist(b, n) → a = b;
          used for: f, lf, nokodkodax;
          butlastN-base :  ⊦ butlastn(0, x) = x;
          used for: s, ls;
          butlastN-rec :  ⊦ butlastn(n + 1, x) = butlastn(n, x.butlast);
          used for: s, ls;
          fillfirst-longer :  ⊦ n ≤ # x → fillfirst(n, a, x) = x;
          used for: s, ls;
          fillfirst-fill :  ⊦ # x < n → fillfirst(n, a, x) = mklist(a, n - # x) + x;
          prefix :  ⊦ x ⊑ y ↔ (∃ z. x + z = y);
          used for: ls;
          postfix :  ⊦ x ⊒ y ↔ (∃ z. z + x = y);
          used for: ls;

   

   
end enrich