Nuprl Definition : SM4-class-du

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

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 : SM4-class-du

SM4-class-du(init;trX1;trX2;trX3;trX4) == let tr1,X1 = trX1 in let tr2,X2 = trX2 in let tr3,X3 = trX3 in let tr4,X4 = trX4 in Accum-loc-class(tr1 + tr2 + tr3 + tr4;init;X1 + X2 + X3 + X4) Date html generated: 2011_10_20-PM-03_41_26 Last ObjectModification: 2011_09_23-PM-09_00_19 Home Index