2. A : Type
3. P : A
T
4. k : Knd
5. i : Id
6. r : Id
7. x : Id
8. A
9. T
10.
x = r
11. (
loc.
(recognizer1(loc;T;A;P;k;i;r;x))) 
Dsys
12. D' : Dsys
13.
loc.(recognizer1(loc;T;A;P;k;i;r;x)) 
D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. vartype(i;r)
r
18.
e:E. loc(e) = i 
first(e) (r when e) = false
19.
e:E. loc(e) = i (r after e) = (r when e) kind(e) = k
20. @i: ma-single-effect1(r;
;x;A;k;T;r,x,v. P(x,v) 
r) Dsys
21. vartype(i;r)
r
22. vartype(i;x)
r A
23.
e:E. loc(e) = i kind(e) = k (valtype(e) r T)
24.
e:E.
24. loc(e) = i
24.
24. kind(e) = k
(r after e) = (P((x when e),val(e)) (r when e))
25. e' : E
26. loc(e') = i
27.
first(e')
28. (r after pred(e'))
28.
28. (
e@0:E.
28. ((e@0 <loc pred(e'))
e@0 = pred(e')
28. (& kind(e@0) = k
28. (& P((x when e@0),val(e@0)))
29. (r after pred(e'))
(e@0:E.
29. (e@0 <loc pred(e'))
e@0 = pred(e')
29. & kind(e@0) = k
29. & P((x when e@0),val(e@0)))
30. (r when e') = (r after pred(e'))
31. (r after e')
32.
(r after pred(e'))
(r after e') = (r when e') 
