---

Step * 1 1 of Lemma omral_times_dom


1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. qs : |omral(g;r)|
5. r↓+gp ∈ AbDMon
6. g ∈ DMon
7. x : |(g↓set)|
8. ↑(x
∈b dom(ps ** qs))
⊢ ↑(x
∈b dom(ps) × dom(qs))
BY
{ (((OnVar `ps' MoveToConcl  THEN BLemma `omralist_ind_a`  THENM RepD) THENA Auto) THEN All Reduce) }

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. ↑(x
∈b 0{g↓oset})
⊢ ↑(x
∈b 0{g↓oset} × 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((<x1,y>* qs) ++ (ps ** qs)))
⊢ ↑(x
∈b (mset_inj{g↓oset}(x1) + dom(ps)) × dom(qs))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
4.  qs  :  |omral(g;r)|
5.  r\mdownarrow{}+gp  \mmember{}  AbDMon
6.  g  \mmember{}  DMon
7.  x  :  |(g\mdownarrow{}set)|
8.  \muparrow{}(x
\mmember{}\msubb{}  dom(ps  **  qs))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  dom(ps)  \mtimes{}  dom(qs))


By

---

Latex:
(((OnVar  `ps'  MoveToConcl    THEN  BLemma  `omralist\_ind\_a`    THENM  RepD)  THENA  Auto)  THEN  All  Reduce)

---

Home Index