---

Step * 1 1 1 1 1 1 1 1 of Lemma free-group-generators


1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. (X + X) List ∈ Type
6. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
7. ∀w1:(X + X) List. word-equiv(X;w1;w1)
8. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
9. w1 : (X + X) List@i
10. w : (X + X) List@i
11. TC(λx,y. word-rel(X;x;y)) w1 w
12. x : (X + X) List@i
13. y : (X + X) List@i
14. word-rel(X;x;y)
⊢ (f x) = (f y) ∈ |G|
BY
{ (D -1 THEN ExRepD THEN (RWO "-1 -2" 0 THENA Auto)) }

1
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. (X + X) List ∈ Type
6. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
7. ∀w1:(X + X) List. word-equiv(X;w1;w1)
8. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
9. w1 : (X + X) List@i
10. w : (X + X) List@i
11. TC(λx,y. word-rel(X;x;y)) w1 w
12. x : (X + X) List@i
13. y : (X + X) List@i
14. x@0 : X + X@i
15. y@0 : X + X@i
16. a : (X + X) List@i
17. b : (X + X) List@i
18. x@0 = -y@0
19. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
20. y = (a @ b) ∈ ((X + X) List)
⊢ (f (a @ [x@0; y@0] @ b)) = (f (a @ b)) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  f  :  |free-group(X)|  {}\mrightarrow{}  |G|
4.  IsMonHom\{free-group(X),G\}(f)
5.  (X  +  X)  List  \mmember{}  Type
6.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
7.  \mforall{}w1:(X  +  X)  List.  word-equiv(X;w1;w1)
8.  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))
9.  w1  :  (X  +  X)  List@i
10.  w  :  (X  +  X)  List@i
11.  TC(\mlambda{}x,y.  word-rel(X;x;y))  w1  w
12.  x  :  (X  +  X)  List@i
13.  y  :  (X  +  X)  List@i
14.  word-rel(X;x;y)
\mvdash{}  (f  x)  =  (f  y)


By

---

Latex:
(D  -1  THEN  ExRepD  THEN  (RWO  "-1  -2"  0  THENA  Auto))

---

Home Index