Nuprl Definition : mu_ex_v5

Nuprl Definition : mu_ex_v5_cs-constraint

mu_ex_v5_cs-constraint{i:l}(es;m1;m2;init;p1;p2) ==

e:E
((

mu_ex_v5_LeaveCS()(e)

(

e':E

i:Id
(<i, make-Msg(``enter cs``;Unit;

)>

mu_ex_v5_main(init;m1;m2;p1;p2)(e')

(e' <loc e)

(

e'':E
((e' <loc e'')

(e'' <loc e)

(

j:Id. (

<j, make-Msg(``enter cs``;Unit;

)>

mu_ex_v5_main(init;m1;m2;p1;p2)(e''))))))))

(||filter(

e.name_eq(es-header(es;e);``leave cs``);

loc(e))||

bag-size([p

e'

loc(e).mu_ex_v5_main(init;m1;m2;p1;p2) es e'|
name_eq(msg-header(snd(p));``enter cs``)])))

Definitions occuring in Statement : mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2), mu_ex_v5_LeaveCS: mu_ex_v5_LeaveCS(), make-Msg: make-Msg(hdr;typ;val), es-header: es-header(es;e), msg-header: msg-header(m), Message: Message, classrel: v

X(e), es-le-before:

loc(e), es-locl: (e <loc e'), es-E: E, Id: Id, name_eq: name_eq(x;y), length: ||as||, it:

, pi2: snd(t), le: A

B, all:

x:A. B[x], exists:

x:A. B[x], not:

A, squash:

T, implies: P

Q, and: P

Q, unit: Unit, apply: f a, lambda:

x.A[x], pair: <a, b>, product: x:A

B[x], cons: [car / cdr], nil: [], token: "$token", filter: filter(P;l), bag-combine:

x

bs.f[x], bag-size: bag-size(bs), bag-filter: [x

b|p[x]]
FDL editor aliases : mu_ex_v5_cs-constraint

mu\_ex\_v5\_cs-constraint\{i:l\}(es;m1;m2;init;p1;p2) == \mforall{}e:E ((\mcdot{} \mmember{} mu\_ex\_v5\_LeaveCS()(e) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E \mexists{}i:Id (<i, make-Msg(``enter cs``;Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e') \mwedge{} (e' <loc e) \mwedge{} (\mforall{}e'':E ((e' <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mforall{}j:Id (\mneg{}<j, make-Msg(``enter cs``;Unit;\mcdot{})> \mmember{} mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e'')))))))) \mwedge{} (||filter(\mlambda{}e.name\_eq(es-header(es;e);``leave cs``); \mleq{}loc(e))|| \mleq{} bag-size([p\mmember{}\mcup{}e'\mmember{}\mleq{}loc(e).mu\_ex\_v5\_main(init;m1;m2;p1;p2) es e'| name\_eq(msg-header(snd(p));``enter cs``)]))) Date html generated: 2012_02_20-PM-06_59_14 Last ObjectModification: 2012_02_02-PM-03_01_14 Home Index