Nuprl Definition : bs_l_tree

bs_l_tree(t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v) tt;
             l_tree_node(v,ltr,rtr) ltrp,rtrp.ltrp
             ∧b rtrp
             ∧b case max_l_tree(ltr;f) of inl(maxl) => f[maxl] <f[v] inr(ul) => tt
             ∧b case min_l_tree(rtr;f) of inl(minr) => f[v] <f[minr] inr(ur) => tt) 



Definitions occuring in Statement :  min_l_tree: min_l_tree(t;f) max_l_tree: max_l_tree(t;f) l_tree_ind: l_tree_ind band: p ∧b q lt_int: i <j btrue: tt so_apply: x[s] decide: case of inl(x) => s[x] inr(y) => t[y]
FDL editor aliases :  bs_l_tree
bs\_l\_tree(t;f)  ==
    l\_tree\_ind(t;
                          l\_tree\_leaf(v){}\mRightarrow{}  tt;
                          l\_tree\_node(v,ltr,rtr){}\mRightarrow{}  ltrp,rtrp.ltrp
                          \mwedge{}\msubb{}  rtrp
                          \mwedge{}\msubb{}  case  max\_l\_tree(ltr;f)  of  inl(maxl)  =>  f[maxl]  <z  f[v]  |  inr(ul)  =>  tt
                          \mwedge{}\msubb{}  case  min\_l\_tree(rtr;f)  of  inl(minr)  =>  f[v]  <z  f[minr]  |  inr(ur)  =>  tt) 



Date html generated: 2015_07_17-AM-07_41_51
Last ObjectModification: 2012_06_25-PM-07_37_57

Home Index