Nuprl Definition : st-lookup

st-lookup(tab;x) ==
  let K,p,f tab in 
  let mu(λn.(p <n ∨bK ≤n ∨bfst((f n)) =a1 x)) in
      if p <n ∨bK ≤then inr ⋅  else inl (snd((f n))) fi 



Definitions occuring in Statement :  mu: mu(f) le_int: i ≤j bor: p ∨bq eq_atom: eq_atom$n(x;y) ifthenelse: if then else fi  lt_int: i <j let: let it: spreadn: spread3 pi1: fst(t) pi2: snd(t) apply: a lambda: λx.A[x] inr: inr  inl: inl x
FDL editor aliases :  st-lookup st-lookup

Latex:
st-lookup(tab;x)  ==
    let  K,p,f  =  tab  in 
    let  n  =  mu(\mlambda{}n.(p  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  \mvee{}\msubb{}fst((f  n))  =a1  x))  in
            if  p  <z  n  \mvee{}\msubb{}K  \mleq{}z  n  then  inr  \mcdot{}    else  inl  (snd((f  n)))  fi 



Date html generated: 2016_05_16-AM-10_00_33
Last ObjectModification: 2013_03_25-PM-01_53_07

Theory : new!event-ordering


Home Index