a,i:Id.
Thm*
loc.
(once(loc;a;i))
Thm* realizes es.
e@i.kind(e) = locl(a)
Thm* realizes es.&
e@i.e'@i.kind(e) = locl(a)
Thm* realizes es.&
e@i.e'@i.
Thm* realizes es.& kind(e') = locl(a)
Knd e = e' Ees:ES, x,i:Id, T:Type, c:T.
Thm* (
x,y:T. Dec(x = y T))
Thm*
Thm* (vartype(i;x)
r T)
Thm*
Thm* (
e:E. loc(e) = i Id first(e) (x when e) = c T)
Thm*
Thm* (
e':E.
Thm* (loc(e') = i
Id
Thm* (
Thm* (
(x after e') = c T
Thm* (
Thm* ((
ev:E. ev 
e' & (x after ev) = (x when ev) T))es:ES, e,e':E. e e' loc(e) = loc(e') Idthe_es:ES, e,e':E.
Thm* (e <loc e')
first(e') & e = pred(e') E 
(e <loc pred(e'))the_es:ES, j:E. first(j) (pred(j) <loc j)