poly2bernstein : THEORY
BEGIN

  IMPORTING multi_polynomial,
            multi_bernstein

  polydegmono,
  bsdegmono   : VAR DegreeMono
  pprod       : VAR Polyproduct
  mpoly       : VAR MultiPolynomial
  nvars,terms : VAR posnat
  cf          : VAR Coeff

  bs_convert_mono(pprod,polydegmono,bsdegmono,nvars)(j:nat)(s:nat): real =
    IF s>bsdegmono(j) THEN 0 
    ELSE sigma(0,s,LAMBDA(i:nat):IF i>s OR i>polydegmono(j) THEN 0 
                                 ELSE pprod(j)(i)*(C(s,i)/C(bsdegmono(j),i)) 
                                 ENDIF) 
    ENDIF
   
  bs_convert_poly(mpoly,polydegmono,bsdegmono,nvars,terms)(r:nat): Polyproduct = 
    bs_convert_mono(mpoly(r),polydegmono,bsdegmono,nvars)

  bs_convert_poly_def: LEMMA le_below_mono?(nvars)(polydegmono,bsdegmono) IMPLIES
    multipoly_eval(mpoly,polydegmono,cf,nvars,terms) = 
    multibs_eval(bs_convert_poly(mpoly,polydegmono,bsdegmono,nvars,terms),
                 bsdegmono,cf,nvars,terms)

END poly2bernstein