---

Step * 2 3 of Lemma lookup_omral_scale_a

.....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|))))
BY
{ (RepeatFor 2 (Thin (-1))
   THEN AbReduceIf (\e t.not is_term `oalist` (subterm t 1)) 0 
        THEN Fold `omralist` 0 THEN RenameBVars [`x',`kp';`y',`kv'] 0 
        THEN ((RepD) THENA Auto)
   ) }

1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. k' : |g|
5. v : |r|
6. r↓+gp ∈ AbDMon
7. g ∈ DMon
8. ws : |omral(g;r)|
9. ((<k,v>* ws)[k * k']) = (v * (ws[k'])) ∈ |r|
10. kp : |g|
11. kv : |r|
12. ↑before(kp;map(λkp.(fst(kp));ws))
13. ¬(kv = 0 ∈ |r|)
⊢ (if (v * kv) =b 0 then <k,v>* ws else [<k * kp, v * kv> / (<k,v>* ws)] fi [k * k'])
= (v * if kp =b k' then kv else ws[k'] fi )
∈ |r|

---

Latex:

---

Latex:
.....antecedent..... 
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{}  \mforall{}ws:|oal(g\mdownarrow{}oset;r\mdownarrow{}+gp)|
        ((((<k,v>*  ws)[k  *  k'])  =  (v  *  (ws[k'])))
        {}\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{}  (((<k,v>*  [<x,  y>  /  ws])[k  *  k'])  =  (v  *  ([<x,  y>  /  ws][k']))))))


By

---

Latex:
(RepeatFor  2  (Thin  (-1))
  THEN  AbReduceIf  (\mbackslash{}e  t.not  is\_term  `oalist`  (subterm  t  1))  0 
            THEN  Fold  `omralist`  0  THEN  RenameBVars  [`x',`kp';`y',`kv']  0 
            THEN  ((RepD)  THENA  Auto)
  )

---

Home Index