---

Step * 1 1 of Lemma not-d-CCC-nat


1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
⊢ False
BY
{ (Assert ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ))) BY
         (ParallelLast
          THEN ExRepD
          THEN ((Decide ⌜∃l:ℕn. 0 < h l⌝⋅ THENA Auto)
                THENL [((OrLeft THENA Auto) THEN ParallelLast)
                      ; (OrRight THEN Auto THEN (D -3 With ⌜l + 1⌝  THENM D -1) THEN Auto)]
          ))) }

1
1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
3. ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ)))
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  (g  n))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  (\muparrow{}(R  n  m))))
2.  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  ((\mexists{}l:\mBbbN{}n.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}m.  ((h  l)  =  0)))
\mvdash{}  False


By

---

Latex:
(Assert  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mexists{}l:\mBbbN{}.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}.  ((h  l)  =  0)))  BY
              (ParallelLast
                THEN  ExRepD
                THEN  ((Decide  \mkleeneopen{}\mexists{}l:\mBbbN{}n.  0  <  h  l\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THENL  [((OrLeft  THENA  Auto)  THEN  ParallelLast)
                                        ;  (OrRight  THEN  Auto  THEN  (D  -3  With  \mkleeneopen{}l  +  1\mkleeneclose{}    THENM  D  -1)  THEN  Auto)]
                )))

---

Home Index