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

By:	NewSpecializeEsLemmaOn Thm: pre-rule (with ds: ds (action a:T (precondition a(v) is (P s v) THEN Subst (loc(e') = i) 0 THEN Try BackThruSomeHyp THEN SplitOrHyps THEN AllHyps (h.Analyze h THEN Complete Auto) THEN AllHyps (h.RevHypSubst h 0 THEN Complete Auto)

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html