[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 dllist
enrich
   cell-heap, 
   list-last
, 
   reflist
with
   

   
   
   functions  dls : ref × ref × list × reflist × ref × ref → heap → bool;
   
   
   variables  head : ref;
              tail : ref;
              next : ref;
              prev : ref;

   

   axioms dls-emp :  ⊦ dls(head, prev, [], rx, next, tail) = (emp ∧ ⌜head = next ∧ tail = prev ∧ rx = []⌝ );
          used for: s, ls;
          dls-rec
          : ⊦   dls(head, prev, a ' + x, rx, next, tail)
              = _∃(λ r. ⌜rx ≠ [] ∧ head = rx.first⌝  ∧ head => mkcell(prev, r, a) * dls(r, head, x, rx.rest, next, tail));

   

   
end enrich