---

Step * 1 1 2 1 2 2 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. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))
7. 0 < K
8. (M (λf.if f J <z K then 0 else 1 fi )) = J ∈ ℕ
⊢ False
BY
{ TACTIC:((InstHyp [⌜λg.((λn.if n <z K then 0 else 1 fi ) (g J))⌝] 3⋅ THENA (Auto THEN ∀h:hyp. Isect2HD h  THEN 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. ∀a:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕK. ((a i) = 0 ∈ ℕ)) ⇒ ((M (λf.(a (f J)))) = J ∈ ℕ))
7. 0 < K
8. (M (λf.if f J <z K then 0 else 1 fi )) = J ∈ ℕ
9. ∀a:ℕ ⟶ ℕ ⋂ Base
     ((∀i:ℕM (λg.if g J <z K then 0 else 1 fi ). ((a i) = 0 ∈ ℕ))
     ⇒ (if a J <z K then 0 else 1 fi  = if 0 <z K then 0 else 1 fi  ∈ ℕ))
⊢ 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{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  \mcap{}  Base.  ((\mforall{}i:\mBbbN{}K.  ((a  i)  =  0))  {}\mRightarrow{}  ((M  (\mlambda{}f.(a  (f  J))))  =  J))
7.  0  <  K
8.  (M  (\mlambda{}f.if  f  J  <z  K  then  0  else  1  fi  ))  =  J
\mvdash{}  False


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}\mlambda{}g.((\mlambda{}n.if  n  <z  K  then  0  else  1  fi  )  (g  J))\mkleeneclose{}]  3\mcdot{}
                  THENA  (Auto  THEN  \mforall{}h:hyp.  Isect2HD  h    THEN  Auto)
                  )
                THEN  Reduce  (-1)
                )

---

Home Index