---

Step * 1 2 1 of Lemma fg-hom_wf


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
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
⊢ fg-hom(G;f;w2) = fg-hom(G;f;w3) ∈ |G|
BY
{ (InstLemma `transitive-closure-minimal` 
   [⌜(X + X) List⌝;⌜λx,y. word-rel(X;x;y)⌝;⌜λx,y. (fg-hom(G;f;x) = fg-hom(G;f;y) ∈ |G|)⌝]⋅
   THENA Auto
   ) }

1
.....antecedent..... 
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
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
⊢ λx,y. word-rel(X;x;y) => λx,y. (fg-hom(G;f;x) = fg-hom(G;f;y) ∈ |G|)

2
.....antecedent..... 
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
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
⊢ Trans((X + X) List;x,y.x (λx,y. (fg-hom(G;f;x) = fg-hom(G;f;y) ∈ |G|)) y)

3
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
8. ∀x:(X + X) List. (fg-hom(G;f;x) ∈ |G|)
9. TC(λx,y. word-rel(X;x;y)) => λx,y. (fg-hom(G;f;x) = fg-hom(G;f;y) ∈ |G|)
⊢ fg-hom(G;f;w2) = fg-hom(G;f;w3) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  w  :  free-word(X)
5.  w2  :  (X  +  X)  List@i
6.  w3  :  (X  +  X)  List@i
7.  TC(\mlambda{}x,y.  word-rel(X;x;y))  w2  w3
8.  \mforall{}x:(X  +  X)  List.  (fg-hom(G;f;x)  \mmember{}  |G|)
\mvdash{}  fg-hom(G;f;w2)  =  fg-hom(G;f;w3)


By

---

Latex:
(InstLemma  `transitive-closure-minimal` 
  [\mkleeneopen{}(X  +  X)  List\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  word-rel(X;x;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (fg-hom(G;f;x)  =  fg-hom(G;f;y))\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index