---

Step * 1 2 1 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))
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))
BY
{ (MoveToConcl (-3)
   THEN GenConclAtAddr [1;1]
   THEN D -2
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN (Decide ⌜k < n - 1⌝⋅ THENA Auto)
   THEN Try ((BackThruSomeHyp THEN Complete (Auto)))
   THEN (D -2 THENA Auto)
   THEN Subst ⌜k ~ n - 1⌝ 0⋅
   THEN Auto
   THEN HypSubst 6 0
   THEN Reduce 0
   THEN Auto)⋅ }

---

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))
6.  y  :  Top
7.  (f  (n  -  1))  =  (inr  y  )
\mvdash{}  case  prior(n  -  1;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:
(MoveToConcl  (-3)
  THEN  GenConclAtAddr  [1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  (Decide  \mkleeneopen{}k  <  n  -  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  Complete  (Auto)))
  THEN  (D  -2  THENA  Auto)
  THEN  Subst  \mkleeneopen{}k  \msim{}  n  -  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  HypSubst  6  0
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index