Nuprl Definition : int-vec-add

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

                                                              in let b,bs2 = bs

                                                                 in [a + b / as2 + bs2]

as + bs ==

  fix((λint-vec-add,as,bs. if as = Ax then as otherwise if bs = Ax then bs otherwise let a,as2 = as

                                                                                     in let b,bs2 = bs

                                                                                        in [a + b /

                                                                                            (int-vec-add as2 bs2)]))

as
bs

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

Latex:
as + bs ==r if as = Ax then as otherwise if bs = Ax then bs otherwise let a,as2 = as in let b,bs2 = bs in [a + b / as2 + bs2]

Latex:
as + bs == fix((\mlambda{}int-vec-add,as,bs. if as = Ax then as otherwise if bs = Ax then bs otherwise let a,as2 = as in let b,bs2 = bs in [a + b / (int-vec-add as2 bs2)])) as bs Date html generated: 2016_05_14-AM-06_56_32 Last ObjectModification: 2015_09_22-PM-05_51_18 Theory : omega Home Index