Step
*
1
of Lemma
oal_mcp_wf
1. s : LOSet@i'
2. g : AbDMon@i'
⊢ <oal_mon(s;g), λk,v. inj(k,v), λh,f,ps. (msFor{h} k ∈ dom(ps). (f k (ps[k])))> ∈ MCopower(s;g)
BY
{ (((MemTypeCD) THEN Auto) THEN Force `5` (Reduce 0)
THEN Try (((BLemma `oal_umap_char`) THEN Auto))
THEN Try (((BLemma `oal_inj_mon_hom`) THEN Auto))) }
Latex:
Latex:
1. s : LOSet@i'
2. g : AbDMon@i'
\mvdash{} <oal\_mon(s;g), \mlambda{}k,v. inj(k,v), \mlambda{}h,f,ps. (msFor\{h\} k \mmember{} dom(ps). (f k (ps[k])))> \mmember{} MCopower(s;g)
By
Latex:
(((MemTypeCD) THEN Auto) THEN Force `5` (Reduce 0)
THEN Try (((BLemma `oal\_umap\_char`) THEN Auto))
THEN Try (((BLemma `oal\_inj\_mon\_hom`) THEN Auto)))
Home
Index