---

Step * 1 2 1 1 1 1 2 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
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)
BY
{ Assert ⌜(λx,y. word-rel(X;x;y)^* (w4 @ w2) (w5 @ w2)) ∧ (λx,y. word-rel(X;x;y)^* (w5 @ w2) (w5 @ w))⌝⋅ }

1
.....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
12. λx,y. word-rel(X;x;y)^* (w3 @ w1) (w5 @ w)
⊢ (λx,y. word-rel(X;x;y)^* (w4 @ w2) (w5 @ w2)) ∧ (λx,y. word-rel(X;x;y)^* (w5 @ w2) (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)
13. (λx,y. word-rel(X;x;y)^* (w4 @ w2) (w5 @ w2)) ∧ (λx,y. word-rel(X;x;y)^* (w5 @ w2) (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
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
12.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  (w3  @  w1)  (w5  @  w)
\mvdash{}  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  (w4  @  w2)  (w5  @  w)


By

---

Latex:
Assert  \mkleeneopen{}(\mlambda{}x,y.  word-rel(X;x;y)\^{}*  (w4  @  w2)  (w5  @  w2))  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  (w5  @  w2)  (w5  @  w))\000C\mkleeneclose{}\mcdot{}

---

Home Index