proposition: Lemma matching_step1_is_sound : forall t1 t2 Wt1 Wt2 sigma pb, is_wf_sol pb sigma -> In pb (wf_solve_loop ((W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2)) :: nil)) -> apply_cf_subst sigma t1 = t2.
proof: Proof. intros t1 t2 Wt1 Wt2 sigma pb Is_sol In_pb. elim (wf_solve_loop_is_sound _ _ sigma In_pb Is_sol). clear pb Is_sol In_pb; intros pb H; elim H; clear H; intros In_pb Is_sol; elim In_pb; clear In_pb; intro In_pb. subst pb; unfold init_pb in Is_sol; simpl in Is_sol; unfold is_sol, is_rough_sol in Is_sol; elim Is_sol; clear Is_sol; intros sigma' H; elim H; clear H; intros Is_sol eq_subst; elim Is_sol; clear Is_sol; intros Is_sol _; simpl in Is_sol; replace (apply_cf_subst sigma t1) with (apply_cf_subst sigma' t1). apply Is_sol; left; trivial. simpl existential_vars in eq_subst; clear t2 Wt2 Wt1 Is_sol. apply sym_eq; pattern t1; apply term_rec3. intro v; elim (eq_subst v); [ contradiction | trivial ]. intros. simpl; replace (map (apply_cf_subst sigma') l) with (map (apply_cf_subst sigma) l); trivial. induction l; trivial. simpl; rewrite (H a). rewrite IHl; trivial. intros; apply H; right; trivial. left; trivial. contradiction. 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)