[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 ebm-vol-abs
enrich
   ebm-vol-inv, 
   ebm-base

with
   

   
   
   functions  abs : leb → aleb;
              abs : abstract-volume → avolume;
   
   
   
   
   

   

   axioms abs-leb-mapped :  ⊦ abs(mapped(buf, n)) = mapped(subarray(buf, 0, n));
          used for: s, ls;
          abs-leb-unmapped :  ⊦ abs(unmapped) = unmapped;
          used for: s, ls;
          abs-leb-erased :  ⊦ abs(erased) = unmapped;
          used for: s, ls;
          abs-size :  ⊦ # abs(evol) = # evol;
          used for: s, ls;
          abs-at :  ⊦ n < # evol → abs(evol)[n] = abs(evol[n]);
          used for: s, ls;

   

   
end enrich