---

Step * 1 of Lemma omral_scale_dom_pred


1. g : OCMon
2. r : CDRng
3. Q : |g| ⟶ 𝔹
4. k : |g|
5. v : |r|
6. p : |g| × |r|
7. ps : (|g| × |r|) List
8. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
        Q[k * x])
9. ↑Q[k * (fst(p))]
10. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps)
         Q[x])
⊢ ↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* [p / ps])
       Q[x])
BY
{ New [`kp';`vp'] (D 6) THEN Reduce 0⋅ }

1
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])

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  Q  :  |g|  {}\mrightarrow{}  \mBbbB{}
4.  k  :  |g|
5.  v  :  |r|
6.  p  :  |g|  \mtimes{}  |r|
7.  ps  :  (|g|  \mtimes{}  |r|)  List
8.  \muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps)
                Q[k  *  x])
9.  \muparrow{}Q[k  *  (fst(p))]
10.  \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));<k,v>*  [p  /  ps])
              Q[x])


By

---

Latex:
New  [`kp';`vp']  (D  6)  THEN  Reduce  0\mcdot{}

---

Home Index