Selected Objects

def	fpf-compatible	f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)
def	fpf-join	f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>
THM	fpf-join-dom	B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. x  dom(f  g)  x  dom(f)  x  dom(g)
THM	fpf-join-dom2	eq:EqDecider(A), f,g:a:A fp-> Top, x:A. x  dom(f  g)  x  dom(f)  x  dom(g)
THM	fpf-join-is-empty	eq:EqDecider(A), f,g:x:A fp-> Top. fpf-is-empty(f  g) ~ (fpf-is-empty(f)fpf-is-empty(g))
THM	fpf-join-ap-sq	eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. f  g(x) ~ if x  dom(f) f(x) else g(x) fi
def	fpf-single	x : v == <[x],x.v>
THM	fpf-cap-single1	eq:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v
THM	fpf-ap-single	eq,x,v:Top. x : v(x) ~ v
THM	fpf-cap-single	eq:EqDecider(A), x,y:A, v,z:Top. x : v(y)?z ~ if eqof(eq)(x,y) v else z fi
THM	fpf-val-single1	eq:EqDecider(A), x:A, v,P:Top. z != x : v(x) ==> P(a,z) ~ (True  P(x,v))
def	fpf-all	xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))
THM	fpf-single-dom	eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y
THM	fpf-single-dom-sq	eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v) ~ (eqof(eq)(y,x))
THM	fpf-all-single-decl	eq:EqDecider(A), P:(ATypeProp), x:A, v:Type. ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
THM	fpf-empty-compatible-right	eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||
THM	fpf-empty-compatible-left	eq:EqDecider(A), B:Top, f:a:A fp-> Top.  || f
def	fpf-dom-list	fpf-dom-list(f) == 1of(f)
def	ma-state	State(ds) == x:Idds(x)?Top
def	ma-valtype	ma-valtype(da; k) == da(k)?Top
def	msga	MsgA == ds:x:Id fp-> Type == da:a:Knd fp-> Type == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void == kl:KndIdLnk fp-> (tg:Id == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
def	ma-ds	M.ds(x) == 1of(M)(x)?Top
def	ma-da	M.da(a) == 1of(2of(M))(a)?Top
def	ma-decla	a declared in M == locl(a)  dom(1of(2of(M)))
def	da-outlink-f	da-outlink-f(da;k) == <lnk(k),tag(k),da(k)>
def	da-outlinks	da-outlinks(da;i) == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
THM	da-outlinks-empty	ltg:(IdLnkIdType), i:Id. (ltg  da-outlinks(;i))  False
def	ma-outlinks	ma-outlinks(M;i) == da-outlinks(1of(2of(M));i)
def	ma-din	M.din(l,tg) == 1of(2of(M))(rcv(l; tg))?Top
def	ma-dout	M.dout(l,tg) == 1of(2of(M))(rcv(l; tg))?Void
def	ma-init	M.init(x,v) == x0 != 1of(2of(2of(M)))(x) ==> v = x0  1of(M)(x)?Void
def	ma-st	M.state == State(1of(M))
def	ma-v	M.V(k) == ma-valtype(1of(2of(M)); k)
def	ma-npre	unsolvable M.pre(a,s) == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v)
def	ma-pre	M.pre(a,s,v) == P != 1of(2of(2of(2of(M))))(a) ==> P(s,v)
def	ma-ef	M.ef(k,x,s,v,w) == E != 1of(2of(2of(2of(2of(M)))))(<k,x>) ==> w = E(s,v)  M.ds(x)
def	tagged-list-messages	tagged-list-messages(s;v;L) == concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L))
def	tagged-messages	tagged-messages(l;s;v;L) == map(x.<l,x>;tagged-list-messages(s;v;L))
def	ma-send	M.send(k;l;s;v;ms;i) == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf.map(x. == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg)) == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List
def	ma-sends-on	M sends on link l == deq-member(IdLnkDeq;l;map(p.2of(p);1of(1of(2of(2of(2of(2of(2of(M)))))))))
def	ma-frame	M.frame(k affects x) == L != 1of(2of(2of(2of(2of(2of(2of(M)))))))(x) ==> deq-member(KindDeq;k;L)
def	ma-sframe	M.sframe(k sends <l,tg>) == L != 1of(2of(2of(2of(2of(2of(2of(2of( == L != 1of(M))))))))(<l,tg>) ==> deq-member(KindDeq;k;L)
def	ma-sub	M1  M2 == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) == & & 1of(2of(2of(2of(2of(2of(2of(2of( == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
def	mk-ma	mk-ma(ds; da; init; pre; ef; send; frame; sframe) == <ds,da,init,pre,ef,send,frame,sframe,>
def	ma-empty	== mk-ma(; ; ; ; ; ; ; )
def	ma-is-empty	ma-is-empty(M) == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M))) == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M))))) == fpf-is-empty(1of(2of(2of(2of(2of(M)))))) == fpf-is-empty(1of(2of(2of(2of(2of(2of(M))))))) == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M)))))))) == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M)))))))))
def	ma-compatible-decls	M1 ||decl M2 == 1of(M1) || 1of(M2) & 1of(2of(M1)) || 1of(2of(M2))
def	ma-join	M1  M2 == mk-ma(1of(M1)  1of(M2); == mk-ma(1of(2of(M1))  1of(2of(M2)); == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2))); == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))); == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))); == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))); == mk-ma(1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( == mk-ma(1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))); == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))
def	ma-compatible	M1 || M2 == M1 ||decl M2 == & 1of(2of(2of(M1))) || 1of(2of(2of(M2))) == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2)))) == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2))))) == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2)))))) == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of( == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2))))))) == & 1of(2of(2of(2of(2of(2of(2of(2of( == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
def	ma-single-init	x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; )
def	ma-single-frame	only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; )
def	ma-single-sframe	only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L)
def	ma-single-effect	ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; )
def	ma-single-effect0	ma-single-effect0(x;A;k;T;f) == ma-single-effect(x : A; k : T; k; x; (s,v. f(s(x),v)))
def	ma-single-effect1	ma-single-effect1(x;A;y;B;k;T;f) == ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
def	ma-single-sends	ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; )
def	ma-single-sends1	ma-single-sends1(A; B; T; x; a; l; tg; f) == ma-single-sends(x : A; a : B  rcv(l; tg) : T; a; l; [<tg,s,v. f(s(x),v)>])
def	ma-single-pre	(with ds: ds (action a:T (precondition a(v) is (P s v) == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )
def	ma-single-pre1	ma-single-pre1(x;A;a;T;y,v.P(y;v)) == (with ds: x : A == (action a:T == (precondition a(v) is == (s,v. P(s(x);v) s v)
def	ma-single-pre-init	(with ds: ds (init: init action a:T aprecondition a(v) is aP) == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )
def	ma-single-pre-init1	ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v)) == (with ds: x : T == (init: x : c == action a:T' == aprecondition a(v) is == as,v. P(s(x);v))
def	ma-feasible	Feasible(M) == xdom(1of(M)). T=1of(M)(x)   T == & kdom(1of(2of(M))). T=1of(2of(M))(k)   Dec(T) == & adom(1of(2of(2of(2of(M))))). p=1of(2of(2of(2of(M))))(a)   == &s:State(1of(M)). Dec(v:1of(2of(M))(locl(a))?Top. p(s,v)) == & kxdom(1of(2of(2of(2of(2of(M)))))). ef=1of(2of(2of(2of(2of(M)))))(kx)   == &M.frame(1of(kx) affects 2of(kx)) == & kldom(1of(2of(2of(2of(2of(2of(M))))))).  == & snd=1of(2of(2of(2of(2of(2of(M))))))(kl)   tg:Id.  == & (tg  map(p.1of(p);snd))  M.sframe(1of(kl) sends <2of(kl),tg>)
THM	ma-empty-feasible	Feasible()
def	ma-frame-compatible	ma-frame-compatible(A; B) == kx:(KndId).  == (kx  dom(1of(2of(2of(2of(2of(A)))))) == ( == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) == ( == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) == ( == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(B)))))))(2of(kx)))) == & (kx  dom(1of(2of(2of(2of(2of(B)))))) == & ( == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) == & ( == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) == & ( == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))
def	ma-sframe-compatible	ma-sframe-compatible(A; B) == kl:(KndIdLnk), tg:Id. == (kl  dom(1of(2of(2of(2of(2of(2of(A))))))) == ( == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl))) == ( == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) == ( == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) == ( == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>))) == & (kl  dom(1of(2of(2of(2of(2of(2of(B))))))) == & ( == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl))) == & ( == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) == & ( == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) == & ( == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))
def	ma-compat	A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B)
def	ma-join-list	(L) == reduce(A,B. A  B;;L)
def	msg-form	MsgAForm == x:Id fp-> Topx:Knd fp-> Typex:Id fp-> Topx:Id fp-> Topx:KndId fp-> Top == x:KndIdLnk fp-> Topx:Id fp-> Topx:IdLnkId fp-> TopTop
THM	ma-single-init-feasible	x:Id, t:Type, v:t. Feasible(x : t initially x = v)
THM	ma-single-frame-feasible	x:Id, L:Knd List, t:Type. t  Feasible(only members of L affect x :t)
THM	ma-single-sframe-feasible	l:IdLnk, tg:Id, L:Knd List. Feasible(only L sends on (l with tg))

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