[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 ubi-io-base
enrich
   mtd-base
, 
   encoding-echeader
, 
   encoding-vidheader
, 
   aecheader, 
   avidheader
with
   

   
   
   
   predicates  ubi-io-initial : pebs;
               ubi-io-peb-initial : peb;
   
   
   
   

   

   axioms ubi-io-initial :  ⊦ ubi-io-initial(pebs) ↔ (∀ n. n < # pebs → ubi-io-peb-initial(pebs[n]));
          used for: ls;
          ubi-io-peb-initial
          : ⊦   ubi-io-peb-initial(peb)
              ↔ mtd-valid-peb(peb) ∧ (¬ peb.bad → peb.fill = EB_PAGE_SIZE ∧ (∃ n. is-encoded(echdr(n), subarray(peb.data, 0, EB_PAGE_SIZE))));
          used for: ls;

   

   
end enrich