(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-pre-init-rule1 2 2 1 1 1 1 2 2 1 1 2 2 1
1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : ATProp
8. (s,v. P(s(x),v))  State(x : A)TProp
9. x@0:Id. x@0  dom(x : A)  x@0  dom(x : c)
10. x : c  x@0:Id fp-> x : A(x@0)?Void
11. @i: (with ds: x : A
11. @init: x : c
11. action a:T
11. aprecondition a(v) is
11. as,v. P(s(x),v))
11.  Dsys
12. D:Dsys. 
12. @i: (with ds: x : A
12. @init: x : c
12. action a:T
12. aprecondition a(v) is
12. as,v. P(s(x),v))  D
12. 
12. (D':Dsys. 
12. (D  D'
12. (
12. ((w:World, p:FairFifo.
12. ((PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i)))
13. D : Dsys
14. @i: (with ds: x : A
14. @init: x : c
14. action a:T
14. aprecondition a(v) is
14. as,v. P(s(x),v))  D
15. D':Dsys. 
15. D  D'
15. 
15. (w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((vartype(i;x) r A) & (e:E. loc(e) = i  first(e)  (x when e) = c))
16. D':Dsys. 
16. D  D'
16. 
16. (w:World, p:FairFifo.
16. (PossibleWorld(D';w)
16. (
16. ((vartype(i;x) r A)
16. (& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
16. (& (e:E. 
16. (& (loc(e) = i
16. (& (
16. (& ((kind(e) = locl(a)  P((x when e),val(e)))
16. (& (& (e':E. 
16. (& (& ((e <loc e')  e = e'
16. (& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v)))))
17. D':Dsys. 
17. D  D'
17. 
17. (w:World, p:FairFifo.
17. (PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i))
18. D' : Dsys
19. D  D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. vartype(i;x) r A
24. e:E. loc(e) = i  first(e)  (x when e) = c
25. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T)
26. vartype(i;x) r A
27. e:E. loc(e) = i  first(e)  (x when e) = c
28. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T)
29. vartype(i;x) r A
30. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T)
31. e:E. 
31. loc(e) = i
31. 
31. (kind(e) = locl(a)  P((x when e),val(e)))
31. & (e':E. 
31. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
32. vartype(i;x) r A
33. e:E. loc(e) = i  first(e)  (x when e) = c
34. e:E. loc(e) = i  kind(e) = locl(a)  P((x when e),val(e))
35. v:T. P(c,v)
  e:E. loc(e) = i  Id & kind(e) = locl(a)  (v:T. P((x after e),v))
By: AllHyps (h.InstHyp [D';w;p] h THENA Complete (Reduce 0)) THEN ExRepD
THEN
InstHyp [e] -3
THEN
ParallelLast
THEN
ExRepD

Generated subgoals:

1 35. v : T
36. P(c,v)
37. e : E
38. loc(e) = i  Id
39. vartype(i;x) r A
40. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
41. e:E. 
41. loc(e) = i  Id
41. 
41. (kind(e) = locl(a)  P((x when e),val(e)))
41. & (e':E. 
41. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
42. vartype(i;x) r A
43. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
44. kind(e) = locl(a)  P((x when e),val(e))
45. e' : E
46. (e <loc e')  e = e'
47. kind(e') = locl(a)  (v:T. P((x after e'),v))
  loc(e') = i  Id
1 step
2 35. v : T
36. P(c,v)
37. e : E
38. loc(e) = i  Id
39. vartype(i;x) r A
40. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
41. e:E. 
41. loc(e) = i  Id
41. 
41. (kind(e) = locl(a)  P((x when e),val(e)))
41. & (e':E. 
41. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
42. vartype(i;x) r A
43. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
44. kind(e) = locl(a)  P((x when e),val(e))
45. e' : E
46. (e <loc e')  e = e'
47. kind(e') = locl(a)  (v:T. P((x after e'),v))
48. e1 : E
49. loc(e1) = i  Id
50. T
  (x after e1)  A
2 steps

About:
assertvoidlambdaapplyfunctionuniverseequalmember
subtype_relpropimpliesandorall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc