---

Step * of Lemma diamond-implies-TC-confluent

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (rel-diamond-property(T;x,y.R[x;y])
  ⇒ (∃m:T ⟶ ℕ. ∀x,y:T.  (R[x;y] ⇒ m y < m x))
  ⇒ rel-confluent(T;x,y.λx,y. R[x;y]^* x y))
BY
{ (Auto THEN UnfoldTopAb 0) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. rel-diamond-property(T;x,y.R[x;y])
4. ∃m:T ⟶ ℕ. ∀x,y:T.  (R[x;y] ⇒ m y < m x)
⊢ ∀x,y,z:T.  ((λx,y. R[x;y]^* x y) ⇒ (λx,y. R[x;y]^* x z) ⇒ (∃w:T. ((λx,y. R[x;y]^* y w) ∧ (λx,y. R[x;y]^* z w))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (rel-diamond-property(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mexists{}m:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  m  y  <  m  x))
    {}\mRightarrow{}  rel-confluent(T;x,y.\mlambda{}x,y.  R[x;y]\^{}*  x  y))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0)

---

Home Index