% $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 __ á __ ñ __,
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 Î 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);
[Index]
[source]
HTML generated using lsl2html.