---

Step * 1 1 1 of Lemma free-word-inv_wf


1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. λx,y. word-rel(X;x;y)^* w1 w
10. λx,y. word-rel(X;x;y)^* w2 w
11. free-word(X) = free-word(X) ∈ Type
12. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
13. u : (X + X) List@i
14. v : (X + X) List@i
15. x : X + X@i
16. y : X + X@i
17. a : (X + X) List@i
18. b : (X + X) List@i
19. x = -y
20. u = (a @ [x; y] @ b) ∈ ((X + X) List)
21. v = (a @ b) ∈ ((X + X) List)
⊢ ∃x,y:X + X
   ∃a,b:(X + X) List
    (x = -y ∧ (free-word-inv(u) = (a @ [x; y] @ b) ∈ ((X + X) List)) ∧ (free-word-inv(v) = (a @ b) ∈ ((X + X) List)))
BY
{ (InstConcl [⌜x⌝;⌜y⌝;⌜free-word-inv(b)⌝;⌜free-word-inv(a)⌝]⋅ THEN Auto) }

1
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. λx,y. word-rel(X;x;y)^* w1 w
10. λx,y. word-rel(X;x;y)^* w2 w
11. free-word(X) = free-word(X) ∈ Type
12. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
13. u : (X + X) List@i
14. v : (X + X) List@i
15. x : X + X@i
16. y : X + X@i
17. a : (X + X) List@i
18. b : (X + X) List@i
19. x = -y
20. u = (a @ [x; y] @ b) ∈ ((X + X) List)
21. v = (a @ b) ∈ ((X + X) List)
22. x = -y
⊢ free-word-inv(u) = (free-word-inv(b) @ [x; y] @ free-word-inv(a)) ∈ ((X + X) List)

2
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. w : (X + X) List@i
9. λx,y. word-rel(X;x;y)^* w1 w
10. λx,y. word-rel(X;x;y)^* w2 w
11. free-word(X) = free-word(X) ∈ Type
12. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
13. u : (X + X) List@i
14. v : (X + X) List@i
15. x : X + X@i
16. y : X + X@i
17. a : (X + X) List@i
18. b : (X + X) List@i
19. x = -y
20. u = (a @ [x; y] @ b) ∈ ((X + X) List)
21. v = (a @ b) ∈ ((X + X) List)
22. x = -y
23. free-word-inv(u) = (free-word-inv(b) @ [x; y] @ free-word-inv(a)) ∈ ((X + X) List)
⊢ free-word-inv(v) = (free-word-inv(b) @ free-word-inv(a)) ∈ ((X + X) List)

---

Latex:

---

Latex:

1.  X  :  Type
2.  (X  +  X)  List  \mmember{}  Type
3.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
4.  \mforall{}w1:(X  +  X)  List.  word-equiv(X;w1;w1)
5.  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))
6.  w1  :  (X  +  X)  List@i
7.  w2  :  (X  +  X)  List@i
8.  w  :  (X  +  X)  List@i
9.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w
10.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w
11.  free-word(X)  =  free-word(X)
12.  \mforall{}w:(X  +  X)  List.  (free-word-inv(w)  \mmember{}  (X  +  X)  List)
13.  u  :  (X  +  X)  List@i
14.  v  :  (X  +  X)  List@i
15.  x  :  X  +  X@i
16.  y  :  X  +  X@i
17.  a  :  (X  +  X)  List@i
18.  b  :  (X  +  X)  List@i
19.  x  =  -y
20.  u  =  (a  @  [x;  y]  @  b)
21.  v  =  (a  @  b)
\mvdash{}  \mexists{}x,y:X  +  X
      \mexists{}a,b:(X  +  X)  List
        (x  =  -y  \mwedge{}  (free-word-inv(u)  =  (a  @  [x;  y]  @  b))  \mwedge{}  (free-word-inv(v)  =  (a  @  b)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}free-word-inv(b)\mkleeneclose{};\mkleeneopen{}free-word-inv(a)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index