1 |
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 Id)
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
D:Dsys.
@i: (with ds: x : A
@init: x : c
action a:T
aprecondition a(v) is
a s,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))))
 | 32 steps |