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;rtr))

(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), gt: i > j, all:

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

Q, and: P

Q, int:

Definitions : prop:

, member: t

T, gt: i > j, 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), cand: A c

B, false: False, not:

A, ge: i

j , 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_min_ltree_wf, outl_wf, and_wf, aa_min_ltree_spec, aa_min_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;rtr)) {}\mRightarrow{} (i > val)) Date html generated: 2013_03_20-AM-09_54_08 Last ObjectModification: 2012_11_27-AM-10_32_58 Home Index