Nuprl Lemma : aa_min_ltree

t:aa_ltree(

)
(aa_binary_search_tree(t)

(

i:

. (aa_bst_member_prop(i;t)

(

j:

. (((inl j ) = aa_min_ltree(t))

(i

j ))))))

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_min_ltree: aa_min_ltree(t), aa_ltree: aa_ltree(T), ge: i

j , all:

x:A. B[x], exists:

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

Q, and: P

Q, unit: Unit, inl: inl x , union: left + right, int:

, equal: s = t
Definitions : member: t

T, all:

x:A. B[x], so_lambda:

x.t[x], prop:

, ge: i

j , and: P

Q, implies: P

Q, aa_min_ltree: aa_min_ltree(t), aa_min_w_unit: aa_min_w_unit(u1;u2), exists:

x:A. B[x], bfalse: ff, false: False, not:

A, le: A

B, btrue: tt, ifthenelse: if b then t else f fi , imin: imin(a;b), true: True, isl: isl(x), assert:

b, outl: outl(x), uall:

[x:A]. B[x], guard: {T}, so_apply: x[s], aa_bst_member_prop: aa_bst_member_prop(i;t), or: P

Q, uiff: uiff(P;Q), uimplies: b supposing a, bool:

, unit: Unit, aa_binary_search_tree: aa_binary_search_tree(t), sq_type: SQType(T), it:

Lemmas : aa_ltree_wf, aa_lt_node_wf, aa_lt_leaf_wf, ge_wf, aa_min_ltree_wf, unit_wf2, exists_wf, aa_bst_member_prop_wf, all_wf, aa_binary_search_tree_wf, aa_ltree-induction, imin_wf, assert_of_lt_int, bnot_of_le_int, assert_functionality_wrt_uiff, eqff_to_assert, bnot_wf, less_than_wf, lt_int_wf, assert_of_le_int, eqtt_to_assert, le_wf, assert_wf, equal_wf, uiff_transitivity, bool_wf, le_int_wf, unit_subtype_base, int_subtype_base, union_subtype_base, subtype_base_sq, outl_wf, and_wf, aa_min_ltree_spec3, it_wf, equal-unit
\mforall{}t:aa\_ltree(\mBbbZ{}) (aa\_binary\_search\_tree(t) {}\mRightarrow{} (\mforall{}i:\mBbbZ{}. (aa\_bst\_member\_prop(i;t) {}\mRightarrow{} (\mexists{}j:\mBbbZ{}. (((inl j ) = aa\_min\_ltree(t)) \mwedge{} (i \mgeq{} j )))))) Date html generated: 2013_03_20-AM-09_53_47 Last ObjectModification: 2012_11_27-AM-10_32_56 Home Index