Who Cites ma-send?
ma-send	Def M.send(k;l;s;v;ms;i) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List
eq_id	Def a = b == eqof(IdDeq)(a,b)
	Thm* a,b:Id. a = b
ma-da	Def M.da(a) == 1of(2of(M))(a)?Top
Kind-deq	Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
product-deq	Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
fpf-val	Def z != f(x) ==> P(a;z) == x  dom(f)  P(x;f(x))
fpf-cap	Def f(x)?z == if x  dom(f) f(x) else z fi
proddeq	Def proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). proddeq(a;b)  ABAB
fpf-ap	Def f(x) == 2of(f)(x)
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
lsrc	Def source(l) == 1of(l)
	Thm* l:IdLnk. source(l)  Id
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
deq-member	Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
union-deq	Def union-deq(A;B;a;b) == <sumdeq(a;b),sum-deq(A;B;a;b)>
sumdeq	Def sumdeq(a;b)(p,q) Def == InjCase(p; pa. InjCase(q; qa. 1of(a)(pa,qa); qb. false); pb. Def == InjCase(q; qa. false; qb. 1of(b)(pb,qb)))
	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). sumdeq(a;b)  (A+B)(A+B)
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
map	Def map(f;as) == Case of as; nil  nil ; a.as'  [(f(a)) / map(f;as')] Def (recursive)
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
concat	Def concat(ll) == reduce(l,l'. l @ l';nil;ll)
	Thm* T:Type, ll:(T List) List. concat(ll)  T List
top	Def Top == Void given Void
	Thm* Top  Type
rcv	Def rcv(l; tg) == inl(<l,tg>)
	Thm* l:IdLnk, tg:Id. rcv(l; tg)  Knd
Knd	Def Knd == (IdLnkId)+Id
	Thm* Knd  Type
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
Id	Def Id == Atom
	Thm* Id  Type
append	Def as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs)  T List
reduce	Def reduce(f;k;as) == Case of as; nil  k ; a.as'  f(a,reduce(f;k;as')) Def (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as)  B
nat	Def  == {i:| 0i }
	Thm*   Type
nat-deq	Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>
prod-deq	Def prod-deq(A;B;a;b) Def == (A,B,a,b,p,q. q/q1,q2. Def == (p/p1,p2. Def == (b/eq,b1. Def == (a/e1,a1. Def == ((%1.%1 Def == ((%1.(<%.<(%1.%1(p1,q1)/%4,%5. %4((%1.%1)((%1.*)(*))))(a1) Def == ((%1.(<%.,(%1.%1(p2,q2)/%4,%5. %4((%1.%1)((%1.*)(*))))(b1)> Def == ((%1.(,%.%/%1,%2. *>)) Def == (((%1.%1.2) Def == ((((%1.%1 Def == ((((%1.(<p1,p2> = <q1,q2>  AB Def == ((((%1.,<p1,p2> = <q1,q2>  AB Def == ((((%1.,((e1(p1,q1))(eq(p2,q2))) Def == ((((%1.,(e1(p1,q1)) & (eq(p2,q2)) Def == ((((%1.,(%1.%1)((%1.<%2.%2,%2.%2>)(*)) Def == ((((%1.,(%1.%1) Def == ((((%1.,((%1.%1(e1(p1,q1),eq(p2,q2))) Def == ((((%1.,((p,q. InjCase(q; x. InjCase(p Def == ((((%1.,((p,q. InjCase(q; x. InjCase; x. <%.<*,*>,%.*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. <%.<any(%),*> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. ,%.%/%1,%2. any(%1)>) Def == ((((%1.,((p,q. ; y. Def == ((((%1.,((p,q. InjCase(p Def == ((((%1.,((p,q. InjCase; x. <%.<*,any(%)>,%.%/%1,%2. any(%2)> Def == ((((%1.,((p,q. InjCase; y. <%.<any(%),any(%)> Def == ((((%1.,((p,q. InjCase; y. ,%.%/%1,%2. any(%2)>)))))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%)> Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%)>>)))) Def == (A Def == ,B Def == ,a Def == ,b)
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>
le	Def AB == B<A
	Thm* i,j:. (ij)  Prop
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
sum-deq	Def sum-deq(A;B;a;b) Def == (A,B,a,b,p,q. Def == (InjCase(q; x. InjCase(p Def == (InjCase(q; x. InjCase; x1. b/eq,b1. Def == (InjCase(q; x. InjCase; x1. a/e1,a1. Def == (InjCase(q; x. InjCase; x1. <%.(%1.%1(x1,x)/%4,%5. Def == (InjCase(q; x. InjCase; x1. <%.(%4 Def == (InjCase(q; x. InjCase; x1. <%.(((%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((%1.*) Def == (InjCase(q; x. InjCase; x1. <%.(((((%1.%1(x)) Def == (InjCase(q; x. InjCase; x1. <%.((((((%1.%1(x1)) Def == (InjCase(q; x. InjCase; x1. <%.(((((((%1.%1(B)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((%1.%1(A)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. (%1.%1) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%1.(%2.*)(*)) Def == (InjCase(q; x. InjCase; x1. <%.((((((((A,B,x1,x,%. ((%)))))))))) Def == (InjCase(q; x. InjCase; x1. <%.(a1) Def == (InjCase(q; x. InjCase; x1. ,%.*> Def == (InjCase(q; x. InjCase; y. b/eq,b1. Def == (InjCase(q; x. InjCase; y. a/e1,a1. Def == (InjCase(q; x. InjCase; y. <%.(%1.any((%1(*)))) Def == (InjCase(q; x. InjCase; y. <%.((%1.%1(x)) Def == (InjCase(q; x. InjCase; y. <%.(((%1.%1(y)) Def == (InjCase(q; x. InjCase; y. <%.((((%1.%1(B)) Def == (InjCase(q; x. InjCase; y. <%.(((((%1.%1(A)) Def == (InjCase(q; x. InjCase; y. <%.(((((A,B,y,x,%. Def == (InjCase(q; x. InjCase; y. <%.((((((%1. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase(%1 Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %2. any(%2) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. (%4.any(%4)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(%6. Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(%5.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%4.(*)) Def == (InjCase(q; x. InjCase; y. <%.((((((InjCase; %3. ((%)))) Def == (InjCase(q; x. InjCase; y. <%.(((((((%1.%1)(inr(%.*)))))))) Def == (InjCase(q; x. InjCase; y. ,%.*>) Def == (; y. Def == (InjCase(p Def == (InjCase; x. b/eq,b1. Def == (InjCase; x. a/e1,a1. Def == (InjCase; x. <%.(%1.any((%1(*)))) Def == (InjCase; x. <%.((%1.%1(y)) Def == (InjCase; x. <%.(((%1.%1(x)) Def == (InjCase; x. <%.((((%1.%1(B)) Def == (InjCase; x. <%.(((((%1.%1(A)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase(%1 Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %2. any(%2) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. (%4.any(%4)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(%6. Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(any(%6)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(%5.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%4.(*)) Def == (InjCase; x. <%.(((((A,B,x,y,%. (%1.InjCase; %3. ((%)))) Def == (InjCase; x. <%.(((((A,B,x,y,%. ((%1.%1)(inr(%.*)))))))) Def == (InjCase; x. ,%.*> Def == (InjCase; y1. b/eq,b1. Def == (InjCase; y1. a/e1,a1. Def == (InjCase; y1. <%.(%1.%1(y1,y)/%4,%5. Def == (InjCase; y1. <%.(%4 Def == (InjCase; y1. <%.(((%1.%1) Def == (InjCase; y1. <%.((((%1.*) Def == (InjCase; y1. <%.(((((%1.%1(y)) Def == (InjCase; y1. <%.((((((%1.%1(y1)) Def == (InjCase; y1. <%.(((((((%1.%1(B)) Def == (InjCase; y1. <%.((((((((%1.%1(A)) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. (%1.%1) Def == (InjCase; y1. <%.((((((((A,B,y1,y,%. ((%1.(%2.*)(*))(%)))))))))) Def == (InjCase; y1. <%.(b1) Def == (InjCase; y1. ,%.*>))) Def == (A Def == ,B Def == ,a Def == ,b)
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
eq_atom	Def x=yAtom == if x=yAtomtrue; false fi
	Thm* x,y:Atom. x=yAtom
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)

Syntax:

M.send(k;l;s;v;ms;i)

has structure:

ma-send(M; k; l; s; v; ms; i)

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