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)
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. & (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. & (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 = s(i;t+1).x)
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)
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)
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
18. (x.init(x)?)  State(ds)
19. v:T. P((x.init(x)?),v)
  e:E. loc(e) = i  Id

1

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

54 steps

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