Selected Objects

def	dsys	Dsys == IdMsgA
def	d-m	M(i) == D(i)
def	d-sub	D1  D2 == i:Id. M(i)  M(i)
def	d-single-init	@i: x:T initially x = v(j) == if eqof(IdDeq)(j,i) x : T initially x = v else  fi
def	d-single-frame	@i: only L affects x : t(j) == if eqof(IdDeq)(j,i) only members of L affect x :t else  fi
def	d-single-sframe	@i: only L sends on (l with tg)(j) == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi
def	d-single-effect	d-single-effect(i; ds; da; k; x; f)(j) == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else  fi
def	d-single-sends	d-single-sends(i; ds; da; k; l; f)(j) == if eqof(IdDeq)(j,i) ma-single-sends(ds; da; k; l; f) else  fi
def	d-single-pre	@i (with ds: ds action a:T precondition a(v) is P s v)(j) == if eqof(IdDeq)(j,i) (with ds: ds action a:T precondition a(v) is P s v) == else  fi
def	d-single-pre-init	@i (with ds: ds init: init action a:T precondition a(v) is P s v)(j) == if eqof(IdDeq)(j,i) == if (with ds: ds == if (init: init == if action a:T == if aprecondition a(v) is == if aP) == else  fi
def	d-feasible	d-feasible(D) == (i:Id. Feasible(M(i))) == & (l:IdLnk, tg:Id. M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)) == & (i:Id.  == & (finite-type({l:IdLnk == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))
def	interface-check	interface-check(D;l;tg;T) == T r M(destination(l)).din(l,tg)
THM	fpf-compatible-singles	eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y). (x = y  v = u  B(x))  x : v || y : u
THM	fpf-trivial-subtype-top	B:(AType), f:a:A fp-> B(a). f  a:A fp-> Top
THM	fpf-sub-functionality	strong-subtype(A;A') (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)
THM	fpf-sub_functionality	strong-subtype(A;A') (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)
THM	fpf-sub_transitivity	B:(AType), eq:EqDecider(A), f,g,h:a:A fp-> B(a). f  g  g  h  f  h
THM	fpf-sub_weakening	B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g  f  g
THM	subtype-fpf-cap	eq:EqDecider(X), f,g:x:X fp-> Type. g  f  (x:X. f(x)?Top r g(x)?Top)
THM	subtype-fpf-cap-top	eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)
THM	fpf-cap-void-subtype	eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top
THM	subtype-fpf-cap-void	eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f  g  (f(x)?Void r g(x)?T)
THM	fpf-join-ap	B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x)
THM	fpf-join-ap-left	B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. x  dom(f)  f  g(x) = f(x)  B(x)
THM	fpf-join-cap-sq	eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi
THM	fpf-sub-join-left	B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). f  f  g
THM	fpf-sub-join-right	B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g
THM	fpf-single-sub-reflexive	B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v  x : v
THM	fpf-compatible-join	eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). h || f  h || g  h || f  g
THM	fpf-compatible-symmetry	eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f
THM	fpf-compatible-join2	eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). f || h  g || h  f  g || h
THM	fpf-all-join-decl	eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. ydom(f). w=f(y)   P(y,w) ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)
THM	fpf-compatible-triple	eq:EqDecider(T), f,g,h:x:T fp-> Type. f || g h || f h || g  g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g
THM	da-outlinks-single	ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. (ltg  da-outlinks(k : T;i)) isrcv(k) & source(lnk(k)) = i & (1of(ltg) ~ lnk(k)) & (1of(2of(ltg)) ~ tag(k)) & 2of(2of(ltg)) = T
THM	da-outlinks-join	ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. (ltg  da-outlinks(da1  da2;i)) (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))
THM	ma-sub_transitivity	M1,M2,M3:MsgA. M1  M2  M2  M3  M1  M3
THM	ma-sub_weakening	M1,M2:MsgA. M1 = M2  M1  M2
THM	assert-ma-is-empty	M:MsgA. ma-is-empty(M)  M =   MsgA
THM	ma-empty-is-empty	ma-is-empty()
THM	ma-empty-sub	M:MsgA.   M
THM	ma-is-empty-sub	A,B:MsgA. ma-is-empty(A)  A  B
THM	ma-sub-join-left	M1,M2:MsgA. M1  M1  M2
THM	ma-state-subtype	ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds))
THM	ma-state-subtype2	ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)
THM	ma-compatible-symmetry	M1,M2:MsgA. M1 || M2  M2 || M1
THM	ma-sub-join-right	M1,M2:MsgA. M1 || M2  M2  M1  M2
THM	ma-empty-compatible-left	A:MsgA.  || A
THM	ma-empty-compatible-right	A:MsgA. A ||
def	possible-world	PossibleWorld(D;w) == FairFifo == & (i,x:Id. vartype(i;x) r M(i).ds(x)) == & & (i:Id, a:Action(i). isnull(a)  (valtype(i;a) r M(i).da(kind(a)))) == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))) == & & (i,x:Id. M(i).init(x,s(i;0).x)) == & & (i:Id, t:. == & & (isnull(a(i;t)) == & & ( == & & ((islocal(kind(a(i;t))) == & & (( == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) == & & (& (x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)) == & & (& (l:IdLnk.  == & & (& (M(i).send(kind(a(i;t));l;x. == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)) == & & (& (x:Id.  == & & (& (M(i).frame(kind(a(i;t)) affects x) == & & (& ( == & & (& (s(i;t).x = s(i;t+1).x  M(i).ds(x)) == & & (& (l:IdLnk, tg:Id. == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>) == & & (& ( == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)) == & & (i,a:Id, t:. == & & (t':.  == & & (tt' == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a) == & & (&  a declared in M(i) == & & (&  unsolvable M(i).pre(a,x.s(i;t').x))
THM	ma-ds-sub	M1,M2:MsgA, x:Id. M1  M2  (M2.ds(x) r M1.ds(x))
THM	ma-da-sub	M1,M2:MsgA, k:Knd. M1  M2  (M2.da(k) r M1.da(k))
THM	ma-init-sub	V:(IdType), M1,M2:MsgA. (x:Id. V(x) r M2.ds(x)) M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v))
THM	ma-pre-sub	M1,M2:MsgA. M1  M2  (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v))
THM	ma-decla-sub	M1,M2:MsgA. M1  M2  (a:Id. a declared in M1  a declared in M2)
THM	ma-npre-sub	M1,M2:MsgA. M1  M2 (a:Id, s:M2.state. (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s))
THM	ma-ef-sub	M1,M2:MsgA. M1  M2 (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x). (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w))
THM	ma-send-sub	M1,M2:MsgA. M1  M2 (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg)) (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List. (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))
THM	ma-frame-sub	M1,M2:MsgA. M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x))
THM	ma-sframe-sub	M1,M2:MsgA. M1  M2 (k:Knd, l:IdLnk, tg:Id. M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>))

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