SSL poly_strategy.pvs

poly_strategy : THEORY 
BEGIN

  IMPORTING polylist,compute_sturm

  pl : VAR Polylist
  I  : VAR RealInt

  realord: VAR (SturmRel?)

  sturm((pl|deg(pl)>0),(I|I`lb<I`ub),realord): bool =
    compute_poly_sat_rational(list2array[rat](0)(pl),deg(pl),I,realord)

  sturm_def: LEMMA 
    I`lb<I`ub AND 
    (deg(pl)>0 OR (EXISTS (j:below(length(pl))):j>0 AND nth(pl,j)/=0))
    IMPLIES
    (sturm(pl,I,realord) IFF
     (FORALL (x:real): contains?(I)(x) IMPLIES realord(polylist(pl)(x),0)))

END poly_strategy