Nuprl Definition : nim-grp
nim-grp() == <ℕ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. nim-sum(x;y), 0, λx.x>
Definitions occuring in Statement :
nim-sum: nim-sum(x;y),
nat: ℕ,
le_int: i ≤z j,
eq_int: (i =z j),
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
nat: ℕ,
eq_int: (i =z j),
le_int: i ≤z j,
nim-sum: nim-sum(x;y),
pair: <a, b>,
natural_number: $n,
lambda: λx.A[x]
FDL editor aliases :
nim-grp
Latex:
nim-grp() == <\mBbbN{}, \mlambda{}x,y. (x =\msubz{} y), \mlambda{}x,y. x \mleq{}z y, \mlambda{}x,y. nim-sum(x;y), 0, \mlambda{}x.x>
Date html generated:
2018_05_21-PM-09_15_28
Last ObjectModification:
2018_02_12-PM-05_57_45
Theory : general
Home
Index