---

Step * 1 of Lemma isl-prior-iff


1. [T] : Type
2. f : ℕ ⟶ (T + Top)
3. n : ℕ
4. x : ℕn × T
5. prior(n;f) = (inl x) ∈ (ℕn × T?)
⊢ let m,x = x in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k))) ⇒ (True ⇐⇒ ∃k:ℕn. (↑isl(f k)))
BY
{ (D (-2) THEN Reduce 0 THEN Auto THEN With ⌜x1⌝ (D 0)⋅ THEN Auto THEN HypSubst' -3 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  \mBbbN{}  {}\mrightarrow{}  (T  +  Top)
3.  n  :  \mBbbN{}
4.  x  :  \mBbbN{}n  \mtimes{}  T
5.  prior(n;f)  =  (inl  x)
\mvdash{}  let  m,x  =  x  in  ((f  m)  =  (inl  x))  \mwedge{}  (\mforall{}k:\{m  +  1..n\msupminus{}\}.  (\mneg{}\muparrow{}isl(f  k)))  {}\mRightarrow{}  (True  \mLeftarrow{}{}\mRightarrow{}  \mexists{}k:\mBbbN{}n.  (\muparrow{}isl(f  k)))


By

---

Latex:
(D  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  With  \mkleeneopen{}x1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  HypSubst'  -3  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index