---

Step * 1 2 of Lemma prior-cases


1. [T] : Type
2. f : ℕ ⟶ (T + Top)
3. n : ℤ
4. [%1] : 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))
⊢ case eval m = n - 1 in
       case f m of inl(x) => inl <m, x> | inr(z) => prior(m;f)
 of inl(p) =>
 let m,x = p 
 in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k)))
 | inr(q) =>
 ∀k:ℕn. (¬↑isl(f k))
BY
{ ((CallByValueReduce 0 THENA Auto) THEN GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. f : ℕ ⟶ (T + Top)
3. n : ℤ
4. [%1] : 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))
6. y : Top
7. (f (n - 1)) = (inr y ) ∈ (T + Top)
⊢ case prior(n - 1;f)
 of inl(p) =>
 let m,x = p 
 in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k)))
 | inr(q) =>
 ∀k:ℕn. (¬↑isl(f k))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  \mBbbN{}  {}\mrightarrow{}  (T  +  Top)
3.  n  :  \mBbbZ{}
4.  [\%1]  :  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{}  case  eval  m  =  n  -  1  in
              case  f  m  of  inl(x)  =>  inl  <m,  x>  |  inr(z)  =>  prior(m;f)
  of  inl(p)  =>
  let  m,x  =  p 
  in  ((f  m)  =  (inl  x))  \mwedge{}  (\mforall{}k:\{m  +  1..n\msupminus{}\}.  (\mneg{}\muparrow{}isl(f  k)))
  |  inr(q)  =>
  \mforall{}k:\mBbbN{}n.  (\mneg{}\muparrow{}isl(f  k))


By

---

Latex:
((CallByValueReduce  0  THENA  Auto)  THEN  GenConclAtAddr  [1;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index