(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
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)
12. ((
12. (((v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),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)
17. (
17. ((v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v))  (e:E. loc(e) = i))
  D':Dsys. 
  D  D'
  
  (w:World, p:FairFifo.
  (PossibleWorld(D';w)
  (
  ((vartype(i;x) r A)
  (& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
  (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  P((x when e),val(e)))
  (& & ((v:T. P(c,v))
  (& & (
  (& & ((e:E. 
  (& & ((loc(e) = i  Id & kind(e) = locl(a)  (v:T. P((x after e),v)))))
By: RepeatFor 6 (Analyze 0)
THEN
AllHyps (h.InstHyp [D';w;p] h THENA Complete (Reduce 0))

Generated subgoals:

1 18. D' : Dsys
19. D  D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. (vartype(i;x) r A)
23. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
23. & (e:E. 
23. & (loc(e) = i  Id
23. & (
23. & ((kind(e) = locl(a)  P((x when e),val(e)))
23. & (& (e':E. 
23. & (& ((e <loc e')  e = e'
23. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
24. (vartype(i;x) r A)
24. & (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  (vartype(i;x) r A)
  & (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
1 step
2 18. D' : Dsys
19. D  D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. (vartype(i;x) r A)
23. & (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
23. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
24. (vartype(i;x) r A)
24. & (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
24. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
25. (vartype(i;x) r A)
25. & (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
25. & (e:E. 
25. & (loc(e) = i  Id
25. & (
25. & ((kind(e) = locl(a)  P((x when e),val(e)))
25. & (& (e':E. 
25. & (& ((e <loc e')  e = e'
25. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
26. (vartype(i;x) r A)
26. & (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  (e:E. loc(e) = i  Id  kind(e) = locl(a)  P((x when e),val(e)))
  & ((v:T. P(c,v))
  & (
  & ((e:E. loc(e) = i  Id & kind(e) = locl(a)  (v:T. P((x after e),v))))
7 steps

About:
assertitvoidlambdaapplyfunctionuniverseequalmember
subtype_relpropimpliesandorallexists
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