[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-maplist-seg
enrich
   dlinked-maplist, 
   list-last
with
   functions 
       dlls : Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool;
      comment: head-pointer × front terminator × end terminator;
       dlls : Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool;
      comment: head-pointer × last-pointer × front terminator × end terminator;
       dll-trav
      : Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A]
        → Map[Ref[Node[A]], Node[A]] → Bool
      ;
   
   variables 
       r : Ref[Node[A]];
       hd : Ref[Node[A]];
       lst : Ref[Node[A]];
       prv : Ref[Node[A]];
       nxt : Ref[Node[A]];
       cur : Ref[Node[A]];
       x : List[A];
       y : List[A];
       z : List[A];
       a : A;
       b : A;
       c : A;
       h : Map[Ref[Node[A]], Node[A]];
       hP : Map[Ref[Node[A]], Node[A]] → Bool;
       nd : Node[A];
   
   
   axioms 
      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;
      
      dlls-last-base: dlls(hd, lst, prv, nxt, []) = (emp ∧ ⌜hd = nxt⌝  ∧ ⌜lst = prv⌝ );
      used for: s, ls;
      
      dlls-last-rec: dlls(hd, lst, prv, nxt, a ' + x) = _∃(λ nxt0. hd => mknode(prv, a, nxt0) * dlls(nxt0, lst, hd, nxt, x));
      used for: s, ls;
      
      dll-trav-null: (dll-trav(prv, hd, lst, null, hd0, lst0, nxt, x) * hP)(h) ↔ hd = hd0 ∧ lst = lst0 ∧ (dlls(hd, lst, prv, nxt, x) * hP)(h);
      used for: ls;
      
      ll-trav-nonnull: 
        cur ≠ null
      → (  (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h)
         ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h)));
      used for: ls;
   
   
end enrich