Step
*
1
1
1
of Lemma
omral_scale_wf2
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
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