---

Step * of Lemma transitive-reflexive-closure-cases

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x R^* y) ⇒ ((x = y ∈ A) ∨ (∃z:A. ((x R z) ∧ (z R^* y)))))
BY
{ ((Auto THEN RepUR ``transitive-reflexive-closure`` -1)
   THEN ParallelLast
   THEN (FLemma `transitive-closure-cases` [-1] THENA Auto)
   THEN D -1) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. x : A
4. y : A
5. TC(R) x y
6. x R y
⊢ ∃z:A. ((x R z) ∧ (z R^* y))

2
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. x : A
4. y : A
5. TC(R) x y
6. ∃z:A. ((x R z) ∧ (z TC(R) y))
⊢ ∃z:A. ((x R z) ∧ (z R^* y))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:A.    ((x  R\^{}*  y)  {}\mRightarrow{}  ((x  =  y)  \mvee{}  (\mexists{}z:A.  ((x  R  z)  \mwedge{}  (z  R\^{}*  y)))))


By

---

Latex:
((Auto  THEN  RepUR  ``transitive-reflexive-closure``  -1)
  THEN  ParallelLast
  THEN  (FLemma  `transitive-closure-cases`  [-1]  THENA  Auto)
  THEN  D  -1)

---

Home Index