P:(A
T
), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm*
x = "trigger"
Thm*
Thm*
locl(a) = k
Thm*
Thm*
loc.
(trigger1(loc;T;A;P;i;k;a;x))
Thm* realizes es.(vartype(i;x)
r A)
Thm* realizes es.&
e@i.kind(e) = k 
Knd (valtype(e) r T)
Thm* realizes es.&
e'@i.kind(e') = locl(a)
Thm* realizes es.&
e'@i.
Thm* realizes es.& (
e:E.
Thm* realizes es.& ((e <loc e') & kind(e) = k
Knd & P((x when e),val(e)))
Thm* realizes es.&
e@i.kind(e) = k Knd
Thm* realizes es.&
e@i.
Thm* realizes es.& P((x when e),val(e))
e'@i.kind(e') = locl(a) Kndes:ES, x:Id, e:E.
Thm*
first(e) (x after pred(e)) = (x when e) vartype(loc(e);x)the_es:ES, e,e':E.
Thm* (e <loc e')
first(e') & e = pred(e') E 
(e <loc pred(e'))