---

Step * 1 of Lemma word-rel-append1


1. X : Type
2. w1 : (X + X) List
3. x : (X + X) List
4. y : (X + X) List
5. x@0 : X + X
6. y@0 : X + X
7. a : (X + X) List
8. b : (X + X) List
9. x@0 = -y@0
10. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
11. y = (a @ b) ∈ ((X + X) List)
⊢ ∃b:(X + X) List
   (x@0 = -y@0 ∧ ((x @ w1) = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)) ∧ ((y @ w1) = (a @ b) ∈ ((X + X) List)))
BY
{ (D 0 With ⌜b @ w1⌝  THEN Auto THEN RWO "-3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  w1  :  (X  +  X)  List
3.  x  :  (X  +  X)  List
4.  y  :  (X  +  X)  List
5.  x@0  :  X  +  X
6.  y@0  :  X  +  X
7.  a  :  (X  +  X)  List
8.  b  :  (X  +  X)  List
9.  x@0  =  -y@0
10.  x  =  (a  @  [x@0;  y@0]  @  b)
11.  y  =  (a  @  b)
\mvdash{}  \mexists{}b:(X  +  X)  List.  (x@0  =  -y@0  \mwedge{}  ((x  @  w1)  =  (a  @  [x@0;  y@0]  @  b))  \mwedge{}  ((y  @  w1)  =  (a  @  b)))


By

---

Latex:
(D  0  With  \mkleeneopen{}b  @  w1\mkleeneclose{}    THEN  Auto  THEN  RWO  "-3"  0  THEN  Auto)

---

Home Index