---

Step * 2 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
⊢ y = ⊤ ∈ 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) }

1
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. (x = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ x1 = ⊥ ∈ (ℕ ⟶ 𝔹)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
12. y ∈ ℕ ⟶ 𝔹
13. y1 ∈ ℕ ⟶ 𝔹
14. (y = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. (λn.let x@0,y@0 = coded-pair(n) 
        in (x x@0) ∧b (y y@0))
= ⊤
∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
16. λn.let x@0,y@0 = coded-pair(n) 
       in (x x@0) ∧b (y y@0) ∈ ℕ ⟶ 𝔹
17. ⊤ ∈ ℕ ⟶ 𝔹
18. ((λn.let x@0,y@0 = coded-pair(n) in (x x@0) ∧b (y y@0)) = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (⊤ = ⊥ ∈ (ℕ ⟶ 𝔹))
19. ((λn.let x@0,y@0 = coded-pair(n) in (x x@0) ∧b (y y@0)) = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ ⊤ = ⊥ ∈ (ℕ ⟶ 𝔹)
20. y = ⊥ ∈ (ℕ ⟶ 𝔹)
21. y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
22. x2 : ℕ
⊢ let x@0,y@0 = coded-pair(x2) in (x x@0) ∧b ff = ff

---

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{}  y  =  \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