Nuprl Definition : pv8_p2_same_proposal
pv8_p2_same_proposal(Cid;Op;eq_Cid) ==
zb.let slt1,cmd1 = zb
in z.let slt2,cmd2 = z
in (eqof(IntDeq) slt1 slt2) 
(pv8_p2_same_command(Cid;Op;eq_Cid) cmd1 cmd2)
Definitions occuring in Statement :
pv8_p2_same_command: pv8_p2_same_command(Cid;Op;eq_Cid),
band: p q,
apply: f a,
lambda: x.A[x],
spread: spread def,
int-deq: IntDeq,
eqof: eqof(d)
FDL editor aliases :
pv8_p2_same_proposal
pv8_p2_same_proposal
pv8\_p2\_same\_proposal(Cid;Op;eq$_{Cid}$) ==
\mlambda{}zb.let slt1,cmd1 = zb
in \mlambda{}z.let slt2,cmd2 = z
in (eqof(IntDeq) slt1 slt2) \mwedge{}\msubb{} (pv8\_p2\_same\_command(Cid;Op;eq$_{Cid}\mbackslash{}ff2\000C4) cmd1 cmd2)
Date html generated:
2012_02_20-PM-07_35_15
Last ObjectModification:
2012_02_06-PM-03_03_42
Home
Index