Specification bag-array

[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 bag-union
 , 
       array-splice
 with
   functions 
       . .elems : array → bag;
       . elems . : array × nat → bag;
   
   axioms 
      elems :  ⊦ ar .elems = ar elems # ar;
      elems-base :  ⊦ ar elems 0 = ∅;
      used for : s, ls;
       
      elems-rec : n < # ar ⊦ ar elems (n + 1) = (ar elems n) ++ ar[n];
      used for : s, ls;
       
end enrich