---

Step * 1 1 of Lemma omral_scale_wf2


1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. r↓+gp ∈ DMon
⊢ <k,v>* ps ∈ |omral(g;r)|
BY
{ ((OnCls [0;5] (Unfold `omralist`) 
THENM D 5 
THENM AbReduce 0 THENM MemTypeCD) THENA Auto)  }

1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |(((g↓oset) × (r↓+gp↓set)) List)|
6. (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))
7. r↓+gp ∈ DMon
⊢ <k,v>* ps ∈ (|g| × |r|) List

2
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |(((g↓oset) × (r↓+gp↓set)) List)|
6. ↑sd_ordered(map(λx.(fst(x));ps))
7. ¬↑(e ∈b map(λx.(snd(x));ps))
8. r↓+gp ∈ DMon
⊢ ↑sd_ordered(map(λx.(fst(x));<k,v>* ps))

3
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |(((g↓oset) × (r↓+gp↓set)) List)|
6. ↑sd_ordered(map(λx.(fst(x));ps))
7. ¬↑(e ∈b map(λx.(snd(x));ps))
8. r↓+gp ∈ DMon
9. ↑sd_ordered(map(λx.(fst(x));<k,v>* ps))
⊢ ¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  k  :  |g|
4.  v  :  |r|
5.  ps  :  |omral(g;r)|
6.  r\mdownarrow{}+gp  \mmember{}  DMon
\mvdash{}  <k,v>*  ps  \mmember{}  |omral(g;r)|


By

---

Latex:
((OnCls  [0;5]  (Unfold  `omralist`) 
THENM  D  5 
THENM  AbReduce  0  THENM  MemTypeCD)  THENA  Auto) 

---

Home Index