Selected Objects

THM	s-sends-rule1	x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)). (rcv(l; tg) = k  T = B) @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  Dsys & (D:Dsys.  & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  D & ( & (D  & (realizes es.(vartype(source(l);x) r A) & (realizes es.& (e:E.  & (realizes es.& (loc(e) = source(l)  Id & (realizes es.& ( & (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) & (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) & (realizes es.& (e:E.  & (realizes es.& (loc(e) = source(l)  Id & (realizes es.& ( & (realizes es.& (kind(e) = k  Knd & (realizes es.& ( & (realizes es.& ((L:{e':E| kind(e') = rcv(l; tg)  Knd } List.  & (realizes es.& (((e':E.  & (realizes es.& ((((e'  L) & (realizes es.& ((( & (realizes es.& (((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E) & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e))  T List)))
THM	s-unconditional-send1-rule	x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. (rcv(l; tg) = k  T = B) (f:(ABT).  (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))  Dsys (& (D:Dsys.  (& (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]))  D (& ( (& (D  (& (realizes es.(vartype(source(l);x) r A) (& (realizes es.& (e:E.  (& (realizes es.& (loc(e) = source(l)  Id (& (realizes es.& ( (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) (& (realizes es.& (e:E.  (& (realizes es.& (loc(e) = source(l)  Id (& (realizes es.& ( (& (realizes es.& (kind(e) = k  Knd (& (realizes es.& ( (& (realizes es.& ((e':E.  (& (realizes es.& ((kind(e') = rcv(l; tg)  Knd (& (realizes es.& ((& sender(e') = e  E (& (realizes es.& ((& & (e'':E.  (& (realizes es.& ((& & (kind(e'') = rcv(l; tg)  Knd (& (realizes es.& ((& & ( (& (realizes es.& ((& & (sender(e'') = e  E  e'' = e'  E) (& (realizes es.& ((& & val(e') = f((x when e),val(e))  T))))
THM	conditional-send1-rule	x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. (rcv(l; tg) = k  T = B) (f:(ABT), c:(AB). (@source(l): ma-single-sends1(A; (@source(l): ma-single-sends1(B; (@source(l): ma-single-sends1(T; (@source(l): ma-single-sends1(x; (@source(l): ma-single-sends1(k; (@source(l): ma-single-sends1(l; (@source(l): ma-single-sends1(tg; (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)) ( Dsys (& (D:Dsys.  (& (@source(l): ma-single-sends1(A; (& (@source(l): ma-single-sends1(B; (& (@source(l): ma-single-sends1(T; (& (@source(l): ma-single-sends1(x; (& (@source(l): ma-single-sends1(k; (& (@source(l): ma-single-sends1(l; (& (@source(l): ma-single-sends1(tg; (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi))  D (& ( (& (D  (& (realizes es.(vartype(source(l);x) r A) (& (realizes es.& (e:E.  (& (realizes es.& (loc(e) = source(l)  Id (& (realizes es.& ( (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) (& (realizes es.& (e:E.  (& (realizes es.& (loc(e) = source(l)  Id (& (realizes es.& ( (& (realizes es.& (kind(e) = k  Knd (& (realizes es.& ( (& (realizes es.& ((c((x when e),val(e)) (& (realizes es.& (( (& (realizes es.& (((e':E.  (& (realizes es.& (((kind(e') = rcv(l; tg)  Knd (& (realizes es.& (((& sender(e') = e  E (& (realizes es.& (((& & (e'':E.  (& (realizes es.& (((& & (kind(e'') = rcv(l; tg)  Knd (& (realizes es.& (((& & ( (& (realizes es.& (((& & (sender(e'') = e  E  e'' = e'  E) (& (realizes es.& (((& & val(e') = f((x when e),val(e))  T)) (& (realizes es.& (& (c((x when e),val(e)) (& (realizes es.& (& ( (& (realizes es.& (& ((e':E.  (& (realizes es.& (& ((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E)))))
THM	s-init-rule	i:Id, T:Type, v:T, x:Id. @i: x : T initially x = v  Dsys & (D:Dsys.  & (@i: x : T initially x = v  D & ( & (D  & (realizes es.(vartype(i;x) r T) & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T))
THM	s-frame-rule	i:Id, L:Knd List, x:Id, T:Type. @i: only members of L affect x :T  Dsys & (D:Dsys.  & (@i: only members of L affect x :T  D & ( & (D  & (realizes es.(vartype(i;x) r T) & (realizes es.& (e:E.  & (realizes es.& (loc(e) = i  Id & (realizes es.& ( & (realizes es.& (((x after e) = (x when e)  T  (kind(e)  L)) & (realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T)))
THM	s-pre-init-rule1	i,a,x:Id, A,T:Type, c:A, P:(ATProp). @i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  Dsys & (D:Dsys.  & (@i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  D & ( & (D  & (realizes es.(vartype(i;x) r A) & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A) & (realizes es.& (e:E.  & (realizes es.& (loc(e) = i  Id & (realizes es.& ( & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) & (realizes es.& (e:E.  & (realizes es.& (loc(e) = i  Id & (realizes es.& ( & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e))) & (realizes es.& & ((v:T. P(c,v)) & (realizes es.& & ( & (realizes es.& & ((e:E.  & (realizes es.& & ((loc(e) = i  Id & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))
THM	frame-rule0	i,x:Id, T:Type. @i: only members of nil affect x :T  Dsys & (D:Dsys.  & (@i: only members of nil affect x :T  D & ( & (D  & (realizes es.(vartype(i;x) r T) & e@i.(x after e) = (x when e)  T)
THM	frame-rule1	i,x:Id, k:Knd, T:Type. @i: only members of [k] affect x :T  Dsys & (D:Dsys.  & (@i: only members of [k] affect x :T  D & ( & (D  & (realizes es.(vartype(i;x) r T) & (realizes es.& e@i.((x after e) = (x when e)  T  kind(e) = k  Knd) & (realizes es.& & (kind(e) = k  Knd  (x after e) = (x when e)  T))
THM	s-sframe-rule	i:Id, L:Knd List, l:IdLnk, tg:Id. @i: only L sends on (l with tg)  Dsys & (D:Dsys.  & (@i: only L sends on (l with tg)  D & ( & (D  & (realizes es.e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L))
THM	better-sframe-rule	L:Knd List, l:IdLnk, tg:Id. @source(l): only L sends on (l with tg)  Dsys & (D:Dsys.  & (@source(l): only L sends on (l with tg)  D & ( & (D  & (realizes es.e:E.  & (realizes es.loc(e) = destination(l)  Id & (realizes es. & (realizes es.kind(e) = rcv(l; tg)  Knd  (kind(sender(e))  L))
THM	ma-single-pre-init-ma-single-pre-compatible	a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top, d1:x:Id fp-> Type, P1:Top. ds || d1 a = a1 (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ (with ds: d1 aaction a1:T1 aprecondition a1(v) is aP1 s v)
THM	ma-single-pre-init-ma-single-sends-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List. ds || d1 locl(a) : T || da (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ ma-single-sends(d1; da; k; l; f)
THM	ma-single-pre-init-ma-single-effect-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top. ds || d1 locl(a) : T || da (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ ma-single-effect(d1; da; k; x; f)
THM	ma-single-pre-init-ma-single-sframe-compatible	a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id, L:Knd List. (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ only L sends on (l with tg)
THM	ma-single-pre-init-ma-single-frame-compatible	a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, L:Knd List, t:Type. ds || x : t (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ only members of L affect x :t
THM	ma-single-pre-init-ma-single-init-compatible	a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id, t:Type, v:t. ds || x : t (x  dom(init)  init(x) = v  t) (with ds: ds (init: init action a:T aprecondition a(v) is aP) ||+ x : t initially x = v
THM	ma-single-pre-ma-single-sends-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List. ds || d1 locl(a) : T || da (with ds: ds (action a:T (precondition a(v) is (P s v) ||+ ma-single-sends(d1; da; k; l; f)
THM	ma-single-sends-ma-single-pre-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List. ds || d1 locl(a) : T || da ma-single-sends(d1; da; k; l; f) ||+ (with ds: ds maction a:T mprecondition a(v) is mP s v)
THM	ma-single-effect-ma-single-pre-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top. ds || d1 locl(a) : T || da ma-single-effect(d1; da; k; x; f) ||+ (with ds: ds maction a:T mprecondition a(v) is mP s v)
THM	ma-single-pre-ma-single-sframe-compatible	a:Id, T:Type, ds:x:Id fp-> Top, P:Top, l:IdLnk, tg:Id, L:Top. (with ds: ds (action a:T (precondition a(v) is (P s v) ||+ only L sends on (l with tg)
THM	ma-single-pre-ma-single-frame-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. ds || x : t (with ds: ds (action a:T (precondition a(v) is (P s v) ||+ only members of L affect x :t
THM	ma-single-frame-ma-single-pre-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. ds || x : t only members of L affect x :t ||+ (with ds: ds oaction a:T oprecondition a(v) is oP s v)
THM	ma-single-pre-ma-single-init-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. ds || x : t (with ds: ds (action a:T (precondition a(v) is (P s v) ||+ x : t initially x = v
THM	ma-single-init-ma-single-pre-compatible	a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. ds || x : t x : t initially x = v ||+ (with ds: ds xaction a:T xprecondition a(v) is xP s v)
THM	ma-single-sends-ma-single-effect-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. ds || d1 da || d2 ma-single-sends(ds; da; k; l; f) ||+ ma-single-effect(d1; d2; k1; x; f1)
THM	ma-single-effect-ma-single-sends-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. ds || d1 da || d2 ma-single-effect(d1; d2; k1; x; f1) ||+ ma-single-sends(ds; da; k; l; f)
THM	ma-single-sends-ma-single-sframe-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, l1:IdLnk, tg:Id, L:Knd List. (l = l1  (tg  map(p.1of(p);f))  (k  L)) ma-single-sends(ds; da; k; l; f) ||+ only L sends on (l1 with tg)
THM	ma-single-sends-ma-single-frame-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, x:Id, L:Top, t:Type. ds || x : t ma-single-sends(ds; da; k; l; f) ||+ only members of L affect x :t
THM	ma-single-frame-ma-single-sends-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, x:Id, L:Top, t:Type. ds || x : t only members of L affect x :t ||+ ma-single-sends(ds; da; k; l; f)
THM	ma-single-sends-ma-single-init-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, x:Id, t:Type, v:t. ds || x : t  ma-single-sends(ds; da; k; l; f) ||+ x : t initially x = v
THM	ma-single-init-ma-single-sends-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, x:Id, t:Type, v:t. ds || x : t  x : t initially x = v ||+ ma-single-sends(ds; da; k; l; f)
THM	ma-single-effect-ma-single-sframe-compatible	x:Id, k:Knd, ds:x:Id fp-> Top, da:a:Knd fp-> Top, f:Top, l:IdLnk, tg:Id, L:Top. ma-single-effect(ds; da; k; x; f) ||+ only L sends on (l with tg)
THM	ma-single-effect-ma-single-frame-compatible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, L:Knd List, t:Type. ds || x1 : t (x = x1  (k  L)) ma-single-effect(ds; da; k; x; f) ||+ only members of L affect x1 :t
THM	ma-single-frame-ma-single-effect-compatible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, L:Knd List, t:Type. ds || x1 : t (x = x1  (k  L)) only members of L affect x1 :t ||+ ma-single-effect(ds; da; k; x; f)
THM	ma-single-effect-ma-single-init-compatible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, v:t. ds || x1 : t  ma-single-effect(ds; da; k; x; f) ||+ x1 : t initially x1 = v
THM	ma-single-init-ma-single-effect-compatible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, v:t. ds || x1 : t  x1 : t initially x1 = v ||+ ma-single-effect(ds; da; k; x; f)
THM	ma-single-frame-ma-single-sframe-compatible	l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top. only members of L1 affect x :t ||+ only L sends on (l with tg)
THM	ma-single-init-ma-single-sframe-compatible	l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top. x : t initially x = v ||+ only L sends on (l with tg)
THM	ma-single-frame-ma-single-init-compatible	x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. x : t || x1 : t1  only members of L affect x :t ||+ x1 : t1 initially x1 = v
THM	ma-single-init-ma-single-frame-compatible	x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. x : t || x1 : t1  x1 : t1 initially x1 = v ||+ only members of L affect x :t
THM	ma-single-sends-ma-single-sends-compatible	k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List. ds || d1 da || d2 <k,l> = <k1,l1> ma-single-sends(ds; da; k; l; f) ||+ ma-single-sends(d1; d2; k1; l1; f1)
THM	ma-single-effect-ma-single-effect-compatible	x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. ds || d1 da || d2 <k,x> = <k1,x1> ma-single-effect(ds; da; k; x; f) ||+ ma-single-effect(d1; d2; k1; x1; f1)
THM	ma-single-frame-ma-single-frame-compatible	x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type. x = x1  only members of L affect x :t ||+ only members of L1 affect x1 :t1
THM	ma-single-init-ma-single-init-compatible	x:Id, t,v:Top, x1:Id, t1,v1:Top. x = x1  x : t initially x = v ||+ x1 : t1 initially x1 = v1
THM	decidable__equal_nat	x,y:. Dec(x = y)
def	Dconstant	Dconstant(loc;T;c;x;i) == if loc = i [x : T initially x = c; only members of nil affect x :T] == else nil fi
THM	Dconstant__compatible	loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A ||+ B)
THM	Dconstant__feasible	c:T, x,i:Id. d-feasible(loc.(Dconstant(loc;T;c;x;i)))
THM	Dconstant__realizes	c:T, x,i:Id. loc.(Dconstant(loc;T;c;x;i)) realizes es.e@i.(x when e) = c  T
def	once	once(loc;a;i) == if loc = i == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);  == if [only members of [locl(a)] affect "done" :;  == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] == else nil fi
THM	once__compatible	loc,a,i:Id. (A,Bonce(loc;a;i).A ||+ B)
THM	once__feasible	a,i:Id. d-feasible(loc.(once(loc;a;i)))
THM	once__realizes	a,i:Id. loc.(once(loc;a;i))  realizes es.e@i.kind(e) = locl(a) realizes es.& e@i.e'@i.kind(e) = locl(a) realizes es.& e@i.e'@i. realizes es.& kind(e') = locl(a)  Knd  e = e'  E
def	send-once	send-once(loc;T;A;a;f;tg;l;x) == [(once(loc;a;source(l)));  == [if loc = source(l) == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))])) == [else  fi]
THM	send-once__compatible	loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. "done" = x  A  T  (A,Bsend-once(loc;T;A;a;f;tg;l;x).A ||+ B)
THM	send-once__feasible	a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. "done" = x  A  T  d-feasible(loc.(send-once(loc;T;A;a;f;tg;l;x)))
THM	send-once__realizes	a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. "done" = x A T loc.(send-once(loc;T;A;a;f;tg;l;x))  realizes es.(vartype(source(l);x) r A) realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) realizes es.& (e:E.  realizes es.& (kind(e) = rcv(l; tg)  Knd realizes es.& (& val(e) = f((x when sender(e)))  T realizes es.& (& & kind(sender(e)) = locl(a)  Knd realizes es.& (& & (e':E.  realizes es.& (& & (kind(e') = rcv(l; tg)  Knd realizes es.& (& & ( realizes es.& (& & (kind(sender(e')) = locl(a)  Knd  e' = e  E))
def	recognizer1	recognizer1(loc;T;A;P;k;i;r;x) == if loc = i == if [r :  initially r = false;  == if [only members of [k] affect r :;  == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)] == else nil fi
THM	recognizer1__compatible	loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. A  T  x = r  (A,Brecognizer1(loc;T;A;P;k;i;r;x).A ||+ B)
THM	recognizer1__feasible	P:(AT), k:Knd, i,r,x:Id. A  T  x = r  d-feasible(loc.(recognizer1(loc;T;A;P;k;i;r;x)))
THM	recognizer1__realizes	P:(AT), k:Knd, i,r,x:Id. A T x = r loc.(recognizer1(loc;T;A;P;k;i;r;x))  realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T) & (vartype(i;x) r A) realizes es.& e@i.first(e)  (r when e) = false   realizes es.& e'@i.(r after e') realizes es.& e'@i. realizes es.& e'@i.(e:E.  realizes es.& e'@i.((e <loc e')  e = e'  E realizes es.& e'@i.(& kind(e) = k  Knd realizes es.& e'@i.(& P((x when e),val(e)))
def	trigger1	trigger1(loc;T;A;P;i;k;a;x) == [(recognizer1(loc;T;A;P;k;i;"trigger";x));  == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else  fi]
THM	trigger1__compatible	loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. A T x = "trigger"  locl(a) = k  (A,Btrigger1(loc;T;A;P;i;k;a;x).A ||+ B)
THM	trigger1__feasible	P:(AT), i:Id, k:Knd, a,x:Id. A T x = "trigger" locl(a) = k  d-feasible(loc.(trigger1(loc;T;A;P;i;k;a;x)))
THM	trigger1__realizes	P:(AT), i:Id, k:Knd, a,x:Id. A T x = "trigger" locl(a) = k loc.(trigger1(loc;T;A;P;i;k;a;x))  realizes es.(vartype(i;x) r A) & e@i.kind(e) = k  Knd  (valtype(e) r T) realizes es.& e'@i.kind(e') = locl(a) realizes es.& e'@i. realizes es.& (e:E. (e <loc e') & kind(e) = k  Knd & P((x when e),val(e))) realizes es.& e@i.kind(e) = k  Knd realizes es.& e@i. realizes es.& P((x when e),val(e))  e'@i.kind(e') = locl(a)  Knd
def	rset	|R| == {i:Id| (R(i)) }
def	ring	ring(R;in;out) == (i:|R|.  == ((R(source(in(i)))) & (R(destination(out(i)))) == (& source(out(i)) = i == (& & destination(in(i)) = i == (& & in(destination(out(i))) = out(i)  IdLnk == (& & out(source(in(i))) = in(i)  IdLnk) == & (i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id) == & |R|
def	rnext	n(i) == destination(out(i))
def	rprev	p(i) == source(in(i))
def	rdist	d(i;j) == mu(k.x.n(x)^k+1(i) = j)+1
THM	rdist-property	R:(Id), in,out:(|R|IdLnk), i,j:|R|. ring(R;in;out)  x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)
THM	rnext-rprev	R:(Id), in,out:(|R|IdLnk), j:|R|. ring(R;in;out)  n(p(j)) = j
THM	rnext-one-one	R:(Id), in,out:(|R|IdLnk). ring(R;in;out)  (i,j:|R|. n(i) = n(j)  i = j)
THM	rdist-rprev	R:(Id), in,out:(|R|IdLnk), i,j:|R|. ring(R;in;out)  i = p(j)  d(i;p(j)) = d(i;j)-1
THM	ring-list	R:(Id), in,out:(|R|IdLnk). ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L)))
THM	rset_sq	R:(Id). SQType(|R|)
THM	decidable__rset_equal	R:(Id), x,y:|R|. Dec(x = y)
def	ring-leader1	ring-leader1(loc;R;uid;out;in) == if R(loc) == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me"));  == if [(trigger1(loc;;;x,y. x=y;loc;rcv == if [((in(loc)); "vote");"leader";"me"));  == if [(Dconstant(loc;;uid(loc);"me";loc));  == if [ma-single-sends1(; == if [ma-single-sends1(; == if [ma-single-sends1(; == if [ma-single-sends1("me"; == if [ma-single-sends1(rcv((in(loc)); "vote"); == if [ma-single-sends1((out(loc)); == if [ma-single-sends1("vote"; == if [ma-single-sends1((a,b. if a<b [b] else nil fi));  == if [only [rcv((in(loc)); "vote");  == if [only [locl("send-me")] sends on (out(loc) with "vote")] == else nil fi
THM	ring-leader1__compatible	loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk). ring(R;in;out) Inj(|R|; ; uid)  (A,Bring-leader1(loc;R;uid;out;in).A ||+ B)
THM	ring-leader1__feasible	R:(Id), uid:(|R|), out,in:(|R|IdLnk). ring(R;in;out) Inj(|R|; ; uid)  d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))
THM	ring-leader1__realizes	R:(Id), uid:(|R|), out,in:(|R|IdLnk). ring(R;in;out) Inj(|R|; ; uid) loc.(ring-leader1(loc;R;uid;out;in))  realizes es.ldr:|R|.  realizes es.e@ldr.kind(e) = locl("leader") realizes es.& (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)
def	bi-graph	bi-graph(G;to;from) == i:|G|.  == (lto(i).destination(l) = i == & (G(source(l))) == & (l  from(source(l))) == & (lnk-inv(l)  from(i))) == & (lfrom(i).source(l) = i == & & (G(destination(l))) == & & (l  to(destination(l))) == & & (lnk-inv(l)  to(i)))
def	bi-graph-edge	Edge(G) == {l:IdLnk| i:|G|. (l  from(i)) }
THM	inv-is-edge	G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G). bi-graph(G;to;from)  lnk-inv(l)  Edge(G)
THM	src-edge	T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T). bi-graph(T;to;from)  source(u)  |T|
THM	dst-edge	T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T). bi-graph(T;to;from)  destination(u)  |T|
def	bi-graph-to	to(i) == to(i)
def	bi-graph-from	from(i) == from(i)
def	bi-graph-inv	inverse(l) == lnk-inv(l)
THM	edge-to	G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. bi-graph(G;to;from)  ((e  to(i))  destination(e) = i)
THM	edge-from	G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. bi-graph(G;to;from)  ((e  from(i))  source(e) = i)
THM	edge-inv-to	G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. bi-graph(G;to;from)  ((inverse(e)  to(i))  source(e) = i)
THM	edge-inv-from	G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. bi-graph(G;to;from)  ((inverse(e)  from(i))  destination(e) = i)
def	bi-tree	bi-tree(T;to;from) == bi-graph(T;to;from) == & (i,j:|T|. == & (p:Edge(T) List.  == & (lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)) == & (L:|T| List. i:|T|. (i  L)) == & |T|
THM	bi-tree-diameter	T:(Id), to,from:(|T|(IdLnk List)). bi-tree(T;to;from)  (n:. p:Edge(T) List. lpath(p)  ||p||n)
def	spanner	spanner(f;T;to;from) == (l:Edge(T). f(l) = f(inverse(l))) == & (i:|T|, l1,l2:Edge(T). == & ((l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  (f(l1))  (f(l2)))
def	spanner-root	spanner-root(f;T;to;from;i) == l:Edge(T). (l  to(i))  (f(l))
THM	spanner-root-exists	T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)). bi-tree(T;to;from) spanner(f;T;to;from)  (i:|T|. spanner-root(f;T;to;from;i))
THM	spanner-root-unique	T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)). bi-tree(T;to;from) spanner(f;T;to;from) (i,j:|T|. spanner-root(f;T;to;from;i)  spanner-root(f;T;to;from;j)  i = j)
def	update	f[x:=v](y) == if eq(y,x) v else f(y) fi

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