---

Step * 1 1 1 1 1 1 1 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. f : ℕ ⟶ T
5. ∀m:ℕ. (¬(∃j:ℕm. ((¬(m = j ∈ ℕ)) ∧ ((f m) = (f j) ∈ T))))
6. L : T List
7. ∀x:T. (x ∈ L)
8. ∀i:ℕ. ∃j:ℕ||L||. ((f i) = L[j] ∈ T)
9. g : i:ℕ ⟶ ℕ||L||
10. ∀i:ℕ. ((f i) = L[g i] ∈ T)
11. a1 : ℕ
12. a2 : ℕ
13. (g a1) = (g a2) ∈ ℕ||L||
14. (f a1) = (f a2) ∈ T
15. a1 < a2
⊢ a1 = a2 ∈ ℕ
BY
{ xxxOnMaybeHyp 5 (\h. ((InstHyp [⌜a2⌝] h⋅ THENM (D -1 THEN With ⌜a1⌝ (D 0) ⋅)) THEN Complete (Auto)))xxx }

---

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.  f  :  \mBbbN{}  {}\mrightarrow{}  T
5.  \mforall{}m:\mBbbN{}.  (\mneg{}(\mexists{}j:\mBbbN{}m.  ((\mneg{}(m  =  j))  \mwedge{}  ((f  m)  =  (f  j)))))
6.  L  :  T  List
7.  \mforall{}x:T.  (x  \mmember{}  L)
8.  \mforall{}i:\mBbbN{}.  \mexists{}j:\mBbbN{}||L||.  ((f  i)  =  L[j])
9.  g  :  i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}||L||
10.  \mforall{}i:\mBbbN{}.  ((f  i)  =  L[g  i])
11.  a1  :  \mBbbN{}
12.  a2  :  \mBbbN{}
13.  (g  a1)  =  (g  a2)
14.  (f  a1)  =  (f  a2)
15.  a1  <  a2
\mvdash{}  a1  =  a2


By

---

Latex:
xxxOnMaybeHyp  5  (\mbackslash{}h.
((InstHyp  [\mkleeneopen{}a2\mkleeneclose{}]  h\mcdot{}  THENM  (D  -1  THEN  With  \mkleeneopen{}a1\mkleeneclose{}  (D  0)  \mcdot{}))  THEN  Complete  (Auto)))xxx

---

Home Index