Nuprl Definition : strong-continuity-test-sp
strong-continuity-test-sp(M;n;f;k) ==
primrec(n;inl k;λi,r. case M i f of inl(m) => if (m =z k) then inr Ax else r fi | inr(x) => r)
Definitions occuring in Statement :
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
axiom: Ax
Definitions occuring in definition :
primrec: primrec(n;b;c),
inl: inl x,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
inr: inr x ,
axiom: Ax
FDL editor aliases :
strong-continuity-test-sp
Latex:
strong-continuity-test-sp(M;n;f;k) ==
primrec(n;inl k;\mlambda{}i,r. case M i f of inl(m) => if (m =\msubz{} k) then inr Ax else r fi | inr(x) => r)
Date html generated:
2016_05_14-PM-09_41_52
Last ObjectModification:
2015_09_22-PM-06_03_36
Theory : continuity
Home
Index