proposition: Theorem wf_solve_loop_is_sound : forall lpb p sigma, In p (wf_solve_loop lpb) -> is_wf_sol p sigma -> exists pb, In pb lpb /\ is_wf_sol pb sigma.
proof: Proof. intro lpb; refine (well_founded_ind well_founded_o_lpb (fun lpb => forall p sigma, In p (wf_solve_loop lpb) -> is_wf_sol p sigma -> exists pb, In pb lpb /\ is_wf_sol pb sigma) _ _); clear lpb; intros lpb IH p sigma In_p Is_sol_p; destruct lpb. rewrite wf_solve_nil in In_p; contradiction. rewrite wf_solve_cons in In_p; destruct w; destruct (unsolved_part pb). elim In_p; clear In_p; intro In_p. exists p; split; trivial; left; subst p; trivial. elim (IH lpb (F_wf_solve_dec1 _ _) p sigma In_p Is_sol_p); intros pb0 H; elim H; clear H; intros In_pb0 Is_sol_pb0; exists pb0; split; trivial; right; trivial. elim (IH (wf_solve (W pb w) ++ lpb) (F_wf_solve_dec2 _ _) p sigma In_p Is_sol_p); intros pb0 H; elim H; clear H; intros In_pb0 Is_sol_pb0; elim (in_app_or _ _ _ In_pb0); clear In_pb0; intro In_pb0. exists (W pb w); split; [ left; trivial | apply (wf_solve_is_sound _ _ _ In_pb0 Is_sol_pb0) ]. 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)