Nuprl Definition : half-cubes

half-cubes(k) ==
  primrec(k;λc.<λx.x, Ax>;λi,x,c. if dim(c ((i + 1) - 1))=1
                                  then let v1,v2 = c ((i + 1) - 1) 
                                       in if q_less(v1;v2)
                                          then map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else <v1, qavg(v1;v2)> fi ;x\000C c)
                                               @ map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else <qavg(v1;v2), v2> fi \000C;x c)
                                          else Ax
                                          fi 
                                  else map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else c i@0 fi ;x c))


Definitions occuring in Statement :  rat-interval-dimension: dim(I),  qavg: qavg(a;b),  q_less: q_less(r;s),  map: map(f;as),  append: as @ bs,  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  add: n + m,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  apply: f a,  natural_number: $n,  add: n + m,  subtract: n - m,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  map: map(f;as),  axiom: Ax,  qavg: qavg(a;b),  pair: <a, b>,  append: as @ bs,  q_less: q_less(r;s),  spread: spread def,  rat-interval-dimension: dim(I),  int_eq: if a=b then c else d,  primrec: primrec(n;b;c)
FDL editor aliases :  half-cubes
Latex:
half-cubes(k)  ==
    primrec(k;\mlambda{}c.<\mlambda{}x.x,  Ax>\mlambda{}i,x,c.  if  dim(c  ((i  +  1)  -  1))=1
                                                                    then  let  v1,v2  =  c  ((i  +  1)  -  1) 
                                                                              in  if  q\_less(v1;v2)
                                                                                    then  map(\mlambda{}h,i@0.  if  i@0  <z  (i  +  1)  -  1
                                                                                                                    then  h  i@0
                                                                                                                    else  <v1,  qavg(v1;v2)>
                                                                                                                    fi  ;x  c)
                                                                                              @  map(\mlambda{}h,i@0.  if  i@0  <z  (i  +  1)  -  1
                                                                                                                        then  h  i@0
                                                                                                                        else  <qavg(v1;v2),  v2>
                                                                                                                        fi  ;x  c)
                                                                                    else  Ax
                                                                                    fi 
                                                                    else  map(\mlambda{}h,i@0.  if  i@0  <z  (i  +  1)  -  1  then  h  i@0  else  c  i@0  fi  ;x\000C  c))


Date html generated: 2019_10_29-AM-07_53_01
Last ObjectModification: 2019_10_21-PM-02_54_21

Theory : rationals


Home Index