---

Step * of Lemma omral_plus_non_zero_vals

∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.
  ((¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));qs))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));ps ++ qs))))
BY
{ ProveSpecializedLemma `oal_merge_non_id_vals` 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:(|g|  \mtimes{}  |r|)  List.
    ((\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
    {}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));qs)))
    {}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps  ++  qs))))


By

---

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

---

Home Index