---

Step * 1 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(<x1,y>* qs) ⋃ dom(ps ** qs))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))
BY
{ ((Fold `oset_of_ocmon` (-1) 
THENM RWH (LemmaC `fset_mem_union`) (-1) 
THENM RW bool_to_propC (-1) 
THENM D (-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 dom(<x1,y>* qs))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))

2
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))
⊢ ↑(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{}  dom(<x1,y>*  qs)  \mcup{}  dom(ps  **  qs))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  (mset\_inj\{g\mdownarrow{}oset\}(x1)  +  dom(ps))  \mtimes{}  dom(qs))


By

---

Latex:
((Fold  `oset\_of\_ocmon`  (-1) 
THENM  RWH  (LemmaC  `fset\_mem\_union`)  (-1) 
THENM  RW  bool\_to\_propC  (-1) 
THENM  D  (-1))  THENA  Auto)

---

Home Index