---

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

(∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m))))
⇒ (∀T:Type. (streamless(T) ⇐⇒ (∀x,y:T.  Dec(x = y ∈ T)) ∧ (¬¬(∃L:T List. ∀x:T. (x ∈ L)))))
BY
{ xxx(Auto
      THEN Try ((BLemma `streamless-dec-equal` THEN Auto))
      THEN Try ((BLemma `streamless-implies-not-not-enum` THEN Auto)))xxx }

1
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)

---

Latex:

---

Latex:
(\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))))
{}\mRightarrow{}  (\mforall{}T:Type.  (streamless(T)  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  =  y))  \mwedge{}  (\mneg{}\mneg{}(\mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L)))))


By

---

Latex:
xxx(Auto
        THEN  Try  ((BLemma  `streamless-dec-equal`  THEN  Auto))
        THEN  Try  ((BLemma  `streamless-implies-not-not-enum`  THEN  Auto)))xxx

---

Home Index