---

Step * of Lemma word-rel-append1

∀X:Type. ∀w1,x,y:(X + X) List.  (word-rel(X;x;y) ⇒ word-rel(X;x @ w1;y @ w1))
BY
{ (Auto THEN RepeatFor 4 (ParallelLast) THEN ExRepD) }

1
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)))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}w1,x,y:(X  +  X)  List.    (word-rel(X;x;y)  {}\mRightarrow{}  word-rel(X;x  @  w1;y  @  w1))


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast)  THEN  ExRepD)

---

Home Index