---

Step * 3 of Lemma word-equiv-equiv


1. [X] : Type
2. Sym((X + X) List;w1,w2.word-equiv(X;w1;w2))
3. a : (X + X) List
4. b : (X + X) List
5. c : (X + X) List
6. word-equiv(X;a;b)
7. word-equiv(X;b;c)
⊢ word-equiv(X;a;c)
BY
{ (All (RepUR  ``word-equiv``)⋅ THEN ExRepD) }

1
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
⊢ ∃w:(X + X) List. ((λx,y. word-rel(X;x;y)^* a w) ∧ (λx,y. word-rel(X;x;y)^* c w))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  Sym((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))
3.  a  :  (X  +  X)  List
4.  b  :  (X  +  X)  List
5.  c  :  (X  +  X)  List
6.  word-equiv(X;a;b)
7.  word-equiv(X;b;c)
\mvdash{}  word-equiv(X;a;c)


By

---

Latex:
(All  (RepUR    ``word-equiv``)\mcdot{}  THEN  ExRepD)

---

Home Index