Nuprl Definition : unit-interval-fan

unit-interval-fan(f;n) ==
  primrec(n;<0, 1>;λi,p. let a,b = p 
               in if f i
                  then eval a' = (2 * a) + b in
                       eval b' = 3 * b in
                         <a', b'>
                  else eval a' = 3 * a in
                       eval b' = a + (2 * b) in
                         <a', b'>
                  fi )


Definitions occuring in Statement :  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  primrec: primrec(n;b;c),  lambda: λx.A[x],  spread: spread def,  ifthenelse: if b then t else f fi ,  apply: f a,  callbyvalue: callbyvalue,  add: n + m,  multiply: n * m,  natural_number: $n,  pair: <a, b>
FDL editor aliases :  unit-interval-fan
Latex:
unit-interval-fan(f;n)  ==
    primrec(n;ɘ,  1>\mlambda{}i,p.  let  a,b  =  p 
                              in  if  f  i
                                    then  eval  a'  =  (2  *  a)  +  b  in
                                              eval  b'  =  3  *  b  in
                                                  <a',  b'>
                                    else  eval  a'  =  3  *  a  in
                                              eval  b'  =  a  +  (2  *  b)  in
                                                  <a',  b'>
                                    fi  )


Date html generated: 2016_05_18-AM-10_54_40
Last ObjectModification: 2015_09_23-AM-09_17_51

Theory : reals


Home Index