[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 encoding-orphans
enrich
   encoding-nat
, 
   nat-set
, 
   eraseblock

with
   

   
   
   
   predicates  is-encoded : nat-set × buffer;
               is-encoded-pad : nat-set × nat × buffer;
   
   
   
   

   

   axioms is-encoded-base :  ⊦ is-encoded(∅, buf) ↔ buf = mkbuf(0);
          used for: s, ls;
          is-encoded-rec
          :  ⊦ ns ≠ ∅ → (is-encoded(ns, buf) ↔ (∃ n, buf0, buf1. n ∈ ns ∧ buf = buf0 + buf1 ∧ is-encoded(n, buf0) ∧ is-encoded(ns -- n, buf1)));
          is-encoded-pad
          : ⊦   is-encoded-pad(ns, n, buf)
              ↔ n = # ns ∧ (∃ buf0, buf1. is-aligned(# buf, EB_PAGE_SIZE) ∧ buf = buf0 + buf1 ∧ is-encoded(ns, buf0));

   

   
end enrich