(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. 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 
12. realizes es.(v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v))
12. realizes es.
12. realizes es.(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 
15. realizes es.(vartype(i;x) r A)
15. realizes es.& (e:E. loc(e) = i  first(e)  (x when e) = c)
16. D 
16. realizes es.(vartype(i;x) r A)
16. realizes es.& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
16. realizes es.& (e:E. 
16. realizes es.& (loc(e) = i
16. realizes es.& (
16. realizes es.& ((kind(e) = locl(a)  P((x when e),val(e)))
16. realizes es.& (& (e':E. 
16. realizes es.& (& ((e <loc e')  e = e'
16. realizes es.& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
17. D 
17. realizes es.(v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v))
17. realizes es.
17. realizes es.(e:E. loc(e) = i)
  D 
  realizes es.(vartype(i;x) r A)
  realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  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.& & ((v:T. P(c,v))
  realizes es.& & (
  realizes es.& & ((e:E. 
  realizes es.& & ((loc(e) = i  Id
  realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v))))
By: All (Unfold `d-realizes`)

Generated subgoal:

1 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))
12. ((
12. (((e:E. loc(e) = i  Id)))
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)
15. (& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A))
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  Id  kind(e) = locl(a)  (valtype(e) r T))
16. (& (e:E. 
16. (& (loc(e) = i  Id
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))
17. (
17. ((e:E. loc(e) = i  Id))
  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)))))
9 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