---

Step * 1 2 1 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. 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)
BY
{ (D 0 With ⌜w5 @ w⌝  THEN Auto) }

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
8. λx,y. word-rel(X;x;y)^* w2 w
9. w5 : (X + X) List@i
10. λx,y. word-rel(X;x;y)^* w3 w5
11. λx,y. word-rel(X;x;y)^* w4 w5
⊢ λx,y. word-rel(X;x;y)^* (w3 @ w1) (w5 @ w)

2
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
8. λx,y. word-rel(X;x;y)^* w2 w
9. w5 : (X + X) List@i
10. λx,y. word-rel(X;x;y)^* w3 w5
11. λx,y. word-rel(X;x;y)^* w4 w5
12. λx,y. word-rel(X;x;y)^* (w3 @ w1) (w5 @ w)
⊢ λx,y. word-rel(X;x;y)^* (w4 @ w2) (w5 @ w)

---

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.  w  :  (X  +  X)  List@i
7.  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)
8.  w5  :  (X  +  X)  List@i
9.  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w3  w5)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w4  w5)
\mvdash{}  word-equiv(X;w3  @  w1;w4  @  w2)


By

---

Latex:
(D  0  With  \mkleeneopen{}w5  @  w\mkleeneclose{}    THEN  Auto)

---

Home Index