[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  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;
   
   
   partial functions  . .last : list → elem with λ x. x ≠ [];
                      . .butlast : list → list with λ x. x ≠ [];
                      butlastn : nat × list → list with λ n, x. n ≤ # x;
                     comment: return list except last n elements;
   

   

   axioms butlast-one :  ⊦ a '.butlast = [];
          used for: s, ls;
          last-one :  ⊦ a '.last = a;
          used for: s, ls;
          butlast-rec :  ⊦ (a ' + b ' + x).butlast = a ' + (b ' + x).butlast;
          used for: s, ls;
          last-rec :  ⊦ (b ' + a ' + x).last = (a ' + x).last;
          used for: s, ls;
          rev-e :  ⊦ rev([]) = [];
          used for: s, ls;
          rev-r :  ⊦ rev(a ' + x) = rev(x) + a;
          used for: s, ls;
          mk-zero :  ⊦ mklist(a, 0) = [];
          used for: s, ls;
          mk-succ :  ⊦ mklist(a, n + 1) = a ' + mklist(a, n);
          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