---

Step * 3 of Lemma sp-join-is-bottom


1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
5. x ∈ ℕ ⟶ 𝔹
6. x1 ∈ ℕ ⟶ 𝔹
7. x = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. y : Sierpinski
9. x = ⊥ ∈ Sierpinski
10. y = ⊥ ∈ Sierpinski
⊢ x ∨ y = ⊥ ∈ Sierpinski
BY
{ TACTIC:((RWO "-1 -2" 0 THENA Auto)
          THEN All Thin
          THEN RepUR ``sp-join Sierpinski-bottom`` 0
          THEN EqTypeCD
          THEN Auto
          THEN BLemma `equal-Sierpinski-bottom`
          THEN Auto
          THEN Reduce 0
          THEN (RWO "b-exists-bfalse" 0 THENA Auto)
          THEN Reduce 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  (\mbot{}  =  \mtop{})  {}\mRightarrow{}  False
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  x1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
7.  x  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  x1  =  \mbot{}
8.  y  :  Sierpinski
9.  x  =  \mbot{}
10.  y  =  \mbot{}
\mvdash{}  x  \mvee{}  y  =  \mbot{}


By

---

Latex:
TACTIC:((RWO  "-1  -2"  0  THENA  Auto)
                THEN  All  Thin
                THEN  RepUR  ``sp-join  Sierpinski-bottom``  0
                THEN  EqTypeCD
                THEN  Auto
                THEN  BLemma  `equal-Sierpinski-bottom`
                THEN  Auto
                THEN  Reduce  0
                THEN  (RWO  "b-exists-bfalse"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  Auto)

---

Home Index