Nuprl Definition : es-prior-fixedpoints

prior-f-fixedpoints(e) ==
  fix((λes-prior-fixedpoints,e. if f e = e
                               then if e ∈b prior(Sys) then (es-prior-fixedpoints prior(Sys)(e)) @ [e] else [e] fi 
                               else es-prior-fixedpoints f**(e)
                               fi )) 
  e


Definitions occuring in Statement :  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e ∈b X,  es-fix: f**(e),  es-eq-E: e = e',  append: as @ bs,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x]
FDL editor aliases :  es-prior-fixedpoints
Latex:
prior-f-fixedpoints(e)  ==
    fix((\mlambda{}es-prior-fixedpoints,e.  if  f  e  =  e
                                                              then  if  e  \mmember{}\msubb{}  prior(Sys)
                                                                        then  (es-prior-fixedpoints  prior(Sys)(e))  @  [e]
                                                                        else  [e]
                                                                        fi 
                                                              else  es-prior-fixedpoints  f**(e)
                                                              fi  )) 
    e


Date html generated: 2015_07_21-PM-03_51_40
Last ObjectModification: 2012_07_02-PM-04_14_58

Home Index