Nuprl Definition : eq-sm-command
eq-sm-command(eq) ==
c1,c2.let clnt1,cid1,op1 = c1 in let clnt2,cid2,op2 = c2 in clnt1 = clnt2 
(cid1 =
cid2) (eq op1 op2)
Proof not projected
Definitions occuring in Statement :
eq_id: a = b,
eq_int: (i = j),
band: p q,
spreadn: spread3,
apply: f a,
lambda: x.A[x]
Definitions :
lambda: x.A[x],
spreadn: spread3,
eq_id: a = b,
band: p q,
eq_int: (i = j),
apply: f a
FDL editor aliases :
eq-sm-command
eq-sm-command(eq) ==
\mlambda{}c1,c2.
let clnt1,cid1,op1 = c1 in
let clnt2,cid2,op2 = c2 in
clnt1 = clnt2 \mwedge{}\msubb{} (cid1 =\msubz{} cid2) \mwedge{}\msubb{} (eq op1 op2)
Date html generated:
2011_10_20-PM-04_06_53
Last ObjectModification:
2011_01_25-PM-01_06_25
Home
Index