---

Step * 1 2 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_ltree_ind(snd(snd(y));inr  ;val,left_subtree,right_subtree,rec1,rec2....))
= (inr  )
 False
BY
{ Fold `aa_max_ltree` 7 THEN InstLemma `aa_max_w_unit_prop1` [fst(y);aa_max_ltree(snd(snd(y)))] THEN Auto THEN D 8
 }

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 )
 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\_ltree\_ind(...;inr  \mcdot{}  ;val,left$_{subtree}$,righ\000Ct$_{subtree}$,rec1,rec2....))
=  (inr  \mcdot{}  )
\mvdash{}  False


By

Fold  `aa\_max\_ltree`  7  THEN  InstLemma  `aa\_max\_w\_unit\_prop1`  [\mkleeneopen{}fst(y)\mkleeneclose{};\mkleeneopen{}aa\_max\_ltree(\mkleeneopen{}snd(snd(y))\mkleeneclose{})\mkleeneclose{}
]  THEN  Auto  THEN  D  8\mcdot{}



Home Index