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@i.first(e) 
(r when e) = false
19.
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))
e@i.kind(e) = k Knd (valtype(e) r T) & (vartype(i;x) r A)
& e@i.first(e) (r when e) = false
& e'@i.(r after e')
& e'@i.
& e'@i.(
e:E.
& e'@i.((e <loc e') e = e' & kind(e) = k Knd & P((x when e),val(e)))
