---

Step * 2 1 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. (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 = ⊥ ∈ (ℕ ⟶ 𝔹)
BY
{ TACTIC:((RWO "equal-Sierpinski-bottom" (-2) THENA Auto)
          THEN (Reduce (-2) THEN (RW assert_pushdownC (-2) THENA Auto))
          THEN BLemma `equal-Sierpinski-bottom`
          THEN Auto
          THEN (InstHyp [⌜n⌝] (-3)⋅ THENA 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. (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)) ∨ (↑(y n))))
21. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
22. n : ℕ@i
23. ¬((↑(x n)) ∨ (↑(y n)))
⊢ ¬↑(y n)

---

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{})  {}\mRightarrow{}  (x1  =  \mbot{})
8.  (x  =  \mbot{})  \mLeftarrow{}{}  x1  =  \mbot{}
9.  y  :  Base
10.  y1  :  Base
11.  y  =  y1
12.  y  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
13.  y1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
14.  (y  =  \mbot{})  {}\mRightarrow{}  (y1  =  \mbot{})
15.  (y  =  \mbot{})  \mLeftarrow{}{}  y1  =  \mbot{}
16.  (\mlambda{}n.((x  n)  \mvee{}\msubb{}(y  n)))  =  \mbot{}
17.  \mlambda{}n.((x  n)  \mvee{}\msubb{}(y  n))  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
18.  \mbot{}  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
19.  \mbot{}  =  \mbot{}
20.  (\mlambda{}n.((x  n)  \mvee{}\msubb{}(y  n)))  =  \mbot{}
21.  \mbot{}  =  \mbot{}
\mvdash{}  y  =  \mbot{}


By

---

Latex:
TACTIC:((RWO  "equal-Sierpinski-bottom"  (-2)  THENA  Auto)
                THEN  (Reduce  (-2)  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto))
                THEN  BLemma  `equal-Sierpinski-bottom`
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))

---

Home Index