To Do: - Replace List of children by Ordered Set implemented via red-black trees datatype set = SET of (int * tree) where int is the number of children key = int, and key 1 corresponds to the first child Functionality of ordered set 1) insert element 2) retrieve "last" element 3) find all elements with condition x (? return all elements with condition x one by one ?) 4) replace element x by element y preserving order otherwise? this optimization seems very important, as the number of children might be large in addition it would easily support different kinds of retrieval and insertion algorithms - set for normalSubs/assignableSubs (does not need to be ordered) datatype set = SET of (int list * tree) where int list is a list of nvars (or bvars) key = int, and key k corresponds to expression e s.t. e / bvar k (or e / nvar k ) 1) lookup element in set 2) find element with condition x 3) Return all elements in the Set one by one i.e. backtrack over the elements in the set 4) Insert element (not really needed?) 5) Join two sets of substitutions this optimization seems important, but not critical? since the number of substitutions stored at a node will not be large? can be bounded by the number of arguments to a term and the depth of its arguments