---

Step * 2 of Lemma lookup_omral_scale_a


1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. v : |r|
6. (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon)
⊢ ∀ps:|omral(g;r)|. (((<k,v>* ps)[k * k']) = (v * (ps[k'])) ∈ |r|)
BY
{ ((InstLemma `cdrng_is_abdmonoid` [⌜r⌝]⋅ THENA Auto)
   THEN (InstLemma `oalist_ind` [⌜g↓oset⌝;⌜r↓+gp⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜λ2ps.((<k,v>* ps)[k * k']) = (v * (ps[k'])) ∈ |r|⌝] (-1)⋅ THENM ParallelLast)) }

1
.....wf..... 
1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. v : |r|
6. (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon)
7. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
8. ∀Q:((|(g↓oset)| × |r↓+gp|) List) ⟶ ℙ
     (Q[[]]
     ⇒ (∀ws:|oal(g↓oset;r↓+gp)|
           (Q[ws]
           ⇒ (∀x:|(g↓oset)|. ∀y:|r↓+gp|.
                 ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |r↓+gp|)) ⇒ Q[[<x, y> / ws]]))))
     ⇒ {∀ws:|oal(g↓oset;r↓+gp)|. Q[ws]})
⊢ λps.(((<k,v>* ps)[k * k']) = (v * (ps[k'])) ∈ |r|) ∈ ((|(g↓oset)| × |r↓+gp|) List) ⟶ ℙ

2
.....antecedent..... 
1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. v : |r|
6. (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon)
7. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
8. ∀Q:((|(g↓oset)| × |r↓+gp|) List) ⟶ ℙ
     (Q[[]]
     ⇒ (∀ws:|oal(g↓oset;r↓+gp)|
           (Q[ws]
           ⇒ (∀x:|(g↓oset)|. ∀y:|r↓+gp|.
                 ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |r↓+gp|)) ⇒ Q[[<x, y> / ws]]))))
     ⇒ {∀ws:|oal(g↓oset;r↓+gp)|. Q[ws]})
⊢ ((<k,v>* [])[k * k']) = (v * ([][k'])) ∈ |r|

3
.....antecedent..... 
1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. v : |r|
6. (r↓+gp ∈ AbDMon) ∧ (g ∈ DMon)
7. (r↓+gp ∈ AbDMon) ∧ (r↓xmn ∈ AbDMon)
8. ∀Q:((|(g↓oset)| × |r↓+gp|) List) ⟶ ℙ
     (Q[[]]
     ⇒ (∀ws:|oal(g↓oset;r↓+gp)|
           (Q[ws]
           ⇒ (∀x:|(g↓oset)|. ∀y:|r↓+gp|.
                 ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |r↓+gp|)) ⇒ Q[[<x, y> / ws]]))))
     ⇒ {∀ws:|oal(g↓oset;r↓+gp)|. Q[ws]})
⊢ ∀ws:|oal(g↓oset;r↓+gp)|
    ((((<k,v>* ws)[k * k']) = (v * (ws[k'])) ∈ |r|)
    ⇒ (∀x:|(g↓oset)|. ∀y:|r↓+gp|.
          ((↑before(x;map(λx.(fst(x));ws)))
          ⇒ (¬(y = e ∈ |r↓+gp|))
          ⇒ (((<k,v>* [<x, y> / ws])[k * k']) = (v * ([<x, y> / ws][k'])) ∈ |r|))))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  k  :  |g|
4.  k'  :  |g|
5.  v  :  |r|
6.  (r\mdownarrow{}+gp  \mmember{}  AbDMon)  \mwedge{}  (g  \mmember{}  DMon)
\mvdash{}  \mforall{}ps:|omral(g;r)|.  (((<k,v>*  ps)[k  *  k'])  =  (v  *  (ps[k'])))


By

---

Latex:
((InstLemma  `cdrng\_is\_abdmonoid`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `oalist\_ind`  [\mkleeneopen{}g\mdownarrow{}oset\mkleeneclose{};\mkleeneopen{}r\mdownarrow{}+gp\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}ps.((<k,v>*  ps)[k  *  k'])  =  (v  *  (ps[k']))\mkleeneclose{}]  (-1)\mcdot{}  THENM  ParallelLast))

---

Home Index