[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-tree-list
enrich
   linked-tree, 
   dlinked-list, 
   nat-pot, 
   nat-even
with
   functions 
       . .toList : tree → list;
   
   predicates 
       ordered≤ : tree;
       . ≤ . : tree × elem;
      comment: t ≤ a <-> all elements in tree t are less or equal than a;
       . ≤ . : elem × tree;
      comment: a ≤ t <-> all elements in tree t are greater or equal than a;
       . ∈ . : elem × tree;
       balanced : tree;
      comment: recursive balanced property: the left subtree contains the same number of elements (+/-1) as the right subtree;
       . ~ . : nat × nat;
      comment: n ~ m <-> n and m differ at most by 1;
   
   variables 
       h : heap;
       head : ref;
       r : ref;
       next : ref;
       root : ref;
       right : ref;
       left : ref;
       a : elem;
       b : elem;
       c : elem;
       x : list;
       y : list;
       z : list;
       t : tree;
   
   
   axioms 
      toList-base: leaf.toList = [];
      used for: s, ls;
      
      toList-rec: branch(t0, a, t1).toList = t0.toList + (a + t1.toList);
      used for: s, ls;
      
      in-base: ¬ a ∈ leaf;
      used for: s, ls;
      
      in-rec: a ∈ branch(t0, b, t1) ↔ a ∈ t0 ∨ a = b ∨ a ∈ t1;
      used for: ws, lws;
      
      tree-le-elem-base: leaf ≤ a;
      used for: s, ls;
      
      tree-le-elem-rec: branch(t0, b, t1) ≤ a ↔ t0 ≤ a ∧ ¬ a < b ∧ t1 ≤ a;
      used for: s, ls;
      
      elem-le-tree-base: a ≤ leaf;
      used for: s, ls;
      
      elem-le-tree-rec: a ≤ branch(t0, b, t1) ↔ a ≤ t0 ∧ ¬ b < a ∧ a ≤ t1;
      used for: s, ls;
      
      ordered-base: ordered≤(leaf);
      used for: s, ls;
      
      ordered-rec: ordered≤(branch(t0, a, t1)) ↔ ordered≤(t0) ∧ t0 ≤ a ∧ a ≤ t1 ∧ ordered≤(t1);
      used for: ws, lws;
      
      balanced-base: balanced(leaf);
      used for: s, ls;
      
      balanced-rec: balanced(branch(t0, a, t1)) ↔ balanced(t0) ∧ balanced(t1) ∧ # t0 ~ # t1;
      used for: s, ls;
      
      equal-or-one-diff: n ~ m ↔ n = m ∨ n = m + 1 ∨ m = n + 1;
      used for: ls, ws;
   
   
end enrich