(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 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;p)  ES
By: Assert
(ESAxioms{i:l}
(ESAxioms(E;
(ESAxioms((i,x. vartype(i;x));
(ESAxioms(w.M;
(ESAxioms((e.loc(e));
(ESAxioms((e.kind(e));
(ESAxioms((e.val(e));
(ESAxioms((x,e. (x when e));
(ESAxioms((x,e. (x after e));
(ESAxioms((l,e. sends(l;e));
(ESAxioms((e.sender(e));
(ESAxioms((e.index(e));
(ESAxioms((e.first(e));
(ESAxioms((e.pred(e));
(ESAxioms((e,e'. e <c e'))
( Type{i'})

Generated subgoals:

1   ESAxioms{i:l}
  ESAxioms(E;
  ESAxioms((i,x. vartype(i;x));
  ESAxioms(w.M;
  ESAxioms((e.loc(e));
  ESAxioms((e.kind(e));
  ESAxioms((e.val(e));
  ESAxioms((x,e. (x when e));
  ESAxioms((x,e. (x after e));
  ESAxioms((l,e. sends(l;e));
  ESAxioms((e.sender(e));
  ESAxioms((e.index(e));
  ESAxioms((e.first(e));
  ESAxioms((e.pred(e));
  ESAxioms((e,e'. e <c e'))
   Type{i'}
1 step
2 4. ESAxioms{i:l}
4. ESAxioms(E;
4. ESAxioms((i,x. vartype(i;x));
4. ESAxioms(w.M;
4. ESAxioms((e.loc(e));
4. ESAxioms((e.kind(e));
4. ESAxioms((e.val(e));
4. ESAxioms((x,e. (x when e));
4. ESAxioms((x,e. (x after e));
4. ESAxioms((l,e. sends(l;e));
4. ESAxioms((e.sender(e));
4. ESAxioms((e.index(e));
4. ESAxioms((e.first(e));
4. ESAxioms((e.pred(e));
4. ESAxioms((e,e'. e <c e'))
4.  Type{i'}
  ES(w;p)  ES
7 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