Nuprl Definition : bs_tree_delete

bs_tree_delete(cmp;x;tr) ==
  case(tr)
  null=>bst_null()
  leaf(v)=>if (cmp x v =z 0) then bst_null() else bst_leaf(v) fi 
  node(a,v,b)=>da,db.if (0) < (cmp x v)
                        then bst_node(da;v;b)
                        else if (0) < (cmp v x)
                                then bst_node(a;v;db)
                                else if bst_null?(a) then b else let m,a' = bs_tree_max(a;v) in bst_node(a';m;b) fi 


Definitions occuring in Statement :  bs_tree_max: bs_tree_max(tr;d),  bs_tree_ind: bs_tree_ind,  bst_null?: bst_null?(v),  bst_node: bst_node(left;value;right),  bst_leaf: bst_leaf(value),  bst_null: bst_null(),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  less: if (a) < (b)  then c  else d,  apply: f a,  spread: spread def,  natural_number: $n
Definitions occuring in definition :  bs_tree_ind: bs_tree_ind,  eq_int: (i =z j),  bst_null: bst_null(),  bst_leaf: bst_leaf(value),  less: if (a) < (b)  then c  else d,  natural_number: $n,  apply: f a,  ifthenelse: if b then t else f fi ,  bst_null?: bst_null?(v),  spread: spread def,  bs_tree_max: bs_tree_max(tr;d),  bst_node: bst_node(left;value;right)
FDL editor aliases :  bs_tree_delete
Latex:
bs\_tree\_delete(cmp;x;tr)  ==
    case(tr)
    null=>bst\_null()
    leaf(v)=>if  (cmp  x  v  =\msubz{}  0)  then  bst\_null()  else  bst\_leaf(v)  fi 
    node(a,v,b)=>da,db.if  (0)  <  (cmp  x  v)
                                                then  bst\_node(da;v;b)
                                                else  if  (0)  <  (cmp  v  x)
                                                                then  bst\_node(a;v;db)
                                                                else  if  bst\_null?(a)
                                                                          then  b
                                                                          else  let  m,a'  =  bs\_tree\_max(a;v) 
                                                                                    in  bst\_node(a';m;b)
                                                                          fi 


Date html generated: 2016_05_15-PM-01_52_05
Last ObjectModification: 2016_04_08-PM-03_32_20

Theory : tree_1


Home Index