(6steps 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: s-pre-rule1 2
1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. P : ATProp
7. @i: (with ds: x : A
7. @action a:T
7. @precondition a(v) is
7. @s,v. P(s(x),v) s v)
7.  Dsys
7. & (D:Dsys. 
7. & (@i: (with ds: x : A
7. & (@action a:T
7. & (@precondition a(v) is
7. & (@s,v. P(s(x),v) s v)  D
7. & (
7. & (D 
7. & (realizes es.(x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
7. & (realizes es.& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
7. & (realizes es.& (e:E. 
7. & (realizes es.& (loc(e) = i
7. & (realizes es.& (
7. & (realizes es.& ((kind(e) = locl(a)
7. & (realizes es.& ((
7. & (realizes es.& (((s,v. P(s(x),v))((z.(z when e)),val(e)))
7. & (realizes es.& (& (e':E. 
7. & (realizes es.& (& ((e <loc e')  e = e'
7. & (realizes es.& (& (& kind(e') = locl(a)
7. & (realizes es.& (& (&  (v:T. (s,v. P(s(x),v))((z.(z after e')),v)))))
  @i: (with ds: x : A
  @action a:T
  @precondition a(v) is
  @s,v. P(s(x),v) s v)
   Dsys
  & (D:Dsys. 
  & (@i: (with ds: x : A
  & (@action a:T
  & (@precondition a(v) is
  & (@s,v. P(s(x),v) s v)  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& ((kind(e) = locl(a)  Knd  P((x when e),val(e)))
  & (realizes es.& (& (e':E. 
  & (realizes es.& (& ((e <loc e')  e = e'  E
  & (realizes es.& (& (& kind(e') = locl(a)  Knd
  & (realizes es.& (& (&  (v:T. P((x after e'),v)))))
By: Analyze -1 THEN Analyze 0 THEN Try Trivial THEN All Reduce THEN ParallelOp -2
THEN
RepeatFor 7 (ParallelOp -1)
THEN
ExRepD
THEN
Analyze 0
THEN
Try Trivial

Generated subgoal:

1 7. @i: (with ds: x : A
7. @action a:T
7. @precondition a(v) is
7. @s,v. P(s(x),v) s v)
7.  Dsys
8. D:Dsys. 
8. @i: (with ds: x : A
8. @action a:T
8. @precondition a(v) is
8. @s,v. P(s(x),v) s v)  D
8. 
8. D 
8. realizes es.(x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
8. realizes es.& (e:E. 
8. realizes es.& (loc(e) = i  Id
8. realizes es.& (
8. realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
8. realizes es.& (e:E. 
8. realizes es.& (loc(e) = i  Id
8. realizes es.& (
8. realizes es.& ((kind(e) = locl(a)  Knd  P((x when e),val(e)))
8. realizes es.& (& (e':E. 
8. realizes es.& (& ((e <loc e')  e = e'  E
8. realizes es.& (& (& kind(e') = locl(a)  Knd  (v:T. P((x after e'),v))))
9. @i: (with ds: x : A
9. @action a:T
9. @precondition a(v) is
9. @s,v. P(s(x),v) s v)
9.  Dsys
10. D : Dsys
11. @i: (with ds: x : A
11. @action a:T
11. @precondition a(v) is
11. @s,v. P(s(x),v) s v)  D
12. D':Dsys. 
12. D  D'
12. 
12. (w:World, p:FairFifo.
12. (PossibleWorld(D';w)
12. (
12. ((x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
12. (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
12. (& (e:E. 
12. (& (loc(e) = i  Id
12. (& (
12. (& ((kind(e) = locl(a)  P((x when e),val(e)))
12. (& (& (e':E. 
12. (& (& ((e <loc e')  e = e'
12. (& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v)))))
13. D' : Dsys
14. D  D'
15. w:World, p:FairFifo.
15. PossibleWorld(D';w)
15. 
15. (x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
15. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
15. & (e:E. 
15. & (loc(e) = i  Id
15. & (
15. & ((kind(e) = locl(a)  P((x when e),val(e)))
15. & (& (e':E. 
15. & (& ((e <loc e')  e = e'
15. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
16. w : World
17. p:FairFifo. 
17. PossibleWorld(D';w)
17. 
17. (x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
17. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
17. & (e:E. 
17. & (loc(e) = i  Id
17. & (
17. & ((kind(e) = locl(a)  P((x when e),val(e)))
17. & (& (e':E. 
17. & (& ((e <loc e')  e = e'
17. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
18. p : FairFifo
19. PossibleWorld(D';w)
20. x@0:Id. vartype(i;x@0) r x : A(x@0)?Top
21. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
22. e:E. 
22. loc(e) = i  Id
22. 
22. (kind(e) = locl(a)  P((x when e),val(e)))
22. & (e':E. 
22. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
  (vartype(i;x) r A)
  & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
3 steps

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

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