Nuprl Definition : int-seg-case

int-seg-case(i;j;d) ==
  if (j) < (i)
     then inr (λk.Ax) 
     else primrec(j - i;inr (λk.Ax) ;λn,x. case x
                                           of inl(p) =>
                                           inl p
                                           | inr(f) =>
                                           case d (i + n)
                                            of inl(z) =>
                                            inl <i + n, z>
                                            | inr(u) =>
                                            inr (λk.if (k) < (i + n)  then f k  else u) )


Definitions occuring in Statement :  primrec: primrec(n;b;c),  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  subtract: n - m,  add: n + m,  axiom: Ax
Definitions occuring in definition :  apply: f a,  add: n + m,  less: if (a) < (b)  then c  else d,  lambda: λx.A[x],  inr: inr x ,  pair: <a, b>,  inl: inl x,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  axiom: Ax,  subtract: n - m,  primrec: primrec(n;b;c)
FDL editor aliases :  int-seg-case
Latex:
int-seg-case(i;j;d)  ==
    if  (j)  <  (i)
          then  inr  (\mlambda{}k.Ax) 
          else  primrec(j  -  i;inr  (\mlambda{}k.Ax)  ;\mlambda{}n,x.  case  x
                                                                                      of  inl(p)  =>
                                                                                      inl  p
                                                                                      |  inr(f)  =>
                                                                                      case  d  (i  +  n)
                                                                                        of  inl(z)  =>
                                                                                        inl  <i  +  n,  z>
                                                                                        |  inr(u)  =>
                                                                                        inr  (\mlambda{}k.if  (k)  <  (i  +  n)    then  f  k    else  u)  )


Date html generated: 2019_10_15-AM-10_19_49
Last ObjectModification: 2019_10_02-PM-05_55_44

Theory : call!by!value_2


Home Index