---

Step * of Lemma isl-prior

∀[T:Type]
  ∀f:ℕ ⟶ (T + Top). ∀n:ℕ.
    let m,x = outl(prior(n;f)) 
    in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k))) 
    supposing ↑isl(prior(n;f))
BY
{ (InstLemma `prior-cases` []
   THEN RepeatFor 3 (ParallelLast')
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  (T  +  Top).  \mforall{}n:\mBbbN{}.
        let  m,x  =  outl(prior(n;f)) 
        in  ((f  m)  =  (inl  x))  \mwedge{}  (\mforall{}k:\{m  +  1..n\msupminus{}\}.  (\mneg{}\muparrow{}isl(f  k))) 
        supposing  \muparrow{}isl(prior(n;f))


By

---

Latex:
(InstLemma  `prior-cases`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index