Nuprl Definition : circle-param
circle-param(t) ==  λi.if (i =z 0) then (r1 - t * t/r1 + (t * t)) else (r(2) * t/r1 + (t * t)) fi 
Definitions occuring in Statement : 
rdiv: (x/y)
, 
rsub: x - y
, 
rmul: a * b
, 
radd: a + b
, 
int-to-real: r(n)
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
lambda: λx.A[x]
, 
natural_number: $n
Definitions occuring in definition : 
lambda: λx.A[x]
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
rsub: x - y
, 
rdiv: (x/y)
, 
radd: a + b
, 
int-to-real: r(n)
, 
natural_number: $n
, 
rmul: a * b
FDL editor aliases : 
circle-param
Latex:
circle-param(t)  ==    \mlambda{}i.if  (i  =\msubz{}  0)  then  (r1  -  t  *  t/r1  +  (t  *  t))  else  (r(2)  *  t/r1  +  (t  *  t))  fi 
Date html generated:
2017_10_03-AM-10_51_08
Last ObjectModification:
2017_06_18-PM-01_23_56
Theory : reals
Home
Index