---

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


1. X : Type
2. G : Group{i}@i'
3. g : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(g)
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. w2 : (X + X) List@i
10. w : (X + X) List@i
11. TC(λx,y. word-rel(X;x;y)) w2 w
12. x : (X + X) List@i
13. y : (X + X) List@i
14. word-rel(X;x;y)
⊢ (g x) = (g y) ∈ |G|
BY
{ (D -1
   THEN ExRepD
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN Fold `free-append` 0
   THEN RepUR ``free-group monoid_hom_p fun_thru_2op`` 4
   THEN D 4
   THEN (RWW "4" 0 THENA Auto)
   THEN (Subst' (g [x@0; y@0]) = e ∈ |G| 0 THENM (RW GrpNormC 0 THEN Auto))
   THEN Auto) }

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

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  g  :  |free-group(X)|  {}\mrightarrow{}  |G|
4.  IsMonHom\{free-group(X),G\}(g)
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.  w2  :  (X  +  X)  List@i
10.  w  :  (X  +  X)  List@i
11.  TC(\mlambda{}x,y.  word-rel(X;x;y))  w2  w
12.  x  :  (X  +  X)  List@i
13.  y  :  (X  +  X)  List@i
14.  word-rel(X;x;y)
\mvdash{}  (g  x)  =  (g  y)


By

---

Latex:
(D  -1
  THEN  ExRepD
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  Fold  `free-append`  0
  THEN  RepUR  ``free-group  monoid\_hom\_p  fun\_thru\_2op``  4
  THEN  D  4
  THEN  (RWW  "4"  0  THENA  Auto)
  THEN  (Subst'  (g  [x@0;  y@0])  =  e  0  THENM  (RW  GrpNormC  0  THEN  Auto))
  THEN  Auto)

---

Home Index