Selected Objects

def	lnk	lnk(k) == 1of(outl(k))
def	tagof	tag(k) == 2of(outl(k))
def	actof	act(k) == outr(k)
def	kindcase	kindcase(k;a.f(a);l,t.g(l;t)) == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi
def	has-src	has-src(i;k) == isrcv(k)source(lnk(k)) = i
def	deq	EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))
def	eqof	eqof(d) == 1of(d)
THM	deq_property	d:EqDecider(T), x,y:T. x = y  eqof(d)(x,y)
THM	eqof_eq_btrue	d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
THM	strong-subtype-deq	d:EqDecider(B). strong-subtype(A;B)  d  EqDecider(A)
THM	strong-subtype-deq-subtype	strong-subtype(A;B)  (EqDecider(B) r EqDecider(A))
THM	nat-deq-aux	a,b:. a = b  a=b
def	nat-deq	NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>
THM	atom-deq-aux	a,b:Atom. a = b  a=bAtom
def	atom-deq	AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
def	proddeq	proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))
THM	proddeq-property	a:EqDecider(A), b:EqDecider(B), p,q:(AB). p = q  proddeq(a;b)(p,q)
def	prod-deq-aux	prod-deq-aux{\\\\v:l,i:l}(A;B;a;b) == ext{proddeq_DASH_property}{i:l}(A,B,a,b)
def	prod-deq	prod-deq(A;B;a;b) == (A,B,a,b,p,q. q/q1,q2. == (p/p1,p2. == (b/eq,b1. == (a/e1,a1. == ((%1.%1 == ((%1.(<%.<(%1.%1(p1,q1)/%4,%5. %4((%1.%1)((%1.*)(*))))(a1) == ((%1.(<%.,(%1.%1(p2,q2)/%4,%5. %4((%1.%1)((%1.*)(*))))(b1)> == ((%1.(,%.%/%1,%2. *>)) == (((%1.%1.2) == ((((%1.%1 == ((((%1.(<p1,p2> = <q1,q2>  AB == ((((%1.,<p1,p2> = <q1,q2>  AB == ((((%1.,((e1(p1,q1))(eq(p2,q2))) == ((((%1.,(e1(p1,q1)) & (eq(p2,q2)) == ((((%1.,(%1.%1)((%1.<%2.%2,%2.%2>)(*)) == ((((%1.,(%1.%1) == ((((%1.,((%1.%1(e1(p1,q1),eq(p2,q2))) == ((((%1.,((p,q. InjCase(q; x. InjCase(p == ((((%1.,((p,q. InjCase(q; x. InjCase; x. <%.<*,*>,%.*> == ((((%1.,((p,q. InjCase(q; x. InjCase; y. <%.<any(%),*> == ((((%1.,((p,q. InjCase(q; x. InjCase; y. ,%.%/%1,%2. any(%1)>) == ((((%1.,((p,q. ; y. == ((((%1.,((p,q. InjCase(p == ((((%1.,((p,q. InjCase; x. <%.<*,any(%)>,%.%/%1,%2. any(%2)> == ((((%1.,((p,q. InjCase; y. <%.<any(%),any(%)>,%.%/%1,%2. any(%2)>)))))) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%5 == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%5 == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%6((%4.%4)((%4.%4)(%3)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%2)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%1) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%5 == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%6 == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%6((%4.%4)((%4.%4)(%3)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%1)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%2)))) == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%)> == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%6 == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%5 == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%5((%4.%4)((%4.%4)(%3)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%2)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%1) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%6 == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%6 == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((((%4.%4) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%4.%4/%5,%6. == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%5((%4.%4)((%4.%4)(%3)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%1)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%2)))) == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%)>>)))) == (A == ,B == ,a == ,b)
def	product-deq	product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
def	sumdeq	sumdeq(a;b)(p,q) == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))
THM	sumdeq-property	a:EqDecider(A), b:EqDecider(B), p,q:A+B. p = q  sumdeq(a;b)(p,q)
def	sum-deq-aux	sum-deq-aux{\\\\v:l,i:l}(A;B;a;b) == ext{sumdeq_DASH_property}{i:l}(A,B,a,b)
def	sum-deq	sum-deq(A;B;a;b) == (A,B,a,b,p,q. == (InjCase(q; x. InjCase(p == (InjCase(q; x. InjCase; x1. b/eq,b1. == (InjCase(q; x. InjCase; x1. a/e1,a1. == (InjCase(q; x. InjCase; x1. <%.(%1.%1(x1,x)/%4,%5. == (InjCase(q; x. InjCase; x1. <%.(%4 == (InjCase(q; x. InjCase; x1. <%.(((%1.%1) == (InjCase(q; x. InjCase; x1. <%.((((%1.*) == (InjCase(q; x. InjCase; x1. <%.(((((%1.%1(x)) == (InjCase(q; x. InjCase; x1. <%.((((((%1.%1(x1)) == (InjCase(q; x. InjCase; x1. <%.(((((((%1.%1(B)) == (InjCase(q; x. InjCase; x1. <%.((((((((%1.%1(A)) == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. (%1.%1) == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%1.(%2.*)(*)) == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%)))))))))) == (InjCase(q; x. InjCase; x1. <%.(a1) == (InjCase(q; x. InjCase; x1. ,%.*> == (InjCase(q; x. InjCase; y. b/eq,b1. == (InjCase(q; x. InjCase; y. a/e1,a1. == (InjCase(q; x. InjCase; y. <%.(%1.any((%1(*)))) == (InjCase(q; x. InjCase; y. <%.((%1.%1(x)) == (InjCase(q; x. InjCase; y. <%.(((%1.%1(y)) == (InjCase(q; x. InjCase; y. <%.((((%1.%1(B)) == (InjCase(q; x. InjCase; y. <%.(((((%1.%1(A)) == (InjCase(q; x. InjCase; y. <%.(((((A,B,y,x,%. == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase(%1 == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %2. any(%2) == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. (%4.any(%4)) == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. ((%4.(%5.(%6. == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. ((%4.(%5.(any(%6)) == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. ((%4.(%5.(*)) == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. ((%4.(*)) == (InjCase(q; x. InjCase; y. <%.((((((%1.InjCase; %3. ((%)))) == (InjCase(q; x. InjCase; y. <%.(((((((%1.%1)(inr(%.*)))))))) == (InjCase(q; x. InjCase; y. ,%.*>) == (; y. == (InjCase(p == (InjCase; x. b/eq,b1. == (InjCase; x. a/e1,a1. == (InjCase; x. <%.(%1.any((%1(*)))) == (InjCase; x. <%.((%1.%1(y)) == (InjCase; x. <%.(((%1.%1(x)) == (InjCase; x. <%.((((%1.%1(B)) == (InjCase; x. <%.(((((%1.%1(A)) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase(%1 == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %2. any(%2) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. (%4.any(%4)) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(%6.any(%6)) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(*)) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(*)) == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%)))) == (InjCase; x. <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*)))))))) == (InjCase; x. ,%.*> == (InjCase; y1. b/eq,b1. == (InjCase; y1. a/e1,a1. == (InjCase; y1. <%.(%1.%1(y1,y)/%4,%5. == (InjCase; y1. <%.(%4 == (InjCase; y1. <%.(((%1.%1) == (InjCase; y1. <%.((((%1.*) == (InjCase; y1. <%.(((((%1.%1(y)) == (InjCase; y1. <%.((((((%1.%1(y1)) == (InjCase; y1. <%.(((((((%1.%1(B)) == (InjCase; y1. <%.((((((((%1.%1(A)) == (InjCase; y1. <%.((((((((A,B,y1,y,%. (%1.%1)((%1.(%2.*)(*))(%)))))))))) == (InjCase; y1. <%.(b1) == (InjCase; y1. ,%.*>))) == (A == ,B == ,a == ,b)
def	union-deq	union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
def	deq-member	deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
THM	assert-deq-member	eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L)
def	discrete_struct	DS(A) == sort:ATypea:AEqDecider(sort(a))
def	dstype	dstype(TypeNames; d; a) == 1of(d)(a)
def	id-deq	IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
def	eq_id	a = b == eqof(IdDeq)(a,b)
THM	eq_id_self	a:Id. a = a ~ true
THM	assert-eq-id	a,b:Id. a = b  a = b
THM	decidable__equal_Id	a,b:Id. Dec(a = b)
def	idlnk-deq	IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
def	eq_lnk	a = b == eqof(IdLnkDeq)(a,b)
THM	assert-eq-lnk	a,b:IdLnk. a = b  a = b
THM	decidable__equal_IdLnk	a,b:IdLnk. Dec(a = b)
THM	decidable__l_member	x:A. (x,y:A. Dec(x = y))  (L:A List. Dec((x  L)))
def	lsrc	source(l) == 1of(l)
def	ldst	destination(l) == 1of(2of(l))
THM	lsrc-inv	l:IdLnk. source(lnk-inv(l)) = destination(l)
THM	ldst-inv	l:IdLnk. destination(lnk-inv(l)) = source(l)
def	lpath	lpath(p) == i:(||p||-1).  == destination(p[i]) = source(p[(i+1)]) & p[(i+1)] = lnk-inv(p[i])  IdLnk
THM	lpath_cons	l:IdLnk, p:IdLnk List. lpath([l / p]) lpath(p) & (||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l))
def	lconnects	lconnects(p;i;j) == lpath(p) == & (||p|| = 0    i = j  Id) == & (||p|| = 0    i = source(hd(p)) & j = destination(last(p)))
THM	lpath-members-connected	p:IdLnk List, i:||p||, j:(i+1). lpath(p)  lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))
def	Kind-deq	KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
def	eq_knd	a = b == eqof(KindDeq)(a,b)
THM	assert-eq-knd	a,b:Knd. a = b  a = b
THM	assert-has-src	i:Id, k:Knd. has-src(i;k)  isrcv(k) & source(lnk(k)) = i
def	event_system_typename	event_system_typename() == 6
def	strongwellfounded	SWellFounded(R(x;y)) == f:(T). x,y:T. R(x;y)  f(x)<f(y)
THM	strongwf-implies	R:(TTType). SWellFounded(R(x,y))  WellFnd{i}(T;x,y.R(x,y))
def	rel_plus	R^+(x,y) == n:. x R^n y
THM	rel_plus_trans	R:(TTProp). Trans x,y:T. x R^+ y
THM	rel_plus_implies	R:(TTProp), x,y:T. (x R^+ y)  (x R y)  (z:T. (x R^+ z) & (z R y))
def	eventtype	eventtype(k;loc;V;M;e) == kindcase(k(e);a.V(loc(e),a);l,t.M(l,t))
def	ESAxioms	ESAxioms{i:l} ESAxioms(E; ESAxioms(T; ESAxioms(M; ESAxioms(loc; ESAxioms(kind; ESAxioms(val; ESAxioms(when; ESAxioms(after; ESAxioms(sends; ESAxioms(sender; ESAxioms(index; ESAxioms(first; ESAxioms(pred; ESAxioms(causl) == (e,e':E. loc(e) = loc(e')  Id  causl(e,e')  e = e'  causl(e',e)) == & (e:E. (first(e))  (e':E. loc(e') = loc(e)  Id  causl(e',e))) == & (e:E.  == & ((first(e)) == & ( == & (loc(pred(e)) = loc(e)  Id & causl(pred(e),e) == & (& (e':E. loc(e') = loc(e)  Id  (causl(pred(e),e') & causl(e',e)))) == & (e:E. (first(e))  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))) == & (Trans e,e':E. causl(e,e')) == & SWellFounded(causl(e,e')) == & (e:E.  == & (isrcv(kind(e)) == & ( == & ((sends(lnk(kind(e)),sender(e)))[(index(e))] == & (= == & (msg(lnk(kind(e));tag(kind(e));val(e)) == & ( Msg(M)) == & (e:E. isrcv(kind(e))  causl(sender(e),e)) == & (e,e':E. == & (causl(e,e') == & ( == & ((first(e')) & causl(e,pred(e'))  e = pred(e') == & ( isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')) == & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))) == & (e:E, l:IdLnk. == & (loc(e) = source(l)  sends(l,e) = nil  Msg_sub(l; M) List) == & (e,e':E. == & (isrcv(kind(e)) == & ( == & (isrcv(kind(e')) == & ( == & (lnk(kind(e)) = lnk(kind(e')) == & ( == & ((causl(e,e') == & (( == & ((causl(sender(e),sender(e')) == & (( sender(e) = sender(e')  E & index(e)<index(e'))) == & (e:E, l:IdLnk, n:||sends(l,e)||. == & (e':E.  == & (isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n)
def	event_system	ES == E:Type == EqDecider(E)(T:IdIdType == EqDecider(E)(V:IdIdType == EqDecider(E)(M:IdLnkIdType == EqDecider(E)(Top(loc:EId == EqDecider(E)(Top(kind:EKnd == EqDecider(E)(Top(val:(e:Eeventtype(kind;loc;V;M;e)) == EqDecider(E)(Top(when:(x:Ide:ET(loc(e),x)) == EqDecider(E)(Top(after:(x:Ide:ET(loc(e),x)) == EqDecider(E)(Top(sends:(l:IdLnkE(Msg_sub(l; M) List)) == EqDecider(E)(Top(sender:{e:E| isrcv(kind(e)) }E == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||sends == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||(lnk(kind(e)) == EqDecider(E)(Top(index:(e:{e:E| isrcv(kind(e)) }||,sender(e))||) == EqDecider(E)(Top(first:E == EqDecider(E)(Top(pred:{e':E| (first(e')) }E == EqDecider(E)(Top(causl:EEProp == EqDecider(E)(Top(ESAxioms{i:l} == EqDecider(E)(Top(ESAxioms(E; == EqDecider(E)(Top(ESAxioms(T; == EqDecider(E)(Top(ESAxioms(M; == EqDecider(E)(Top(ESAxioms(loc; == EqDecider(E)(Top(ESAxioms(kind; == EqDecider(E)(Top(ESAxioms(val; == EqDecider(E)(Top(ESAxioms(when; == EqDecider(E)(Top(ESAxioms(after; == EqDecider(E)(Top(ESAxioms(sends; == EqDecider(E)(Top(ESAxioms(sender; == EqDecider(E)(Top(ESAxioms(index; == EqDecider(E)(Top(ESAxioms(first; == EqDecider(E)(Top(ESAxioms(pred; == EqDecider(E)(Top(ESAxioms(causl) == EqDecider(E)(Top(Top))
def	mk-es	mk-es(E; eq; T; V; M; loc; k; v; w; a; snds; sndr; i; f; prd; cl; p) == <E,eq,T,V,M,,loc,k,v,w,a,snds,sndr,i,f,prd,cl,p,>
def	es-E	E == 1of(es)
def	es-eq-E	e = e' == eqof(1of(2of(es)))(e,e')
THM	assert-es-eq-E	the_es:ES, e,e':E. e = e'  e = e'
THM	decidable__es-E_equal	the_es:ES, e,e':E. Dec(e = e')
def	es-Msg	Msg == Msg(1of(2of(2of(2of(2of(es))))))
def	es-Msgl	(Msg on l) == {m:Msg| haslink(l; m) }
def	es-loc	loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e)
def	es-kind	kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e)
def	es-isrcv	isrcv(e) == isrcv(kind(e))
def	es-tag	tag(e) == tag(kind(e))
def	es-lnk	lnk(e) == lnk(kind(e))
def	es-act	act(e) == act(kind(e))
def	es-rcvtype	rcvtype(e) == 1of(2of(2of(2of(2of(es)))))(lnk(e),tag(e))
def	es-acttype	acttype(e) == 1of(2of(2of(2of(es))))(loc(e),act(e))
def	es-valtype	valtype(e) == if isrcv(e) rcvtype(e) else acttype(e) fi
def	es-vartype	vartype(i;x) == 1of(2of(2of(es)))(i,x)
def	es-val	val(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))(e)
def	es-when	(x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e)
def	es-after	(x after e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))(x,e)
def	es-sends	sends(l;e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))))(l,e)
def	es-sender	sender(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))))(e)
def	es-index	index(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))))))(e)
def	es-first	first(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))))))) == (e)
def	es-pred	pred(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of( == 1of(es)))))))))))))))) == (e)
def	es-causl	(e < e') == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of( == 1of(es))))))))))))))))) == (e == ,e')
def	es-locl	(e <loc e') == loc(e) = loc(e')  Id & (e < e')
def	es-le	e  e'  == (e <loc e')  e = e'  E
THM	es-axioms	the_es:ES.  (Trans e,e':E. (e <loc e')) & SWellFounded((e <loc e')) & (e,e':E. loc(e) = loc(e')  Id  (e <loc e')  e = e'  (e' <loc e)) & (e:E. first(e)  (e':E. (e' <loc e))) & (e:E.  & (first(e)  (pred(e) <loc e) & (e':E. ((pred(e) <loc e') & (e' <loc e)))) & (e:E.  & (first(e)  (x:Id. (x when e) = (x after pred(e))  vartype(loc(e);x))) & (Trans e,e':E. (e < e')) & SWellFounded((e < e')) & (e:E.  & (isrcv(e) & ( & (sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))  Msg) & (e,e':E. (e <loc e')  (e < e')) & (e:E. isrcv(e)  (sender(e) < e)) & (e,e':E. & ((e < e') & ( & (first(e') & (e < pred(e'))  e = pred(e')  E & ( isrcv(e') & (e < sender(e'))  e = sender(e')  E) & (e:E. isrcv(e)  loc(e) = destination(lnk(e))) & (e:E, l:IdLnk. loc(e) = source(l)  sends(l;e) = nil  (Msg on l) List) & (e,e':E. & (isrcv(e) & ( & (isrcv(e') & ( & (lnk(e) = lnk(e') & ( & (((e <loc e') & (( & (((sender(e) <loc sender(e')) & (( sender(e) = sender(e')  E & index(e)<index(e'))) & (e:E, l:IdLnk, n:||sends(l;e)||. & (e':E. isrcv(e') & lnk(e') = l & sender(e') = e  E & index(e') = n  )
THM	es-locl-wellfnd	the_es:ES. WellFnd{i}(E;x,y.(x <loc y))
THM	es-locl-trans	the_es:ES. Trans x,y:E. (x <loc y)
THM	es-le-trans	the_es:ES. Trans x,y:E. x  y
THM	es-locl-swellfnd	the_es:ES. SWellFounded((x <loc y))
THM	es-locl-antireflexive	the_es:ES, e:E. (e <loc e)
THM	es-pred-locl	the_es:ES, j:E. first(j)  (pred(j) <loc j)
THM	es-first-implies	the_es:ES, j,e:E. first(j)  (e <loc j)
THM	es-loc-pred	the_es:ES, e:E. first(e)  loc(pred(e)) = loc(e)  Id
THM	es-loc-rcv	es:ES, e:E, l:IdLnk, tg:Id. kind(e) = rcv(l; tg)  loc(e) = destination(l) & loc(sender(e)) = source(l)
THM	es-le-loc	es:ES, e,e':E. e  e'   loc(e) = loc(e')  Id
THM	es-locl-iff	the_es:ES, e,e':E. (e <loc e')  first(e') & e = pred(e')  E  (e <loc pred(e'))
THM	decidable__es-locl	the_es:ES, e',e:E. Dec((e <loc e'))

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