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