---

Step * 1 1 of Lemma prior-cases

.....equality..... 
1. T : Type
2. f : ℕ ⟶ (T + Top)
3. n : ℤ
4. 0 < n
5. case prior(n - 1;f)
 of inl(p) =>
 let m,x = p 
 in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n - 1-}. (¬↑isl(f k)))
 | inr(q) =>
 ∀k:ℕn - 1. (¬↑isl(f k))
⊢ prior(n;f) ~ eval m = n - 1 in
               case f m of inl(x) => inl <m, x> | inr(z) => prior(m;f)
BY
{ (RW (AddrC [1] UnfoldTopAbC) 0⋅
   THEN (RWO "natrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN RepeatFor 2 (EqCD)
   THEN Try (Trivial)
   THEN Unfold `prior` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  f  :  \mBbbN{}  {}\mrightarrow{}  (T  +  Top)
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  case  prior(n  -  1;f)
  of  inl(p)  =>
  let  m,x  =  p 
  in  ((f  m)  =  (inl  x))  \mwedge{}  (\mforall{}k:\{m  +  1..n  -  1\msupminus{}\}.  (\mneg{}\muparrow{}isl(f  k)))
  |  inr(q)  =>
  \mforall{}k:\mBbbN{}n  -  1.  (\mneg{}\muparrow{}isl(f  k))
\mvdash{}  prior(n;f)  \msim{}  eval  m  =  n  -  1  in
                              case  f  m  of  inl(x)  =>  inl  <m,  x>  |  inr(z)  =>  prior(m;f)


By

---

Latex:
(RW  (AddrC  [1]  UnfoldTopAbC)  0\mcdot{}
  THEN  (RWO  "natrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (Trivial)
  THEN  Unfold  `prior`  0
  THEN  Auto)

---

Home Index