i,a,x:Id, A,T:Type, P:(ATProp).
  @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys
  & (D:Dsys. 
  & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r 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.& (& (e':E. 
  & (realizes es.& (& ((e <loc e')  e = e'  E
  & (realizes es.& (& (& kind(e') = locl(a)  Knd
  & (realizes es.& (& (&  (v:T. P((x after e'),v)))))

By:	Unfold `ma-single-pre1` 0 THEN UnivCD THEN Inst Thm: s-pre-rule [i;a;T;x : A;s,v. P(s(x),v)] THENA Try (Complete Auto) THEN Try (Unfold `s-decl` 0)

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

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