proposition: Lemma decompose_nf : forall e, match decompose e with | Normal _ _ => False | Not_appliable _ (mk_pb sigma l) => l = nil | No_solution _ => True end.
proof: Proof. intros e; pattern e; apply (well_founded_ind wf_lt_exc_pb_ok); clear e. intros [ [pb | pb | ] Inv_pb] IH; rewrite decompose_unfold; simpl. apply IH; refine (decomposition_step_decreases_e _ Inv_pb). simpl in Inv_pb; destruct pb; trivial. trivial. Qed.
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)