Nuprl Definition : SM-gen-class-du

SM-gen-class-du(init;n;m;trXs) ==
Y
(

SM-gen-class-du,m.
if (n =

m)
    then trXs m
    else let tr1,X1 = trXs m
         in let tr2,X2 = SM-gen-class-du (m + 1)
            in <

l,a,s.if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi , X1 + X2>
fi )
m

Proof not projected

Definitions occuring in Statement : disjoint-union-class: X + Y, outr: outr(x), outl: outl(x), isl: isl(x), eq_int: (i =

j), ifthenelse: if b then t else f fi , ycomb: Y, apply: f a, lambda:

x.A[x], spread: spread def, pair: <a, b>, add: n + m, natural_number: $n
FDL editor aliases : SM-gen-class-du SM-gen-class-du SM-gen-class-du SM-gen-class-du

SM-gen-class-du(init;n;m;trXs) == Y (\mlambda{}SM-gen-class-du,m. if (n =\msubz{} m) then trXs m else let tr1,X1 = trXs m in let tr2,X2 = SM-gen-class-du (m + 1) in <\mlambda{}l,a,s.if isl(a) then tr1 l outl(a) s else tr2 l outr(a) s fi , X1 + X2> fi ) m Date html generated: 2011_10_20-PM-03_40_17 Last ObjectModification: 2011_09_23-PM-05_37_34 Home Index