---

Step * of Lemma omral_plus_assoc

∀g:OCMon. ∀r:CDRng. ∀ps,qs,rs:|omral(g;r)|.  ((ps ++ (qs ++ rs)) = ((ps ++ qs) ++ rs) ∈ |omral(g;r)|)
BY
{ ProveSpecializedLemma `oal_merge_assoc` 2 [parm{i};g↓oset;r↓+gp
... }

1
.....wf..... 
1. g : OCMon
2. r : CDRng
⊢ r↓+gp ∈ AbDMon

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps,qs,rs:|omral(g;r)|.    ((ps  ++  (qs  ++  rs))  =  ((ps  ++  qs)  ++  rs))


By

---

Latex:
ProveSpecializedLemma  `oal\_merge\_assoc`  2  [parm\{i\};g\mdownarrow{}oset;r\mdownarrow{}+gp
...

---

Home Index