---

feedback-df-prog2(B;G;P;buf;dfp1;dfp2) ==
  let C1,S1,s1,F1 = dfp1
  in let C2,S2,s2,F2 = dfp2
     in <B
        , S1?  S2?  bag(B)
        , <inl s1 , inl s2 , buf>
        , s,a.
           evalall(let hs1,hs2,buf = s in 
           let s1',out1 = case hs1 of inl(s1) => F1 s1 a | inr(z) => <hs1, {}> 
           in let s2',out2 = case hs2
              of inl(s2) =>
               F2 s2 a
               | inr(z) =>
               <hs2, {}> 
              in let x = G out1 out2 buf in
                     <if (isl(s1'))  (isl(s2'))
                      then inr  
                      else inl <s1', s2', if P[x] then x else buf fi > 
                      fi 
                     , x
                     >)>    

---

Definitions occuring in Statement :  isl: isl(x),  band: p  q,  bnot: b,  ifthenelse: if b then t else f fi ,  let: let,  it: ,  spreadn: spread4,  spreadn: spread3,  so_apply: x[s],  unit: Unit,  apply: f a,  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 ,  union: left + right,  empty-bag: {},  bag: bag(T),  evalall: evalall(t)
Definitions :  spreadn: spread4,  product: x:A  B[x],  union: left + right,  unit: Unit,  bag: bag(T),  lambda: x.A[x],  evalall: evalall(t),  spreadn: spread3,  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  empty-bag: {},  let: let,  apply: f a,  band: p  q,  bnot: b,  isl: isl(x),  inr: inr x ,  it: ,  inl: inl x ,  pair: <a, b>,  ifthenelse: if b then t else f fi ,  so_apply: x[s]
FDL editor aliases :  feedback-df-prog2

---

feedback-df-prog2(B;G;P;buf;dfp1;dfp2)  ==
    let  C1,S1,s1,F1  =  dfp1
    in  let  C2,S2,s2,F2  =  dfp2
          in  <B
                ,  S1?  \mtimes{}  S2?  \mtimes{}  bag(B)
                ,  <inl  s1  ,  inl  s2  ,  buf>
                ,  \mlambda{}s,a.
                      evalall(let  hs1,hs2,buf  =  s  in 
                      let  s1',out1  =  case  hs1  of  inl(s1)  =>  F1  s1  a  |  inr(z)  =>  <hs1,  \{\}> 
                      in  let  s2',out2  =  case  hs2  of  inl(s2)  =>  F2  s2  a  |  inr(z)  =>  <hs2,  \{\}> 
                            in  let  x  =  G  out1  out2  buf  in
                                          <if  (\mneg{}\msubb{}isl(s1'))  \mwedge{}\msubb{}  (\mneg{}\msubb{}isl(s2'))
                                            then  inr  \mcdot{} 
                                            else  inl  <s1',  s2',  if  P[x]  then  x  else  buf  fi  > 
                                            fi 
                                          ,  x
                                          >)>       


Date html generated: 2011_08_16-AM-09_43_26
Last ObjectModification: 2011_06_03-AM-00_06_02

Home Index