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