---

Step * 2 of Lemma word-rel-confluent


1. [X] : Type
⊢ ∃m:((X + X) List) ⟶ ℕ. ∀x,y:(X + X) List.  (word-rel(X;x;y) ⇒ m y < m x)
BY
{ (D 0 With ⌜λw.||w||⌝  THEN Reduce 0 THEN Auto) }

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

---

Latex:

---

Latex:

1.  [X]  :  Type
\mvdash{}  \mexists{}m:((X  +  X)  List)  {}\mrightarrow{}  \mBbbN{}.  \mforall{}x,y:(X  +  X)  List.    (word-rel(X;x;y)  {}\mRightarrow{}  m  y  <  m  x)


By

---

Latex:
(D  0  With  \mkleeneopen{}\mlambda{}w.||w||\mkleeneclose{}    THEN  Reduce  0  THEN  Auto)

---

Home Index