---

Step * 2 1 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. 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 ))
BY
{ ((SplitOnConclITE THENM AbReduce 0) THENA Auto) }

1
.....truecase..... 
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)))
11. (v * vq) = 0 ∈ |r|
⊢ ¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps))

2
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)))
11. ¬((v * vq) = 0 ∈ |r|)
⊢ ¬↑(((v * vq) =b 0) ∨b(0 ∈b map(λx.(snd(x));<k,v>* ps)))

---

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.  kq  :  |g|
7.  vq  :  |r|
8.  ps  :  (|g|  \mtimes{}  |r|)  List
9.  (\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)))
10.  (\mneg{}(vq  =  0))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
\mvdash{}  \mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));if  (v  *  vq)  =\msubb{}  0
                            then  <k,v>*  ps
                            else  [<k  *  kq,  v  *  vq>  /  (<k,v>*  ps)]
                            fi  ))


By

---

Latex:
((SplitOnConclITE  THENM  AbReduce  0)  THENA  Auto)

---

Home Index