Nuprl Definition : hdf-compose2

==
  mk-hdf(XY,a.let X,Y XY 
              in let X',fs X(a) 
                 in let Y',bs Y(a) 
                    in let out ←─ ∪f∈fs.∪b∈bs.f b
                       in <<X', Y'>out>;XY.let X,Y XY 
                                          in hdf-halted(X) ∨bhdf-halted(Y);<X, Y>)



Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-halted: hdf-halted(P) hdf-ap: X(a) bor: p ∨bq callbyvalueall: callbyvalueall apply: a spread: spread def pair: <a, b> bag-combine: x∈bs.f[x]
FDL editor aliases :  hdf-compose2
X  o  Y  ==
    mk-hdf(XY,a.let  X,Y  =  XY 
                            in  let  X',fs  =  X(a) 
                                  in  let  Y',bs  =  Y(a) 
                                        in  let  out  \mleftarrow{}{}  \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f  b
                                              in  <<X',  Y'>,  out>XY.let  X,Y  =  XY 
                                                                                    in  hdf-halted(X)  \mvee{}\msubb{}hdf-halted(Y);<X,  Y>)



Date html generated: 2015_07_17-AM-08_05_26
Last ObjectModification: 2012_11_23-PM-02_09_30

Home Index