1. i : Id
2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)TProp
6. init : x:Id fp-> ds(x)?Void
7. x:Id. x  dom(ds)  x  dom(init)
  @i (with ds: ds
  @i init: init
  @i action a:T
  @i precondition a(v) is
  @i P s v) realizes2 es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)

By:

let maops let  [`ma-ds` let  ;`ma-da` let  ;`ma-din` let  ;`ma-dout` let  ;`ma-pre` let  ;`ma-npre` let  ;`ma-ef` let  ;`ma-init` let  ;`ma-decla`] in RepeatFor 3 (Analyze 0 THENA Complete Auto) THEN AssertBY ((eqof(IdDeq)(i,i)) ~ true) (BackThru Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true) THEN ES_Reduce THEN PW_Reduce -2 THEN AllHyps (h. (InstHyp [i] h THENA Complete Auto THEN Subst ((eqof(IdDeq)(i,i)) ~ true) -1 (THENL ([Trivial;Thin h THEN Reduce -1 THEN Repeat (Unfolds maops -1 THEN Reduce -1)])

1

8. w : World 9. FairFifo 10. FairFifo 11. l:IdLnk, tg:Id. 11. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i) 11. (w.M(l,tg)) r if (with ds: ds 11. (w.M(l,tg)) r if (init: init 11. (w.M(l,tg)) r if action a:T 11. (w.M(l,tg)) r if aprecondition a(v) is 11. (w.M(l,tg)) r if aP) 11. (w.M(l,tg)) r else  fi.da(rcv(l; tg)) 12. (eqof(IdDeq)(i,i)) ~ true 13. a@0:Id, t:. 13. t':.  13. tt' 13. & isnull(a(i;t')) & kind(a(i;t')) = locl(a@0) 13. &  locl(a@0)  dom(1of(2of((with ds: ds 13. &  locl(a@0)  dom(1of(2init: init 13. &  locl(a@0)  dom(1of(action a:T 13. &  locl(a@0)  dom(1of(aprecondition a(v) is 13. &  locl(a@0)  dom(1of(aP)))) 13. &  P@0 != 1of(2of(2of(2of((with ds: ds 13. &  P@0 != 1of(2init: init 13. &  P@0 != 1of(action a:T 13. &  P@0 != 1of(aprecondition a(v) is 13. &  P@0 != 1of(aP)))))(a@0) ==> v:1of(2of((with ds: ds 13. &  P@0 != 1of(aP)))))(a@0) ==> v:1of(2init: init 13. &  P@0 != 1of(aP)))))(a@0) ==> v:1of(action a:T 13. &  P@0 != 1of(aP)))))(a@0) ==> v:1of(aprecondition a(v) is 13. &  P@0 != 1of(aP)))))(a@0) ==> v:1of(aP)))(locl(a@0))?Top. 13. &  P@0((x.s(i;t').x),v) 14. t:.  14. isnull(a(i;t)) 14.  14. (islocal(kind(a(i;t))) 14. ( 14. (deq-member(IdDeq;act(kind(a(i;t)));1of(1of(2of(2of(2of((with ds: ds 14. (deq-member(IdDeq;act(kind(a(i;t)));1of(1of(2init: init 14. (deq-member(IdDeq;act(kind(a(i;t)));1of(1of(action a:T 14. (deq-member(IdDeq;act(kind(a(i;t)));1of(1of(aprecondition a(v) is 14. (deq-member(IdDeq;act(kind(a(i;t)));1of(1of(aP))))))) 14. ( 14. (2of(1of(2of(2of(2of((with ds: ds 14. (2of(1of(2init: init 14. (2of(1of(action a:T 14. (2of(1of(aprecondition a(v) is 14. (2of(1of(aP)))))) 14. ((act(kind(a(i;t))) 14. (,x.s(i;t).x 14. (,val(a(i;t)))) 14. & (x:Id.  14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)) 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of( 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;2of(2of(2of(2of( 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;(with ds: ds 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;(init: init 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;action a:T 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;aprecondition a(v) is 14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;aP)))))))) 14. & ( 14. & (s(i;t+1).x 14. & (= 14. & (2of(1of(2of(2of(2of(2of((with ds: ds 14. & (2of(1of(2init: init 14. & (2of(1of(action a:T 14. & (2of(1of(aprecondition a(v) is 14. & (2of(1of(aP))))))) 14. & ((<kind(a(i;t)),x> 14. & (,x.s(i;t).x 14. & (,val(a(i;t))) 14. & ( if deq-member(IdDeq;x;1of(1of((with ds: ds 14. & ( if deq-member(IdDeq;x;1init: init 14. & ( if deq-member(IdDeq;x;action a:T 14. & ( if deq-member(IdDeq;x;aprecondition a(v) is 14. & ( if deq-member(IdDeq;x;aP)))) 14. & ( if 2of(1of((with ds: ds 14. & ( if 2of(1init: init 14. & ( if 2of(action a:T 14. & ( if 2of(aprecondition a(v) is 14. & ( if 2of(aP))) 14. & ( if (x) 14. & ( else Top fi) 14. & (l:IdLnk.  14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)) 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;1of(1of( 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;2of(2of(2of(2of( 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;2of((with ds: ds 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;2init: init 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;action a:T 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;aprecondition a(v) is 14. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);,l>;aP))))))))) 14. & ( 14. & (withlnk(l;m(i;t)) 14. & (= 14. & (if source(l) = i 14. & (if concat(map(tgf.map(x. 14. & (if <1of(tgf),x>;2of(tgf) 14. & (if <1of(tgf),x>;((x.s(i;t).x) 14. & (if <1of(tgf),x>;,val(a(i;t))));2of(1of(2of(2of(2of(2of(2of((with ds: ds 14. & (if <1of(tgf),x>;,val(a(i;t))));2of(1of(2init: init 14. & (if <1of(tgf),x>;,val(a(i;t))));2of(1of(action a:T 14. & (if <1of(tgf),x>;,val(a(i;t))));2of(1of(aprecondition a(v) is 14. & (if <1of(tgf),x>;,val(a(i;t))));2of(1of(aP)))))))) 14. & (if <1of(tgf),x>;,val(a(i;t))));(<kind(a(i;t)),l>))) 14. & (else nil fi 14. & ( (tg:Id 14. & ( (if source(l) = i 14. & ( (if 1of(2of((with ds: ds 14. & ( (if 1of(2init: init 14. & ( (if 1of(action a:T 14. & ( (if 1of(aprecondition a(v) is 14. & ( (if 1of(aP)))(rcv(l; tg))?Top 14. & ( (else Top fi) List) 14. & (x:Id.  14. & ((deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of((with ds: ds 14. & ((deq-member(IdDeq;x;1of(1of(2init: init 14. & ((deq-member(IdDeq;x;1of(1of(action a:T 14. & ((deq-member(IdDeq;x;1of(1of(aprecondition a(v) is 14. & ((deq-member(IdDeq;x;1of(1of(aP)))))))))) 14. & (( 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(2of(2of(2of(2of(2of(2of( 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of((with ds: ds 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of((init: init 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(action a:T 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(aprecondition a(v) is 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(aP))))))))) 14. & ((deq-member(KindDeq;kind(a(i;t));(x))) 14. & ( 14. & (s(i;t).x 14. & (= 14. & (s(i;t+1).x 14. & ( if deq-member(IdDeq;x;1of(1of((with ds: ds 14. & ( if deq-member(IdDeq;x;1init: init 14. & ( if deq-member(IdDeq;x;action a:T 14. & ( if deq-member(IdDeq;x;aprecondition a(v) is 14. & ( if deq-member(IdDeq;x;aP)))) 14. & ( if 2of(1of((with ds: ds 14. & ( if 2of(1init: init 14. & ( if 2of(action a:T 14. & ( if 2of(aprecondition a(v) is 14. & ( if 2of(aP))) 14. & ( if (x) 14. & ( else Top fi) 14. & (l:IdLnk, tg:Id. 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of( 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of( 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of( 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;(with ds: ds 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;(init: init 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;action a:T 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;aprecondition a(v) is 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;aP))))))))))) 14. & (( 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(2of(2of(2of(2of(2of(2of(2of( 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of((with ds: ds 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of((init: init 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(action a:T 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(aprecondition a(v) is 14. & ((deq-member(KindDeq;kind(a(i;t));2of(1of(aP)))))))))) 14. & ((deq-member(KindDeq;kind(a(i;t));(<l,tg>))) 14. & ( 14. & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List) 15. x:Id.  15. deq-member(IdDeq;x;1of(1of(2of(2of((with ds: ds 15. deq-member(IdDeq;x;1of(1of(2init: init 15. deq-member(IdDeq;x;1of(1of(action a:T 15. deq-member(IdDeq;x;1of(1of(aprecondition a(v) is 15. deq-member(IdDeq;x;1of(1of(aP)))))) 15.  15. s(i;0).x 15. = 15. 2of(1of(2of(2of((with ds: ds 15. 2of(1of(2init: init 15. 2of(1of(action a:T 15. 2of(1of(aprecondition a(v) is 15. 2of(1of(aP))))) 15. (x) 15.  if deq-member(IdDeq;x;1of(1of((with ds: ds 15.  if deq-member(IdDeq;x;1init: init 15.  if deq-member(IdDeq;x;action a:T 15.  if deq-member(IdDeq;x;aprecondition a(v) is 15.  if deq-member(IdDeq;x;aP)))) 15.  if 2of(1of((with ds: ds init: initaction a:T precondition a(v) is P)))(x) 15.  else Void fi 16. a@0:Action(i).  16. isnull(a@0) 16.  16. (valtype(i;a@0) r 1of(2of((with ds: ds 16. (valtype(i;a@0) r 1of(2init: init 16. (valtype(i;a@0) r 1of(action a:T 16. (valtype(i;a@0) r 1of(aprecondition a(v) is 16. (valtype(i;a@0) r 1of(aP)))(kind(a@0))?Top) 17. x:Id.  17. vartype(i;x) r if deq-member(IdDeq;x;1of(1of((with ds: ds 17. vartype(i;x) r if deq-member(IdDeq;x;1init: init 17. vartype(i;x) r if deq-member(IdDeq;x;action a:T 17. vartype(i;x) r if deq-member(IdDeq;x;aprecondition a(v) is 17. vartype(i;x) r if deq-member(IdDeq;x;aP)))) 17. vartype(i;x) r if 2of(1of((with ds: ds 17. vartype(i;x) r if 2of(1init: init 17. vartype(i;x) r if 2of(action a:T 17. vartype(i;x) r if 2of(aprecondition a(v) is 17. vartype(i;x) r if 2of(aP))) 17. vartype(i;x) r if (x) 17. vartype(i;x) r else Top fi   (v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)

64 steps

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