---

Step * 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 : f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
4. lub(n.B[n]) = ⊥ ∈ Sierpinski
⊢ B[n] = ⊥ ∈ Sierpinski
BY
{ TACTIC:(D 3
          THEN Unfold `Sierpinski-bottom` 0
          THEN (EqTypeCD THENA Auto)
          THEN RepUR ``sp-lub Sierpinski-bottom`` -2
          THEN (EqTypeHD (-2) THENA Auto)
          THEN Thin (-1)
          THEN (RepeatFor 2 (D -1) THENA Auto)
          THEN Thin (-2)
          THEN All (\h. TACTIC:((RWO "equal-Sierpinski-bottom" h THENA Auto)
                                THEN Reduce h
                                THEN (RWW "assert-b-exists" h THENA Auto)))⋅) }

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)
⊢ ∀n1:ℕ. (¬↑(B[n] n1))

---

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)
4.  lub(n.B[n])  =  \mbot{}
\mvdash{}  B[n]  =  \mbot{}


By

---

Latex:
TACTIC:(D  3
                THEN  Unfold  `Sierpinski-bottom`  0
                THEN  (EqTypeCD  THENA  Auto)
                THEN  RepUR  ``sp-lub  Sierpinski-bottom``  -2
                THEN  (EqTypeHD  (-2)  THENA  Auto)
                THEN  Thin  (-1)
                THEN  (RepeatFor  2  (D  -1)  THENA  Auto)
                THEN  Thin  (-2)
                THEN  All  (\mbackslash{}h.  TACTIC:((RWO  "equal-Sierpinski-bottom"  h  THENA  Auto)
                                                            THEN  Reduce  h
                                                            THEN  (RWW  "assert-b-exists"  h  THENA  Auto)))\mcdot{})

---

Home Index