---

Step * 2 1 of Lemma fg-hom_wf


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. (X + X) List ∈ Type
5. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
6. ∀w1:(X + X) List. word-equiv(X;w1;w1)
7. ∀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|))
8. w1 : (X + X) List@i
9. w2 : (X + X) List@i
10. w : (X + X) List@i
11. λx,y. word-rel(X;x;y)^* w1 w
12. λx,y. word-rel(X;x;y)^* w2 w
⊢ fg-hom(G;f;w1) = fg-hom(G;f;w2) ∈ |G|
BY
{ (Assert ⌜(fg-hom(G;f;w1) = fg-hom(G;f;w) ∈ |G|) ∧ (fg-hom(G;f;w2) = fg-hom(G;f;w) ∈ |G|)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  (X  +  X)  List  \mmember{}  Type
5.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
6.  \mforall{}w1:(X  +  X)  List.  word-equiv(X;w1;w1)
7.  \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)))
8.  w1  :  (X  +  X)  List@i
9.  w2  :  (X  +  X)  List@i
10.  w  :  (X  +  X)  List@i
11.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w1  w
12.  \mlambda{}x,y.  word-rel(X;x;y)\^{}*  w2  w
\mvdash{}  fg-hom(G;f;w1)  =  fg-hom(G;f;w2)


By

---

Latex:
(Assert  \mkleeneopen{}(fg-hom(G;f;w1)  =  fg-hom(G;f;w))  \mwedge{}  (fg-hom(G;f;w2)  =  fg-hom(G;f;w))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index