---

Step * of Lemma red-black-example

No Annotations
∀[A,D:Type]. ∀[Red,Black:D ⟶ ℙ]. ∀[R:D ⟶ D ⟶ ℙ].
  ((∀x:D. (Red[x] ∨ Black[x]))
  ⇒ (∀x,y,z:D.  (R[x;y] ⇒ R[y;z] ⇒ R[x;z]))
  ⇒ (∀x:D. (R[x;x] ⇒ A))
  ⇒ (∀x:D. (Red[x] ⇒ (∃y:D. (Black[y] ∧ R[x;y]))))
  ⇒ (∀x:D. (Black[x] ⇒ (∃y:D. (Red[y] ∧ R[x;y]))))
  ⇒ (∃m:D. ((∀x:D. (Red[x] ⇒ R[x;m])) ∨ (∀x:D. (Black[x] ⇒ R[x;m]))))
  ⇒ A)
BY
{ ((Auto THEN ExRepD) THEN D -1 THEN (InstHyp [⌜m⌝] 6⋅ THENA Auto) THEN D -1) }

1
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. Red[m]
⊢ A

2
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

3
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. (Black[x] ⇒ R[x;m])
13. Red[m]
⊢ A

4
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. (Black[x] ⇒ R[x;m])
13. Black[m]
⊢ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,D:Type].  \mforall{}[Red,Black:D  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:D  {}\mrightarrow{}  D  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:D.  (Red[x]  \mvee{}  Black[x]))
    {}\mRightarrow{}  (\mforall{}x,y,z:D.    (R[x;y]  {}\mRightarrow{}  R[y;z]  {}\mRightarrow{}  R[x;z]))
    {}\mRightarrow{}  (\mforall{}x:D.  (R[x;x]  {}\mRightarrow{}  A))
    {}\mRightarrow{}  (\mforall{}x:D.  (Red[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Black[y]  \mwedge{}  R[x;y]))))
    {}\mRightarrow{}  (\mforall{}x:D.  (Black[x]  {}\mRightarrow{}  (\mexists{}y:D.  (Red[y]  \mwedge{}  R[x;y]))))
    {}\mRightarrow{}  (\mexists{}m:D.  ((\mforall{}x:D.  (Red[x]  {}\mRightarrow{}  R[x;m]))  \mvee{}  (\mforall{}x:D.  (Black[x]  {}\mRightarrow{}  R[x;m]))))
    {}\mRightarrow{}  A)


By

---

Latex:
((Auto  THEN  ExRepD)  THEN  D  -1  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index