Nuprl Lemma : aa_max_ltree

t:aa_ltree(

)
(aa_binary_search_tree(t)

(

i:

. (aa_bst_member_prop(i;t)

(

j:

. (((inl j ) = aa_max_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_max_ltree: aa_max_ltree(t), aa_ltree: aa_ltree(T), le: A

B, 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 : all:

x:A. B[x], member: t

T, so_lambda:

x.t[x], prop:

, and: P

Q, implies: P

Q, aa_max_ltree: aa_max_ltree(t), aa_max_w_unit: aa_max_w_unit(u1;u2), exists:

x:A. B[x], le: A

B, or: P

Q, not:

A, false: False, true: True, ifthenelse: if b then t else f fi , btrue: tt, isl: isl(x), assert:

b, outl: outl(x), guard: {T}, aa_ltree: aa_ltree(T), so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]), uall:

[x:A]. B[x], so_apply: x[s], aa_bst_member_prop: aa_bst_member_prop(i;t), iff: P

Q, rev_implies: P

Q, aa_binary_search_tree: aa_binary_search_tree(t), sq_type: SQType(T), uimplies: b supposing a, decidable: Dec(P), aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]), so_apply: x[s1;s2;s3;s4;s5]
Lemmas : aa_ltree_wf, aa_lt_node_wf, aa_lt_leaf_wf, le_wf, aa_max_ltree_wf, unit_wf2, exists_wf, aa_bst_member_prop_wf, all_wf, aa_binary_search_tree_wf, aa_ltree-induction, imax_wf, imax_ub, unit_subtype_base, int_subtype_base, union_subtype_base, subtype_base_sq, outl_wf, equal_wf, and_wf, decidable__le, aa_ltree_ind_wf, it_wf, aa_max_w_unit_wf, pi2_wf
\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\_max\_ltree(t)) \mwedge{} (i \mleq{} j)))))) Date html generated: 2013_03_20-AM-09_53_32 Last ObjectModification: 2012_11_27-AM-10_32_55 Home Index