---

Step * of Lemma omral_scale_sd_ordered

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑sd_ordered(map(λz.(fst(z));ps))) ⇒ (↑sd_ordered(map(λz.(fst(z));<k,v>* ps))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `cdrng_is_abdmonoid` [⌜r⌝]⋅ THENA Auto)
   THEN InductionOnListA
   THEN Reduce 0) }

1
1. g : OCMon
2. r : CDRng
3. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
4. k : |g|
5. v : |r|
⊢ True ⇒ True

2
1. g : OCMon
2. r : CDRng
3. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
4. k : |g|
5. v : |r|
6. p : |g| × |r|
7. ps : (|g| × |r|) List
8. (↑sd_ordered(map(λz.(fst(z));ps))) ⇒ (↑sd_ordered(map(λz.(fst(z));<k,v>* ps)))
⊢ (↑(before(fst(p);map(λz.(fst(z));ps)) ∧b sd_ordered(map(λz.(fst(z));ps))))
⇒ (↑sd_ordered(map(λz.(fst(z));<k,v>* [p / ps])))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `cdrng\_is\_abdmonoid`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InductionOnListA
  THEN  Reduce  0)

---

Home Index