Nuprl Definition : disjoint-union-class

X + Y ==

b1,b2.if bag-null(b1) then bag-map(

x.(inr x );b2) else bag-map(

x.(inl x );b1) fi |X, Y|

Proof not projected

Definitions occuring in Statement : simple-comb-2: F|X, Y|, ifthenelse: if b then t else f fi , lambda:

x.A[x], inr: inr x , inl: inl x , bag-null: bag-null(bs), bag-map: bag-map(f;bs)
FDL editor aliases : disjoint-union-class

X + Y == \mlambda{}b1,b2.if bag-null(b1) then bag-map(\mlambda{}x.(inr x );b2) else bag-map(\mlambda{}x.(inl x );b1) fi |X, Y| Date html generated: 2011_10_20-PM-03_37_55 Last ObjectModification: 2011_09_22-PM-07_26_54 Home Index