Nuprl Definition : bs_tree

Nuprl Definition : bs_tree_max

bs_tree_max(tr;d) ==
  case(tr)
  null=><d, bst_null()>
  leaf(v)=><v, bst_null()>
  node(a,v,b)=>ma,mb.if bst_null?(b) then <v, a> else let m,b' = mb in <m, bst_node(a;v;b')> fi

Definitions occuring in Statement : bs_tree_ind: bs_tree_ind, bst_null?: bst_null?(v), bst_node: bst_node(left;value;right), bst_null: bst_null(), ifthenelse: if b then t else f fi , spread: spread def, pair: <a, b>
Definitions occuring in definition : bs_tree_ind: bs_tree_ind, bst_null: bst_null(), ifthenelse: if b then t else f fi , bst_null?: bst_null?(v), spread: spread def, pair: <a, b>, bst_node: bst_node(left;value;right)
FDL editor aliases : bs_tree_max

Latex:
bs\_tree\_max(tr;d) == case(tr) null=><d, bst\_null()> leaf(v)=><v, bst\_null()> node(a,v,b)=>ma,mb.if bst\_null?(b) then <v, a> else let m,b' = mb in <m, bst\_node(a;v;b')> fi Date html generated: 2016_05_15-PM-01_51_38 Last ObjectModification: 2016_04_08-PM-03_20_56 Theory : tree_1 Home Index