---

Step * 3 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 : Sierpinski
9. x = ⊤ ∈ Sierpinski
10. y = ⊤ ∈ Sierpinski
⊢ x ∧ y = ⊤ ∈ Sierpinski
BY
{ TACTIC:((RWO "-1 -2" 0 THENA Auto)
          THEN All Thin
          THEN RepUR ``sp-meet Sierpinski-top`` 0
          THEN EqTypeCD
          THEN Auto
          THEN All (\h. TACTIC:((RWO "equal-Sierpinski-bottom" h THENA Auto) THEN Reduce h))⋅
          THEN (InstHyp [⌜code-pair(1;1)⌝] (-1)⋅ THEN Auto)
          THEN (RWO "coded-code-pair" (-1) THENA Auto)
          THEN Reduce (-1)
          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  =  \mtop{}
10.  y  =  \mtop{}
\mvdash{}  x  \mwedge{}  y  =  \mtop{}


By

---

Latex:
TACTIC:((RWO  "-1  -2"  0  THENA  Auto)
                THEN  All  Thin
                THEN  RepUR  ``sp-meet  Sierpinski-top``  0
                THEN  EqTypeCD
                THEN  Auto
                THEN  All  (\mbackslash{}h.  TACTIC:((RWO  "equal-Sierpinski-bottom"  h  THENA  Auto)  THEN  Reduce  h))\mcdot{}
                THEN  (InstHyp  [\mkleeneopen{}code-pair(1;1)\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                THEN  (RWO  "coded-code-pair"  (-1)  THENA  Auto)
                THEN  Reduce  (-1)
                THEN  Auto)

---

Home Index