---

Step * 1 1 2 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) ++ (ps ** qs)))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))
BY
{ % A good example of monotone reasoning % 
 
((RWH (LemmaC `omral_plus_dom`) (-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) ⋃ 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)  ++  (ps  **  qs)))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  (mset\_inj\{g\mdownarrow{}oset\}(x1)  +  dom(ps))  \mtimes{}  dom(qs))


By

---

Latex:
\%  A  good  example  of  monotone  reasoning  \% 
 
((RWH  (LemmaC  `omral\_plus\_dom`)  (-1))  THENA  Auto)

---

Home Index