(164steps 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-rule 2 1 2 2 1 1 1 2 2 3 1 2 2 2 2 1 1 1 1 1 1 1 1 2
1. i : Id
2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)TProp
6. w : World
7. p1 : i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil
8. p3 : 
8. i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
9. p4 : 
9. (i:Id, t:, l:IdLnk.
9. (isrcv(l;a(i;t))
9. (
9. (destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t)))
9. & (l:IdLnk, t:.
9. & (t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil)
10. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil
11. i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
12. (i:Id, t:, l:IdLnk.
12. (isrcv(l;a(i;t))
12. (
12. (destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t)))
12. & (l:IdLnk, t:.
12. & (t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil)
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)],x.T>,,<[a],x.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)],x.T>)
15. &  P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.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. ((eqof(IdDeq)(a,act(kind(a(i;t))))  false)
16. (
16. (P((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())  s(i;0).x = 2of()(x)
18. a@0:Action(i). 
18. isnull(a@0)  (valtype(i;a@0) r <[locl(a)],x.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:Id. vartype(i;x) r ds(x)?Top
22. j : Id
23. t : 
24. j = i
25. isnull(a(j;t))
26. isnull(a(i;t))
27. (x.s(i;t).x)  State(ds)
28. t' : 
29. t+1t'
30. v:T. P((x.s(i;t').x),v)
31. t2 : 
32. t2<t'
33. isnull(a(i;t2))
34. t3:. t2<t3 & t3<t'  isnull(a(i;t3))
35. tt2
36. loc(<j,t>) = loc(<i,t2>) & (<j,t> < <i,t2>)  <j,t> = <i,t2>
37. v : T
38. P((x.s(i;t').x),v)
39. z : Id
40. t3 : 
41. 0<t3
42. t2+1t3
43. t3t'
44. t2+1t3-1
45. s(i;t2+1).z = s(i;t3-1).z
46. isnull(a(i;t3-1))
47. x:Id. s(i;t3-1+1).x = s(i;t3-1).x
48. m(i;t3-1) = nil
49. s(i;t3-1+1).z = s(i;t3-1).z
50. x:Id. s(i;t3-1+1).x = s(i;t3-1).x
51. m(i;t3-1) = nil
52. s(i;t3).z = s(i;t3-1).z
  s(i;t2+1).z = s(i;t3).z  ds(z)?Top
By: HypSubst -1 0

Generated subgoal:

1 9. p5 : 
9. i:Id, t:, l:IdLnk.
9. isrcv(l;a(i;t))
9. 
9. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg
10. p6 : 
10. l:IdLnk, t:.
10. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List
11. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List
12. i:Id, t:.
12. isnull(a(i;t))
12. 
12. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
13. i:Id, t:, l:IdLnk.
13. isrcv(l;a(i;t))
13. 
13. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg
14. l:IdLnk, t:.
14. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List
15. l:IdLnk, tg:Id.
15. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i)
15. (w.M(l,tg)) r if <ds,<[locl(a)],x.T>,,<[a],x.P>,,,,,>
15. (w.M(l,tg)) r else  fi.da(rcv(l; tg))
16. (eqof(IdDeq)(i,i)) ~ true
17. a@0:Id, t:.
17. t':. 
17. tt'
17. & isnull(a(i;t')) & kind(a(i;t')) = locl(a@0)
17. &  locl(a@0)  dom(<[locl(a)],x.T>)
17. &  P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.T>(locl(a@0))?Top. 
17. &  P@0((x.s(i;t').x),v)
18. t:. 
18. isnull(a(i;t))
18. 
18. (islocal(kind(a(i;t)))
18. (
18. ((eqof(IdDeq)(a,act(kind(a(i;t))))  false)
18. (
18. (P((x.s(i;t).x),val(a(i;t))))
18. & (x:Id. 
18. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
18. & (
18. & (s(i;t+1).x
18. & (=
18. & (2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t)))
18. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
18. & (l:IdLnk. 
18. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of(
18. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;))
18. & (
18. & (withlnk(l;m(i;t))
18. & (=
18. & (if source(l) = i
18. & (if concat(map(tgf.map(x.<1of(tgf)
18. & (if concat(map(tgf.map(x.,x>;2of(tgf)
18. & (if concat(map(tgf.map(x.,x>;((x.s(i;t).x)
18. & (if concat(map(tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
18. & (else nil fi
18. & ( (tg:Id
18. & ( (if source(l) = i <[locl(a)],x.T>(rcv(l; tg))?Top else Top fi) List)
18. & (x:Id. 
18. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
18. & (
18. & (s(i;t).x
18. & (=
18. & (s(i;t+1).x
18. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
18. & (l:IdLnk, tg:Id.
18. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
18. & ((
18. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
18. & (
18. & (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)
19. x:Id. 
19. deq-member(IdDeq;x;1of())
19. 
19. s(i;0).x
19. =
19. 2of()(x)
19.  if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Void fi
20. a@0:Action(i). 
20. isnull(a@0)  (valtype(i;a@0) r <[locl(a)],x.T>(kind(a@0))?Top)
21. x:Id. 
21. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
22. IdDeq  EqDecider(Id)
23. x:Id. vartype(i;x) r ds(x)?Top
24. j : Id
25. t : 
26. j = i
27. isnull(a(j;t))
28. isnull(a(i;t))
29. (x.s(i;t).x)  State(ds)
30. t' : 
31. t+1t'
32. v:T. P((x.s(i;t').x),v)
33. t2 : 
34. t2<t'
35. isnull(a(i;t2))
36. t3:. t2<t3 & t3<t'  isnull(a(i;t3))
37. tt2
38. loc(<j,t>) = loc(<i,t2>)  Id & (<j,t> < <i,t2>)  <j,t> = <i,t2>  E
39. v : T
40. P((x.s(i;t').x),v)
41. z : Id
42. t3 : 
43. 0<t3
44. t2+1t3
45. t3t'
46. t2+1t3-1
47. s(i;t2+1).z = s(i;t3-1).z  ds(z)?Top
48. isnull(a(i;t3-1))
49. x:Id. s(i;t3-1+1).x = s(i;t3-1).x  vartype(i;x)
50. m(i;t3-1) = nil  Msg List
51. s(i;t3-1+1).z = s(i;t3-1).z  vartype(i;z)
52. x:Id. s(i;t3-1+1).x = s(i;t3-1).x  vartype(i;x)
53. m(i;t3-1) = nil  Msg List
54. s(i;t3).z = s(i;t3-1).z  vartype(i;z)
55. z1 : vartype(i;z)
  z1  ds(z)?Top
2 steps

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

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