### Nuprl Definition : finite-cantor-decider

`finite-cantor-decider(dcdr;n;F) ==`
`  case primrec(n;λs,t. if dcdr (F (λi.s[i])) (F (λi.t[i]))`
`                      then inl <λi.s[i], λi.t[i]>`
`                      else inr (λ%8.Ax) `
`                      fi ;λi,x,s,t. case x (s @ [tt]) (t @ [ff])`
`                                of inl(fg) =>`
`                                inl fg`
`                                | inr(_) =>`
`                                case x (s @ [ff]) (t @ [tt])`
`                                 of inl(fg) =>`
`                                 inl fg`
`                                 | inr(_) =>`
`                                 case x (s @ [ff]) (t @ [ff])`
`                                  of inl(fg) =>`
`                                  inl fg`
`                                  | inr(_) =>`
`                                  case x (s @ [tt]) (t @ [tt]) of inl(fg) => inl fg | inr(_) => inr (λ_.Ax) ) `
`       [] `
`       []`
`   of inl(fg) =>`
`   inl let f,g = fg `
`       in <f, g, case dcdr (F f) (F g) 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]` spread: spread def 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]` bfalse: `ff` append: `as @ bs` cons: `[a / b]` btrue: `tt` nil: `[]` inl: `inl x` spread: spread def 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 :  finite-cantor-decider

Latex:
finite-cantor-decider(dcdr;n;F)  ==
case  primrec(n;\mlambda{}s,t.  if  dcdr  (F  (\mlambda{}i.s[i]))  (F  (\mlambda{}i.t[i]))
then  inl  <\mlambda{}i.s[i],  \mlambda{}i.t[i]>
else  inr  (\mlambda{}\%8.Ax)
fi  ;\mlambda{}i,x,s,t.  case  x  (s  @  [tt])  (t  @  [ff])
of  inl(fg)  =>
inl  fg
|  inr(\$_{}\$)  =>
case  x  (s  @  [ff])  (t  @  [tt])
of  inl(fg)  =>
inl  fg
|  inr(\$_{}\$)  =>
case  x  (s  @  [ff])  (t  @  [ff])
of  inl(fg)  =>
inl  fg
|  inr(\$_{}\$)  =>
case  x  (s  @  [tt])  (t  @  [tt])
of  inl(fg)  =>
inl  fg
|  inr(\$_{}\$)  =>
inr  (\mlambda{}\$_{}\$.Ax)  )
[]
[]
of  inl(fg)  =>
inl  let  f,g  =  fg
in  <f,  g,  case  dcdr  (F  f)  (F  g)  of  inl(x)  =>  x  |  inr(\$_{}\$)  =>  Ax>
|  inr(\$_{}\$)  =>
inr  (\mlambda{}\$_{}\$.Ax)

Date html generated: 2016_05_14-PM-09_33_30
Last ObjectModification: 2015_11_15-PM-11_49_17

Theory : continuity

Home Index