Nuprl Definition : es-interface-match

es-interface-match(A;B;R) ==
  eclass-compose2(λx,y. if (#(x) =z 1)
                       then if (#(y) =z 1)
                            then case find-first(λa.(R a only(x));only(y)) of inl(a) => {<a, only(x)>} | inr(z) => {}
                            else {}
                            fi 
                       else {}
                       fi ;B;Prior(es-interface-unmatched(A; B; R)))


Definitions occuring in Statement :  primed-class: Prior(X),  es-interface-unmatched: es-interface-unmatched(A; B; R),  eclass-compose2: eclass-compose2(f;X;Y),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  find-first: find-first(P;L),  bag-only: only(bs),  bag-size: #(bs),  single-bag: {x},  empty-bag: {}
FDL editor aliases :  es-interface-match
Latex:
es-interface-match(A;B;R)  ==
    eclass-compose2(\mlambda{}x,y.  if  (\#(x)  =\msubz{}  1)
                                              then  if  (\#(y)  =\msubz{}  1)
                                                        then  case  find-first(\mlambda{}a.(R  a  only(x));only(y))
                                                                    of  inl(a)  =>
                                                                    \{<a,  only(x)>\}
                                                                    |  inr(z)  =>
                                                                    \{\}
                                                        else  \{\}
                                                        fi 
                                              else  \{\}
                                              fi  ;B;Prior(es-interface-unmatched(A;  B;  R)))


Date html generated: 2015_07_21-PM-03_26_24
Last ObjectModification: 2012_02_25-PM-02_26_18

Home Index