---

Step * of Lemma omral_times_assoc

∀g:OCMon. ∀a:CDRng.  Assoc(|omral(g;a)|;λps,qs. (ps ** qs))
BY
{ (Force `5` (Eval ``assoc`` 0) 
   THEN RenameBVars [`x',`ps';`y',`qs';`z',`rs'] 0 
   THEN ((RepD) THENA Auto)
   THEN (Assert g ∈ DMon BY
               (BLemma `omon_inc` THEN Auto))
   THEN PromoteHyp (-1) 2) }

1
1. g : OCMon
2. g ∈ DMon
3. a : CDRng
4. ps : |omral(g;a)|
5. qs : |omral(g;a)|
6. rs : |omral(g;a)|
⊢ (ps ** (qs ** rs)) = ((ps ** qs) ** rs) ∈ |omral(g;a)|

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a:CDRng.    Assoc(|omral(g;a)|;\mlambda{}ps,qs.  (ps  **  qs))


By

---

Latex:
(Force  `5`  (Eval  ``assoc``  0) 
  THEN  RenameBVars  [`x',`ps';`y',`qs';`z',`rs']  0 
  THEN  ((RepD)  THENA  Auto)
  THEN  (Assert  g  \mmember{}  DMon  BY
                          (BLemma  `omon\_inc`  THEN  Auto))
  THEN  PromoteHyp  (-1)  2)

---

Home Index