---

Step * of Lemma omral_scale_dom_pred

∀g:OCMon. ∀r:CDRng. ∀Q:|g| ⟶ 𝔹. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). Q[k * x])) ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps). Q[x])))
BY
{ (InductionOnListA THEN Reduce 0 THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index