[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-ref-node
instantiate parameter
   elem
< 
   encoding-page-size-nonempty

with 
   ref-node, 
   eraseblock


   
by mapping
      : elem → ref-node; 
      a → rnd; 
      b → rnd0; 
      c → rnd1
   rename 
      ENCODED_ELEM_SIZE → ENCODED_REF_NODE_SIZE; 
      encoding-size → encoding-size; 
      is-garbage-pagesize → is-garbage-rnode; 
      is-garbage-nonempty → is-garbage-rnode-nonempty; 
      is-garbage → is-garbage-rnode-empty; 
      is-encoded-nonempty → is-encoded-nonempty; 
      is-encoded-pagesize → is-encoded; 
      is-encoded → is-encoded-empty; 
      encode_pagesize# → encode_ref_node#; 
      encode_nonempty# → encode_ref_node_nonempty#; 
      encode# → encode_ref_node_empty#; 
      decode_pagesize# → decode_ref_node#; 
      decode_nonempty# → decode_ref_node_nonempty#; 
      decode# → decode_ref_node_empty#
end instantiate