---

Step * 1 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. x : Unit
5. t = (inl x )
6. (inr  ) = (inr  )
7. aa_ltree_ind(inl x ;False;v,ltr,rtr,ltrm,rtrm.(v = i)  ((i < v)  ltrm)  ((v < i)  rtrm))
 False
BY
{ RecUnfold `aa_ltree_ind` 7 THEN Reduce 7 THEN Trivial }



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.  x  :  Unit
5.  t  =  (inl  x  )
6.  (inr  \mcdot{}  )  =  (inr  \mcdot{}  )
7.  aa\_ltree\_ind(inl  x  ;False;v,ltr,rtr,ltrm,rtrm.(v  =  i)  \mvee{}  ((i  <  v)  \mwedge{}  ltrm)  \mvee{}  ((v  <  i)  \mwedge{}  rtrm))
\mvdash{}  False


By

RecUnfold  `aa\_ltree\_ind`  7  THEN  Reduce  7  THEN  Trivial



Home Index