---

Step * of Lemma omral_scale_non_zero_vals

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `cdrng_is_abdmonoid` [⌜r⌝]⋅ THENA Auto)
   THEN InductionOnListA
   THEN Reduce 0) }

1
1. g : OCMon
2. r : CDRng
3. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
4. k : |g|
5. v : |r|
⊢ (¬False) ⇒ (¬False)

2
1. g : OCMon
2. r : CDRng
3. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
4. k : |g|
5. v : |r|
6. p : |g| × |r|
7. ps : (|g| × |r|) List
8. (¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps)))
⊢ (¬↑(((snd(p)) =b 0) ∨b(0 ∈b map(λx.(snd(x));ps)))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));<k,v>* [p / ps])))

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k:|g|.  \mforall{}v:|r|.  \mforall{}ps:(|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));<k,v>*  ps))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `cdrng\_is\_abdmonoid`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InductionOnListA
  THEN  Reduce  0)

---

Home Index