proposition: Theorem wf_solve_loop_is_complete : forall lpb p sigma, In p lpb -> is_wf_wf_sol p sigma -> exists pb, In pb (wf_solve_loop lpb) /\ is_wf_wf_sol pb sigma.
proof: Proof. intro lpb; refine (well_founded_ind well_founded_o_lpb (fun lpb => forall p sigma, In p lpb -> is_wf_wf_sol p sigma -> exists pb, In pb (wf_solve_loop lpb) /\ is_wf_wf_sol pb sigma) _ _); clear lpb; intros lpb IH p sigma In_p Is_sol_p; destruct lpb. contradiction. rewrite wf_solve_cons; elim In_p; clear In_p; intro In_p. generalize (wf_solve_is_complete p sigma Is_sol_p); subst p; simpl. destruct w; destruct (unsolved_part pb). intros _; exists (W pb w); split; trivial; left; trivial. clear p; intro H; elim H; clear H; intros p H; elim H; clear H; intros In_p Is_sol; refine (IH (wf_solve (W pb w) ++ lpb) (F_wf_solve_dec2 _ _) p sigma (in_or_app _ _ _ (or_introl _ In_p)) Is_sol). destruct w; destruct (unsolved_part pb). elim (IH lpb (F_wf_solve_dec1 _ _) p sigma In_p Is_sol_p). intros pb0 H; elim H; clear H; intros; exists pb0; split; trivial; right; trivial. elim (IH (wf_solve (W pb w) ++ lpb) (F_wf_solve_dec2 _ _) p sigma (in_or_app _ _ _ (or_intror _ In_p)) Is_sol_p). intros pb0 H; elim H; clear H; intros; exists pb0; split; trivial; right; trivial. Qed.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)