Def == FairFifo
Def == & (
i,x:Id. vartype(i;x) 
r M(i).ds(x))
Def == & & (
i:Id, a:Action(i).
Def == & & (
isnull(a) 
(valtype(i;a) r M(i).da(kind(a))))
Def == & & (
l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg)))
Def == & & (
i,x:Id. M(i).init(x,s(i;0).x))
Def == & & (
i:Id, t:
.
Def == & & (
isnull(a(i;t))
Def == & & (
Def == & & ((
islocal(kind(a(i;t)))
Def == & & ((
Def == & & ((M(i).pre(act(kind(a(i;t))),
x.s(i;t).x,val(a(i;t))))
Def == & & (& (
x:Id.
Def == & & (& (M(i).ef(kind(a(i;t)),x,
x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
Def == & & (& (
l:IdLnk.
Def == & & (& (M(i).send(kind(a(i;t));l;
x.
Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
Def == & & (& (
x:Id.
Def == & & (& (
M(i).frame(kind(a(i;t)) affects x)
Def == & & (& (
Def == & & (& (s(i;t).x = s(i;t+1).x
M(i).ds(x))
Def == & & (& (
l:IdLnk, tg:Id.
Def == & & (& (
M(i).sframe(kind(a(i;t)) sends <l,tg>)
Def == & & (& (
Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil
Msg List))
Def == & & (
i,a:Id, t:.
Def == & & (
t':.
Def == & & (t
t'
Def == & & (&
isnull(a(i;t')) & kind(a(i;t')) = locl(a)
Def == & & (&
a declared in M(i)
Def == & & (&
unsolvable M(i).pre(a,x.s(i;t').x))