---

Step * of Lemma word-rel-confluent

No Annotations
∀[X:Type]
  ∀b,w1,w:(X + X) List.
    ((λx,y. word-rel(X;x;y)^* b w1)
    ⇒ (λx,y. word-rel(X;x;y)^* b w)
    ⇒ (∃z:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 z) ∧ (λx,y. word-rel(X;x;y)^* w z))))
BY
{ (Fold `rel-confluent` 0 THEN (D 0 THENA Auto) THEN BLemma `diamond-implies-TC-confluent` THEN Auto) }

1
1. [X] : Type
⊢ rel-diamond-property((X + X) List;x,y.word-rel(X;x;y))

2
1. [X] : Type
⊢ ∃m:((X + X) List) ⟶ ℕ. ∀x,y:(X + X) List.  (word-rel(X;x;y) ⇒ m y < m x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type]
    \mforall{}b,w1,w:(X  +  X)  List.
        ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w1)
        {}\mRightarrow{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w)
        {}\mRightarrow{}  (\mexists{}z:(X  +  X)  List.  ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  z)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w  z))))


By

---

Latex:
(Fold  `rel-confluent`  0  THEN  (D  0  THENA  Auto)  THEN  BLemma  `diamond-implies-TC-confluent`  THEN  Auto)

---

Home Index