| Some definitions of interest. |
|
w-Msg | Def Msg == Msg(w.M) |
|
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'} |
|
IdLnk | Def IdLnk == Id Id  |
| | Thm* IdLnk Type |
|
w-queue | Def queue(l;t) == nth_tl(||rcvs(l;t)||;snds(l;t)) |
|
w-isrcvl | Def isrcv(l;a) ==  isnull(a) isrcv(kind(a)) lnk(kind(a)) = l |
|
Id | Def Id == Atom  |
| | Thm* Id Type |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
ge | Def i j == j i |
| | Thm* i,j: . (i j) Prop |
|
isrcv | Def isrcv(k) == isl(k) |
| | Thm* k:Knd. isrcv(k)  |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l||  |
| | Thm* ||nil||  |
|
w-msg | Def msg(a) == msg(lnk(kind(a));tag(kind(a));val(a)) |
|
lnk | Def lnk(k) == 1of(outl(k)) |
| | Thm* k:Knd. isrcv(k)  lnk(k) IdLnk |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |
|
w-a | Def a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t) |
|
w-isnull | Def isnull(a) == isl(a) |
|
w-kind | Def kind(a) == 1of(outr(a)) |