---

Step * 1 2 of Lemma islist-iff-length-has-value


1. T : Type
2. j : ℤ
3. 0 < j
4. λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
⊢ λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j ⊥ t)↓ ⇒ (||t||)↓)
BY
{ ((Assert ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓) BY
          (UseWitness ⌜λt,x. Ax⌝⋅ THEN Trivial))
   THEN Fold `is-list-approx` 0
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))) }

1
.....subterm..... T:t
1:n
1. T : Type
2. j : ℤ
3. 0 < j
4. λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
5. ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
6. t : colist(T)
7. x : (is-list-approx(j) t)↓
⊢ Ax ∈ (||t||)↓

2
.....eq aux..... 
1. T : Type
2. j : ℤ
3. 0 < j
4. λt,x. Ax ∈ ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
5. ∀t:colist(T). ((is-list-fun()^j - 1 ⊥ t)↓ ⇒ (||t||)↓)
6. t : colist(T)
⊢ istype((is-list-approx(j) t)↓)

---

Latex:

---

Latex:

1.  T  :  Type
2.  j  :  \mBbbZ{}
3.  0  <  j
4.  \mlambda{}t,x.  Ax  \mmember{}  \mforall{}t:colist(T).  ((is-list-fun()\^{}j  -  1  \mbot{}  t)\mdownarrow{}  {}\mRightarrow{}  (||t||)\mdownarrow{})
\mvdash{}  \mlambda{}t,x.  Ax  \mmember{}  \mforall{}t:colist(T).  ((is-list-fun()\^{}j  \mbot{}  t)\mdownarrow{}  {}\mRightarrow{}  (||t||)\mdownarrow{})


By

---

Latex:
((Assert  \mforall{}t:colist(T).  ((is-list-fun()\^{}j  -  1  \mbot{}  t)\mdownarrow{}  {}\mRightarrow{}  (||t||)\mdownarrow{})  BY
                (UseWitness  \mkleeneopen{}\mlambda{}t,x.  Ax\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  Fold  `is-list-approx`  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto)))))

---

Home Index