---

Step * 3 of Lemma fma_from_gcp_wf

.....subterm..... T:t
2:n
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower_sig{i:l}(g↓set;r↓+gp)@i'
4. a : algebra{i:l}(r)@i'
5. (a↓grp) = c.grp ∈ GrpSig@i'
⊢ λa.(λh:|g| ⟶ a.car. c.umap (a↓grp) (λp:|g|. λv:|r|. a.act v (h p))) ∈ N:algebra{i:l}(r)
  ⟶ (|g| ⟶ N.car)
  ⟶ a.car
  ⟶ N.car
BY
{ ((RepeatMFor 2 MemCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower_sig{i:l}(g↓set;r↓+gp)@i'
4. a : algebra{i:l}(r)@i'
5. (a↓grp) = c.grp ∈ GrpSig@i'
6. a1 : algebra{i:l}(r)@i'
7. h : |g| ⟶ a1.car@i
⊢ c.umap (a1↓grp) (λp:|g|. λv:|r|. a1.act v (h p)) ∈ a.car ⟶ a1.car

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  g  :  GrpSig@i'
2.  r  :  RngSig@i'
3.  c  :  gcopower\_sig\{i:l\}(g\mdownarrow{}set;r\mdownarrow{}+gp)@i'
4.  a  :  algebra\{i:l\}(r)@i'
5.  (a\mdownarrow{}grp)  =  c.grp@i'
\mvdash{}  \mlambda{}a.(\mlambda{}h:|g|  {}\mrightarrow{}  a.car.  c.umap  (a\mdownarrow{}grp)  (\mlambda{}p:|g|.  \mlambda{}v:|r|.  a.act  v  (h  p)))  \mmember{}  N:algebra\{i:l\}(r)
    {}\mrightarrow{}  (|g|  {}\mrightarrow{}  N.car)
    {}\mrightarrow{}  a.car
    {}\mrightarrow{}  N.car


By

---

Latex:
((RepeatMFor  2  MemCD)  THENA  Auto)

---

Home Index