Selected Objects

def	tree_con	tree_con(E;T) == E+(TT)
def	tree_leaf	tree_leaf(x) == inl(x)
def	case_tree_leaf	Case tree_leaf(x) => body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
def	tree_node	tree_node(x) == inr(x)
def	tree	Tree(E) == rec(T.tree_con(E;T))
THM	tree_subtype2	tree_con(E;Tree(E))  Tree(E)
def	node	tree_node(<x, y>) == tree_node(<x,y>)
def	case_node	Case x;y => body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0))
def	t_iterate	t_iterate(l;n;t) == Case(t) == Case x;y => == Casen(t_iterate(l;n;x),t_iterate(l;n;y)) == Case tree_leaf(x) => == Casel(x) == Default => True (recursive)
def	is_leaf	is_leaf(t) == Case(t) Case tree_leaf(l) => true Default => false
def	left_child	left_child(t) == Case(t) Case x;y => x Default => t
def	right_child	right_child(t) == Case(t) Case x;y => y Default => t
def	leaf_value	leaf_value(t) == Case(t) Case tree_leaf(l) => l Default => True
THM	tree_leaf_one_one	x1,x2:E. tree_leaf(x1) = tree_leaf(x2)  Tree(E)  x1 = x2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html