Nuprl Definition : es-decl-set-join

es-decl-set-join(dd1;dd2) ==
  let S1,ds1,da1 = dd1 in
  let S2,ds2,da2 = dd2 in
  <remove-repeats(IdDeq;S1 @ S2)
  , λi.if i ∈_b S1)
       then if i ∈_b S2)
            then if null(fpf-domain(da1 i)) then ds2 i
                 if null(fpf-domain(da2 i)) then ds1 i
                 else ds1 i ⊕ ds2 i
                 fi
            else ds1 i
            fi
       else ds2 i
       fi

  , λi.if i ∈_b S1) then if i ∈_b S2) then da1 i ⊕ da2 i else da1 i fi  else da2 i fi >

Definitions occuring in Statement : fpf-join: f ⊕ g, fpf-domain: fpf-domain(f), Kind-deq: KindDeq, id-deq: IdDeq, remove-repeats: remove-repeats(eq;L), deq-member: x ∈_b L), append: as @ bs, null: null(as), ifthenelse: if b then t else f fi , spreadn: spread3, apply: f a, lambda: λx.A[x], pair: <a, b>
FDL editor aliases : es-decl-set-join
es-decl-set-join(dd1;dd2) == let S1,ds1,da1 = dd1 in let S2,ds2,da2 = dd2 in <remove-repeats(IdDeq;S1 @ S2) , \mlambda{}i.if i \mmember{}\msubb{} S1) then if i \mmember{}\msubb{} S2) then if null(fpf-domain(da1 i)) then ds2 i if null(fpf-domain(da2 i)) then ds1 i else ds1 i \moplus{} ds2 i fi else ds1 i fi else ds2 i fi , \mlambda{}i.if i \mmember{}\msubb{} S1) then if i \mmember{}\msubb{} S2) then da1 i \moplus{} da2 i else da1 i fi else da2 i fi > Date html generated: 2015_07_17-AM-11_56_50 Last ObjectModification: 2013_03_27-AM-10_38_54 Home Index