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] <z f[v] | inr(ul) => tt
             ∧b case min_l_tree(rtr;f) of inl(minr) => f[v] <z 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 <z j,  btrue: tt,  so_apply: x[s],  decide: case b 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