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. 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