i,a,x:Id, A,T:Type, P:(A
TProp).
Thm* @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))
Dsys
Thm* & (
D:Dsys.
Thm* & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))
D
Thm* & (
Thm* & (D
Thm* & (realizes es.(vartype(i;x)
r A)
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((x 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((x after e'),v)))))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)))))d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true