proposition: Lemma matching_step1_is_complete : forall t1 t2 Wt1 Wt2 sigma, well_formed_cf_subst sigma -> apply_cf_subst sigma t1 = t2 -> (exists pb, is_wf_wf_sol pb sigma /\ In pb (wf_solve_loop ((W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2)) :: nil))).
proof: Proof. intros t1 t2 Wt1 Wt2 sigma Wsigma Is_sol. set (pb:=(W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2))). elim (wf_solve_loop_is_complete (pb :: nil) pb) with sigma. intros pb0 H; elim H; clear H; intros In_pb0 Is_sol0; exists pb0; split; trivial. left; trivial. unfold is_wf_wf_sol, is_well_formed_sol, is_rough_sol. simpl; exists sigma; intuition. injection H0; intros; subst t0 t3; 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)