fact: Definition weight_exc_pb_ok e := match e with | OK (Normal _ pb) _ => (2, measure_for_unif_pb pb) | OK (Not_appliable _ pb) _ => (1, measure_for_unif_pb pb) | OK (No_solution _) _ => (0, (0,(nil,0))) end.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)