2 |
e'@i. first(e')
e'@i.
((r after pred(e'))
(
(( e@0:E.
(((e@0 <loc pred(e')) e@0 = pred(e') E
((& kind(e@0) = k Knd
((& P((x when e@0),val(e@0))))

((r after e')
(
(( e@0:E.
(((e@0 <loc e') e@0 = e' E
((& kind(e@0) = k Knd
((& P((x when e@0),val(e@0))))
 | 35 steps |