[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 linked-maplist-seg
enrich
   linked-maplist, 
   list-last
with
   functions 
       lls : Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool;
       ll-trav : Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool;
       ll-trav : Ref[Cell[A]] × Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool;
   
   variables 
       r : Ref[Cell[A]];
       a : A;
       b : A;
       x : List[A];
       y : List[A];
       h : Map[Ref[Cell[A]], Cell[A]];
       hP : Map[Ref[Cell[A]], Cell[A]] → Bool;
       ce : Cell[A];
   
   
   axioms 
      lls-base: lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ );
      used for: s, ls;
      
      lls-rec: lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x));
      used for: s, ls;
      
      ll-trav1-def: (ll-trav(r0, r1, x) * hP)(h) ↔ (∃ x0, x1. x = x0 + x1 ∧ (lls(r0, r1, x0) * lls(r1, null, x1) * hP)(h));
      used for: ls;
      
      ll-trav2-null-def: (ll-trav(r0, null, r2, x) * hP)(h) ↔ r2 = r0 ∧ (lls(r0, null, x) * hP)(h);
      used for: ls;
      
      ll-trav2-nonnull-def: 
        r1 ≠ null
      → ((ll-trav(r0, r1, r2, x) * hP)(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ (lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * hP)(h)));
      used for: ls;
   
   
end enrich