---

Step * 2 of Lemma red-black-example


1. [A] : Type
2. [D] : Type
3. [Red] : D ⟶ ℙ
4. [Black] : D ⟶ ℙ
5. [R] : D ⟶ D ⟶ ℙ
6. ∀x:D. (Red[x] ∨ Black[x])
7. ∀x,y,z:D.  (R[x;y] ⇒ R[y;z] ⇒ R[x;z])
8. ∀x:D. (R[x;x] ⇒ A)
9. ∀x:D. (Red[x] ⇒ (∃y:D. (Black[y] ∧ R[x;y])))
10. ∀x:D. (Black[x] ⇒ (∃y:D. (Red[y] ∧ R[x;y])))
11. m : D
12. ∀x:D. (Red[x] ⇒ R[x;m])
13. Black[m]
⊢ A
BY
{ (((FHyp 10 [-1] THENM ExRepD) THEN Auto) THEN (Assert R[y;m] BY Auto) THEN (Assert R[m;m] BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [D]  :  Type
3.  [Red]  :  D  {}\mrightarrow{}  \mBbbP{}
4.  [Black]  :  D  {}\mrightarrow{}  \mBbbP{}
5.  [R]  :  D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}x:D.  (Red[x]  \mvee{}  Black[x])
7.  \mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  R[y;z]  {}\mRightarrow{}  R[x;z])
8.  \mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A)
9.  \mforall{}x:D.  (Red[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Black[y]  \mwedge{}  R[x;y])))
10.  \mforall{}x:D.  (Black[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Red[y]  \mwedge{}  R[x;y])))
11.  m  :  D
12.  \mforall{}x:D.  (Red[x]  {}\mRightarrow{}  R[x;m])
13.  Black[m]
\mvdash{}  A


By

---

Latex:
(((FHyp  10  [-1]  THENM  ExRepD)  THEN  Auto)
  THEN  (Assert  R[y;m]  BY
                          Auto)
  THEN  (Assert  R[m;m]  BY
                          Auto)
  THEN  Auto)

---

Home Index