---

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

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. b1 : (X + X) List
10. x@0 = -y@0
11. x = [x@0; [y@0 / b1]] ∈ ((X + X) List)
12. y = b1 ∈ ((X + X) List)
13. x1 : X + X
14. y1 : X + X
15. u : X + X
16. u1 : X + X
17. v : (X + X) List
18. b : (X + X) List
19. x1 = -y1
20. x = [u; [u1 / (v @ [x1; [y1 / b]])]] ∈ ((X + X) List)
21. z = [u; [u1 / (v @ b)]] ∈ ((X + X) List)
22. x@0 = u ∈ (X + X)
23. y@0 = u1 ∈ (X + X)
24. b1 = (v @ [x1; [y1 / b]]) ∈ ((X + X) List)
⊢ ∃x,y:X + X
   ∃a,b@0:(X + X) List. (x = -y ∧ (b1 = (a @ [x; y] @ b@0) ∈ ((X + X) List)) ∧ ((v @ b) = (a @ b@0) ∈ ((X + X) List)))

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. b1 : (X + X) List
10. x@0 = -y@0
11. x = [x@0; [y@0 / b1]] ∈ ((X + X) List)
12. y = b1 ∈ ((X + X) List)
13. x1 : X + X
14. y1 : X + X
15. u : X + X
16. u1 : X + X
17. v : (X + X) List
18. b : (X + X) List
19. x1 = -y1
20. x = [u; [u1 / (v @ [x1; [y1 / b]])]] ∈ ((X + X) List)
21. z = [u; [u1 / (v @ b)]] ∈ ((X + X) List)
22. x@0 = u ∈ (X + X)
23. y@0 = u1 ∈ (X + X)
24. b1 = (v @ [x1; [y1 / b]]) ∈ ((X + X) List)
25. word-rel(X;b1;v @ b)
⊢ ∃x,y:X + X
   ∃a,b@0:(X + X) List
    (x = -y ∧ ([u; [u1 / (v @ b)]] = (a @ [x; y] @ b@0) ∈ ((X + X) List)) ∧ ((v @ b) = (a @ b@0) ∈ ((X + X) List)))

---

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


By

---

Latex:
((OrRight  THENA  Auto)  THEN  (D  0  With  \mkleeneopen{}v  @  b\mkleeneclose{}    THEN  Auto)  THEN  Unfold  `word-rel`  0)

---

Home Index