---

feedback-df-prog1(B;G;P;buf;dfp) ==
  let C,S,s0,F = dfp
  in <B
     , S  bag(B)
     , <s0, buf>
     , s,a.
        evalall(let s1,s2 = s 
                in let s',out = F[s1;a] 
                   in <case s'
                       of inl(s3) =>
                        inl <s3, if P[G[out;s2]] then G[out;s2] else s2 fi > 
                        | inr(z) =>
                        inr  
                      , G[out;s2]
                      >)>  

---

Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  it: ,  spreadn: spread4,  so_apply: x[s1;s2],  so_apply: x[s],  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x ,  bag: bag(T),  evalall: evalall(t)
Definitions :  spreadn: spread4,  product: x:A  B[x],  bag: bag(T),  lambda: x.A[x],  evalall: evalall(t),  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x ,  pair: <a, b>,  ifthenelse: if b then t else f fi ,  so_apply: x[s],  inr: inr x ,  it: ,  so_apply: x[s1;s2]
FDL editor aliases :  feedback-df-prog1

---

feedback-df-prog1(B;G;P;buf;dfp)  ==
    let  C,S,s0,F  =  dfp
    in  <B
          ,  S  \mtimes{}  bag(B)
          ,  <s0,  buf>
          ,  \mlambda{}s,a.
                evalall(let  s1,s2  =  s 
                                in  let  s',out  =  F[s1;a] 
                                      in  <case  s'
                                              of  inl(s3)  =>
                                                inl  <s3,  if  P[G[out;s2]]  then  G[out;s2]  else  s2  fi  > 
                                                |  inr(z)  =>
                                                inr  \mcdot{} 
                                            ,  G[out;s2]
                                            >)>   


Date html generated: 2011_08_16-AM-09_42_52
Last ObjectModification: 2011_06_02-PM-06_33_37

Home Index