2. A : Type
3. P : A
T
4. i : Id
5. k : Knd
6. a : Id
7. x : Id
8. A
9. T
10.
x = "trigger"
11.
locl(a) = k
12. (
loc.
(trigger1(loc;T;A;P;i;k;a;x))) 
Dsys
13. D' : Dsys
14.
loc.(trigger1(loc;T;A;P;i;k;a;x)) 
D'
15. w : World
16. p : FairFifo
17. PossibleWorld(D';w)
18.
e:E. loc(e) = i 
kind(e) = k (valtype(e) r T)
19. vartype(i;x)
r A
20.
e:E. loc(e) = i first(e) ("trigger" when e) = false
21.
e':E.
21. loc(e') = i
21.
21. (("trigger" after e')
21. (
21. ((
e:E. (e <loc e') 
e = e' & kind(e) = k & P((x when e),val(e))))
22. @i: ma-single-pre1("trigger";
;a;Unit;x,v.x) Dsys
23. vartype(i;"trigger")
r
24.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r Unit)
25.
e:E.
25. loc(e) = i
25.
25. (kind(e) = locl(a)
("trigger" when e))
25. & (
e':E.
25. & ((e <loc e')
e = e'
25. & (& kind(e') = locl(a)
(v:Unit. ("trigger" after e')))
e:E.
loc(e) = i Id
kind(e) = k Knd P((x when e),val(e)) e'@i.kind(e') = locl(a)
