Nuprl Definition : itop
Π(op,id) lb ≤ i < ub. E[i] == Y (λitop,ub. if lb <z ub then (itop (ub - 1)) op E[ub - 1] else id fi ) ub
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
infix_ap: x f y,
ycomb: Y,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
infix_ap: x f y,
apply: f a,
subtract: n - m,
natural_number: $n
Latex:
\mPi{}(op,id) lb \mleq{} i < ub. E[i] ==
Y (\mlambda{}itop,ub. if lb <z ub then (itop (ub - 1)) op E[ub - 1] else id fi ) ub
Date html generated:
2016_05_15-PM-00_14_23
Last ObjectModification:
2015_09_23-AM-06_24_56
Theory : groups_1
Home
Index