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)
(
v:T. P(c,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)
(v:T. P(c,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
24.
e:E. loc(e) = i first(e) (x when e) = c
25.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T)
26. vartype(i;x)
r A
27.
e:E. loc(e) = i first(e) (x when e) = c
28.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T)
29. vartype(i;x)
r A
30.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r T)
31.
e:E.
31. loc(e) = i
31.
31. (kind(e) = locl(a)
P((x when e),val(e)))
31. & (
e':E.
31. & ((e <loc e')
e = e' & kind(e') = locl(a) (v:T. P((x after e'),v)))
32. vartype(i;x)
r A
33.
e:E. loc(e) = i first(e) (x when e) = c
e:E. loc(e) = i Id kind(e) = locl(a) P((x when e),val(e))
