---

Step * 1 1 1 1 1 of Lemma sp-lub-is-bottom


1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B
= B1
∈ pertype(λf,g. ((f ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)))
6. B ∈ ℕ ⟶ ℕ ⟶ 𝔹
7. B1 ∈ ℕ ⟶ ℕ ⟶ 𝔹
8. fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);B;B1)
9. (λn.let i,j = coded-pair(n) 
       in B[i] j)
= (λn.ff)
∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
10. λn.let i,j = coded-pair(n) 
       in B[i] j ∈ ℕ ⟶ 𝔹
11. λn.ff ∈ ℕ ⟶ 𝔹
12. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in B[i] j)
⊢ ∀n1:ℕ. (¬↑(B[n] n1))
BY
{ TACTIC:(Auto THEN RenameVar `m' (-1) THEN SupposeNot) }

1
1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B
= B1
∈ pertype(λf,g. ((f ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)))
6. B ∈ ℕ ⟶ ℕ ⟶ 𝔹
7. B1 ∈ ℕ ⟶ ℕ ⟶ 𝔹
8. fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);B;B1)
9. (λn.let i,j = coded-pair(n) 
       in B[i] j)
= (λn.ff)
∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
10. λn.let i,j = coded-pair(n) 
       in B[i] j ∈ ℕ ⟶ 𝔹
11. λn.ff ∈ ℕ ⟶ 𝔹
12. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in B[i] j)
13. m : ℕ
14. ¬¬↑(B[n] m)
⊢ ¬↑(B[n] m)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  EquivRel(\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{};f,g.fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))
3.  B  :  Base
4.  B1  :  Base
5.  B  =  B1
6.  B  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
7.  B1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
8.  fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};B;B1)
9.  (\mlambda{}n.let  i,j  =  coded-pair(n)  in  B[i]  j)  =  (\mlambda{}n.ff)
10.  \mlambda{}n.let  i,j  =  coded-pair(n) 
              in  B[i]  j  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
11.  \mlambda{}n.ff  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
12.  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  i,j  =  coded-pair(n)  in  B[i]  j)
\mvdash{}  \mforall{}n1:\mBbbN{}.  (\mneg{}\muparrow{}(B[n]  n1))


By

---

Latex:
TACTIC:(Auto  THEN  RenameVar  `m'  (-1)  THEN  SupposeNot)

---

Home Index