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':Dsys.
12. (D
D'
12. (
12. ((
w:World, p:FairFifo.
12. ((PossibleWorld(D';w)
12. ((
12. (((
v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?
),v)) (e:E. loc(e) = i)))
13. D : Dsys
14. @i: (with ds: x : A
14. @init: x : c
14. action a:T
14. aprecondition a(v) is
14. a
s,v. P(s(x),v)) D
15.
D':Dsys.
15. D
D'
15.
15. (
w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((vartype(i;x)
r A) & (e:E. loc(e) = i first(e) (x when e) = c))
16.
D':Dsys.
16. D
D'
16.
16. (
w:World, p:FairFifo.
16. (PossibleWorld(D';w)
16. (
16. ((vartype(i;x)
r A)
16. (& (
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T))
16. (& (
e:E.
16. (& (loc(e) = i
16. (& (
16. (& ((kind(e) = locl(a)
P((x when e),val(e)))
16. (& (& (
e':E.
16. (& (& ((e <loc e')
e = e'
16. (& (& (& kind(e') = locl(a)
(v:T. 
P((x after e'),v)))))
17.
D':Dsys.
17. D
D'
17.
17. (
w:World, p:FairFifo.
17. (PossibleWorld(D';w)
17. (
17. ((
v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v)) (e:E. loc(e) = i))
18. D' : Dsys
19. D
D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. (vartype(i;x)
r A)
23. & (
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T))
23. & (
e:E.
23. & (loc(e) = i
23. & (
23. & ((kind(e) = locl(a)
P((x when e),val(e)))
23. & (& (
e':E.
23. & (& ((e <loc e')
e = e'
23. & (& (& kind(e') = locl(a)
(v:T. P((x after e'),v))))
24. (vartype(i;x)
r A) & (e:E. loc(e) = i first(e) (x when e) = c)
(vartype(i;x) r A)
& (e:E. loc(e) = i Id first(e) (x when e) = c A)
& (e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T))
