Nuprl Definition : bs_tree

Nuprl Definition : bs_tree_ordered

bs_tree_ordered(E;cmp;tr) ==
  case(tr)
  null=>True
  leaf(v)=>True
  node(a,v,b)=>oa,ob.oa
  ∧ ob
  ∧ (∀x:E. (member_bs_tree(E;x;a) ⇒ 0 < cmp x v))
  ∧ (∀x:E. (member_bs_tree(E;x;b) ⇒ 0 < cmp v x))

Definitions occuring in Statement : member_bs_tree: member_bs_tree(E;x;tr), bs_tree_ind: bs_tree_ind, less_than: a < b, all: ∀x:A. B[x], implies: P ⇒ Q, and: P ∧ Q, true: True, apply: f a, natural_number: $n
Definitions occuring in definition : bs_tree_ind: bs_tree_ind, true: True, and: P ∧ Q, all: ∀x:A. B[x], implies: P ⇒ Q, member_bs_tree: member_bs_tree(E;x;tr), less_than: a < b, natural_number: $n, apply: f a
FDL editor aliases : bs_tree_ordered

Latex:
bs\_tree\_ordered(E;cmp;tr) == case(tr) null=>True leaf(v)=>True node(a,v,b)=>oa,ob.oa \mwedge{} ob \mwedge{} (\mforall{}x:E. (member\_bs\_tree(E;x;a) {}\mRightarrow{} 0 < cmp x v)) \mwedge{} (\mforall{}x:E. (member\_bs\_tree(E;x;b) {}\mRightarrow{} 0 < cmp v x)) Date html generated: 2016_05_15-PM-01_51_07 Last ObjectModification: 2016_04_07-PM-07_02_57 Theory : tree_1 Home Index