---

Step * of Lemma word-rel-append2

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

1
1. X : Type@i'
2. w1 : (X + X) List@i
3. x : (X + X) List@i
4. y : (X + X) List@i
5. x@0 : X + X@i
6. y@0 : X + X@i
7. a : (X + X) List@i
8. b : (X + X) List@i
9. x@0 = -y@0
10. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
11. y = (a @ b) ∈ ((X + X) List)
⊢ ∃a,b:(X + X) List
   (x@0 = -y@0 ∧ ((w1 @ x) = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)) ∧ ((w1 @ y) = (a @ b) ∈ ((X + X) List)))

---

Latex:

---

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


By

---

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

---

Home Index