---

Step * 2 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 : 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-join`` -1 THEN EqTypeHD (-1) THEN Auto THEN EqTypeCD THEN Auto THEN ThinTrivial) }

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. (y = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ y1 = ⊥ ∈ (ℕ ⟶ 𝔹)
16. (λn.((x n) ∨b(y n))) = ⊥ ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
17. λn.((x n) ∨b(y n)) ∈ ℕ ⟶ 𝔹
18. ⊥ ∈ ℕ ⟶ 𝔹
19. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
20. (λn.((x n) ∨b(y n))) = ⊥ ∈ (ℕ ⟶ 𝔹)
21. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ y = ⊥ ∈ (ℕ ⟶ 𝔹)

---

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


By

---

Latex:
TACTIC:(RepUR  ``sp-join``  -1  THEN  EqTypeHD  (-1)  THEN  Auto  THEN  EqTypeCD  THEN  Auto  THEN  ThinTrivial)

---

Home Index