Nuprl Definition : pv11_p1_same_pvalue

pv11_p1_same_pvalue(Cmd) ==
  λzd,z. let bnum1,prp1 = zd 
         in let bnum2,prp2 = z 
            in (pv11_p1_eq_bnums() bnum1 bnum2) ∧b (pv11_p1_same_proposal(Cmd) prp1 prp2)


Definitions occuring in Statement :  pv11_p1_same_proposal: pv11_p1_same_proposal(Cmd),  pv11_p1_eq_bnums: pv11_p1_eq_bnums(),  band: p ∧b q,  apply: f a,  lambda: λx.A[x],  spread: spread def
FDL editor aliases :  pv11_p1_same_pvalue
Latex:
pv11\_p1\_same\_pvalue(Cmd)  ==
    \mlambda{}zd,z.  let  bnum1,prp1  =  zd 
                  in  let  bnum2,prp2  =  z 
                        in  (pv11\_p1\_eq\_bnums()  bnum1  bnum2)  \mwedge{}\msubb{}  (pv11\_p1\_same\_proposal(Cmd)  prp1  prp2)


Date html generated: 2015_07_23-PM-04_11_24
Last ObjectModification: 2014_11_26-AM-11_22_57

Home Index