2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : A
TProp
8. (
s,v. P(s(x),v)) 
State(x : A)TProp
9.
x@0:Id. x@0 dom(x : A) 
x@0 dom(x : c)
10. x : c
x@0:Id fp-> x : A(x@0)?Void
11. @i: (with ds: x : A
11. @init: x : c
11. action a:T
11. aprecondition a(v) is
11. a
s,v. P(s(x),v))
11.
Dsys
12.
D:Dsys.
12. @i: (with ds: x : A
12. @init: x : c
12. action a:T
12. aprecondition a(v) is
12. a
s,v. P(s(x),v)) 
D
12.
12. D
12. realizes es.(
v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?
),v))
12. realizes es.
12. realizes es.(
e:E. loc(e) = i)
13. @i: (with ds: x : A
13. @init: x : c
13. action a:T
13. aprecondition a(v) is
13. a
s,v. P(s(x),v))
13.
Dsys
14. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))
Dsys
15.
D:Dsys.
15. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))
D
15.
15. D
15. realizes es.(vartype(i;x)
r A)
15. realizes es.& (
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T))
15. realizes es.& (
e:E.
15. realizes es.& (loc(e) = i
15. realizes es.& (
15. realizes es.& ((kind(e) = locl(a)
P((x when e),val(e)))
15. realizes es.& (& (
e':E.
15. realizes es.& (& ((e <loc e')
e = e'
15. realizes es.& (& (& kind(e') = locl(a)
(v:T. 
P((x after e'),v))))
16. @i: x : A initially x = c
Dsys
17.
D:Dsys.
17. @i: x : A initially x = c
D
17.
17. D
17. realizes es.(vartype(i;x)
r A)
17. realizes es.& (
e:E. loc(e) = i first(e) (x when e) = c)
D:Dsys.
@i: (with ds: x : A
@init: x : c
action a:T
aprecondition a(v) is
as,v. P(s(x),v)) D
D
realizes es.(vartype(i;x) r A)
realizes es.& (e:E. loc(e) = i Id first(e) (x when e) = c A)
realizes es.& (e:E.
realizes es.& (loc(e) = i Id
realizes es.& (
realizes es.& (kind(e) = locl(a) Knd (valtype(e) r T))
realizes es.& (e:E.
realizes es.& (loc(e) = i Id
realizes es.& (
realizes es.& (kind(e) = locl(a) Knd P((x when e),val(e)))
realizes es.& & ((v:T. P(c,v))
realizes es.& & (
realizes es.& & ((e:E.
realizes es.& & ((loc(e) = i Id
realizes es.& & ((& kind(e) = locl(a) Knd (v:T. P((x after e),v))))
