i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)
TProp),
Thm*
init:x:Id fp-> ds(x)?Void.
Thm* (
x:Id. x 
dom(ds) 
x dom(init))
Thm*
Thm* @i: (with ds: ds init: initaction a:T precondition a(v) is P)
Dsys
Thm* & (
D:Dsys.
Thm* & (@i: (with ds: ds
Thm* & (@init: init
Thm* & (action a:T
Thm* & (aprecondition a(v) is
Thm* & (aP)
D
Thm* & (
Thm* & (D
Thm* & (realizes es.(
v:T. P((
x.init(x)?
),v)) (e:E. loc(e) = i Id))i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp),
Thm*
init:x:Id fp-> ds(x)?Void.
Thm* (
x:Id. x dom(ds) x dom(init))
Thm*
Thm* @i (with ds: ds
Thm* @i init: init
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v)
Thm* realizes es.(
v:T. P((x.init(x)?),v)) (e:E. loc(e) = i Id)