proposition: Lemma total_acc_inst_idem : forall c sigma, is_a_total_oc_ordering sigma c = true -> VSet.without_red c -> (forall x, In x c -> VSet.mem x (domain_of_subst sigma)) -> (forall x y, In x c -> In y c -> var_in_term x (apply_subst (acc_inst c sigma) (Var y)) = false).
proof: Proof. intro c; induction c as [ | v c]; intros sigma Hoc W H x y x_in_dom y_in_dom. contradiction. assert (v_case := total_acc_inst_head c v sigma W Hoc). assert (v_in_dom := H v (or_introl _ (eq_refl _))); rewrite var_in_domain_of_subst in v_in_dom. case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma; rewrite v_sigma in v_in_dom; [ clear v_in_dom | absurd (@None term = None); trivial]. simpl in Hoc; rewrite v_sigma in Hoc. case_eq (var_in_term v v_val); intro v_in_v_val; rewrite v_in_v_val in Hoc; [discriminate | simpl in Hoc]. case_eq (list_exists (fun z : variable => var_in_term z v_val) c); intro H'; rewrite H' in Hoc; [discriminate | simpl in Hoc]. simpl in y_in_dom; destruct y_in_dom as [y_eq_v | y_in_dom]. subst y; unfold DecVar.A in *; rewrite v_case. simpl; rewrite v_sigma; simpl in x_in_dom; destruct x_in_dom as [x_eq_v | x_in_dom]. subst x; trivial. apply (list_exists_is_complete_false _ _ H' _ x_in_dom). simpl in x_in_dom; destruct x_in_dom as [x_eq_v | x_in_dom]. subst x. apply (no_var_in_subst_inv v (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma)) with c y. intros z z_val F. assert (H'' := elim_var_in_subst sigma v v_val z). simpl in H''; rewrite F in H''. apply H''; trivial. assert (F' : find X.eq_bool z (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma) <> None). rewrite F; discriminate. rewrite <- var_in_domain_of_subst in F'. rewrite domain_of_subst_map_subst in F'; trivial. rewrite domain_of_subst_map_subst; apply H; right; trivial. assert (y_in_dom' : VSet.mem y (domain_of_subst (acc_inst (v :: c) sigma))). rewrite <- acc_inst_dom; apply H; right; trivial. rewrite var_in_domain_of_subst in y_in_dom'. simpl in y_in_dom'; rewrite v_sigma in y_in_dom'; simpl; rewrite v_sigma. destruct (find X.eq_bool y (acc_inst c (map_subst (fun (_ : variable) (t : term) => apply_subst ((v, v_val) :: nil) t) sigma))); [idtac | absurd (@None term = None)]; trivial. apply IHc; trivial. apply tail_total_ordering; trivial. simpl; rewrite v_sigma; trivial. apply (VSet.without_red_remove v nil c W). intros w w_in_c; rewrite domain_of_subst_map_subst; apply H; right; 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)