---

Step * of Lemma fg-hom-append

∀[X:Type]. ∀[G:Group{i}]. ∀[f:X ⟶ |G|]. ∀[a,b:(X + X) List].
  (fg-hom(G;f;a @ b) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|)
BY
{ (Auto
   THEN Unfold `fg-hom` 0
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN Fold `fg-hom` 0
   THEN (GenConcl ⌜fg-hom(G;f;a) = x ∈ |G|⌝⋅ THENA (Auto THEN RepUR ``fg-hom`` 0 THEN Auto))
   THEN ThinVar `a') }

1
1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. b : (X + X) List
5. x : |G|@i
⊢ accumulate (with value x and list item u):
   x * case u of inl(a) => f a | inr(b) => ~ (f b)
  over list:
    b
  with starting value:
   x)
= (x * fg-hom(G;f;b))
∈ |G|

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[G:Group\{i\}].  \mforall{}[f:X  {}\mrightarrow{}  |G|].  \mforall{}[a,b:(X  +  X)  List].
    (fg-hom(G;f;a  @  b)  =  (fg-hom(G;f;a)  *  fg-hom(G;f;b)))


By

---

Latex:
(Auto
  THEN  Unfold  `fg-hom`  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  Fold  `fg-hom`  0
  THEN  (GenConcl  \mkleeneopen{}fg-hom(G;f;a)  =  x\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  RepUR  ``fg-hom``  0  THEN  Auto))
  THEN  ThinVar  `a')

---

Home Index