Nuprl Definition : SM3-class-du

SM3-class-du(init;trX1;trX2;trX3) ==
  let tr1,X1 = trX1
  in let tr2,X2 = trX2
     in let tr3,X3 = trX3
        in Accum-loc-class(tr1 + tr2 + tr3;init;X1 + X2 + X3)

Proof not projected

Definitions occuring in Statement : disjoint-union-tr: tr1 + tr2, disjoint-union-class: X + Y, Accum-loc-class: Accum-loc-class(f;init;X), spread: spread def
FDL editor aliases : SM3-class-du

SM3-class-du(init;trX1;trX2;trX3) == let tr1,X1 = trX1 in let tr2,X2 = trX2 in let tr3,X3 = trX3 in Accum-loc-class(tr1 + tr2 + tr3;init;X1 + X2 + X3) Date html generated: 2011_10_20-PM-03_41_10 Last ObjectModification: 2011_09_23-PM-08_59_05 Home Index