---

Step * of Lemma omral_scale_dom_bound

∀g:OCMon. ∀r:CDRng. ∀bound,k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
         (x <b bound)))
  ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps)
           (x <b (k * bound)))))
BY
{ ((RepD THENM BLemma `omral_scale_dom_pred`) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. bound : |g|
4. k : |g|
5. v : |r|
6. ps : (|g| × |r|) List
7. ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
        (x <b bound))
⊢ ↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
       ((k * x) <b (k * bound)))

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}bound,k:|g|.  \mforall{}v:|r|.  \mforall{}ps:(|g|  \mtimes{}  |r|)  List.
    ((\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps)
                  (x  <\msubb{}  bound)))
    {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));<k,v>*  ps)
                      (x  <\msubb{}  (k  *  bound)))))


By

---

Latex:
((RepD  THENM  BLemma  `omral\_scale\_dom\_pred`)  THENA  Auto)

---

Home Index