Specification vtbl-conv

[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
   vtbl, 
   eraseblock
, 
   volumes
with
   

   
   constants  VTBL_VOLID : volid;
              VTBL_LNUM : nat;
   functions  to-vtbl : volumes → vtbl;
   
   
   
   
   

   

   axioms to-vtbl-base :  ⊦ to-vtbl(∅) = ∅;
          used for: s, ls;
          to-vtbl-rec :  ⊦ to-vtbl(vols[v, ebatbl]) = to-vtbl(vols -- v)[v, # ebatbl];
          used for: ls;

   

   
end enrich