proposition: Lemma acc_rwr_subst : forall R sigma, (forall x val, In (x,val) sigma -> Acc (one_step R) val) <-> Acc (rwr_subst R) sigma.
proof: Proof. intros R sigma; split. intro Acc_sigma; unfold rwr_subst. apply Acc_incl with (trans_clos (D.multiset_extension_step (fun yval' xval => rwr R (snd yval') (snd xval)))). intros t1 t2; trivial. apply acc_trans; apply D.dickson_strong. intros [x val] H. assert (Acc_rwr_val : Acc (rwr R) val). apply acc_trans; apply Acc_sigma with x; trivial. clear H; revert x; induction Acc_rwr_val as [val Acc_val IH]. intros x; apply Acc_intro; intros [y val'] H; simpl in H. apply IH; trivial. intros Acc_sigma; induction Acc_sigma as [sigma Acc_sigma IH]. intros y val yval_in_sigma; apply Acc_intro; intros val' H. destruct (In_split _ _ yval_in_sigma) as [sigma1 [sigma2 H']]; subst. apply (IH (sigma1 ++ (y,val') :: sigma2)) with y. unfold rwr_subst; apply t_step. refine (@D.rmv_case _ (sigma1 ++ (y, val') :: sigma2) (sigma1 ++ (y, val) :: sigma2) (sigma1 ++ sigma2) ((y,val') :: nil) (y,val) _ _ _). unfold D.LP.EDS.eq_A. intros b [H' | H']; [subst; simpl; apply t_step; trivial | contradiction]. simpl; apply D.LP.permut_sym; rewrite <- D.LP.permut_cons_inside; auto. unfold D.LP.EDS.eq_A; trivial. simpl; apply D.LP.permut_sym; rewrite <- D.LP.permut_cons_inside; auto. unfold D.LP.EDS.eq_A, D.LP.EDS.eq_A; trivial. apply in_or_app; right; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)