(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. i : Id
2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)TProp
6. w : World
7. p : FairFifo
8. FairFifo
9. l:IdLnk, tg:Id.
9. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i)
9. (w.M(l,tg)) r if <ds,<[locl(a)],x.T>,,<[a],x.P>,,,,,>
9. (w.M(l,tg)) r else  fi.da(rcv(l; tg))
10. (eqof(IdDeq)(i,i)) ~ true
11. a@0:Id, t:.
11. t':. 
11. tt'
11. & isnull(a(i;t')) & kind(a(i;t')) = locl(a@0)
11. &  locl(a@0)  dom(<[locl(a)],x.T>)
11. &  P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.T>(locl(a@0))?Top. 
11. &  P@0((x.s(i;t').x),v)
12. t:. 
12. isnull(a(i;t))
12. 
12. (islocal(kind(a(i;t)))
12. (
12. ((eqof(IdDeq)(a,act(kind(a(i;t))))  false)
12. (
12. (P((x.s(i;t).x),val(a(i;t))))
12. & (x:Id. 
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
12. & (
12. & (s(i;t+1).x = 2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t))))
12. & (l:IdLnk. 
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of(
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;))
12. & (
12. & (withlnk(l;m(i;t))
12. & (=
12. & (if source(l) = i
12. & (if concat(map(tgf.map(x.<1of(tgf)
12. & (if concat(map(tgf.map(x.,x>;2of(tgf)
12. & (if concat(map(tgf.map(x.,x>;((x.s(i;t).x)
12. & (if concat(map(tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
12. & (else nil fi)
12. & (x:Id. 
12. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
12. & (
12. & (s(i;t).x = s(i;t+1).x)
12. & (l:IdLnk, tg:Id.
12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
12. & ((
12. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
12. & (
12. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
13. x:Id. deq-member(IdDeq;x;1of())  s(i;0).x = 2of()(x)
14. a@0:Action(i). 
14. isnull(a@0)  (valtype(i;a@0) r <[locl(a)],x.T>(kind(a@0))?Top)
15. x:Id. 
15. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
16. IdDeq  EqDecider(Id)
17. x:Id. vartype(i;x) r ds(x)?Top
18. j : Id
19. t : 
20. j = i
21. isnull(a(j;t))
22. isnull(a(i;t))
23. (x.s(i;t).x)  State(ds)
24. t' : 
25. t+1t'
26. v:T. P((x.s(i;t').x),v)
27. t2 : 
28. t2<t'
29. isnull(a(i;t2))
30. t3:. t2<t3 & t3<t'  isnull(a(i;t3))
31. tt2
32. loc(<j,t>) = loc(<i,t2>) & (<j,t> < <i,t2>)  <j,t> = <i,t2>
33. v : T
34. P((x.s(i;t').x),v)
35. z : Id
36. t3 : 
37. 0<t3
38. t2+1t3
39. t3t'
40. t2+1t3-1
41. s(i;t2+1).z = s(i;t3-1).z
42. isnull(a(i;t3-1))
  s(i;t2+1).z = s(i;t3).z  ds(z)?Top
By: AllHyps
(h.
(Analyze h THEN Analyze h+1 THEN InstHyp [i;t3-1] h+1 THEN Analyze -1
(THEN
(InstHyp [z] -2
(THENA
((Auto THEN D_ES_Subtype))

Generated subgoal:

1 7. p1 : i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List
8. p3 : 
8. i:Id, t:.
8. isnull(a(i;t))
8. 
8. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
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))  Msg)
9. & (l:IdLnk, t:.
9. & (t':. 
9. & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
10. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List
11. i:Id, t:.
11. isnull(a(i;t))
11. 
11. (x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List
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))  Msg)
12. & (l:IdLnk, t:.
12. & (t':. 
12. & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
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
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:Id
16. & ( (if source(l) = i <[locl(a)],x.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())
17. 
17. s(i;0).x
17. =
17. 2of()(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)],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>)  Id & (<j,t> < <i,t2>)  <j,t> = <i,t2>  E
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  ds(z)?Top
46. isnull(a(i;t3-1))
47. x:Id. s(i;t3-1+1).x = s(i;t3-1).x  vartype(i;x)
48. m(i;t3-1) = nil  Msg List
49. s(i;t3-1+1).z = s(i;t3-1).z  vartype(i;z)
50. x:Id. s(i;t3-1+1).x = s(i;t3-1).x  vartype(i;x)
51. m(i;t3-1) = nil  Msg List
52. s(i;t3-1+1).z = s(i;t3-1).z  vartype(i;z)
  s(i;t2+1).z = s(i;t3).z  ds(z)?Top
5 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