(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 2 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
27. t : 
28. 0<t
29. tt'
30. s(i;0).z = s(i;t-1).z
  s(i;t-1).z = s(i;t).z  ds(z)?Top
By: AssertBY
(i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil)
(AllHyps (h.Unfold `fair-fifo` h THEN Analyze h THEN Analyze h+1 THEN Trivial))

Generated subgoal:

1 31. i:Id, t:.
31. isnull(a(i;t))
31. 
31. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
  s(i;t-1).z = s(i;t).z  ds(z)?Top
8 steps

About:
pairproductlistnilbtrueifthenelseassertitvoidint
natural_numberaddsubtractless_thanlambdaapplyfunctionuniverseequalmember
sqequaltopsubtype_relpropimpliesandortrueall
exists
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