/top,compute_sturm,sturm,polynomial_division,number_sign_changes,gcd_coeff,remainder_sequence,polynomial_pseudo_divide,clear_denominators,sturmsquarefree,polylist,poly_strategy,strategies,examples
interval_arith/interval
structures/listn,sort_array,for_iterate,array2list,permutations,min_array_def,more_list_props,max_array_def,below_arrays,Unit_adt,Unit,sort_array_def
reals/binomial_identities,factorial,binomial,abs_lems,sign,log_nat,polynomials,prelude_aux,root,real_orders,real_fun_ops,more_polynomial_props,RealInt,sigma_upto,sigma_swap,min_max,product,real_order_ep,sigma,sq,sigma_nat
ints/factorial,div,gcd,divides_lems,div_nat,floor_div_lems,mod_lems,max_bounded_posnat,min_posnat,floor_more,pigeonhole,abs_rews
top:compute_sturm,gcd_coeff,number_sign_changes,polynomial_division,polynomial_pseudo_divide,remainder_sequence,sturm,sturmsquarefree,polylist,poly_strategy,strategies,examples
compute_sturm:sturm,remainder_sequence,clear_denominators,reals@RealInt,reals@more_polynomial_props,reals@real_orders,reals@real_order_ep
sturm:reals@polynomials,reals@more_polynomial_props,reals@sign,polynomial_division,structures@more_list_props,ints@gcd,number_sign_changes,structures@sort_array,gcd_coeff
polynomial_division:reals@polynomials,structures@array2list
number_sign_changes:reals@sign
gcd_coeff:reals@polynomials,reals@more_polynomial_props,reals@sign,polynomial_division,structures@more_list_props,ints@gcd,structures@listn,structures@array2list,reals@sigma
remainder_sequence:polynomial_pseudo_divide
polynomial_pseudo_divide:reals@polynomials,structures@array2list,polynomial_division,gcd_coeff
clear_denominators:ints@gcd
sturmsquarefree:reals@polynomials,reals@more_polynomial_props,reals@sign,polynomial_division,number_sign_changes,structures@more_list_props,ints@gcd,gcd_coeff,structures@sort_array
polylist:structures@array2list,reals@polynomials,reals@sq
poly_strategy:polylist,compute_sturm
strategies:poly_strategy,structures@Unit,reals@abs_lems,interval_arith@interval
examples:strategies