---

Step * 1 1 2 1 1 1 of Lemma unsquashed-weak-continuity-base-false


1. M : Base
2. M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕM F. ((a i) = 0 ∈ ℕ)) ⇒ ((F a) = (F (λx.0)) ∈ ℕ))
4. ∀a:ℕ ⟶ ℕ ⋂ Base
     ((∀i:ℕM (λb.(M (λf.(b (f (M (λn.0))))))). ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f (M (λn.0)))))) = (M (λf.0)) ∈ ℕ))
⊢ ∃J,K:ℕ. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))
BY
{ TACTIC:(MoveToConcl (-1)
          THEN (GenConcl ⌜(M (λn.0)) = J ∈ ℕ⌝⋅ THENA Auto)
          THEN (GenConcl ⌜(M (λb.(M (λf.(b (f J)))))) = K ∈ ℕ⌝⋅ THENA (Auto THEN ∀h:hyp. Isect2HD h  THEN Auto))) }

1
1. M : Base
2. M ∈ ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base ⟶ ℕ
3. ∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base. ∀a:ℕ ⟶ ℕ ⋂ Base.  ((∀i:ℕM F. ((a i) = 0 ∈ ℕ)) ⇒ ((F a) = (F (λx.0)) ∈ ℕ))
4. J : ℕ
5. (M (λn.0)) = J ∈ ℕ
6. K : ℕ
7. (M (λb.(M (λf.(b (f J)))))) = K ∈ ℕ
⊢ (∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f J)))) = J ∈ ℕ)))
⇒ (∃J,K:ℕ. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f J)))) = J ∈ ℕ)))

---

Latex:

---

Latex:

1.  M  :  Base
2.  M  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}
3.  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.    ((\mforall{}i:\mBbbN{}M  F.  ((a  i)  =  0))  {}\mRightarrow{}  ((F  a)  =  (F  (\mlambda{}x.0))))
4.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base
          ((\mforall{}i:\mBbbN{}M  (\mlambda{}b.(M  (\mlambda{}f.(b  (f  (M  (\mlambda{}n.0))))))).  ((a  i)  =  0))
          {}\mRightarrow{}  ((M  (\mlambda{}f.(a  (f  (M  (\mlambda{}n.0))))))  =  (M  (\mlambda{}f.0))))
\mvdash{}  \mexists{}J,K:\mBbbN{}.  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  ((\mforall{}i:\mBbbN{}K.  ((a  i)  =  0))  {}\mRightarrow{}  ((M  (\mlambda{}f.(a  (f  J))))  =  J))


By

---

Latex:
TACTIC:(MoveToConcl  (-1)
                THEN  (GenConcl  \mkleeneopen{}(M  (\mlambda{}n.0))  =  J\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}(M  (\mlambda{}b.(M  (\mlambda{}f.(b  (f  J))))))  =  K\mkleeneclose{}\mcdot{}
                            THENA  (Auto  THEN  \mforall{}h:hyp.  Isect2HD  h    THEN  Auto)
                            ))

---

Home Index