% $Id: ListTree.lsl,v 1.3 2000/01/17 21:33:40 connolly Exp $

ListTree(E, R): trait
    % make a list into a tree by way of a children operator
    includes
        List(E),
        Relation(E, R,
	 __ \< __ \> __ for __ \langle __ \rangle __,
	bot for \bot, top for \top)
    introduces
        children: E -> List[E]
        flatten: List[E] -> List[E]
	child: -> R
	descendant: -> R
    asserts
	forall i, i1, i2: E, li, li1: List[E]

	(i1 \< child \> i2) = (i1 \in children(i2));
	irreflexive(child);
	descendant = (child \superplus);

	flatten(empty) = empty;

	children(i) = empty
	=> flatten(i -| li) = i -| flatten(li);

	children(i) = i1 -| li1
	=> flatten(i -| li) = i -| (flatten({i1})
 	                           || flatten(li1) || flatten(li));
    implies
	forall i: E
	transitive(descendant);