Def P & Q == PQ

is mentioned by

Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B)	[ma-compat]
Def ma-sframe-compatible(A; B) Def == kl:(KndIdLnk), tg:Id. Def == (kl  dom(1of(2of(2of(2of(2of(2of(A))))))) Def == ( Def == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == ( Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>))) Def == & (kl  dom(1of(2of(2of(2of(2of(2of(B))))))) Def == & ( Def == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))	[ma-sframe-compatible]
Def ma-frame-compatible(A; B) Def == kx:(KndId).  Def == (kx  dom(1of(2of(2of(2of(2of(A)))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == ( Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx)))) Def == & (kx  dom(1of(2of(2of(2of(2of(B)))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))	[ma-frame-compatible]
Def Feasible(M) Def == xdom(1of(M)). T=1of(M)(x)   T Def == & kdom(1of(2of(M))). T=1of(2of(M))(k)   Dec(T) Def == & adom(1of(2of(2of(2of(M))))). p=1of(2of(2of(2of(M))))(a)   Def == &s:State(1of(M)). Dec(v:1of(2of(M))(locl(a))?Top. p(s,v)) Def == & kxdom(1of(2of(2of(2of(2of(M)))))).  Def == ef=1of(2of(2of(2of(2of(M)))))(kx)   M.frame(1of(kx) affects 2of(kx)) Def == & kldom(1of(2of(2of(2of(2of(2of(M))))))).  Def == & snd=1of(2of(2of(2of(2of(2of(M))))))(kl)   tg:Id.  Def == & (tg  map(p.1of(p);snd))  M.sframe(1of(kl) sends <2of(kl),tg>)	[ma-feasible]
Def M1 || M2 Def == M1 ||decl M2 Def == & 1of(2of(2of(M1))) || 1of(2of(2of(M2))) Def == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2)))) Def == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2))))) Def == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2)))))) Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of( Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2))))))) Def == & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-compatible]
Def M1 ||decl M2 == 1of(M1) || 1of(M2) & 1of(2of(M1)) || 1of(2of(M2))	[ma-compatible-decls]
Def M1  M2 Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2)) Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-sub]
Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)	[fpf-compatible]

In prior sections: core int 1 bool 1 int 2 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 fun 1 rel 1

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html