---

Step * 1 1 of Lemma omral_scale_dom_pred


1. g : OCMon
2. r : CDRng
3. Q : |g| ⟶ 𝔹
4. k : |g|
5. v : |r|
6. kp : |g|
7. vp : |r|
8. ps : (|g| × |r|) List
9. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
        Q[k * x])
10. ↑Q[k * (fst(<kp, vp>))]
11. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps)
         Q[x])
⊢ ↑(∀bx(:|g|) ∈ map(λz.(fst(z));if (v * vp) =b 0 then <k,v>* ps else [<k * kp, v * vp> / (<k,v>* ps)] fi )
       Q[x])
BY
{ ((SplitOnConclITE THENM Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  Q  :  |g|  {}\mrightarrow{}  \mBbbB{}
4.  k  :  |g|
5.  v  :  |r|
6.  kp  :  |g|
7.  vp  :  |r|
8.  ps  :  (|g|  \mtimes{}  |r|)  List
9.  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps)
                Q[k  *  x])
10.  \muparrow{}Q[k  *  (fst(<kp,  vp>))]
11.  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));<k,v>*  ps)
                  Q[x])
\mvdash{}  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));if  (v  *  vp)  =\msubb{}  0
                                        then  <k,v>*  ps
                                        else  [<k  *  kp,  v  *  vp>  /  (<k,v>*  ps)]
                                        fi  )
              Q[x])


By

---

Latex:
((SplitOnConclITE  THENM  Reduce  0)  THEN  Auto)

---

Home Index