---

Step * 1 of Lemma prior-cases

.....upcase..... 
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 prior(n;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
{ Subst ⌜prior(n;f) ~ eval m = n - 1 in
                      case f m of inl(x) => inl <m, x> | inr(z) => prior(m;f)⌝ 0⋅ }

1
.....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)

2
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))

---

Latex:

---

Latex:
.....upcase..... 
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  prior(n;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:
Subst  \mkleeneopen{}prior(n;f)  \msim{}  eval  m  =  n  -  1  in
                                        case  f  m  of  inl(x)  =>  inl  <m,  x>  |  inr(z)  =>  prior(m;f)\mkleeneclose{}  0\mcdot{}

---

Home Index