Nuprl Definition : Moessner-aux
Moessner-aux(r;x;y;h;d;k)==r if (k =z 0) then h else ([Moessner-aux(r;x;y;h;d;k - 1)]_Σ(d i | i < k)(y:=1)*Δ(x,y)) fi
Moessner-aux(r;x;y;h;d;k) ==
fix((λMoessner-aux,k. if (k =z 0) then h else ([Moessner-aux (k - 1)]_Σ(d i | i < k)(y:=1)*Δ(x,y)) fi )) k
Definitions occuring in Statement :
fps-set-to-one: [f]_n(y:=1),
fps-pascal: Δ(x,y),
fps-mul: (f*g),
sum: Σ(f[x] | x < k),
atom-deq: AtomDeq,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
fps-mul: (f*g),
atom-deq: AtomDeq,
fps-set-to-one: [f]_n(y:=1),
subtract: n - m,
natural_number: $n,
sum: Σ(f[x] | x < k),
apply: f a,
fps-pascal: Δ(x,y)
FDL editor aliases :
Moessner-aux
Latex:
Moessner-aux(r;x;y;h;d;k)
==r if (k =\msubz{} 0) then h else ([Moessner-aux(r;x;y;h;d;k - 1)]\_\mSigma{}(d i | i < k)(y:=1)*\mDelta{}(x,y)) fi
Latex:
Moessner-aux(r;x;y;h;d;k) ==
fix((\mlambda{}Moessner-aux,k. if (k =\msubz{} 0)
then h
else ([Moessner-aux (k - 1)]\_\mSigma{}(d i | i < k)(y:=1)*\mDelta{}(x,y))
fi ))
k
Date html generated:
2016_05_15-PM-10_00_54
Last ObjectModification:
2015_09_23-AM-08_21_50
Theory : power!series
Home
Index