[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-log
enrich
   encoding-ref-node
, 
   nat-list-less

with
   

   
   
   
   predicates  is-encoded : nat-list × buffer;
   
   
   
   

   

   axioms is-encoded-base :  ⊦ is-encoded([], buf) ↔ buf = mkbuf(0);
          used for: s, ls;
          is-encoded-rec :  ⊦ is-encoded(n ' + nx, buf) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ is-encoded(rnode(n), buf0) ∧ is-encoded(nx, buf1));
          used for: ls;

   

   
end enrich