---

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

.....subterm..... T:t
2:n
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. ∀[a1,a2:free-word(X)].  ((f a1 + a2) = ((f a1) * (f a2)) ∈ |G|)
5. (f 0) = e ∈ |G|
6. g : |free-group(X)| ⟶ |G|
7. ∀[a1,a2:free-word(X)].  ((g a1 + a2) = ((g a1) * (g a2)) ∈ |G|)
8. (g 0) = e ∈ |G|
9. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
10. (X + X) List ∈ Type
11. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
12. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
13. u : X + X@i
14. v : (X + X) List@i
15. (f v) = (g v) ∈ |G|
⊢ (f [u]) = (g [u]) ∈ |G|
BY
{ DVar `u' }

1
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. ∀[a1,a2:free-word(X)].  ((f a1 + a2) = ((f a1) * (f a2)) ∈ |G|)
5. (f 0) = e ∈ |G|
6. g : |free-group(X)| ⟶ |G|
7. ∀[a1,a2:free-word(X)].  ((g a1 + a2) = ((g a1) * (g a2)) ∈ |G|)
8. (g 0) = e ∈ |G|
9. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
10. (X + X) List ∈ Type
11. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
12. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
13. x : X@i
14. v : (X + X) List@i
15. (f v) = (g v) ∈ |G|
⊢ (f [inl x]) = (g [inl x]) ∈ |G|

2
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. ∀[a1,a2:free-word(X)].  ((f a1 + a2) = ((f a1) * (f a2)) ∈ |G|)
5. (f 0) = e ∈ |G|
6. g : |free-group(X)| ⟶ |G|
7. ∀[a1,a2:free-word(X)].  ((g a1 + a2) = ((g a1) * (g a2)) ∈ |G|)
8. (g 0) = e ∈ |G|
9. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
10. (X + X) List ∈ Type
11. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
12. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
13. y : X@i
14. v : (X + X) List@i
15. (f v) = (g v) ∈ |G|
⊢ (f [inr y ]) = (g [inr y ]) ∈ |G|

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  f  :  |free-group(X)|  {}\mrightarrow{}  |G|
4.  \mforall{}[a1,a2:free-word(X)].    ((f  a1  +  a2)  =  ((f  a1)  *  (f  a2)))
5.  (f  0)  =  e
6.  g  :  |free-group(X)|  {}\mrightarrow{}  |G|
7.  \mforall{}[a1,a2:free-word(X)].    ((g  a1  +  a2)  =  ((g  a1)  *  (g  a2)))
8.  (g  0)  =  e
9.  \mforall{}x:X.  ((f  free-letter(x))  =  (g  free-letter(x)))
10.  (X  +  X)  List  \mmember{}  Type
11.  \mforall{}[a:free-word(X)].  ((f  free-word-inv(a))  =  (\msim{}  (f  a)))
12.  \mforall{}[a:free-word(X)].  ((g  free-word-inv(a))  =  (\msim{}  (g  a)))
13.  u  :  X  +  X@i
14.  v  :  (X  +  X)  List@i
15.  (f  v)  =  (g  v)
\mvdash{}  (f  [u])  =  (g  [u])


By

---

Latex:
DVar  `u'

---

Home Index