Nuprl Definition : df-opt-prog

df-opt-prog(dfp;b) ==
  let B,S,init,nxt = dfp
  in <B
     , S?
     , inl init 
     , s,m.
        case s of inl(s) => let s',o = nxt s m in <inl s' , if bag-null(o) then b else o fi > | inr(z) => <inl s , b>>  


Proof not projected



Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  spreadn: spread4,  unit: Unit,  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],  inl: inl x ,  union: left + right,  bag-null: bag-null(bs)
FDL editor aliases :  df-opt-prog
df-opt-prog(dfp;b)  ==
    let  B,S,init,nxt  =  dfp
    in  <B
          ,  S?
          ,  inl  init 
          ,  \mlambda{}s,m.
                case  s
                of  inl(s)  =>
                  let  s',o  =  nxt  s  m 
                  in  <inl  s'  ,  if  bag-null(o)  then  b  else  o  fi  >
                  |  inr(z)  =>
                  <inl  s  ,  b>>   


Date html generated: 2011_10_20-PM-03_16_21
Last ObjectModification: 2011_08_17-PM-06_10_47

Home Index