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 


Definitions occuring in Statement :  outr: outr(x),  outl: outl(x),  ifthenelse: if b then t else f fi ,  isl: isl(x),  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  disjoint-union-tr
Latex:
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: 2016_05_17-AM-09_14_40
Last ObjectModification: 2012_11_29-AM-11_13_27

Theory : classrel!lemmas


Home Index