---

Step * 2 of Lemma omral_scale_non_zero_vals


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])))
BY
{ ((New [`kq';`vq'] (OnVar `p' D)  
THENM AbReduce 0 THENM RW bool_to_propC 0 
THENM D 0 THENM RWH (LemmaC `not_over_or`) (-1)) THENA Auto)⋅ }

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

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  (r\mdownarrow{}+gp  \mmember{}  AbDMon)  \mwedge{}  (r\mdownarrow{}xmn  \mmember{}  AbDMon)
4.  k  :  |g|
5.  v  :  |r|
6.  p  :  |g|  \mtimes{}  |r|
7.  ps  :  (|g|  \mtimes{}  |r|)  List
8.  (\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)))
\mvdash{}  (\mneg{}\muparrow{}(((snd(p))  =\msubb{}  0)  \mvee{}\msubb{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps))))  {}\mRightarrow{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));<k,v>*  [p  /  ps])))


By

---

Latex:
((New  [`kq';`vq']  (OnVar  `p'  D)   
THENM  AbReduce  0  THENM  RW  bool\_to\_propC  0 
THENM  D  0  THENM  RWH  (LemmaC  `not\_over\_or`)  (-1))  THENA  Auto)\mcdot{}

---

Home Index