2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)
TProp
(
es.(
x:Id. vartype(i;x) 
r ds(x)?Top)
(& (e:E. loc(e) = i 
Id 
kind(e) = locl(a) Knd (valtype(e) r T))
(& (e:E.
(& (loc(e) = i Id
(& (
(& ((kind(e) = locl(a) Knd P((z.(z when e)),val(e)))
(& (& (
e':E.
(& (& ((e <loc e') 
e = e' E
(& (& (& kind(e') = locl(a) Knd (v:T. 
P((z.(z after e')),v)))))
{es:ES
{| es is an event system of @i (with ds: ds
{| es is an event system of @i action a:T
{| es is an event system of @i precondition a(v) is
{| es is an event system of @i P s v) }
Prop{i'}
