---

Step * 1 1 1 of Lemma aa_max_ltree_spec3

.....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))  
BY
{ (Assert z  aa_ltree()
   THEN Auto
   THEN skip{MaAuto would work here}
   THEN Unfold `aa_ltree` 0
   THEN MemTypeCD
   THEN Try (Fold `aa_ltree` 0)
   THEN Auto) }


.....wf..... 
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(t;False;v,ltr,rtr,ltrm,rtrm.(v  =  i)  \mvee{}  ((i  <  v)  \mwedge{}  ltrm)  \mvee{}  ((v  <  i)  \mwedge{}  rtrm))
8.  z  :  Unit  +  (val:\mBbbZ{}  \mtimes{}  left$_{subtree}$:aa\_ltree(\mBbbZ{})  \mtimes{}  aa\_ltree(\mBbbZ{}))
\mvdash{}  aa\_ltree\_ind(z;False;v,ltr,rtr,ltrm,rtrm.(v  =  i)  \mvee{}  ((i  <  v)  \mwedge{}  ltrm)  \mvee{}  ((v  <  i)  \mwedge{}  rtrm))  \mmember{}  \mBbbP{}


By

(Assert  \mkleeneopen{}z  \mmember{}  aa\_ltree(\mBbbZ{})\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  skip\{MaAuto  would  work  here\}
  THEN  Unfold  `aa\_ltree`  0
  THEN  MemTypeCD
  THEN  Try  (Fold  `aa\_ltree`  0)
  THEN  Auto)



Home Index