IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
w-es wf
2
2
1
1
1
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)
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
world_DASH_event_DASH_system{1:l, i:l}
the_w:World
FairFifo
the_w:World


ESAxioms{i:l}
ESAxioms(E;
ESAxioms((
i,x. vartype(i;x));
ESAxioms(the_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'))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html