---

Step * 1 2 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. f : {m..n-} ⟶ T
8. x : T
⊢ (x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T)
BY
{ xxx(RecUnfold `listify` 0 THEN BoolCase ⌜n ≤z m⌝⋅ THEN Auto THEN ExRepD THEN Auto)xxx }

1
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. (x ∈ [f m / listify(f;m + 1;n)])
⊢ ∃i:{m..n-}. (x = (f i) ∈ T)

2
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 / listify(f;m + 1;n)])

---

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.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
8.  x  :  T
\mvdash{}  (x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i))


By

---

Latex:
xxx(RecUnfold  `listify`  0  THEN  BoolCase  \mkleeneopen{}n  \mleq{}z  m\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  ExRepD  THEN  Auto)xxx

---

Home Index