Nuprl Definition : pv8_p1_same_pvalue
pv8_p1_same_pvalue(Cid;Op;eq_Cid) ==
ze.let bnum1,prp1 = ze
in z.let bnum2,prp2 = z
in (eqof(union-deq(
Id;Unit;product-deq(;Id;IntDeq;IdDeq);unit-deq())) bnum1 bnum2)
(pv8_p1_same_proposal(Cid;Op;eq_Cid) prp1 prp2)
Definitions occuring in Statement :
pv8_p1_same_proposal: pv8_p1_same_proposal(Cid;Op;eq_Cid),
id-deq: IdDeq,
Id: Id,
band: p q,
unit: Unit,
apply: f a,
lambda: x.A[x],
spread: spread def,
product: x:A B[x],
int: ,
union-deq: union-deq(A;B;a;b),
product-deq: product-deq(A;B;a;b),
unit-deq: unit-deq(),
int-deq: IntDeq,
eqof: eqof(d)
FDL editor aliases :
pv8_p1_same_pvalue
pv8_p1_same_pvalue
pv8\_p1\_same\_pvalue(Cid;Op;eq$_{Cid}$) ==
\mlambda{}ze.let bnum1,prp1 = ze
in \mlambda{}z.let bnum2,prp2 = z
in (eqof(union-deq(\mBbbZ{} \mtimes{} Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);unit-deq())) bnum1 bnum2)
\mwedge{}\msubb{} (pv8\_p1\_same\_proposal(Cid;Op;eq$_{Cid}$) prp1 prp2)
Date html generated:
2012_02_20-PM-07_15_50
Last ObjectModification:
2012_02_06-PM-01_37_49
Home
Index