---

Step * 1 of Lemma word-rel-diamond


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)))
BY
{ ((Assert (a1 @ [x@0; y@0] @ b1) = (a @ [x1; y1] @ b) ∈ ((X + X) List) BY
          Eq)
   THEN (SubstFor ⌜y⌝ 0⋅ THENA Auto)
   THEN (SubstFor ⌜z⌝ 0⋅ THENA Auto)) }

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)
21. (a1 @ [x@0; y@0] @ b1) = (a @ [x1; y1] @ b) ∈ ((X + X) List)
⊢ ((a1 @ b1) = (a @ b) ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;a1 @ b1;w) ∧ word-rel(X;a @ b;w)))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  n  :  \mBbbN{}
3.  x  :  (X  +  X)  List
4.  \mforall{}x1:(X  +  X)  List
          (||x1||  <  ||x||
          {}\mRightarrow{}  (\mforall{}y,z:(X  +  X)  List.
                      (word-rel(X;x1;y)
                      {}\mRightarrow{}  word-rel(X;x1;z)
                      {}\mRightarrow{}  ((y  =  z)  \mvee{}  (\mexists{}w:(X  +  X)  List.  (word-rel(X;y;w)  \mwedge{}  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)
13.  y  =  (a1  @  b1)
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)
20.  z  =  (a  @  b)
\mvdash{}  (y  =  z)  \mvee{}  (\mexists{}w:(X  +  X)  List.  (word-rel(X;y;w)  \mwedge{}  word-rel(X;z;w)))


By

---

Latex:
((Assert  (a1  @  [x@0;  y@0]  @  b1)  =  (a  @  [x1;  y1]  @  b)  BY
                Eq)
  THEN  (SubstFor  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (SubstFor  \mkleeneopen{}z\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index