1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : ATProp
8. (s,v. P(s(x),v))  State(x : A)TProp
9. x@0:Id. x@0  dom(x : A)  x@0  dom(x : c)
10. x : c  x@0:Id fp-> x : A(x@0)?Void
  @i: (with ds: x : A
  @init: x : c
  action a:T
  aprecondition a(v) is
  as,v. P(s(x),v))
   Dsys
  & (D:Dsys. 
  & (@i: (with ds: x : A
  & (@init: x : c
  & (action a:T
  & (aprecondition a(v) is
  & (as,v. P(s(x),v))  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  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.& & ((v:T. P(c,v))
  & (realizes es.& & (
  & (realizes es.& & ((e:E. 
  & (realizes es.& & ((loc(e) = i  Id
  & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))

By:	Inst Thm: s-pre-init-rule [i;a;T;x : A;s,v. P(s(x),v);x : c] THEN Reduce 0 THEN Try (Complete Auto) THEN Analyze -1 THEN Analyze 0 THEN Try Trivial

1

11. @i: (with ds: x : A 11. @init: x : c 11. action a:T 11. aprecondition a(v) is 11. as,v. P(s(x),v)) 11.  Dsys 12. D:Dsys.  12. @i: (with ds: x : A 12. @init: x : c 12. action a:T 12. aprecondition a(v) is 12. as,v. P(s(x),v))  D 12.  12. D  12. realizes es.(v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v)) 12. realizes es. 12. realizes es.(e:E. loc(e) = i  Id) 13. @i: (with ds: x : A 13. @init: x : c 13. action a:T 13. aprecondition a(v) is 13. as,v. P(s(x),v)) 13.  Dsys   D:Dsys.    @i: (with ds: x : A   @init: x : c   action a:T   aprecondition a(v) is   as,v. P(s(x),v))  D      D    realizes es.(vartype(i;x) r A)   realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  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.& & ((v:T. P(c,v))   realizes es.& & (   realizes es.& & ((e:E.    realizes es.& & ((loc(e) = i  Id   realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v))))

32 steps

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