Nuprl Definition : bs_tree_insert
bs_tree_insert(cmp;x;tr) ==
case(tr)
null=>bst_leaf(x)
leaf(v)=>eval c = cmp v x in
if (0) < (c)
then bst_node(bst_leaf(v);x;bst_null())
else if (c) < (0) then bst_node(bst_null();x;bst_leaf(v)) else bst_leaf(x)
node(l,v,r)=>a,b.eval c = cmp v x in
if (0) < (c) then bst_node(l;v;b) else if (c) < (0) then bst_node(a;v;r) else bst_node(l;x;r)
Definitions occuring in Statement :
bs_tree_ind: bs_tree_ind,
bst_node: bst_node(left;value;right),
bst_leaf: bst_leaf(value),
bst_null: bst_null(),
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
natural_number: $n
Definitions occuring in definition :
bs_tree_ind: bs_tree_ind,
bst_null: bst_null(),
bst_leaf: bst_leaf(value),
callbyvalue: callbyvalue,
apply: f a,
less: if (a) < (b) then c else d,
natural_number: $n,
bst_node: bst_node(left;value;right)
FDL editor aliases :
bs_tree_insert
Latex:
bs\_tree\_insert(cmp;x;tr) ==
case(tr)
null=>bst\_leaf(x)
leaf(v)=>eval c = cmp v x in
if (0) < (c)
then bst\_node(bst\_leaf(v);x;bst\_null())
else if (c) < (0) then bst\_node(bst\_null();x;bst\_leaf(v)) else bst\_leaf(x)
node(l,v,r)=>a,b.eval c = cmp v x in
if (0) < (c)
then bst\_node(l;v;b)
else if (c) < (0) then bst\_node(a;v;r) else bst\_node(l;x;r)
Date html generated:
2016_05_15-PM-01_51_16
Last ObjectModification:
2016_04_07-PM-06_00_38
Theory : tree_1
Home
Index