---

Step * of Lemma lookup_omral_plus

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps,qs:|omral(g;r)|.  (((ps ++ qs)[k]) = ((ps[k]) +r (qs[k])) ∈ |r|)
BY
{ (ProveSpecializedLemma `lookup_merge` 2 [parm{i};g↓oset;r↓+gp
   ...
   THEN BLemma `cdrng_is_abdmonoid`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveSpecializedLemma  `lookup\_merge`  2  [parm\{i\};g\mdownarrow{}oset;r\mdownarrow{}+gp
  ...
  THEN  BLemma  `cdrng\_is\_abdmonoid`
  THEN  Auto)

---

Home Index