---

Step * 1 of Lemma fg-hom_wf

.....assertion..... 
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
⊢ ∀w2,w:(X + X) List.  ((λx,y. word-rel(X;x;y)^* w2 w) ⇒ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|))
BY
{ (Auto THEN RepUR ``transitive-reflexive-closure`` -1 THEN D -1) }

1
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. w2 = w3 ∈ ((X + X) List)
⊢ fg-hom(G;f;w2) = fg-hom(G;f;w3) ∈ |G|

2
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. w : free-word(X)
5. w2 : (X + X) List@i
6. w3 : (X + X) List@i
7. TC(λx,y. word-rel(X;x;y)) w2 w3
⊢ fg-hom(G;f;w2) = fg-hom(G;f;w3) ∈ |G|

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  w  :  free-word(X)
\mvdash{}  \mforall{}w2,w:(X  +  X)  List.    ((\mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w)  {}\mRightarrow{}  (fg-hom(G;f;w2)  =  fg-hom(G;f;w)))


By

---

Latex:
(Auto  THEN  RepUR  ``transitive-reflexive-closure``  -1  THEN  D  -1)

---

Home Index