---

Step * 1 1 4 4 2 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. u : X + X
10. v : (X + X) List
11. b1 : (X + X) List
12. x@0 = -y@0
13. x = [u / (v @ [x@0; [y@0 / b1]])] ∈ ((X + X) List)
14. y = [u / (v @ b1)] ∈ ((X + X) List)
15. x1 : X + X
16. y1 : X + X
17. u1 : X + X
18. v1 : (X + X) List
19. b : (X + X) List
20. x1 = -y1
21. x = [u1 / (v1 @ [x1; [y1 / b]])] ∈ ((X + X) List)
22. z = [u1 / (v1 @ b)] ∈ ((X + X) List)
23. u = u1 ∈ (X + X)
24. (v @ [x@0; [y@0 / b1]]) = (v1 @ [x1; [y1 / b]]) ∈ ((X + X) List)
25. ∃w:(X + X) List. (word-rel(X;v @ b1;w) ∧ word-rel(X;v1 @ b;w))
⊢ ∃w:(X + X) List. (word-rel(X;[u / (v @ b1)];w) ∧ word-rel(X;[u1 / (v1 @ b)];w))
BY
{ ((D -1 THEN D 0 With ⌜[u / w]⌝ ) THEN 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. u : X + X
10. v : (X + X) List
11. b1 : (X + X) List
12. x@0 = -y@0
13. x = [u / (v @ [x@0; [y@0 / b1]])] ∈ ((X + X) List)
14. y = [u / (v @ b1)] ∈ ((X + X) List)
15. x1 : X + X
16. y1 : X + X
17. u1 : X + X
18. v1 : (X + X) List
19. b : (X + X) List
20. x1 = -y1
21. x = [u1 / (v1 @ [x1; [y1 / b]])] ∈ ((X + X) List)
22. z = [u1 / (v1 @ b)] ∈ ((X + X) List)
23. u = u1 ∈ (X + X)
24. (v @ [x@0; [y@0 / b1]]) = (v1 @ [x1; [y1 / b]]) ∈ ((X + X) List)
25. w : (X + X) List
26. word-rel(X;v @ b1;w)
27. word-rel(X;v1 @ b;w)
⊢ word-rel(X;[u / (v @ b1)];[u / w])

2
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. u : X + X
10. v : (X + X) List
11. b1 : (X + X) List
12. x@0 = -y@0
13. x = [u / (v @ [x@0; [y@0 / b1]])] ∈ ((X + X) List)
14. y = [u / (v @ b1)] ∈ ((X + X) List)
15. x1 : X + X
16. y1 : X + X
17. u1 : X + X
18. v1 : (X + X) List
19. b : (X + X) List
20. x1 = -y1
21. x = [u1 / (v1 @ [x1; [y1 / b]])] ∈ ((X + X) List)
22. z = [u1 / (v1 @ b)] ∈ ((X + X) List)
23. u = u1 ∈ (X + X)
24. (v @ [x@0; [y@0 / b1]]) = (v1 @ [x1; [y1 / b]]) ∈ ((X + X) List)
25. w : (X + X) List
26. word-rel(X;v @ b1;w)
27. word-rel(X;v1 @ b;w)
28. word-rel(X;[u / (v @ b1)];[u / w])
⊢ word-rel(X;[u1 / (v1 @ b)];[u / 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.  u  :  X  +  X
10.  v  :  (X  +  X)  List
11.  b1  :  (X  +  X)  List
12.  x@0  =  -y@0
13.  x  =  [u  /  (v  @  [x@0;  [y@0  /  b1]])]
14.  y  =  [u  /  (v  @  b1)]
15.  x1  :  X  +  X
16.  y1  :  X  +  X
17.  u1  :  X  +  X
18.  v1  :  (X  +  X)  List
19.  b  :  (X  +  X)  List
20.  x1  =  -y1
21.  x  =  [u1  /  (v1  @  [x1;  [y1  /  b]])]
22.  z  =  [u1  /  (v1  @  b)]
23.  u  =  u1
24.  (v  @  [x@0;  [y@0  /  b1]])  =  (v1  @  [x1;  [y1  /  b]])
25.  \mexists{}w:(X  +  X)  List.  (word-rel(X;v  @  b1;w)  \mwedge{}  word-rel(X;v1  @  b;w))
\mvdash{}  \mexists{}w:(X  +  X)  List.  (word-rel(X;[u  /  (v  @  b1)];w)  \mwedge{}  word-rel(X;[u1  /  (v1  @  b)];w))


By

---

Latex:
((D  -1  THEN  D  0  With  \mkleeneopen{}[u  /  w]\mkleeneclose{}  )  THEN  Auto)

---

Home Index