Nuprl Lemma : aa_bst_member

ltr,rtr:aa_ltree(

).

val,i:

.
((aa_binary_search_tree(aa_lt_node(val;ltr;rtr))

aa_bst_member_prop(i;ltr))

(i < val))

Proof

Definitions occuring in Statement : aa_binary_search_tree: aa_binary_search_tree(t), aa_bst_member_prop: aa_bst_member_prop(i;t), aa_lt_node: aa_lt_node(val;left_subtree;right_subtree), aa_ltree: aa_ltree(T), all:

x:A. B[x], implies: P

Q, and: P

Q, less_than: a < b, int:

Definitions : prop:

, member: t

T, and: P

Q, implies: P

Q, all:

x:A. B[x], exists:

x:A. B[x], true: True, ifthenelse: if b then t else f fi , btrue: tt, isl: isl(x), assert:

b, outl: outl(x), uall:

[x:A]. B[x], aa_binary_search_tree: aa_binary_search_tree(t), guard: {T}, uimplies: b supposing a, sq_type: SQType(T), false: False, not:

A, cand: A c

B, le: A

B
Lemmas : aa_ltree_wf, aa_bst_member_prop_wf, aa_lt_node_wf, aa_binary_search_tree_wf, unit_subtype_base, int_subtype_base, union_subtype_base, subtype_base_sq, unit_wf2, equal_wf, aa_max_ltree_wf, outl_wf, and_wf, aa_max_ltree_spec, aa_max_ltree_spec3, it_wf, equal-unit
\mforall{}ltr,rtr:aa\_ltree(\mBbbZ{}). \mforall{}val,i:\mBbbZ{}. ((aa\_binary\_search\_tree(aa\_lt\_node(val;ltr;rtr)) \mwedge{} aa\_bst\_member\_prop(i;ltr)) {}\mRightarrow{} (i < val)) Date html generated: 2013_03_20-AM-09_54_01 Last ObjectModification: 2012_11_27-AM-10_32_57 Home Index