---

Step * 2 1 of Lemma lookup_omral_scale_a

.....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) ⟶ ℙ
BY
{ (Thin (-1) THEN Reduce 0 THEN MemCD THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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)
7.  (r\mdownarrow{}+gp  \mmember{}  AbDMon)  \mwedge{}  (r\mdownarrow{}xmn  \mmember{}  AbDMon)
8.  \mforall{}Q:((|(g\mdownarrow{}oset)|  \mtimes{}  |r\mdownarrow{}+gp|)  List)  {}\mrightarrow{}  \mBbbP{}
          (Q[[]]
          {}\mRightarrow{}  (\mforall{}ws:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|
                      (Q[ws]
                      {}\mRightarrow{}  (\mforall{}x:|(g\mdownarrow{}oset)|.  \mforall{}y:|r\mdownarrow{}+gp|.
                                  ((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws)))  {}\mRightarrow{}  (\mneg{}(y  =  e))  {}\mRightarrow{}  Q[[<x,  y>  /  ws]]))))
          {}\mRightarrow{}  \{\mforall{}ws:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|.  Q[ws]\})
\mvdash{}  \mlambda{}ps.(((<k,v>*  ps)[k  *  k'])  =  (v  *  (ps[k'])))  \mmember{}  ((|(g\mdownarrow{}oset)|  \mtimes{}  |r\mdownarrow{}+gp|)  List)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(Thin  (-1)  THEN  Reduce  0  THEN  MemCD  THEN  Auto)

---

Home Index