Who Cites event system?
event_system	Def ES Def == E:Type Def == EqDecider(E)(T:IdIdType Def == EqDecider(E)(V:IdIdType Def == EqDecider(E)(M:IdLnkIdType Def == EqDecider(E)(Top(loc:EId Def == EqDecider(E)(Top(kind:EKnd Def == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e)) Def == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x)) Def == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List)) Def == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e)) Def == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||) Def == EqDecider(E)(Top(first:E Def == EqDecider(E)(Top(pred:{e':E| (first(e')) }E Def == EqDecider(E)(Top(causl:EEProp Def == EqDecider(E)(Top(ESAxioms{i:l} Def == EqDecider(E)(Top(ESAxioms(E; Def == EqDecider(E)(Top(ESAxioms(T; Def == EqDecider(E)(Top(ESAxioms(M; Def == EqDecider(E)(Top(ESAxioms(loc; Def == EqDecider(E)(Top(ESAxioms(kind; Def == EqDecider(E)(Top(ESAxioms(val; Def == EqDecider(E)(Top(ESAxioms(when; Def == EqDecider(E)(Top(ESAxioms(after; Def == EqDecider(E)(Top(ESAxioms(sends; Def == EqDecider(E)(Top(ESAxioms(sender; Def == EqDecider(E)(Top(ESAxioms(index; Def == EqDecider(E)(Top(ESAxioms(first; Def == EqDecider(E)(Top(ESAxioms(pred; Def == EqDecider(E)(Top(ESAxioms(causl) Def == EqDecider(E)(Top(Top))
	Thm* ES  Type{i'}
top	Def Top == Void given Void
	Thm* Top  Type
ESAxioms	Def ESAxioms{i:l} Def ESAxioms(E; Def ESAxioms(T; Def ESAxioms(M; Def ESAxioms(loc; Def ESAxioms(kind; Def ESAxioms(val; Def ESAxioms(when; Def ESAxioms(after; Def ESAxioms(sends; Def ESAxioms(sender; Def ESAxioms(index; Def ESAxioms(first; Def ESAxioms(pred; Def ESAxioms(causl) Def == (e,e':E. loc(e) = loc(e')  Id  causl(e,e')  e = e'  causl(e',e)) Def == & (e:E. (first(e))  (e':E. loc(e') = loc(e)  Id  causl(e',e))) Def == & (e:E.  Def == & ((first(e)) Def == & ( Def == & (loc(pred(e)) = loc(e)  Id & causl(pred(e),e) Def == & (& (e':E.  Def == & (& (loc(e') = loc(e)  Id  (causl(pred(e),e') & causl(e',e)))) Def == & (e:E.  Def == & ((first(e))  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))) Def == & (Trans e,e':E. causl(e,e')) Def == & SWellFounded(causl(e,e')) Def == & (e:E.  Def == & (isrcv(kind(e)) Def == & ( Def == & ((sends(lnk(kind(e)),sender(e)))[(index(e))] Def == & (= Def == & (msg(lnk(kind(e));tag(kind(e));val(e)) Def == & ( Msg(M)) Def == & (e:E. isrcv(kind(e))  causl(sender(e),e)) Def == & (e,e':E. Def == & (causl(e,e') Def == & ( Def == & ((first(e')) & causl(e,pred(e'))  e = pred(e') Def == & ( isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')) Def == & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))) Def == & (e:E, l:IdLnk. Def == & (loc(e) = source(l)  sends(l,e) = nil  Msg_sub(l; M) List) Def == & (e,e':E. Def == & (isrcv(kind(e)) Def == & ( Def == & (isrcv(kind(e')) Def == & ( Def == & (lnk(kind(e)) = lnk(kind(e')) Def == & ( Def == & ((causl(e,e') Def == & (( Def == & ((causl(sender(e),sender(e')) Def == & (( sender(e) = sender(e')  E & index(e)<index(e'))) Def == & (e:E, l:IdLnk, n:||sends(l,e)||. Def == & (e':E.  Def == & (isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n)
	Thm* E:Type{i}, T,V:(IdIdType{i}), M:(IdLnkIdType{i}), loc:(EId), Thm* kind:(EKnd), val:(e:Eeventtype(kind;loc;V;M;e)), Thm* when,after:(x:Ide:ET(loc(e),x)), Thm* sends:(l:IdLnkE(Msg_sub(l; M) List)), Thm* sender:({e:E| isrcv(kind(e)) }E), Thm* index:(e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||), Thm* first:(E), pred:({e':E| first(e') }E), causl:(EEProp{i}). Thm* ESAxioms{i:l} Thm* ESAxioms(E; Thm* ESAxioms(T; Thm* ESAxioms(M; Thm* ESAxioms(loc; Thm* ESAxioms(kind; Thm* ESAxioms(val; Thm* ESAxioms(when; Thm* ESAxioms(after; Thm* ESAxioms(sends; Thm* ESAxioms(sender; Thm* ESAxioms(index; Thm* ESAxioms(first; Thm* ESAxioms(pred; Thm* ESAxioms(causl) Thm*  Prop{i'}
deq	Def EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))
	Thm* T:Type. EqDecider(T)  Type
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
Msg_sub	Def Msg_sub(l; M) == {m:Msg(M)| haslink(l; m) }
	Thm* M:(IdLnkIdType), l:IdLnk. Msg_sub(l; M)  Type
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
Msg	Def Msg(M) == l:IdLnkt:IdM(l,t)
	Thm* M:(IdLnkIdType). Msg(M)  Type
haslink	Def haslink(l; m) == mlnk(m) = l
	Thm* M:(IdLnkIdType), l:IdLnk, m:Msg(M). haslink(l; m)  Prop
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
strongwellfounded	Def SWellFounded(R(x;y)) == f:(T). x,y:T. R(x;y)  f(x)<f(y)
	Thm* T:Type, R:(TTType). SWellFounded(R(x,y))  Prop
lelt	Def i  j < k == ij & j<k
nat	Def  == {i:| 0i }
	Thm*   Type
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
eventtype	Def eventtype(k;loc;V;M;e) == kindcase(k(e);a.V(loc(e),a);l,t.M(l,t))
	Thm* E:Type, V:(IdIdType), M:(IdLnkIdType), loc:(EId), k:(EKnd), Thm* e:E. eventtype(k;loc;V;M;e)  Type
kindcase	Def kindcase(k;a.f(a);l,t.g(l;t)) Def == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi
	Thm* B:Type, k:Knd, f:(IdB), g:(IdLnkIdB). Thm* kindcase(k;a.f(a);l,t.g(l,t))  B
lnk	Def lnk(k) == 1of(outl(k))
	Thm* k:Knd. isrcv(k)  lnk(k)  IdLnk
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
isrcv	Def isrcv(k) == isl(k)
	Thm* k:Knd. isrcv(k)
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
ldst	Def destination(l) == 1of(2of(l))
	Thm* l:IdLnk. destination(l)  Id
tagof	Def tag(k) == 2of(outl(k))
	Thm* k:Knd. isrcv(k)  tag(k)  Id
select	Def l[i] == hd(nth_tl(i;l))
	Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n]  A
trans	Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)
	Thm* T:Type, E:(TTProp). (Trans x,y:T. E(x,y))  Prop
outl	Def outl(x) == InjCase(x; y. y; z. "???")
	Thm* A,B:Type, x:A+B. isl(x)  outl(x)  A
mlnk	Def mlnk(m) == 1of(m)
	Thm* M:(IdLnkIdType), m:Msg(M). mlnk(m)  IdLnk
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
islocal	Def islocal(k) == isl(k)
	Thm* k:Knd. islocal(k)
isl	Def isl(x) == InjCase(x; y. true; z. false)
	Thm* A,B:Type, x:A+B. isl(x)
rev_implies	Def P  Q == Q  P
	Thm* A,B:Prop. (A  B)  Prop
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
nth_tl	Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi  (recursive)
	Thm* A:Type, as:A List, i:. nth_tl(i;as)  A List
hd	Def hd(l) == Case of l; nil  "?" ; h.t  h
	Thm* A:Type, l:A List. ||l||1  hd(l)  A
actof	Def act(k) == outr(k)
	Thm* k:Knd. islocal(k)  act(k)  Id
tl	Def tl(l) == Case of l; nil  nil ; h.t  t
	Thm* A:Type, l:A List. tl(l)  A List
le_int	Def ij == j<i
	Thm* i,j:. (ij)
outr	Def outr(x) == InjCase(x; y. "???"; z. z)
	Thm* A,B:Type, x:A+B. isl(x)  outr(x)  B
bnot	Def b == if b false else true fi
	Thm* b:. b
lt_int	Def i<j == if i<j true ; false fi
	Thm* i,j:. (i<j)

Syntax:

ES

has structure:

event_system{i:l}

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