---

Step * 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. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
10. ∀w1:(X + X) List. word-equiv(X;w1;w1)
11. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
12. w1 : (X + X) List@i
13. w2 : (X + X) List@i
14. w : (X + X) List@i
15. λx,y. word-rel(X;x;y)^* w1 w
16. λx,y. word-rel(X;x;y)^* w2 w
⊢ (f w1) = (g w2) ∈ |G|
BY
{ ((Assert ⌜(((f w1) = (f w) ∈ |G|) ∧ ((g w2) = (g w) ∈ |G|)) ∧ ((f w) = (g w) ∈ |G|)⌝⋅ THENM Auto) THEN D 0) }

1
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
10. ∀w1:(X + X) List. word-equiv(X;w1;w1)
11. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
12. w1 : (X + X) List@i
13. w2 : (X + X) List@i
14. w : (X + X) List@i
15. λx,y. word-rel(X;x;y)^* w1 w
16. λx,y. word-rel(X;x;y)^* w2 w
⊢ ((f w1) = (f w) ∈ |G|) ∧ ((g w2) = (g w) ∈ |G|)

2
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
10. ∀w1:(X + X) List. word-equiv(X;w1;w1)
11. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
12. w1 : (X + X) List@i
13. w2 : (X + X) List@i
14. w : (X + X) List@i
15. λx,y. word-rel(X;x;y)^* w1 w
16. λx,y. word-rel(X;x;y)^* w2 w
⊢ (f w) = (g w) ∈ |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.  g  :  |free-group(X)|  {}\mrightarrow{}  |G|
6.  IsMonHom\{free-group(X),G\}(g)
7.  \mforall{}x:X.  ((f  free-letter(x))  =  (g  free-letter(x)))
8.  (X  +  X)  List  \mmember{}  Type
9.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
10.  \mforall{}w1:(X  +  X)  List.  word-equiv(X;w1;w1)
11.  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))
12.  w1  :  (X  +  X)  List@i
13.  w2  :  (X  +  X)  List@i
14.  w  :  (X  +  X)  List@i
15.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w
16.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w
\mvdash{}  (f  w1)  =  (g  w2)


By

---

Latex:
((Assert  \mkleeneopen{}(((f  w1)  =  (f  w))  \mwedge{}  ((g  w2)  =  (g  w)))  \mwedge{}  ((f  w)  =  (g  w))\mkleeneclose{}\mcdot{}  THENM  Auto)  THEN  D  0)

---

Home Index