Nuprl Definition : sequential-composition-class

sequential-composition-class(X;Y;hdr) ==
  λes,e. let xs = X(e) in
          let not_hdr = [x∈xs|¬bname_eq(msg-header(x.msg);hdr)] in
          let has_hdr = [x∈xs|name_eq(msg-header(x.msg);hdr)] in
          not_hdr
          + if (#(has_hdr) =z 1)
            then let Infos = sequential-composition-inputs(es;e;X;hdr) in
                     Y list-eo(Infos;loc(e)) (||Infos|| - 1)
            else {}
            fi 


Definitions occuring in Statement :  sequential-composition-inputs: sequential-composition-inputs(es;e;X;hdr),  msg-interface-message: mi.msg,  msg-header: msg-header(m),  list-eo: list-eo(L;i),  class-ap: X(e),  es-loc: loc(e),  name_eq: name_eq(x;y),  length: ||as||,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  let: let,  apply: f a,  lambda: λx.A[x],  subtract: n - m,  natural_number: $n,  bag-size: #(bs),  bag-filter: [x∈b|p[x]],  bag-append: as + bs,  empty-bag: {}
FDL editor aliases :  sequential-composition-class
Latex:
sequential-composition-class(X;Y;hdr)  ==
    \mlambda{}es,e.  let  xs  =  X(e)  in
                    let  not$_{hdr}$  =  [x\mmember{}xs|\mneg{}\msubb{}name\_eq(msg-header(x.msg);hdr)]  in
                    let  has$_{hdr}$  =  [x\mmember{}xs|name\_eq(msg-header(x.msg);hdr)]  in
                    not$_{hdr}$
                    +  if  (\#(has$_{hdr}$)  =\msubz{}  1)
                        then  let  Infos  =  sequential-composition-inputs(es;e;X;hdr)  in
                                          Y  list-eo(Infos;loc(e))  (||Infos||  -  1)
                        else  \{\}
                        fi 


Date html generated: 2016_05_17-AM-09_01_49
Last ObjectModification: 2014_08_18-PM-02_03_13

Theory : messages


Home Index