---

Step * 1 1 2 1 2 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. J : ℕ
5. K : ℕ
6. ∀b:ℕ ⟶ ℕ ⋂ Base. (((λb.(M (λa.(b (a J))))) b) = J ∈ ℕ)
⊢ False
BY
{ TACTIC:((InstHyp [⌜λx.x⌝] (-1)⋅ THENA Auto) THEN Reduce (-1)) }

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. K : ℕ
6. ∀b:ℕ ⟶ ℕ ⋂ Base. (((λb.(M (λa.(b (a J))))) b) = J ∈ ℕ)
7. (M (λa.(a J))) = J ∈ ℕ
⊢ False

---

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.  J  :  \mBbbN{}
5.  K  :  \mBbbN{}
6.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  (((\mlambda{}b.(M  (\mlambda{}a.(b  (a  J)))))  b)  =  J)
\mvdash{}  False


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index