---

Step * 1 2 1 of Lemma aa_min_ltree_spec3


1. t : rec(X.Unit + (val:  left_subtree:X  X))
2. aa_binary_search_tree(t)@i
3. i : @i
4. aa_bst_member_prop(i;t)@i
5. y : val:  left_subtree:aa_ltree()  aa_ltree()
6. t = (inr y )
7. aa_min_w_unit(inl (fst(y)) ;aa_min_ltree(fst(snd(y)))) = (inr  )
8. j:. (aa_min_w_unit(inl (fst(y)) ;aa_min_ltree(fst(snd(y)))) = (inl j ))
 False
BY
{ D 8 THEN Assert (inr  ) = (inl j ) THEN Auto' }

1
1. t : rec(X.Unit + (val:  left_subtree:X  X))
2. aa_binary_search_tree(t)@i
3. i : @i
4. aa_bst_member_prop(i;t)@i
5. y : val:  left_subtree:aa_ltree()  aa_ltree()
6. t = (inr y )
7. aa_min_w_unit(inl (fst(y)) ;aa_min_ltree(fst(snd(y)))) = (inr  )
8. j : 
9. aa_min_w_unit(inl (fst(y)) ;aa_min_ltree(fst(snd(y)))) = (inl j )
10. (inr  ) = (inl j )
 False



1.  t  :  rec(X.Unit  +  (val:\mBbbZ{}  \mtimes{}  left$_{subtree}$:X  \mtimes{}  X))
2.  aa\_binary\_search\_tree(t)@i
3.  i  :  \mBbbZ{}@i
4.  aa\_bst\_member\_prop(i;t)@i
5.  y  :  val:\mBbbZ{}  \mtimes{}  left$_{subtree}$:aa\_ltree(\mBbbZ{})  \mtimes{}  aa\_ltree(\mBbbZ{})
6.  t  =  (inr  y  )
7.  aa\_min\_w\_unit(inl  (fst(y))  ;aa\_min\_ltree(fst(snd(y))))  =  (inr  \mcdot{}  )
8.  \mexists{}j:\mBbbZ{}.  (aa\_min\_w\_unit(inl  (fst(y))  ;aa\_min\_ltree(fst(snd(y))))  =  (inl  j  ))
\mvdash{}  False


By

D  8  THEN  Assert  \mkleeneopen{}(inr  \mcdot{}  )  =  (inl  j  )\mkleeneclose{}  THEN  Auto'\mcdot{}



Home Index