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-init-rule
  i,a:Id, T:Type, ds:a:Id fp-> Type, P:(State(ds)TProp),
  init:x:Id fp-> ds(x)?Void.
  (x:Id. x  dom(ds)  x  dom(init))
  
  @i: (with ds: ds init: initaction a:T precondition a(v) is P)  Dsys
  & (D:Dsys. 
  & (@i: (with ds: ds
  & (@init: init
  & (action a:T
  & (aprecondition a(v) is
  & (aP)  D
  & (
  & (D 
  & (realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id))
By: NewSpecializeEsLemmaOn Thm: pre-init-rule
(with ds: ds
(init: init
action a:T
aprecondition a(v) is
aP)

Generated subgoals:

None

About:
assertitvoidlambdaapplyfunctionuniverseequal
memberpropimpliesallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc