---

Step * 1 2 1 of Lemma aa_max_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_max_w_unit(inl (fst(y)) ;aa_max_ltree(snd(snd(y)))) = (inr  )
8. j : 
9. aa_max_w_unit(inl (fst(y)) ;aa_max_ltree(snd(snd(y)))) = (inl j )
 False
BY
{ 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_max_w_unit(inl (fst(y)) ;aa_max_ltree(snd(snd(y)))) = (inr  )
8. j : 
9. aa_max_w_unit(inl (fst(y)) ;aa_max_ltree(snd(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\_max\_w\_unit(inl  (fst(y))  ;aa\_max\_ltree(snd(snd(y))))  =  (inr  \mcdot{}  )
8.  j  :  \mBbbZ{}
9.  aa\_max\_w\_unit(inl  (fst(y))  ;aa\_max\_ltree(snd(snd(y))))  =  (inl  j  )
\mvdash{}  False


By

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



Home Index