(11steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-es wf
  w:World, p:FairFifo. ES(w)  ES
By: Auto
THEN
Assert
(e:E. 
(V(loc(e);kind(e)) = eventtype(e.kind(e);e.loc(e);i,a. V(i;locl(a));w.M;e))

Generated subgoals:

1 1. w : World
2. FairFifo
  e:E. 
  V(loc(e);kind(e)) = eventtype(e.kind(e);e.loc(e);i,a. V(i;locl(a));w.M;e)
1 step
2 1. w : World
2. p : FairFifo
3. e:E. 
3. V(loc(e);kind(e)) = eventtype(e.kind(e);e.loc(e);i,a. V(i;locl(a));w.M;e)
  ES(w)  ES
9 steps

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

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