proposition: Lemma mgu_founded : forall sigma c, is_a_total_oc_ordering sigma c = true -> VSet.without_red c -> (VSet.LP.permut c (VSet.support (domain_of_subst sigma))) -> forall tau, is_a_solution (mk_pb sigma nil) tau <-> (exists theta, (forall x, apply_subst tau (Var x) = apply_subst theta (apply_subst (acc_inst c sigma) (Var x)))).
proof: Proof. intros sigma c Hoc W c_in_dom tau; rewrite <- (total_acc_inst_inv c); trivial. split; intro Sol. exists tau. revert Sol; generalize (acc_inst c sigma); intros rho [_ Sol]. intro x; assert (Solx := Sol x); simpl in Solx; simpl. case_eq (find X.eq_bool x tau); [intro x_val | idtac ]; intro x_tau; rewrite x_tau in Solx. case_eq (find X.eq_bool x rho); [intro x_val' | idtac ]; intro x_rho; rewrite x_rho in Solx. subst x_val; reflexivity. simpl; rewrite x_tau; reflexivity. case_eq (find X.eq_bool x rho); [intro x_val' | idtac ]; intro x_rho; rewrite x_rho in Solx. trivial. simpl; rewrite x_tau; reflexivity. destruct Sol as [theta Sol]. assert (Idem : forall x y : variable, VSet.mem x (domain_of_subst (acc_inst c sigma)) -> VSet.mem y (domain_of_subst (acc_inst c sigma)) -> var_in_term x (apply_subst (acc_inst c sigma) (Var y)) = false). intros x y x_in_dom y_in_dom; apply (total_acc_inst_idem _ _ Hoc W). intros z z_in_c; rewrite <- (VSet.LP.mem_permut_mem z c_in_dom); apply in_impl_mem; trivial. reflexivity. rewrite <- acc_inst_dom in x_in_dom; rewrite <- (VSet.LP.mem_permut_mem x c_in_dom) in x_in_dom. revert x_in_dom; generalize c; unfold VSet.mem, VSet.singleton, DecVar.eq_A; simpl. intro l; induction l as [ | z l]. intros; contradiction. intros [x_eq_z | x_in_l]; [left; subst | right; apply IHl]; trivial. rewrite <- acc_inst_dom in y_in_dom; rewrite <- (VSet.LP.mem_permut_mem y c_in_dom) in y_in_dom. revert y_in_dom; generalize c; unfold VSet.mem, VSet.singleton, DecVar.eq_A; simpl. intro l; induction l as [ | z l]. intros; contradiction. intros [y_eq_z | y_in_l]; [left; subst | right; apply IHl]; trivial. revert Sol Idem; generalize (acc_inst c sigma). intros rho Sol_tau Idem. assert (Sol_rho := idem_sol _ Idem); destruct Sol_rho as [_ Sol_rho]. split. intros; contradiction. intro x; assert (Sol_taux := Sol_tau x); simpl; simpl in Sol_taux. assert (Sol_rhox := Sol_rho x); simpl; simpl in Sol_rhox. case_eq (find X.eq_bool x rho); [intro x_valr | trivial ]. intro x_rho; rewrite x_rho in Sol_taux; rewrite x_rho in Sol_rhox. case_eq (find X.eq_bool x tau); [intro x_valt | idtac ]; intro x_tau; rewrite x_tau in Sol_taux. rewrite Sol_taux. rewrite Sol_rhox at 1. rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros v _; rewrite subst_comp_is_subst_comp. symmetry; apply Sol_tau. rewrite Sol_taux. rewrite Sol_rhox at 1. rewrite <- subst_comp_is_subst_comp. rewrite <- subst_eq_vars. intros v _; rewrite subst_comp_is_subst_comp. symmetry; apply Sol_tau. 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)