---

Step * 3 1 1 of Lemma word-equiv-equiv


1. [X] : Type
2. Sym((X + X) List;w1,w2.∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* w1 w) ∧ (λx,y. word-rel(X;x;y)^* w2 w)))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. w1 : (X + X) List
7. λx,y. word-rel(X;x;y)^* a w1
8. λx,y. word-rel(X;x;y)^* b w1
9. w : (X + X) List
10. λx,y. word-rel(X;x;y)^* b w
11. λx,y. word-rel(X;x;y)^* c w
12. z : (X + X) List
13. λx,y. word-rel(X;x;y)^* w z
14. λx,y. word-rel(X;x;y)^* w1 z
⊢ λx,y. word-rel(X;x;y)^* a z
BY
{ (FLemma `transitive-reflexive-closure_transitivity` [7;-1] THEN Auto) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  Sym((X  +  X)  List;w1,w2.\mexists{}w:(X  +  X)  List
                                                      ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w)  \mwedge{}  (\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)))
3.  a  :  (X  +  X)  List
4.  b  :  (X  +  X)  List
5.  c  :  (X  +  X)  List
6.  w1  :  (X  +  X)  List
7.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  a  w1
8.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w1
9.  w  :  (X  +  X)  List
10.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  b  w
11.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  c  w
12.  z  :  (X  +  X)  List
13.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w  z
14.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  z
\mvdash{}  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  a  z


By

---

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

---

Home Index