Specification build-base

[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 intlist , 
       treeorfail , 
       int-min
 with
   
   functions 
      depths : tree × int → list;
      min : list → int;
      max : list → int;
   predicates 
      is_empty : list;
   
   axioms 
      is-empty :  ⊦ is_empty(x) ↔ x = []; used for : s, ls;
      depths-leaf :  ⊦ depths(Leaf, i) = i '; used for : s, ls;
      depths-node :  ⊦ depths(Node(t0, t1), i) = depths(t0, i + 1) + depths(t1, i + 1); used for : s, ls;
      max-one :  ⊦ max(i ') = i; used for : s, ls;
      max-rec :  ⊦ max(i ' + j ' + x) = max(max(i, j), max(min(i, j) ' + x)); used for : s, ls;
      min-one :  ⊦ min(i ') = i; used for : s, ls;
      min-rec :  ⊦ min(i ' + j ' + x) = min(min(i, j), min(max(i, j) ' + x)); used for : s, ls;
   
end enrich