Nuprl Definition : fun2tree

fun2tree(M;p)
==r let n,br = p 
    in case M n br
        of inl(x) =>
        Wsup(inl x;λi.i)
        | inr(_) =>
        Wsup(inr n ;λi.fun2tree(M;<n + 1, λx.if (x =z n) then i else br x fi >))
fun2tree(M;p) ==
  fix((λfun2tree,p. let n,br = p 
                    in eval t = M n br in
                       if t = Ax then Wsup(inr n ;λi.(fun2tree <n + 1, λx.if (x =z n) then i else br x fi >))
                       otherwise Wsup(inl t;λi.i))) 
  p


Definitions occuring in Statement :  Wsup: Wsup(a;b),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  spread: spread def,  callbyvalue: callbyvalue,  isaxiom: if z = Ax then a otherwise b,  inr: inr x ,  pair: <a, b>,  add: n + m,  natural_number: $n,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  Wsup: Wsup(a;b),  inl: inl x,  lambda: λx.A[x]
FDL editor aliases :  fun2tree
Latex:
fun2tree(M;p)
==r  let  n,br  =  p 
        in  case  M  n  br
                of  inl(x)  =>
                Wsup(inl  x;\mlambda{}i.i)
                |  inr($_{}$)  =>
                Wsup(inr  n  ;\mlambda{}i.fun2tree(M;<n  +  1,  \mlambda{}x.if  (x  =\msubz{}  n)  then  i  else  br  x  fi  >))
Latex:
fun2tree(M;p)  ==
    fix((\mlambda{}fun2tree,p.  let  n,br  =  p 
                                        in  eval  t  =  M  n  br  in
                                              if  t  =  Ax  then  Wsup(inr  n  ;\mlambda{}i.(fun2tree 
                                                                                                            <n  +  1,  \mlambda{}x.if  (x  =\msubz{}  n)  then  i  else  br  x  fi  >))
                                              otherwise  Wsup(inl  t;\mlambda{}i.i))) 
    p


Date html generated: 2019_06_20-PM-03_08_34
Last ObjectModification: 2018_08_14-PM-02_06_56

Theory : continuity


Home Index