proposition: Lemma total_acc_inst_sol : forall sigma c, VSet.without_red c -> is_a_total_oc_ordering sigma c = true -> VSet.LP.permut c (VSet.support (domain_of_subst sigma)) -> is_a_solution (mk_pb (acc_inst c sigma) nil) (acc_inst c sigma).
proof: Proof. intros sigma c W Hoc P. apply idem_sol. assert (H : forall z, In z c -> VSet.mem z (domain_of_subst sigma)). intros z z_in_c; apply (VSet.LP.mem_permut_mem z P). apply in_impl_mem; trivial. reflexivity. intros x y x_in_dom y_in_dom; apply total_acc_inst_idem; trivial. rewrite <- acc_inst_dom in x_in_dom. rewrite <- (VSet.LP.mem_permut_mem x P) in x_in_dom. revert x_in_dom; generalize c; intro l; induction l as [ | u l]; simpl. trivial. unfold DecVar.eq_A; intros [x_eq_u | x_in_l]; [left; subst; reflexivity | right; apply IHl; trivial]. rewrite <- acc_inst_dom in y_in_dom. rewrite <- (VSet.LP.mem_permut_mem y P) in y_in_dom. revert y_in_dom; generalize c; intro l; induction l as [ | u l]; simpl. trivial. unfold DecVar.eq_A; intros [y_eq_u | y_in_l]; [left; subst; reflexivity | right; apply IHl; trivial]. 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)