Nuprl Lemma : aa_binary_search_tree_insert

Nuprl Lemma : aa_binary_search_tree_insert_long

f:aa_ltree(

)

aa_ltree(

)

t:aa_ltree(

).

i:

.
((((aa_binary_search_tree(t)

aa_binary_search_tree(f t i))

(

aa_bst_member(i;f t i)))

(

j:

. ((

aa_bst_member(j;t))

(

aa_bst_member(j;f t i)))))

(

j:

. ((

aa_bst_member(j;f t i))

((j = i)

(

aa_bst_member(j;t))))))

Proof not projected

Error : references
\mexists{}f:aa\_ltree(\mBbbZ{}) {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} aa\_ltree(\mBbbZ{}) \mforall{}t:aa\_ltree(\mBbbZ{}). \mforall{}i:\mBbbZ{}. ((((aa\_binary\_search\_tree(t) {}\mRightarrow{} aa\_binary\_search\_tree(f t i)) \mwedge{} (\muparrow{}aa\_bst\_member(i;f t i))) \mwedge{} (\mforall{}j:\mBbbZ{}. ((\muparrow{}aa\_bst\_member(j;t)) {}\mRightarrow{} (\muparrow{}aa\_bst\_member(j;f t i))))) \mwedge{} (\mforall{}j:\mBbbZ{}. ((\muparrow{}aa\_bst\_member(j;f t i)) {}\mRightarrow{} ((j = i) \mvee{} (\muparrow{}aa\_bst\_member(j;t)))))) Date html generated: 2013_03_20-AM-11_02_19 Last ObjectModification: 2012_11_27-AM-10_32_52 Home Index