Specification linked-tree-path

[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,

enrich
   linked-tree, 
   tree-path
with
   variables 
       t : Tree[A];
       h : Heap[Node[A]];
       nd : Node[A];
       a : A;
       p : List[Bool];
       b : Bool;
       hP : Heap[Node[A]] → Bool;
       r : Ref[Node[A]];
   
   partial functions 
       trp : Ref[Node[A]] × Tree[A] × List[Bool] × Ref[Node[A]] → Heap[Node[A]] → Bool with λ r, t, p, r0. λ h. p ∈ t;
   
   
   axioms 
      trp-base: trp(r, t, [], r0) = (⌜r = r0⌝  ∧ emp);
      used for: s, ls;
      
      trp-leaf: trp(r, leaf, b ' + p, r0) = false;
      used for: s, ls;
      
      trp-branch-rec: 
        trp(r, branch(t1, a, t2), b ' + p, r0)
      = _∃(λ r1, r2. r => mknode(r1, a, r2) * (b ⊃ tr(r1, t1) * trp(r2, t2, p, r0);trp(r1, t1, p, r0) * tr(r2, t2)));
   
   
end enrich