(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 2 1 1 3 1 2 2 1 1 1 1 1 1 1 1 1 1 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. 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. & (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. & (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 = s(i;t+1).x)
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)
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)
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. IdDeq  EqDecider(Id)
21. (x.init(x)?)  State(ds)
22. t' : 
23. 0t'
24. True  (v:T. P((x.s(i;t').x),v))
25. (t:t'. isnull(a(i;t)))
26. z : Id
  0t'  s(i;0).z = s(i;0).z  ds(z)?Top
By: AllHyps (h.Repeat (Unfolds [`ma-single-pre-init`;`mk-ma`] h THEN Reduce h))
THEN
Fold `member` 0
THEN
DoSubsume

Generated subgoal:

1 13. l:IdLnk, tg:Id.
13. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i)
13. (w.M(l,tg)) r if <ds,locl(a) : T,init,a : P,,,,,>
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(locl(a) : T)
15. &  P@0 != a : P(a@0) ==> v:locl(a) : T(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(a : P))
16. (
16. (2of(a : P)(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
16. & (x:Id. 
16. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
16. & (
16. & (s(i;t+1).x
16. & (=
16. & (2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t)))
16. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
16. & (l:IdLnk. 
16. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of(
16. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;))
16. & (
16. & (withlnk(l;m(i;t))
16. & (=
16. & (if source(l) = i
16. & (if concat(map(tgf.map(x.<1of(tgf)
16. & (if concat(map(tgf.map(x.,x>;2of(tgf)
16. & (if concat(map(tgf.map(x.,x>;((x.s(i;t).x)
16. & (if concat(map(tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
16. & (else nil fi
16. & ( (tg:Idif source(l) = i locl(a) : T(rcv(l; tg))?Top else Top fi) List)
16. & (x:Id. 
16. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
16. & (
16. & (s(i;t).x
16. & (=
16. & (s(i;t+1).x
16. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
16. & (l:IdLnk, tg:Id.
16. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
16. & ((
16. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
16. & (
16. & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)
17. x:Id. 
17. deq-member(IdDeq;x;1of(init))
17. 
17. s(i;0).x
17. =
17. 2of(init)(x)
17.  if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Void fi
18. a@0:Action(i). 
18. isnull(a@0)  (valtype(i;a@0) r locl(a) : T(kind(a@0))?Top)
19. x:Id. 
19. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
20. IdDeq  EqDecider(Id)
21. (x.init(x)?)  State(ds)
22. t' : 
23. 0t'
24. True  (v:T. P((x.s(i;t').x),v))
25. (t:t'. isnull(a(i;t)))
26. z : Id
27. 0t'
  vartype(i;z) r ds(z)?Top
1 step

About:
pairproductlistnilbtrueifthenelseassertitvoid
natural_numberaddlambdaapplyfunctionuniverseequalmembersqequal
topsubtype_relpropimpliesandortrueallexists
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