Nuprl Definition : disjoint-union-tr
tr1 + tr2 == 
l,a,s.if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi
Proof not projected
Definitions occuring in Statement :
outr: outr(x),
outl: outl(x),
isl: isl(x),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: x.A[x]
FDL editor aliases :
disjoint-union-tr
tr1 + tr2 == \mlambda{}l,a,s.if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi
Date html generated:
2011_10_20-PM-03_39_38
Last ObjectModification:
2011_09_23-PM-08_47_53
Home
Index