Nuprl Definition : app_permf

app_permf(m;n;p;q) ==  λi.if i <z m then p i else (q (i - m)) + m fi 


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  lambda: λx.A[x],  subtract: n - m,  add: n + m
Definitions occuring in definition :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  add: n + m,  apply: f a,  subtract: n - m
Latex:
app\_permf(m;n;p;q)  ==    \mlambda{}i.if  i  <z  m  then  p  i  else  (q  (i  -  m))  +  m  fi 


Date html generated: 2016_05_16-AM-07_30_32
Last ObjectModification: 2015_09_23-AM-09_51_21

Theory : perms_1


Home Index