---

Step * 2 1 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)) ∨ (↑(y n))))
21. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
22. n : ℕ@i
23. ¬((↑(x n)) ∨ (↑(y n)))
⊢ ¬↑(y n)
BY
{ TACTIC:(ParallelLast 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{})  {}\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.  \mforall{}n:\mBbbN{}.  (\mneg{}((\muparrow{}(x  n))  \mvee{}  (\muparrow{}(y  n))))
21.  \mbot{}  =  \mbot{}
22.  n  :  \mBbbN{}@i
23.  \mneg{}((\muparrow{}(x  n))  \mvee{}  (\muparrow{}(y  n)))
\mvdash{}  \mneg{}\muparrow{}(y  n)


By

---

Latex:
TACTIC:(ParallelLast  THEN  Auto)

---

Home Index