---

Step * 1 1 2 1 1 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 fs-map(λk'.(k' * x1), dom(qs)))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))
BY
{ Unfold `fset_map` (-1) 
THENM ((RWH (LemmaC `fset_of_mset_mem`) (-1)) 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 msmap{g↓oset,g↓oset}(λk'.(k' * x1);dom(qs)))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))

---

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{}  fs-map(\mlambda{}k'.(k'  *  x1),  dom(qs)))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  (mset\_inj\{g\mdownarrow{}oset\}(x1)  +  dom(ps))  \mtimes{}  dom(qs))


By

---

Latex:
Unfold  `fset\_map`  (-1) 
THENM  ((RWH  (LemmaC  `fset\_of\_mset\_mem`)  (-1))  THENA  Auto)

---

Home Index