Def @i (with ds: ds init: init action a:T precondition a(v) is P s v)(j)
Def == if eqof(IdDeq)(j,i)
Def == if (with ds: ds
Def == if (init: init
Def == if action a:T
Def == if aprecondition a(v) is
Def == if aP)
Def == else  fi

is mentioned by

Thm* i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp), Thm* init:x:Id fp-> ds(x)?Void. Thm* (x:Id. x  dom(ds)  x  dom(init)) Thm*  Thm* @i (with ds: ds Thm* @i init: init Thm* @i action a:T Thm* @i precondition a(v) is Thm* @i P s v)  Thm* realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)

[pre-init-rule]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html