1. w : World
2. 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)
  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'}

By:

let A let  Auto THEN Try (Analyze -1 THEN Unhide THEN Complete Auto) let  THEN let  Try (Analyze -2 THEN Unhide THEN Complete Auto) let  THEN let  Try (Unfold `w-E` 0 THEN DeqSubtype) let  THEN let  Try (DoSubsume THEN SubtypeRelEq THEN BackThruSomeHyp) , let B let  Analyze let  THENL let  [Analyze let  [THENL let  [[BackThru let  [[Thm* the_w:World, l:IdLnk, e:E. sends(l;e)  Msg_sub(l; the_w.M) List let  [;Auto] let  ;Auto] in Using [`V',(i,a. V(i;locl(a)))] Analyze THEN Reduce 0 THEN Try (Complete A) THEN Try (Complete B)

None

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