P:(A
T
), k:Knd, i,r,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm*
x = r
Thm*
Thm*
loc.
(recognizer1(loc;T;A;P;k;i;r;x))
Thm* realizes es.
e@i.kind(e) = k 
Knd (valtype(e) 
r T)
Thm* realizes es.& (vartype(i;x)
r A)
Thm* realizes es.&
e@i.first(e) (r when e) = false
Thm* realizes es.&
e'@i.(r after e')
Thm* realizes es.&
e'@i.
Thm* realizes es.&
e'@i.(
e:E.
Thm* realizes es.&
e'@i.((e <loc e') 
e = e' E
Thm* realizes es.&
e'@i.(& kind(e) = k Knd
Thm* realizes es.&
e'@i.(& P((x when e),val(e)))es:ES, i:Id, P:({e:E| loc(e) = i Id }Prop).
Thm*
e@i.P(e) e@i.first(e) P(e) & e@i.first(e) P(pred(e)) P(e)the_es:ES, e,e':E.
Thm* (e <loc e')
first(e') & e = pred(e') E (e <loc pred(e'))