[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 dlinked-list
enrich
   node-heap, 
   olist-min-max
with
   functions 
       dll : ref × list → heap → bool;
       dlls : ref × ref × ref × list → heap → bool;
   
   variables 
       r : ref;
       x : list;
       y : list;
       z : list;
       a : elem;
       b : elem;
       c : elem;
       h : heap;
       hP : heap → bool;
   
   
   axioms 
      dll: dll(r, x) = dlls(r, null, null, x);
      used for: s, ls;
      
      dlls-base: dlls(r, r0, r1, []) = (emp ∧ ⌜r = r1⌝ );
      used for: s, ls;
      
      dlls-rec: dlls(r, r0, r1, a ' + x) = _∃(λ r2. r => mknode(r0, a, r2) * dlls(r2, r, r1, x));
      used for: s, ls;
   
   
end enrich