Step * 1 1 1 of Lemma omral_scale_wf2


1. OCMon
2. CDRng
3. |g|
4. |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
BY
Auto }


Latex:


Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  k  :  |g|
4.  v  :  |r|
5.  ps  :  |(((g\mdownarrow{}oset)  \mtimes{}  (r\mdownarrow{}+gp\mdownarrow{}set))  List)|
6.  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(e  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))
7.  r\mdownarrow{}+gp  \mmember{}  DMon
\mvdash{}  <k,v>*  ps  \mmember{}  (|g|  \mtimes{}  |r|)  List


By


Latex:
Auto




Home Index