---

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


1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
⊢ λn.(B n) ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
BY
{ ((Assert B ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g) BY Declaration) THEN D 3) }

1
1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B = B1 ∈ (f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
6. B ∈ ℕ ⟶ ℕ ⟶ 𝔹
7. B1 ∈ ℕ ⟶ ℕ ⟶ 𝔹
8. fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);B;B1)
9. B ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
⊢ (λn.(B n)) = (λn.(B1 n)) ∈ (f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))

2
.....aux..... 
1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
⊢ istype((B ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ (B1 ∈ ℕ ⟶ ℕ ⟶ 𝔹) ∧ fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);B;B1))

---

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  :  f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)
\mvdash{}  \mlambda{}n.(B  n)  \mmember{}  f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)


By

---

Latex:
((Assert  B  \mmember{}  f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)  BY  Declaration)  THEN  D  3)

---

Home Index