| Some definitions of interest. |
|
possible-world | Def PossibleWorld(D;w)
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)) |
|
ma-decla | Def a declared in M == locl(a) dom(1of(2of(M))) |
|
ma-npre | Def unsolvable M.pre(a,s)
Def == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v) |
|
ma-send | Def M.send(k;l;s;v;ms;i)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> =
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map( tgf.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map( x.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> (tg:Id
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ( if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ( if M.da(rcv(l; tg))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ( else Top fi) List |
|
ma-valtype | Def ma-valtype(da; k) == da(k)?Top |
|
Kind-deq | Def KindDeq == union-deq(IdLnk Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) |
|
w-action | Def Action(i) == action(w-action-dec(w.TA;w.M;i)) |
|
world | Def World
Def == T:Id Id Type
Def == TA:Id Id Type
Def == M:IdLnk Id Type
Def == (i:Id    (x:Id T(i,x))) (i:Id    action(w-action-dec(TA;M;i)))
Def == (i:Id    ({m:Msg(M)| source(mlnk(m)) = i } List)) Top |
| | Thm* World Type{i'} |
|
Knd | Def Knd == (IdLnk Id)+Id |
| | Thm* Knd Type |
|
fair-fifo | Def FairFifo
Def == ( i:Id, t: , l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil Msg List)
Def == & ( i:Id, t: .
Def == & ( isnull(a(i;t))
Def == & (
Def == & (( x:Id. s(i;t+1).x = s(i;t).x vartype(i;x))
Def == & (& m(i;t) = nil Msg List)
Def == & ( i:Id, t: , l:IdLnk.
Def == & ( isrcv(l;a(i;t))
Def == & (
Def == & (destination(l) = i
Def == & (& ||queue(l;t)|| 1 & hd(queue(l;t)) = msg(a(i;t)) Msg)
Def == & ( l:IdLnk, t: .
Def == & ( t': .
Def == & (t t' & isrcv(l;a(destination(l);t')) queue(l;t') = nil Msg List) |
|
w-Msg | Def Msg == Msg(w.M) |
|
IdLnk | Def IdLnk == Id Id  |
| | Thm* IdLnk Type |
|
w-es | Def ES(the_w;p)
Def == <E
Def == ,product-deq(Id; ;IdDeq;NatDeq)
Def == ,( i,x. vartype(i;x))
Def == ,( i,a. V(i;locl(a)))
Def == ,the_w.M
Def == ,
Def == ,( e.loc(e))
Def == ,( e.kind(e))
Def == ,( e.val(e))
Def == ,( x,e. (x when e))
Def == ,( x,e. (x after e))
Def == ,( l,e. sends(l;e))
Def == ,( e.sender(e))
Def == ,( e.index(e))
Def == ,( e.first(e))
Def == ,( e.pred(e))
Def == ,( e,e'. e <c e')
Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p)
Def == , > |
|
w-causl | Def e <c e' == e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^+ e' |
|
w-index | Def index(e)
Def == ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));time(sender(e)))|| |
|
w-sender | Def sender(e) == <source(lnk(kind(e))),mu( t.match(lnk(kind(e));t;time(e)))> |
|
w-sends | Def sends(l;e) == onlnk(l;m(loc(e);time(e))) |
|
w-onlnk | Def onlnk(l;mss) == filter( ms.mlnk(ms) = l;mss) |
|
w-withlnk | Def withlnk(l;mss) == mapfilter( ms.2of(ms); ms.mlnk(ms) = l;mss) |
|
idlnk-deq | Def IdLnkDeq == product-deq(Id;Id ;IdDeq;product-deq(Id; ;IdDeq;NatDeq)) |
|
ma-state | Def State(ds) == x:Id ds(x)?Top |
|
w-E | Def E == {p:(Id )|  isnull(a(1of(p);2of(p))) } |
|
Id | Def Id == Atom  |
| | Thm* Id Type |
|
es-valtype | Def valtype(e) == if isrcv(e) rcvtype(e) else acttype(e) fi |
|
w-V | Def V(i;k) == kindcase(k;a.1of(2of(w))(i,a);l,tg.1of(2of(2of(w)))(l,tg)) |
|
w-valtype | Def valtype(i;a) == kindcase(kind(a);a.w.TA(i,a);l,tg.w.M(l,tg)) |
|
actof | Def act(k) == outr(k) |
| | Thm* k:Knd. islocal(k)  act(k) Id |
|
d-single-effect | Def d-single-effect(i; ds; da; k; x; f)(j)
Def == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else fi |
|
fpf-val | Def z != f(x) ==> P(a;z) == x dom(f)  P(x;f(x)) |
|
w-tagged | Def w-tagged(tg; mss) == filter( ms.mtag(ms) = tg;mss) |
|
id-deq | Def IdDeq == product-deq(Atom; ;AtomDeq;NatDeq) |
|
product-deq | Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)> |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
fpf-cap | Def f(x)?z == if x dom(f) f(x) else z fi |
|
deq-member | Def deq-member(eq;x;L) == reduce( a,b. eqof(eq)(a,x)  b;false ;L) |
|
eqof | Def eqof(d) == 1of(d) |
| | Thm* T:Type, d:EqDecider(T). eqof(d) T T   |
|
es-E | Def E == 1of(es) |
|
es-after | Def (x after e)
Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))(x,e) |
|
es-kind | Def kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e) |
|
es-loc | Def loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e) |
|
es-val | Def val(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))(e) |
|
es-vartype | Def vartype(i;x) == 1of(2of(2of(es)))(i,x) |
|
es-when | Def (x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e) |
|
fpf | Def a:A fp-> B(a) == d:A List a:{a:A| (a d) } B(a) |
| | Thm* A:Type, B:(A Type). a:A fp-> B(a) Type |
|
ma-empty | Def == mk-ma(; ; ; ; ; ; ; ) |
|
fpf-empty | Def == <nil, x. > |
|
fpf-single | Def x : v == <[x], x.v> |
|
islocal | Def islocal(k) ==  isl(k) |
| | Thm* k:Knd. islocal(k)  |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
locl | Def locl(a) == inr(a) |
| | Thm* a:Id. locl(a) Knd |
|
lsrc | Def source(l) == 1of(l) |
| | Thm* l:IdLnk. source(l) Id |
|
nat-deq | Def NatDeq == < a,b. a= b,nat_DASH_deq_DASH_aux{1:l}> |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |
|
w-M | Def w.M == 1of(2of(2of(w))) |
|
w-ekind | Def kind(e) == kind(act(e)) |
|
w-eval | Def val(e) == val(act(e)) |
|
w-first | Def first(e)
Def == if time(e)= 0 true
Def == i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>)
Def == else false fi
Def (recursive) |
|
w-pred | Def pred(e)
Def == if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>)
Def == else <loc(e),time(e)-1> fi
Def (recursive) |
|
w-a | Def a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t) |
|
w-after | Def (x after e) == s(1of(e);2of(e)+1).x |
|
w-kind | Def kind(a) == 1of(outr(a)) |
|
w-loc | Def loc(e) == 1of(e) |
|
w-m | Def m(i;t) == 1of(2of(2of(2of(2of(2of(w))))))(i,t) |
|
w-when | Def (x when e) == s(1of(e);2of(e)).x |
|
w-s | Def s(i;t).x == 1of(2of(2of(2of(w))))(i,t,x) |
|
w-vartype | Def vartype(i;x) == w.T(i,x) |
|
pi1 | Def 1of(t) == t.1 |
| | Thm* A:Type, B:(A Type), p:(a:A B(a)). 1of(p) A |
|
w-val | Def val(a) == 2of(outr(a)) |
|
pi2 | Def 2of(t) == t.2 |
| | Thm* A:Type, B:(A Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
rcv | Def rcv(l; tg) == inl(<l,tg>) |
| | Thm* l:IdLnk, tg:Id. rcv(l; tg) Knd |
|
top | Def Top == Void given Void |
| | Thm* Top Type |
|
w-isnull | Def isnull(a) == isl(a) |