---

Step * 1 of Lemma fg-hom-append


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|
BY
{ (MoveToConcl (-1)
   THEN Unfold `fg-hom` 0
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "-2" 0 THENA Auto)
   THEN (RWO  "mon_assoc" 0 THENM EqCD)
   THEN Auto
   THEN RW GrpNormC 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  Unfold  `fg-hom`  0
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "-2"  0  THENA  Auto)
  THEN  (RWO    "mon\_assoc"  0  THENM  EqCD)
  THEN  Auto
  THEN  RW  GrpNormC  0
  THEN  Auto)

---

Home Index