|
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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
