[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-prefixn
enrich
   list-del

with
   

   
   
   functions  prefixn : nat × list → list;
              dropn : nat × list → list;
              slice : nat × nat × list → list;
   
   
   
   
   

   

   axioms prefixn :  ⊦ prefixn(n, x) = (n ≤ # x ⊃ firstn(n, x);x);
          used for: ls;
          dropn :  ⊦ dropn(n, x) = (n ≤ # x ⊃ restn(n, x);[]);
          used for: ls;
          slice :  ⊦ slice(n0, n1, x) = (n0 ≤ n1 ⊃ prefixn(n1 - n0, dropn(n0, x));[]);
          used for: ls;

   

   
end enrich