Nuprl Definition : integer-dot-product

as ⋅ bs
==r if as = Ax then 0 otherwise if bs = Ax then 0 otherwise let a,as2 = as

                                                            in let b,bs2 = bs

                                                               in (a * b) + as2 ⋅ bs2

as ⋅ bs ==

  fix((λinteger-dot-product,as,bs. if as = Ax then 0 otherwise if bs = Ax then 0 otherwise let a,as2 = as

                                                                                           in let b,bs2 = bs

                                                                                              in (a * b)

                                                                                                 + (integer-dot-product

as2

                                                                                                    bs2)))

as
bs

Definitions occuring in Statement : isaxiom: if z = Ax then a otherwise b, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, multiply: n * m, add: n + m, natural_number: $n
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], isaxiom: if z = Ax then a otherwise b, natural_number: $n, spread: spread def, add: n + m, multiply: n * m, apply: f a
FDL editor aliases : z-dot

Latex:
as \mcdot{} bs ==r if as = Ax then 0 otherwise if bs = Ax then 0 otherwise let a,as2 = as in let b,bs2 = bs in (a * b) + as2 \mcdot{} bs2

Latex:
as \mcdot{} bs == fix((\mlambda{}integer-dot-product,as,bs. if as = Ax then 0 otherwise if bs = Ax then 0 otherwise let a,as2 = as in let b,bs2 = bs in (a * b) + (integer-dot-product as2 bs2)\000C)) as bs Date html generated: 2016_05_14-AM-06_56_04 Last ObjectModification: 2015_09_22-PM-05_51_16 Theory : omega Home Index