---

Step * 1 2 2 1 of Lemma member-listify


1. [T] : Type
2. d : ℤ
3. [%1] : 0 < d
4. ∀m:ℤ. ∀n:{m..m + (d - 1)-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
5. m : ℤ
6. n : {m..m + d-}
7. ¬(n ≤ m)
8. f : {m..n-} ⟶ T
9. x : T
10. i : {m..n-}
11. x = (f i) ∈ T
⊢ (x = (f m) ∈ T) ∨ (∃i:{m + 1..n-}. (x = (f i) ∈ T))
BY
{ xxx(Decide i = m ∈ ℤ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  d  :  \mBbbZ{}
3.  [\%1]  :  0  <  d
4.  \mforall{}m:\mBbbZ{}.  \mforall{}n:\{m..m  +  (d  -  1)\msupminus{}\}.  \mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.  \mforall{}x:T.
          ((x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i)))
5.  m  :  \mBbbZ{}
6.  n  :  \{m..m  +  d\msupminus{}\}
7.  \mneg{}(n  \mleq{}  m)
8.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
9.  x  :  T
10.  i  :  \{m..n\msupminus{}\}
11.  x  =  (f  i)
\mvdash{}  (x  =  (f  m))  \mvee{}  (\mexists{}i:\{m  +  1..n\msupminus{}\}.  (x  =  (f  i)))


By

---

Latex:
xxx(Decide  i  =  m  THEN  Auto)xxx

---

Home Index