Nuprl Definition : fun2tree

==r let n,br 
    in case br
        of inl(x) =>
        Wsup(inl x;λi.i)
        inr(_) =>
        Wsup(inr i.fun2tree(M;<1, λx.if (x =z n) then else br fi >))

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

Definitions occuring in Statement :  Wsup: Wsup(a;b) callbyvalue: callbyvalue ifthenelse: if then else fi  eq_int: (i =z j) isaxiom: if Ax then otherwise b apply: a fix: fix(F) lambda: λx.A[x] spread: spread def pair: <a, b> inr: inr  inl: inl x add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) spread: spread def callbyvalue: callbyvalue isaxiom: if Ax then otherwise b inr: inr  pair: <a, b> add: m natural_number: $n ifthenelse: if then else fi  eq_int: (i =z j) apply: a Wsup: Wsup(a;b) inl: inl x lambda: λx.A[x]
FDL editor aliases :  fun2tree
==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  >))

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))) 

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

Theory : continuity

Home Index