2. i : Id
3. (
loc.
(once(loc;a;i))) 
Dsys
4. D' : Dsys
5.
loc.(once(loc;a;i)) 
D'
6. w : World
7. p : FairFifo
8. PossibleWorld(D';w)
9. @i: ma-single-pre-init1("done";
;false
;a;Unit;x,v.
x) Dsys
10. vartype(i;"done")
r
11.
e:E. loc(e) = i 
first(e) ("done" when e) = false
12.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r Unit)
13.
e:E. loc(e) = i kind(e) = locl(a) ("done" when e)
14. e : E
15. loc(e) = i
16. kind(e) = locl(a)
(v:Unit. ("done" after e))
17.
e@i.("done" after e) = ("done" when e) kind(e) = locl(a)
18. e1 : E
19. loc(e1) = i
20. kind(e1) = locl(a)
21. WellFnd{i}(E;x,y.(x <loc y))
22. j : E
23.
k:E. (k <loc j) (e1 <loc k) ("done" when k)
24.
first(j)
25. e1 = pred(j)
26. "done"
Id
27. ("done" when j) = ("done" after pred(j))
28. @i: ma-single-effect0("done";
;locl(a);Unit;x,v. true) Dsys
29. vartype(i;"done")
r
30.
e:E. loc(e) = i kind(e) = locl(a) (valtype(e) r Unit)
31.
e:E. loc(e) = i kind(e) = locl(a) ("done" after e) = true
32. ("done" after e1) = true
("done" after e1)
