---

Step * 1 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. x : Unit
6. t = (inl x )
7. (inr  ) = (inr  )
 False
BY
{ RepUR ``aa_bst_member_prop`` 4 THEN MoveToHyp 0 4 THEN At  (HypSubst 5 7) THENA Auto }

1
.....wf..... 
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(t;False;v,ltr,rtr,ltrm,rtrm.(v = i)  ((i < v)  ltrm)  ((v < i)  rtrm))
8. z : Unit + (val:  left_subtree:aa_ltree()  aa_ltree())
 aa_ltree_ind(z;False;v,ltr,rtr,ltrm,rtrm.(v = i)  ((i < v)  ltrm)  ((v < i)  rtrm))  

2
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



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.  x  :  Unit
6.  t  =  (inl  x  )
7.  (inr  \mcdot{}  )  =  (inr  \mcdot{}  )
\mvdash{}  False


By

RepUR  ``aa\_bst\_member\_prop``  4  THEN  MoveToHyp  0  4  THEN  At  \mkleeneopen{}\mBbbP{}\mkleeneclose{}  (HypSubst  5  7)  THENA  Auto\mcdot{}



Home Index