i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)
TProp).
Thm* @i (with ds: ds
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v)
Thm* realizes es.(
x:Id. vartype(i;x) 
r ds(x)?Top)
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = locl(a)
Knd (valtype(e) r T))
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& ((kind(e) = locl(a)
Knd P((
z.(z when e)),val(e)))
Thm* realizes es.& (& (
e':E.
Thm* realizes es.& (& ((e <loc e')
e = e' E
Thm* realizes es.& (& (& kind(e') = locl(a)
Knd
Thm* realizes es.& (& (&
(v:T. 
P((z.(z after e')),v))))D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
Thm* D realizes2 es.P(es)
D realizes es.P(es)eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x L)x:A, y:B. inl(x) = inr(y) A+B Falsea:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a) Falsea,b:Id. locl(a) = locl(b) a = bd:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true