---

Step * 1 2 1 1 1 of Lemma free-append_wf


1. X : Type@i'
2. w1 : (X + X) List@i
3. w2 : (X + X) List@i
4. w3 : (X + X) List@i
5. w4 : (X + X) List@i
6. word-equiv(X;w1;w2)
7. word-equiv(X;w3;w4)
⊢ word-equiv(X;w3 @ w1;w4 @ w2)
BY
{ (D -2 THEN D -1) }

1
1. X : Type@i'
2. w1 : (X + X) List@i
3. w2 : (X + X) List@i
4. w3 : (X + X) List@i
5. w4 : (X + X) List@i
6. w : (X + X) List@i
7. (λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w)
8. w5 : (X + X) List@i
9. (λx,y. word-rel(X;x;y)^* w3 w5) ∧ (λx,y. word-rel(X;x;y)^* w4 w5)
⊢ word-equiv(X;w3 @ w1;w4 @ w2)

---

Latex:

---

Latex:

1.  X  :  Type@i'
2.  w1  :  (X  +  X)  List@i
3.  w2  :  (X  +  X)  List@i
4.  w3  :  (X  +  X)  List@i
5.  w4  :  (X  +  X)  List@i
6.  word-equiv(X;w1;w2)
7.  word-equiv(X;w3;w4)
\mvdash{}  word-equiv(X;w3  @  w1;w4  @  w2)


By

---

Latex:
(D  -2  THEN  D  -1)

---

Home Index