---

Step * of Lemma word-rel-diamond

∀[X:Type]
  ∀x,y,z:(X + X) List.
    (word-rel(X;x;y)
    ⇒ word-rel(X;x;z)
    ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))
BY
{ (InductionOnLength THEN Auto THEN D -2 THEN D -1 THEN ExRepD) }

1
1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. a1 : (X + X) List
10. b1 : (X + X) List
11. x@0 = -y@0
12. x = (a1 @ [x@0; y@0] @ b1) ∈ ((X + X) List)
13. y = (a1 @ b1) ∈ ((X + X) List)
14. x1 : X + X
15. y1 : X + X
16. a : (X + X) List
17. b : (X + X) List
18. x1 = -y1
19. x = (a @ [x1; y1] @ b) ∈ ((X + X) List)
20. z = (a @ b) ∈ ((X + X) List)
⊢ (y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}x,y,z:(X  +  X)  List.
        (word-rel(X;x;y)
        {}\mRightarrow{}  word-rel(X;x;z)
        {}\mRightarrow{}  ((y  =  z)  \mvee{}  (\mexists{}w:(X  +  X)  List.  (word-rel(X;y;w)  \mwedge{}  word-rel(X;z;w)))))


By

---

Latex:
(InductionOnLength  THEN  Auto  THEN  D  -2  THEN  D  -1  THEN  ExRepD)

---

Home Index