---

Step * 1 2 1 1 1 1 2 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)
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)
BY
{ (D -1 THEN FLemma `transitive-reflexive-closure_transitivity` [-1;-2] THEN Auto) }

---

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


By

---

Latex:
(D  -1  THEN  FLemma  `transitive-reflexive-closure\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index