i,x:Id, a:Knd, T,A:Type, f:(ATA).
  @i: ma-single-effect0(x;A;a;T;f)  Dsys
  & (D:Dsys. 
  & (@i: ma-single-effect0(x;A;a;T;f)  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id  kind(e) = a  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = a  Knd
  & (realizes es.& (
  & (realizes es.& ((x after e) = f((x when e),val(e))  A))

By:

Unfold `ma-single-effect0` 0 THEN UnivCD THEN AssertBY (x : A  x:Id fp-> Type) Auto THEN AssertBY (a : T  k:Knd fp-> Type) Auto THEN Inst Thm: s-effect-rule [i;x;a;x : A;a : T;s,v. f(s(x),v)] THENA Try (Complete (Try (Unfolds [`ma-valtype`] 0 THEN Reduce 0) THEN Fold `ma-state` 0)) THEN ExRepD THEN BetterSplitAndConcl THEN Try Trivial THEN All Reduce THEN ParallelOp -2 THEN RepeatFor 7 (ParallelOp -1) THEN Unfold `ma-valtype` -1 THEN Reduce -1 THEN ExRepD THEN BetterSplitAndConcl THEN Try Trivial THEN AllHyps (h.InstHyp [x] h THEN Reduce -1 THEN Complete Auto) THEN AllHyps (h. (ParallelOp h THEN ThinTrivial THEN WeakSubstFor kind(e) -1 THEN Reduce -1 (THEN (Complete Auto)

None

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