i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)
TProp).
Thm* @i: (with ds: ds action a:T precondition a(v) is P s v)
Dsys
Thm* & (
D:Dsys.
Thm* & (@i: (with ds: ds
Thm* & (@action a:T
Thm* & (@precondition a(v) is
Thm* & (@P s v)
D
Thm* & (
Thm* & (D
Thm* & (realizes es.(
x:Id. vartype(i;x) r ds(x)?Top)
Thm* & (realizes es.& (
e:E.
Thm* & (realizes es.& (loc(e) = i
Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = locl(a)
Knd (valtype(e) r T))
Thm* & (realizes es.& (
e:E.
Thm* & (realizes es.& (loc(e) = i
Id
Thm* & (realizes es.& (
Thm* & (realizes es.& ((kind(e) = locl(a)
Knd P((
z.(z when e)),val(e)))
Thm* & (realizes es.& (& (
e':E.
Thm* & (realizes es.& (& ((e <loc e')
e = e' E
Thm* & (realizes es.& (& (& kind(e') = locl(a)
Knd
Thm* & (realizes es.& (& (&
(v:T. 
P((z.(z after e')),v)))))i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
Thm* @i (with ds: ds
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v)
Thm* realizes es.(
x:Id. vartype(i;x) r ds(x)?Top)
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = locl(a)
Knd (valtype(e) r T))
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& ((kind(e) = locl(a)
Knd P((z.(z when e)),val(e)))
Thm* realizes es.& (& (
e':E.
Thm* realizes es.& (& ((e <loc e')
e = e' E
Thm* realizes es.& (& (& kind(e') = locl(a)
Knd
Thm* realizes es.& (& (&
(v:T. P((z.(z after e')),v))))