Nuprl Lemma : aa_bst_insert_sublemma_left
left_subtree,right_subtree,tp:aa_ltree(). val,i:.
  ((aa_binary_search_tree(tp)
   aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))
   (i < val)
   (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree))))
   (j:
        (aa_bst_member_prop(j;aa_lt_node(val;tp;right_subtree))
         (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree)))))
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], 
iff: P  Q, 
implies: P  Q, 
or: P  Q, 
and: P  Q, 
less_than: a < b, 
int: , 
equal: s = t
Definitions : 
so_lambda: x.t[x], 
prop: , 
member: t  T, 
rev_implies: P  Q, 
or: P  Q, 
iff: P  Q, 
and: P  Q, 
implies: P  Q, 
all: x:A. B[x], 
guard: {T}, 
not: A, 
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]), 
aa_bst_member_prop: aa_bst_member_prop(i;t), 
so_apply: x[s], 
uall: [x:A]. B[x], 
uiff: uiff(P;Q), 
uimplies: b supposing a, 
unit: Unit, 
bool: , 
so_apply: x[s1;s2;s3;s4;s5], 
false: False, 
bfalse: ff, 
btrue: tt, 
it:
Lemmas : 
aa_ltree_wf, 
iff_wf, 
all_wf, 
aa_binary_search_tree_wf, 
equal_wf, 
or_wf, 
aa_lt_node_wf, 
aa_bst_member_prop_wf, 
assert_of_bnot, 
eqff_to_assert, 
iff_weakening_uiff, 
not_wf, 
bnot_wf, 
iff_transitivity, 
assert_of_eq_int, 
eqtt_to_assert, 
assert_wf, 
uiff_transitivity, 
bool_wf, 
eq_int_wf, 
subtype_rel_self, 
false_wf, 
aa_ltree_ind_wf
\mforall{}left$_{subtree}$,right$_{subtree}$,tp:aa\_ltree(\mBbbZ{}).  \mforall{}val,i:\mBbbZ{}\000C.
    ((aa\_binary\_search\_tree(tp)
    \mwedge{}  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{su\000Cbtree}$))
    \mwedge{}  (i  <  val)
    \mwedge{}  (\mforall{}j:\mBbbZ{}.  (aa\_bst\_member\_prop(j;tp)  \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;left$_{subtree\mbackslash{}f\000Cf7d$))))
    {}\mRightarrow{}  (\mforall{}j:\mBbbZ{}
                (aa\_bst\_member\_prop(j;aa\_lt\_node(val;tp;right$_{subtree}$))
                \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right\000C$_{subtree}$)))))
Date html generated:
2013_03_20-AM-09_54_19
Last ObjectModification:
2012_11_27-AM-10_32_59
Home
Index