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:
2015_07_23-PM-04_11_02
Last ObjectModification:
2014_11_26-AM-11_22_13
Home
Index