---

Step * 1 of Lemma sp-meet-is-top


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 : Base
9. y1 : Base
10. y = y1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. y ∈ ℕ ⟶ 𝔹
12. y1 ∈ ℕ ⟶ 𝔹
13. y = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
14. x ∧ y = ⊤ ∈ Sierpinski
⊢ x = ⊤ ∈ Sierpinski
BY
{ TACTIC:(RepUR ``sp-meet`` -1
          THEN EqTypeHD (-1)
          THEN Auto
          THEN EqTypeCD
          THEN Auto
          THEN BackThruSomeHyp
          THEN (RWO  "-1 -2" 0 THEN Auto)
          THEN RepUR ``Sierpinski-bottom`` 0
          THEN Ext
          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  :  Base
9.  y1  :  Base
10.  y  =  y1
11.  y  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
12.  y1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
13.  y  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  y1  =  \mbot{}
14.  x  \mwedge{}  y  =  \mtop{}
\mvdash{}  x  =  \mtop{}


By

---

Latex:
TACTIC:(RepUR  ``sp-meet``  -1
                THEN  EqTypeHD  (-1)
                THEN  Auto
                THEN  EqTypeCD
                THEN  Auto
                THEN  BackThruSomeHyp
                THEN  (RWO    "-1  -2"  0  THEN  Auto)
                THEN  RepUR  ``Sierpinski-bottom``  0
                THEN  Ext
                THEN  Reduce  0
                THEN  Auto)

---

Home Index