proposition: Lemma decompose_is_complete : forall e sigma, is_a_solution_e e sigma -> match decompose e with | Normal _ _ => False | Not_appliable _ pb' => is_a_solution pb' sigma | No_solution _ => False end.
proof: Proof. intro e; pattern e; apply (well_founded_ind wf_lt_exc_pb_ok); clear e. intros [[pb | pb | ] Inv_pb] IH theta theta_is_sol; rewrite decompose_unfold; unfold F_decompose; trivial. assert (H := IH _ (decomposition_step_decreases_e _ Inv_pb) theta). destruct pb as [sigma l]. destruct (decompose (decomposition_step_e (OK (Normal unification_problem (mk_pb sigma l)) Inv_pb))); apply H; simpl; simpl in theta_is_sol; apply decomposition_step_is_complete; 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)