---

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


1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
⊢ False
BY
{ (Assert ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ))) BY
         ((D 0 THENA Auto)
          THEN (Assert ∀n,m:ℕ.  Dec((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ))) BY
                      Auto)
          THEN RenameVar `d' (-1)
          THEN (D 1 With ⌜λn,m. isl(d n m)⌝  THENA Auto)
          THEN Reduce -1
          THEN (D -1
          THENM (RepeatFor 2 (ParallelLast)
                 THEN MoveToConcl (-1)
                 THEN (GenConclTerm ⌜d n m⌝⋅ THENA Auto)
                 THEN D -2
                 THEN Reduce 0
                 THEN Auto)
          )
          THEN Auto
          THEN ((Decide ⌜∃l:ℕg 0. 0 < h l⌝⋅ THENA Auto)
                THENL [(D 0 With ⌜g 0⌝ 
                        THEN Auto
                        THEN GenConclAtAddr [1;1]
                        THEN D -2
                        THEN Reduce 0
                        THEN Auto
                        THEN D -2
                        THEN Auto)
                      ; ((D 0 With ⌜0⌝  THENM GenConclAtAddr [1;1] THENM (D -2 THEN Reduce 0))
                         THEN Auto
                         THEN D -2
                         THEN (OrRight THEN Auto)
                         THEN SupposeNot
                         THEN D -5
                         THEN D 0 With ⌜l⌝ 
                         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 ∈ ℤ)))
⊢ 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))))
\mvdash{}  False


By

---

Latex:
(Assert  \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)))  BY
              ((D  0  THENA  Auto)
                THEN  (Assert  \mforall{}n,m:\mBbbN{}.    Dec((\mexists{}l:\mBbbN{}n.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}m.  ((h  l)  =  0)))  BY
                                        Auto)
                THEN  RenameVar  `d'  (-1)
                THEN  (D  1  With  \mkleeneopen{}\mlambda{}n,m.  isl(d  n  m)\mkleeneclose{}    THENA  Auto)
                THEN  Reduce  -1
                THEN  (D  -1
                THENM  (RepeatFor  2  (ParallelLast)
                              THEN  MoveToConcl  (-1)
                              THEN  (GenConclTerm  \mkleeneopen{}d  n  m\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  D  -2
                              THEN  Reduce  0
                              THEN  Auto)
                )
                THEN  Auto
                THEN  ((Decide  \mkleeneopen{}\mexists{}l:\mBbbN{}g  0.  0  <  h  l\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THENL  [(D  0  With  \mkleeneopen{}g  0\mkleeneclose{} 
                                            THEN  Auto
                                            THEN  GenConclAtAddr  [1;1]
                                            THEN  D  -2
                                            THEN  Reduce  0
                                            THEN  Auto
                                            THEN  D  -2
                                            THEN  Auto)
                                        ;  ((D  0  With  \mkleeneopen{}0\mkleeneclose{}    THENM  GenConclAtAddr  [1;1]  THENM  (D  -2  THEN  Reduce  0))
                                              THEN  Auto
                                              THEN  D  -2
                                              THEN  (OrRight  THEN  Auto)
                                              THEN  SupposeNot
                                              THEN  D  -5
                                              THEN  D  0  With  \mkleeneopen{}l\mkleeneclose{} 
                                              THEN  Auto)]
                )))

---

Home Index