| Def | | Dsys | [dsys] |
| Def | | D1  D2 | [d-sub] |
| Def | | @i: x:T
@i: xinitially x = v | [d-single-init] |
| Def | | @i: only L affects x : t | [d-single-frame] |
| Def | | @i: only L sends on (l with tg) | [d-single-sframe] |
| Def | | d-single-effect(i; ds; da; k; x; f) | [d-single-effect] |
| Def | | d-single-sends(i; ds; da; k; l; f) | [d-single-sends] |
| Def | | @i (with ds: ds
@i action a:T
@i precondition a(v) is
@i P s v) | [d-single-pre] |
| Def | | @i (with ds: ds
@i init: init
@i action a:T
@i precondition a(v) is
@i P s v) | [d-single-pre-init] |
| Def | | d-feasible(D) | [d-feasible] |
| Def | | interface-check(D;l;tg;T) | [interface-check] |
| Def | | PossibleWorld(D;w) | [possible-world] |
| Def | | x : t initially x = v | [ma-single-init] | mb event system 4 |
| Def | | only members of L affect x :t | [ma-single-frame] | mb event system 4 |
| Def | | only L sends on (l with tg) | [ma-single-sframe] | mb event system 4 |
| Def | | ma-single-effect(ds; da; k; x; f) | [ma-single-effect] | mb event system 4 |
| Def | | ma-single-sends(ds; da; k; l; f) | [ma-single-sends] | mb event system 4 |
| Def | | (with ds: ds
(action a:T
(precondition a(v) is
(P s v) | [ma-single-pre] | mb event system 4 |
| Def | | (with ds: ds
(init: init
action a:T
aprecondition a(v) is
aP) | [ma-single-pre-init] | mb event system 4 |
| Def | | x : v | [fpf-single] | mb event system 4 |
| Def | | M1 || M2 | [ma-compatible] | mb event system 4 |
| Def | | M1 ||decl M2 | [ma-compatible-decls] | mb event system 4 |
| Def | | f || g | [fpf-compatible] | mb event system 4 |
| Def | | ES | [event_system] | mb event system 2 |
| Def | | EqDecider(T) | [deq] | mb event system 2 |
| Def | | Prop | [prop] | core |
| Def | | M1  M2 | [ma-join] | mb event system 4 |
| Def | | f g | [fpf-join] | mb event system 4 |
| Def | | M.state | [ma-st] | mb event system 4 |
| Def | | M.V(k) | [ma-v] | mb event system 4 |
| Def | | MsgA | [msga] | mb event system 4 |
| Def | | M1 M2 | [ma-sub] | mb event system 4 |
| Def | | Feasible(M) | [ma-feasible] | mb event system 4 |
| Def | | State(ds) | [ma-state] | mb event system 4 |
| Def | | ma-valtype(da; k) | [ma-valtype] | mb event system 4 |
| Def | | M.din(l,tg) | [ma-din] | mb event system 4 |
| Def | | M.dout(l,tg) | [ma-dout] | mb event system 4 |
| Def | | unsolvable M.pre(a,s) | [ma-npre] | mb event system 4 |
| Def | | M.send(k;l;s;v;ms;i) | [ma-send] | mb event system 4 |
| Def | | M.ef(k,x,s,v,w) | [ma-ef] | mb event system 4 |
| Def | | M.init(x,v) | [ma-init] | mb event system 4 |
| Def | | M.da(a) | [ma-da] | mb event system 4 |
| Def | | M.ds(x) | [ma-ds] | mb event system 4 |
| Def | | f(x)?z | [fpf-cap] | mb event system 3 |
| Def | | f g | [fpf-sub] | mb event system 3 |
| Def | |  x dom(f). v=f(x)   P(x;v) | [fpf-all] | mb event system 4 |
| Def | | a declared in M | [ma-decla] | mb event system 4 |
| Def | | M.sframe(k sends <l,tg>) | [ma-sframe] | mb event system 4 |
| Def | | M.frame(k affects x) | [ma-frame] | mb event system 4 |
| Def | | M.pre(a,s,v) | [ma-pre] | mb event system 4 |
| Def | | z != f(x) ==> P(a;z) | [fpf-val] | mb event system 3 |
| Def | | x dom(f) | [fpf-dom] | mb event system 3 |
| Def | | a:A fp-> B(a) | [fpf] | mb event system 3 |
| Def | | World | [world] | mb event system 3 |
| Def | | Top | [top] | core |
| Def | | strong-subtype(A;B) | [strong-subtype] | mb event system 1 |
| Def | | {T} | [guard] | core |
| Def | | da-outlinks(da;i) | [da-outlinks] | mb event system 4 |
| Def | | da-outlink-f(da;k) | [da-outlink-f] | mb event system 4 |
| Def | | f(x) | [fpf-ap] | mb event system 3 |
| Def | | FairFifo | [fair-fifo] | mb event system 3 |
| Def | | ESAxioms{i:l}
ESAxioms(E;
ESAxioms(T;
ESAxioms(M;
ESAxioms(loc;
ESAxioms(kind;
ESAxioms(val;
ESAxioms(when;
ESAxioms(after;
ESAxioms(sends;
ESAxioms(sender;
ESAxioms(index;
ESAxioms(first;
ESAxioms(pred;
ESAxioms(causl) | [ESAxioms] | mb event system 2 |
| Def | | has-src(i;k) | [has-src] | mb event system 2 |
| Def | | queue(l;t) | [w-queue] | mb event system 3 |
| Def | | rcvs(l;t) | [w-rcvs] | mb event system 3 |
| Def | | isrcv(l;a) | [w-isrcvl] | mb event system 3 |
| Def | | isrcv(k) | [isrcv] | mb event system 1 |
| Def | | KindDeq | [Kind-deq] | mb event system 2 |
| Def | | valtype(i;a) | [w-valtype] | mb event system 3 |
| Def | | Action(i) | [w-action] | mb event system 3 |
| Def | | eventtype(k;loc;V;M;e) | [eventtype] | mb event system 2 |
| Def | | w-action-dec(TA;M;i) | [w-action-dec] | mb event system 3 |
| Def | | kindcase(k;a.f(a);l,t.g(l;t)) | [kindcase] | mb event system 2 |
| Def | | msg(a) | [w-msg] | mb event system 3 |
| Def | | tag(k) | [tagof] | mb event system 2 |
| Def | | w-tagged(tg; mss) | [w-tagged] | mb event system 3 |
| Def | | a = b | [eq_id] | mb event system 2 |
| Def | | ma-is-empty(M) | [ma-is-empty] | mb event system 4 |
| Def | | M sends on link l | [ma-sends-on] | mb event system 4 |
| Def | | snds(l;t) | [w-snds] | mb event system 3 |
| Def | | m(l;t) | [w-ml] | mb event system 3 |
| Def | | onlnk(l;mss) | [w-onlnk] | mb event system 3 |
| Def | | withlnk(l;mss) | [w-withlnk] | mb event system 3 |
| Def | | a = b | [eq_lnk] | mb event system 2 |
| Def | | IdLnkDeq | [idlnk-deq] | mb event system 2 |
| Def | | IdDeq | [id-deq] | mb event system 2 |
| Def | | destination(l) | [ldst] | mb event system 2 |
| Def | | Msg | [w-Msg] | mb event system 3 |
| Def | | m(i;t) | [w-m] | mb event system 3 |
| Def | | val(a) | [w-val] | mb event system 3 |
| Def | | a(i;t) | [w-a] | mb event system 3 |
| Def | | s(i;t).x | [w-s] | mb event system 3 |
| Def | | w.M | [w-M] | mb event system 3 |
| Def | | product-deq(A;B;a;b) | [product-deq] | mb event system 2 |
| Def | | mtag(m) | [mtag] | mb event system 1 |
| Def | | w.TA | [w-TA] | mb event system 3 |
| Def | | proddeq(a;b) | [proddeq] | mb event system 2 |
| Def | | 2of(t) | [pi2] | core |
| Def | | lnk(k) | [lnk] | mb event system 2 |
| Def | | deq-member(eq;x;L) | [deq-member] | mb event system 2 |
| Def | | eqof(d) | [eqof] | mb event system 2 |
| Def | | source(l) | [lsrc] | mb event system 2 |
| Def | | kind(a) | [w-kind] | mb event system 3 |
| Def | | vartype(i;x) | [w-vartype] | mb event system 3 |
| Def | | Msg_sub(l; M) | [Msg_sub] | mb event system 1 |
| Def | | haslink(l; m) | [haslink] | mb event system 1 |
| Def | | mlnk(m) | [mlnk] | mb event system 1 |
| Def | | union-deq(A;B;a;b) | [union-deq] | mb event system 2 |
| Def | | fpf-dom-list(f) | [fpf-dom-list] | mb event system 4 |
| Def | | fpf-is-empty(f) | [fpf-is-empty] | mb event system 3 |
| Def | | w.T | [w-T] | mb event system 3 |
| Def | | sumdeq(a;b) | [sumdeq] | mb event system 2 |
| Def | | 1of(t) | [pi1] | core |
| Def | | (x l) | [l_member] | mb list 1 |
| Def | |  | [bool] | bool 1 |
| Def | | P  Q | [iff] | core |
| Def | | S T | [subtype] | core |
| Def | | action(dec) | [action] | mb event system 3 |
| Def | | Knd | [Knd] | mb event system 1 |
| Def | | Msg(M) | [Msg] | mb event system 1 |
| Def | | IdLnk | [IdLnk] | mb event system 1 |
| Def | | Id | [Id] | mb event system 1 |
| Def | | M(i) | [d-m] |
| Def | | x:A. B(x) | [all] | core |
| Def | | | [ma-empty] | mb event system 4 |
| Def | | if b t else f fi | [ifthenelse] | bool 1 |
| Def | | prod-deq(A;B;a;b) | [prod-deq] | mb event system 2 |
| Def | |  b | [assert] | bool 1 |
| Def | | finite-type(T) | [finite-type] | mb event system 1 |
| Def | | P & Q | [and] | core |
| Def | | locl(a) | [locl] | mb event system 1 |
| Def | | P  Q | [or] | core |
| Def | | SWellFounded(R(x;y)) | [strongwellfounded] | mb event system 2 |
| Def | |  | [nat] | int 1 |
| Def | | {i..j } | [int_seg] | int 1 |
| Def | | i j | [ge] | core |
| Def | | i  j < k | [lelt] | int 1 |
| Def | | AB | [le] | core |
| Def | |  x:A. B(x) | [exists] | core |
| Def | | act(k) | [actof] | mb event system 2 |
| Def | | islocal(k) | [islocal] | mb event system 1 |
| Def | | rcv(l; tg) | [rcv] | mb event system 1 |
| Def | | isnull(a) | [w-isnull] | mb event system 3 |
| Def | | Dec(P) | [decidable] | core |
| Def | |  A | [not] | core |
| Def | | P Q | [implies] | core |
| Def | | A & B | [cand] | core |
| Def | | ||as|| | [length] | list 1 |
| Def | | l[i] | [select] | list 1 |
| Def | | nth_tl(n;as) | [nth_tl] | list 1 |
| Def | | i j | [le_int] | bool 1 |
| Def | | b | [bnot] | bool 1 |
| Def | | mapfilter(f;P;L) | [mapfilter] | mb list 2 |
| Def | | filter(P;l) | [filter] | mb list 1 |
| Def | | concat(ll) | [concat] | mb event system 1 |
| Def | | upto(n) | [upto] | mb event system 1 |
| Def | | as @ bs | [append] | list 1 |
| Def | | isl(x) | [isl] | union |
| Def | | outl(x) | [outl] | union |
| Def | | p q | [band] | bool 1 |
| Def | | P Q | [rev_implies] | core |
| Def | | mk-ma(ds; da; init; pre; ef; send; frame; sframe) | [mk-ma] | mb event system 4 |
| Def | | | [fpf-empty] | mb event system 3 |
| Def | | NatDeq | [nat-deq] | mb event system 2 |
| Def | | AtomDeq | [atom-deq] | mb event system 2 |
| Def | | map(f;as) | [map] | list 1 |
| Def | | Surj(A; B; f) | [surject] | fun 1 |
| Def | | outr(x) | [outr] | union |
| Def | | hd(l) | [hd] | list 1 |
| Def | | p q | [bor] | bool 1 |
| Def | | reduce(f;k;as) | [reduce] | list 1 |
| Def | | Trans x,y:T. E(x;y) | [trans] | rel 1 |
| Def | | sum-deq(A;B;a;b) | [sum-deq] | mb event system 2 |
| Def | | i=j | [eq_int] | bool 1 |
| Def | | x=yAtom | [eq_atom] | bool 1 |
| Def | | tl(l) | [tl] | list 1 |
| Def | | i<j | [lt_int] | bool 1 |
