Nuprl Definition : strong-continuity-test-bound

strong-continuity-test-bound(M;n;f;b) ==
  primrec(n;inr Ax ;λi,r. if i <z b then inr Ax  if (i =z b) then inl b if isl(M i f) then inr Ax  else r fi )


Definitions occuring in Statement :  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  isl: isl(x),  lt_int: i <z j,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  inr: inr x ,  inl: inl x,  axiom: Ax
Definitions occuring in definition :  axiom: Ax,  inr: inr x ,  apply: f a,  isl: isl(x),  ifthenelse: if b then t else f fi ,  inl: inl x,  eq_int: (i =z j),  lt_int: i <z j,  lambda: λx.A[x],  primrec: primrec(n;b;c)
FDL editor aliases :  strong-continuity-test-bound strong-continuity-test-bound
Latex:
strong-continuity-test-bound(M;n;f;b)  ==
    primrec(n;inr  Ax  ;\mlambda{}i,r.  if  i  <z  b  then  inr  Ax 
                                                  if  (i  =\msubz{}  b)  then  inl  b
                                                  if  isl(M  i  f)  then  inr  Ax 
                                                  else  r
                                                  fi  )


Date html generated: 2016_05_19-AM-11_59_31
Last ObjectModification: 2016_05_17-AM-08_56_24

Theory : continuity


Home Index