---

Step * 1 1 2 1 2 1 of Lemma omral_times_dom


1. g : OCMon
2. r : CDRng
3. qs : {ps:(|g| × |r|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))} 
4. r↓+gp ∈ AbDMon
5. g ∈ DMon
6. x : |g|
7. ps : {ps:(|g| × |r|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))} 
8. (↑(x ∈b dom(ps ** qs))) ⇒ (↑(x ∈b dom(ps) × dom(qs)))
9. x1 : |g|
10. y : |r|
11. ↑before(x1;map(λx.(fst(x));ps))
12. ¬(y = 0 ∈ |r|)
13. ↑(x
∈b dom(ps ** qs))
14. ↑(x
∈b dom(ps) × dom(qs))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))
BY
{ % would be more elegant to prove some more monotonicity  
  lemmas and use them here % 
 
((OnMCls [0;-1] (RWH (LemmaC `mset_prod_mem`))) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. qs : {ps:(|g| × |r|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))} 
4. r↓+gp ∈ AbDMon
5. g ∈ DMon
6. x : |g|
7. ps : {ps:(|g| × |r|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))} 
8. (↑(x ∈b dom(ps ** qs))) ⇒ (↑(x ∈b dom(ps) × dom(qs)))
9. x1 : |g|
10. y : |r|
11. ↑before(x1;map(λx.(fst(x));ps))
12. ¬(y = 0 ∈ |r|)
13. ↑(x
∈b dom(ps ** qs))
14. ↑(∃b{g↓set} v ∈ dom(ps)
                 ∃b{g↓set} w ∈ dom(qs)
                            (x =b (v * w)))
⊢ ↑(∃b{g↓set} v ∈ mset_inj{g↓oset}(x1) + dom(ps)
               ∃b{g↓set} w ∈ dom(qs)
                          (x =b (v * w)))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  qs  :  \{ps:(|g|  \mtimes{}  |r|)  List|  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))\} 
4.  r\mdownarrow{}+gp  \mmember{}  AbDMon
5.  g  \mmember{}  DMon
6.  x  :  |g|
7.  ps  :  \{ps:(|g|  \mtimes{}  |r|)  List|  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))\} 
8.  (\muparrow{}(x  \mmember{}\msubb{}  dom(ps  **  qs)))  {}\mRightarrow{}  (\muparrow{}(x  \mmember{}\msubb{}  dom(ps)  \mtimes{}  dom(qs)))
9.  x1  :  |g|
10.  y  :  |r|
11.  \muparrow{}before(x1;map(\mlambda{}x.(fst(x));ps))
12.  \mneg{}(y  =  0)
13.  \muparrow{}(x
\mmember{}\msubb{}  dom(ps  **  qs))
14.  \muparrow{}(x
\mmember{}\msubb{}  dom(ps)  \mtimes{}  dom(qs))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  (mset\_inj\{g\mdownarrow{}oset\}(x1)  +  dom(ps))  \mtimes{}  dom(qs))


By

---

Latex:
\%  would  be  more  elegant  to  prove  some  more  monotonicity   
    lemmas  and  use  them  here  \% 
 
((OnMCls  [0;-1]  (RWH  (LemmaC  `mset\_prod\_mem`)))  THENA  Auto)

---

Home Index