Nuprl Definition : oal_mcp
oal_mcp(s;g) == <oal_mon(s;g), λk,v. inj(k,v), λh,f,ps. (msFor{h} k ∈ dom(ps). (f k (ps[k])))>
Definitions occuring in Statement :
oal_inj: inj(k,v),
oal_mon: oal_mon(a;b),
lookup: as[k],
oal_dom: dom(ps),
mset_for: mset_for,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
grp_id: e
Definitions occuring in definition :
oal_mon: oal_mon(a;b),
pair: <a, b>,
oal_inj: inj(k,v),
lambda: λx.A[x],
mset_for: mset_for,
oal_dom: dom(ps),
apply: f a,
lookup: as[k],
grp_id: e
Latex:
oal\_mcp(s;g) == <oal\_mon(s;g), \mlambda{}k,v. inj(k,v), \mlambda{}h,f,ps. (msFor\{h\} k \mmember{} dom(ps). (f k (ps[k])))>
Date html generated:
2016_05_16-AM-08_23_02
Last ObjectModification:
2015_09_23-AM-09_53_12
Theory : polynom_2
Home
Index