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` [parm{i};g↓oset;r↓+gp
... }

1
.....wf..... 
1. OCMon
2. 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