the_w:World.
Thm* FairFifo
Thm*
Thm* ESAxioms{i:l}
Thm* ESAxioms(E;
Thm* ESAxioms((
i,x. vartype(i;x));
Thm* ESAxioms(the_w.M;
Thm* ESAxioms((
e.loc(e));
Thm* ESAxioms((
e.kind(e));
Thm* ESAxioms((
e.val(e));
Thm* ESAxioms((
x,e. (x when e));
Thm* ESAxioms((
x,e. (x after e));
Thm* ESAxioms((
l,e. sends(l;e));
Thm* ESAxioms((
e.sender(e));
Thm* ESAxioms((
e.index(e));
Thm* ESAxioms((
e.first(e));
Thm* ESAxioms((
e.pred(e));
Thm* ESAxioms((
e,e'. e <c e'))Def == <E
Def == ,product-deq(Id;
;IdDeq;NatDeq)
Def == ,(
i,x. vartype(i;x))
Def == ,(
i,a. V(i;locl(a)))
Def == ,the_w.M
Def == ,
Def == ,(
e.loc(e))
Def == ,(
e.kind(e))
Def == ,(
e.val(e))
Def == ,(
x,e. (x when e))
Def == ,(
x,e. (x after e))
Def == ,(
l,e. sends(l;e))
Def == ,(
e.sender(e))
Def == ,(
e.index(e))
Def == ,(
e.first(e))
Def == ,(
e.pred(e))
Def == ,(
e,e'. e <c e')
Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p)
Def == ,
>