theory Scratch
imports
  Wellfounded
begin

text \<open>Bachmair and Dershowitz 1986, Lemma 2.\<close>

lemma qc_wf_relto_iff:
  assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
proof
  assume "wf ?S"
  moreover have "R \<subseteq> ?S" by auto
  ultimately show "wf R" using wf_subset by auto
next
  assume "wf R"
  show "wf ?S"
  proof (rule wfI_pf)
    fix A assume A: "A \<subseteq> ?S `` A"
    let ?X = "(R \<union> S)\<^sup>* `` A"
    have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
      proof -
        { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
          then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
          proof (induct y z)
            case rtrancl_refl then show ?case by auto
          next
            case (rtrancl_into_rtrancl a b c)
            then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
            then show ?case by simp
          qed }
        then show ?thesis by auto
      qed
    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
    also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" by (simp add: O_assoc[symmetric] relcomp_mono)
    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
    ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
    then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
    moreover have "A \<subseteq> ?X" by auto
    ultimately show "A = {}" by simp
  qed
qed