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