---

Step * 1 of Lemma markov-streamless-iff-not-not-enum


1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. T : Type
3. ∀x,y:T.  Dec(x = y ∈ T)
4. ¬¬(∃L:T List. ∀x:T. (x ∈ L))
⊢ streamless(T)
BY
{ xxx((D 0 THENA Auto) THEN InstHyp [⌜λ2i.∃j:ℕi. ((¬(i = j ∈ ℕ)) ∧ ((f i) = (f j) ∈ T))⌝] 1⋅ THEN Auto)xxx }

1
.....antecedent..... 
1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m)))
2. T : Type
3. ∀x,y:T.  Dec(x = y ∈ T)
4. ¬¬(∃L:T List. ∀x:T. (x ∈ L))
5. f : ℕ ⟶ T
⊢ ¬(∀m:ℕ. (¬(∃j:ℕm. ((¬(m = j ∈ ℕ)) ∧ ((f m) = (f j) ∈ T)))))

---

Latex:

---

Latex:

1.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}m:\mBbbN{}.  ((P  m)  \mvee{}  (\mneg{}(P  m))))  {}\mRightarrow{}  (\mneg{}(\mforall{}m:\mBbbN{}.  (\mneg{}(P  m))))  {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  (P  m)))
2.  T  :  Type
3.  \mforall{}x,y:T.    Dec(x  =  y)
4.  \mneg{}\mneg{}(\mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L))
\mvdash{}  streamless(T)


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}i.\mexists{}j:\mBbbN{}i.  ((\mneg{}(i  =  j))  \mwedge{}  ((f  i)  =  (f  j)))\mkleeneclose{}]  1\mcdot{}  THEN  Auto)xxx

---

Home Index