% $Id: ListTree.html,v 1.1 2003/10/01 07:22:16 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 ⊥, top for ⊤)
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]
HTML generated using lsl2html.