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 (i n)
                                            of inl(z) =>
                                            inl <n, z>
                                            inr(u) =>
                                            inr k.if (k) < (i n)  then k  else u) )

Definitions occuring in Statement :  primrec: primrec(n;b;c) less: if (a) < (b)  then c  else d apply: a lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x subtract: m add: m axiom: Ax
Definitions occuring in definition :  apply: a add: m less: if (a) < (b)  then c  else d lambda: λx.A[x] inr: inr  pair: <a, b> inl: inl x decide: case of inl(x) => s[x] inr(y) => t[y] axiom: Ax subtract: m primrec: primrec(n;b;c)
FDL editor aliases :  int-seg-case

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