Nuprl Definition : simple-finite-cantor-decider
FiniteCantorDecide(dcdr;n;F) ==
case primrec(n;λs.if dcdr (F (λi.s[i])) then inl (λi.s[i]) else inr (λ%6.Ax) fi ;λi,x,s. case x (s @ [tt])
of inl(f) =>
inl f
| inr(_) =>
case x (s @ [ff])
of inl(f) =>
inl f
| inr(_) =>
inr (λ_.Ax) )
[]
of inl(f) =>
inl <f, case dcdr (F f) of inl(x) => x | inr(_) => Ax>
| inr(_) =>
inr (λ_.Ax)
Definitions occuring in Statement :
select: L[n],
append: as @ bs,
cons: [a / b],
nil: [],
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
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),
ifthenelse: if b then t else f fi ,
select: L[n],
btrue: tt,
append: as @ bs,
cons: [a / b],
bfalse: ff,
nil: [],
inl: inl x,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
inr: inr x ,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
simple-finite-cantor-decider
Latex:
FiniteCantorDecide(dcdr;n;F) ==
case primrec(n;\mlambda{}s.if dcdr (F (\mlambda{}i.s[i]))
then inl (\mlambda{}i.s[i])
else inr (\mlambda{}\%6.Ax)
fi ;\mlambda{}i,x,s. case x (s @ [tt])
of inl(f) =>
inl f
| inr($_{}$) =>
case x (s @ [ff]) of inl(f) => inl f | inr($_{}$\000C) => inr (\mlambda{}$_{}$.Ax) )
[]
of inl(f) =>
inl <f, case dcdr (F f) of inl(x) => x | inr($_{}$) => Ax>
| inr($_{}$) =>
inr (\mlambda{}$_{}$.Ax)
Date html generated:
2016_05_14-PM-09_33_37
Last ObjectModification:
2015_11_15-PM-10_19_05
Theory : continuity
Home
Index