Nuprl Definition : sum_aux
sum_aux(k;v;i;x.f[x])==r if (i) < (k) then eval v' = f[i] + v in eval i' = i + 1 in sum_aux(k;v';i';x.f[x]) else v
sum_aux(k;v;i;x.f[x]) ==
fix((λsum_aux,v,i. if (i) < (k) then eval v' = f[i] + v in eval i' = i + 1 in sum_aux v' i' else v)) v i
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
less: if (a) < (b) then c else d,
callbyvalue: callbyvalue,
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
sum_aux
Latex:
sum\_aux(k;v;i;x.f[x])
==r if (i) < (k) then eval v' = f[i] + v in eval i' = i + 1 in sum\_aux(k;v';i';x.f[x]) else v
Latex:
sum\_aux(k;v;i;x.f[x]) ==
fix((\mlambda{}sum$_{aux}$,v,i. if (i) < (k)
then eval v' = f[i] + v in
eval i' = i + 1 in
sum$_{aux}$ v' i'
else v))
v
i
Date html generated:
2016_05_14-AM-07_30_58
Last ObjectModification:
2015_09_22-PM-05_46_35
Theory : int_2
Home
Index