(74steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pre-init-rule 1 2 1
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
  (v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)
By: Assert ((x.init(x)?)  State(ds))

Generated subgoals:

1   (x.init(x)?)  State(ds)
7 steps
2 18. (x.init(x)?)  State(ds)
  (v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)
56 steps

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

(74steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc