---

Step * 2 1 of Lemma word-rel-confluent


1. X : Type
2. x : (X + X) List
3. y : (X + X) List
4. word-rel(X;x;y)
⊢ ||y|| < ||x||
BY
{ (BLemma `word-rel-length` THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  x  :  (X  +  X)  List
3.  y  :  (X  +  X)  List
4.  word-rel(X;x;y)
\mvdash{}  ||y||  <  ||x||


By

---

Latex:
(BLemma  `word-rel-length`  THEN  Auto)

---

Home Index