(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 2 1 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. 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 <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 = 2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t))))
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. & (x:Id. 
16. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(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,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)
17. x:Id. deq-member(IdDeq;x;1of(init))  s(i;0).x = 2of(init)(x)
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. x : Id
27. x  dom(init)
28. x  dom(ds)
  s(i;0).x =   ds(x)
By: Analyze -2 THEN BackThruSomeHyp

Generated subgoals:

None

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