---

Step * of Lemma confluent-equiv-is-equiv

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Refl(T;x,y.R[x;y])
  ⇒ Trans(T;x,y.R[x;y])
  ⇒ rel-confluent(T;x,y.R[x;y])
  ⇒ EquivRel(T;a,b.confluent-equiv(T;x,y.R[x;y]) a b))
BY
{ (Auto THEN D 0 THEN Auto THEN D 0 THEN RepUR ``confluent-equiv`` 0 THEN Auto THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Refl(T;x,y.R[x;y])
4. Trans(T;x,y.R[x;y])
5. rel-confluent(T;x,y.R[x;y])
6. Sym(T;a,b.confluent-equiv(T;x,y.R[x;y]) a b)
7. a : T
8. b : T
9. c : T
10. w1 : T
11. R[a;w1]
12. R[b;w1]
13. w : T
14. R[b;w]
15. R[c;w]
⊢ ∃w:T. (R[a;w] ∧ R[c;w])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Refl(T;x,y.R[x;y])
    {}\mRightarrow{}  Trans(T;x,y.R[x;y])
    {}\mRightarrow{}  rel-confluent(T;x,y.R[x;y])
    {}\mRightarrow{}  EquivRel(T;a,b.confluent-equiv(T;x,y.R[x;y])  a  b))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  0  THEN  RepUR  ``confluent-equiv``  0  THEN  Auto  THEN  ExRepD)

---

Home Index