Step
*
2
1
1
of Lemma
markov-streamless-function
1. ∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) 
⇒ (¬(∀m:ℕ. (¬(P m)))) 
⇒ (∃m:ℕ. (P m)))
2. A : Type
3. B : Type
4. a : ℕ
5. A ~ ℕa
6. ∀x,y:B.  Dec(x = y ∈ B)
7. ∀x,y:A ⟶ B.  Dec(x = y ∈ (A ⟶ B))
8. b : ℕ
9. B ~ ℕb
⊢ A ⟶ B ~ ℕb^a
BY
{ xxx((RWO "equipollent-exp<" 0 THEN Auto)
      THEN (RWO "9" 0 THENA Auto)
      THEN (RWO "5" 0 THENA Auto)
      THEN RelRST
      THEN 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.  A  :  Type
3.  B  :  Type
4.  a  :  \mBbbN{}
5.  A  \msim{}  \mBbbN{}a
6.  \mforall{}x,y:B.    Dec(x  =  y)
7.  \mforall{}x,y:A  {}\mrightarrow{}  B.    Dec(x  =  y)
8.  b  :  \mBbbN{}
9.  B  \msim{}  \mBbbN{}b
\mvdash{}  A  {}\mrightarrow{}  B  \msim{}  \mBbbN{}b\^{}a
By
Latex:
xxx((RWO  "equipollent-exp<"  0  THEN  Auto)
        THEN  (RWO  "9"  0  THENA  Auto)
        THEN  (RWO  "5"  0  THENA  Auto)
        THEN  RelRST
        THEN  Auto)xxx
Home
Index