proposition: Lemma acc_psi_acc : forall t, Acc (one_step R) (psi t) -> Acc (one_step R) t.
proof: Proof. intros t Acc_psi_t; assert (Acc_t := acc_psi_acc_ooo _ Acc_psi_t t (eq_refl _)). generalize Acc_psi_t; clear Acc_psi_t; induction Acc_t as [t Acc_t IH]. intros Acc_psi_t; apply Acc_intro; intros s H. destruct (Psi_sim_one_step t s H) as [H1 | [H1 | [s' [H1 H2]]]]; unfold ooo, oo, psi_id in *. apply IH; unfold lex. generalize (eq_bool_ok (psi s) (psi t)); case (eq_bool (psi s) (psi t)); [intro psi_s_eq_psi_t | intro psi_s_diff_psi_t]; trivial. absurd (Acc (rwr R) (psi t)). apply cycle_not_acc; rewrite psi_s_eq_psi_t in H1; trivial. rewrite <- acc_one_step; trivial. rewrite acc_one_step; rewrite acc_one_step in Acc_psi_t. destruct Acc_psi_t as [Acc_psi_t]; apply Acc_psi_t; trivial. apply IH; unfold lex. generalize (eq_bool_ok (psi s) (psi t)); case (eq_bool (psi s) (psi t)); [intro psi_s_eq_psi_t | intro psi_s_diff_psi_t]; trivial. apply t_step; trivial. assert (P := Psi_sim_inner _ _ H1). inversion P as [p H2 H2'| ps pt H2]; clear P; trivial. absurd (psi s = psi t); trivial. assert (P := Psi_sim_inner _ _ H1). inversion P as [p H2 H2'| ps pt H2]; clear P. rewrite H2'; trivial. rewrite acc_one_step; rewrite acc_one_step in Acc_psi_t. destruct Acc_psi_t as [Acc_psi_t]; apply Acc_psi_t; trivial. assert (Acc_s' : Acc (rwr R) s'). rewrite <- acc_one_step. apply IH; unfold lex. generalize (eq_bool_ok (psi s') (psi t)); case (eq_bool (psi s') (psi t)); [intro psi_s_eq_psi_t | intro psi_s_diff_psi_t]; trivial. apply t_step; trivial. assert (P := Psi_sim_inner _ _ H2). inversion P as [p H3 H3'| ps' pt H3]; clear P; trivial. absurd (psi s' = psi t); trivial. assert (P := Psi_sim_inner _ _ H2). inversion P as [p H3 H3'| ps' pt H3]; clear P; trivial. rewrite H3'; trivial. rewrite acc_one_step; rewrite acc_one_step in Acc_psi_t. destruct Acc_psi_t as [Acc_psi_t]; apply Acc_psi_t; trivial. rewrite acc_one_step. destruct Acc_s' as [Acc_s']; apply Acc_s'; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)