Nuprl Definition : pv11_p1_eq_bnums
pv11_p1_eq_bnums() ==  λbn1,bn2. (union-deq(ℤ × Id;Unit;product-deq(ℤ;Id;IntDeq;IdDeq);UnitDeq) bn1 bn2)
Definitions occuring in Statement : 
id-deq: IdDeq
, 
Id: Id
, 
union-deq: union-deq(A;B;a;b)
, 
product-deq: product-deq(A;B;a;b)
, 
unit-deq: UnitDeq
, 
int-deq: IntDeq
, 
unit: Unit
, 
apply: f a
, 
lambda: λx.A[x]
, 
product: x:A × B[x]
, 
int: ℤ
FDL editor aliases : 
pv11_p1_eq_bnums
Latex:
pv11\_p1\_eq\_bnums()  ==
    \mlambda{}bn1,bn2.  (union-deq(\mBbbZ{}  \mtimes{}  Id;Unit;product-deq(\mBbbZ{};Id;IntDeq;IdDeq);UnitDeq)  bn1  bn2)
Date html generated:
2016_05_17-PM-02_47_27
Last ObjectModification:
2014_11_26-AM-11_22_13
Theory : paxos!synod
Home
Index