Nuprl Definition : bs_l

Nuprl Definition : bs_l_tree

bs_l_tree(t;f) ==
  l_tree_ind(t;
             Leaf(v)⇒ tt;
             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

Latex:
bs\_l\_tree(t;f) == l\_tree\_ind(t; Leaf(v){}\mRightarrow{} tt; 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: 2018_05_22-PM-09_39_56 Last ObjectModification: 2012_06_25-PM-07_37_57 Theory : labeled!trees Home Index