Nuprl Definition : pv8_p1_same_proposal
pv8_p1_same_proposal(Cid;Op;eq_Cid) ==
zd.let slt1,cmd1 = zd
in z.let slt2,cmd2 = z
in (eqof(IntDeq) slt1 slt2) 
(pv8_p1_same_command(Cid;Op;eq_Cid) cmd1 cmd2)
Definitions occuring in Statement :
pv8_p1_same_command: pv8_p1_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_p1_same_proposal
pv8_p1_same_proposal
pv8\_p1\_same\_proposal(Cid;Op;eq$_{Cid}$) ==
\mlambda{}zd.let slt1,cmd1 = zd
in \mlambda{}z.let slt2,cmd2 = z
in (eqof(IntDeq) slt1 slt2) \mwedge{}\msubb{} (pv8\_p1\_same\_command(Cid;Op;eq$_{Cid}\mbackslash{}ff2\000C4) cmd1 cmd2)
Date html generated:
2012_02_20-PM-07_15_36
Last ObjectModification:
2012_02_06-PM-01_37_40
Home
Index