---

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

.....assertion..... 
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 @ w1)) ∧ (λx,y. word-rel(X;x;y)^* (w5 @ w1) (w5 @ w))
BY
{ D 0 }

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 @ w1)

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
⊢ λx,y. word-rel(X;x;y)^* (w5 @ w1) (w5 @ w)

---

Latex:

---

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


By

---

Latex:
D  0

---

Home Index