Theory Open_Terms

theory Open_Terms
  imports Rew_Seq
begin

(* Convenient abbreviations *)
abbreviation "srstep ℱ ℛ ≡ sig_step ℱ (rstep ℛ)"
abbreviation "srrstep ℱ ℛ ≡ sig_step ℱ (rrstep ℛ)"
abbreviation "gsrstep ℱ ℛ ≡ Restr (sig_step ℱ (rstep ℛ)) {t. ground t}"
abbreviation "srsteps_with_root_step ℱ ℛ ≡ relto (sig_step ℱ (rrstep ℛ)) (srstep ℱ ℛ)"
abbreviation "comp_rrstep_rel ℱ ℛ 𝒮 ≡ srsteps_with_root_step ℱ ℛ O (srstep ℱ 𝒮)⇧* ∪
  (srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ 𝒮"

  (* move me *)

lemma set_take_nth:
  assumes "x ∈ set (take n xs)"
  obtains i where "x = xs ! i" "i < n" "i < length xs" using assms
  by (smt dual_order.strict_trans in_set_conv_nth leI le_eq_less_or_eq length_take min.absorb2 nth_take take_all)

lemma set_drop_nth:
  assumes "x ∈ set (drop n xs)"
  obtains i where "n < length xs" "x = xs ! (i + n)" "i < length xs - n"
proof -
  assume a: "⋀i. n < length xs ⟹ x = xs ! (i + n) ⟹ i < length xs - n ⟹ thesis"
  from assms have nl: "n < length xs" using leI by fastforce
  from assms obtain i where "i < length (drop n xs)" "x = (drop n xs) ! i"
    by (auto dest!: in_set_idx)
  then show ?thesis using nl  nth_drop[of n xs i]
    by (intro a) (auto simp add: add.commute)
qed

lemma eqf_imp_subt_nth:
  "s =⇩f (C, ss) ⟹ i < length ss ⟹ s ⊵ ss ! i"
  by (simp add: eqf_imp_subt)

lemma Ex_list_of_length_P3:
  assumes "∀ i < n. ∃ x y z. P x y z i"
  shows "∃xs ys zs. length xs = length ys ∧ length ys = length zs ∧ length zs = n ∧ (∀ i < n. P (xs ! i) (ys ! i) (zs ! i)  i)"
proof -
  from assms Ex_list_of_length_P[of n "λ x i. P (fst x) (fst (snd x)) (snd (snd x)) i"]
  obtain xs where "length xs = n ∧ (∀i<n. P (fst (xs ! i)) (fst (snd (xs ! i))) (snd (snd (xs ! i))) i)"
    by auto
  then show ?thesis
    by (rule_tac x = "map fst xs" in exI, rule_tac x = "map (fst ∘ snd) xs" in exI, rule_tac x = "map (snd ∘ snd) xs" in exI) auto
qed

lemma converse_prod_swapI [intro]:
  "a ∈ r ⟹ prod.swap a ∈ r¯"
  by (cases a) auto

lemma dropWhile_eq_drop_P_nth:
  assumes "⋀i. i < n ⟹ P (xs ! i)"
    and "n < length xs" "¬ P (xs ! n)"
  shows "dropWhile P xs = drop n xs" using assms
  using dropWhile_eq_drop length_takeWhile_eq_P_nth by blast

lemma remove_prefix_append2 [simp]:
  "remove_prefix (xs @ zs) (xs @ ys) = remove_prefix zs ys"
  by (induct xs) auto

lemma less_eq_pos_left_max_false [dest]:
  "p ≤⇩p q ⟹ ∀y. q ≠ p @ y ⟹ False"
  by (auto simp: less_eq_pos_def)

lemma first_varposs_unique [simp]:
  assumes "x ∈ vars_term l" and "y ∈ vars_term l"
  shows "the (first_varposs_of x l) ≤⇩p the (first_varposs_of y l) @ z ⟷ x = y" (is "?Ls ⟷ ?Rs")
proof -
  have "?Rs ⟹ ?Ls" by auto
  moreover have "?Ls ⟹ ?Rs" using assms
    using first_varposs_of_neq_or_par[of x l y]
    using pos_less_eq_append_not_parallel
    by (auto simp: less_eq_pos_def)
  ultimately show ?thesis
    by auto
qed

lemma rrstep_rstep_mono: "rrstep ℛ ⊆ rstep ℛ"
  by (simp add: rrstep_imp_rstep subrelI)

lemma sig_step_mono:
  "ℱ ⊆ 𝒢 ⟹ sig_step ℱ ℛ ⊆ sig_step 𝒢 ℛ"
  using sig_stepI by fastforce

lemma sig_step_mono2:
  "ℛ ⊆ ℒ ⟹ sig_step ℱ ℛ ⊆ sig_step ℱ ℒ"
  using sig_stepI by fastforce

lemma sig_step_restep_conv:
  "sig_step ℱ (ℛ¯) = (sig_step ℱ ℛ)¯"
  by (auto simp: sig_step_def)

lemma sig_step_conversion:
  "(sig_step ℱ ℛ)⇧↔ = sig_step ℱ (ℛ⇧↔)"
  by (auto simp: sig_step_def)

lemma Restr_converse: "Restr (r¯) A = (Restr r A)¯"
  by auto

(* Removing constants not appearing in the signature preserves rules of a sequence *)
definition "funas_rel ℛ = (⋃ (l, r) ∈ ℛ. funas_term l ∪ funas_term r)"

fun term_to_sig where
  "term_to_sig ℱ v (Var x) = Var x"
| "term_to_sig ℱ v (Fun f ts) =
    (if (f, length ts) ∈ ℱ then Fun f (map (term_to_sig ℱ v) ts) else Var v)"

fun inv_const_ctxt where
  "inv_const_ctxt ℱ v Hole = Hole"
| "inv_const_ctxt ℱ v ((More f ss C ts)) 
              = (More f (map (term_to_sig ℱ v) ss) (inv_const_ctxt ℱ v C) (map (term_to_sig ℱ v) ts))"

fun inv_const_ctxt' where
  "inv_const_ctxt' ℱ v Hole = Var v"
| "inv_const_ctxt' ℱ v ((More f ss C ts)) 
              = (if (f, Suc (length ss + length ts)) ∈ ℱ then Fun f (map (term_to_sig ℱ v) ss @ inv_const_ctxt' ℱ v C # map (term_to_sig ℱ v) ts) else Var v)"

fun ctxt_well_def_hole_path where
  "ctxt_well_def_hole_path ℱ Hole ⟷ True"
| "ctxt_well_def_hole_path ℱ (More f ss C ts) ⟷ (f, Suc (length ss + length ts)) ∈ ℱ ∧ ctxt_well_def_hole_path ℱ C"


lemma fuans_term_term_to_sig [simp]: "funas_term (term_to_sig ℱ v t) ⊆ ℱ"
  by (induct t) auto

lemma term_to_sig_id [simp]:
  "funas_term t ⊆ ℱ ⟹ term_to_sig ℱ v t = t"
  by (induct t) (auto simp add: UN_subset_iff map_idI)

lemma term_to_sig_subst_sig [simp]:
  "funas_term t ⊆ ℱ ⟹ term_to_sig ℱ v (t ⋅ σ) = t ⋅ (λ x.  term_to_sig ℱ v (σ x))"
  by (induct t) auto

lemma funas_ctxt_ctxt_inv_const_ctxt_ind [simp]:
  "funas_ctxt C ⊆ ℱ ⟹ inv_const_ctxt ℱ v C = C"
  by (induct C) (auto simp add: UN_subset_iff intro!: nth_equalityI)

lemma term_to_sig_ctxt_apply [simp]:
  "ctxt_well_def_hole_path ℱ C ⟹ term_to_sig ℱ v C⟨s⟩ = (inv_const_ctxt ℱ v C)⟨term_to_sig ℱ v s⟩"
  by (induct C) auto

lemma term_to_sig_ctxt_apply' [simp]:
  "¬ ctxt_well_def_hole_path ℱ C ⟹ term_to_sig ℱ v C⟨s⟩ = inv_const_ctxt' ℱ v C"
  by (induct C) auto

lemma funas_ctxt_ctxt_well_def_hole_path:
  "funas_ctxt C ⊆ ℱ ⟹ ctxt_well_def_hole_path ℱ C"
  by (induct C) auto

lemma rstep_term_to_sig_right:
  assumes "(s, t) ∈ rstep ℛ" and "funas_rel ℛ ⊆ ℱ" and "funas_term s ⊆ ℱ"
  shows "(s, term_to_sig ℱ v t) ∈ rstep ℛ"
proof -
  from assms(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  from assms(2, 3) *(3) have "funas_ctxt C ⊆ ℱ" "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ"
    by (auto simp: *(1) funas_rel_def funas_term_subst subset_eq)
  then have "(term_to_sig ℱ v s, term_to_sig ℱ v t) ∈ rstep ℛ" using *(3)
    by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
  then show ?thesis using assms(3) by auto
qed

lemma rstep_term_to_sig_left:
  assumes "(s, t) ∈ rstep ℛ" and "funas_rel ℛ ⊆ ℱ" and "funas_term t ⊆ ℱ"
  shows "(term_to_sig ℱ v s, t) ∈ rstep ℛ"
proof -
  from assms(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  from assms(2, 3) *(3) have "funas_ctxt C ⊆ ℱ" "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ"
    by (auto simp: *(2) funas_rel_def funas_term_subst subset_eq)
  then have "(term_to_sig ℱ v s, term_to_sig ℱ v t) ∈ rstep ℛ" using *(3)
    by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
  then show ?thesis using assms(3) by auto
qed

lemma rstep_trancl_sig_step_right:
  assumes "(s, t) ∈ (rstep ℛ)⇧+" and "funas_rel ℛ ⊆ ℱ" and "funas_term s ⊆ ℱ"
  shows "(s, term_to_sig ℱ v t) ∈ (srstep ℱ ℛ)⇧+" using assms
proof (induct)
  case (base t)
  then show ?case using subsetD[OF fuans_term_term_to_sig, of _ ℱ v]
    by (auto simp: rstep_term_to_sig_right sig_step_def intro!: r_into_trancl)
next
  case (step t u)
  then have st: "(s, term_to_sig ℱ v t) ∈ (srstep ℱ ℛ)⇧+" by auto
  from step(2) obtain  C l r σ where
    *: "t = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  show ?case
  proof (cases "ctxt_well_def_hole_path ℱ C")
    case True
    from *(3) step(4) have "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" by (auto simp: funas_rel_def)
    then have "(term_to_sig ℱ v t, term_to_sig ℱ v u) ∈ rstep ℛ"
      using True step(2) *(3) unfolding *
      by auto
    then have "(term_to_sig ℱ v t, term_to_sig ℱ v u) ∈ srstep ℱ ℛ"
      by (auto simp:_ sig_step_def)
    then show ?thesis using st by auto
  next
    case False
    then have "term_to_sig ℱ v t = term_to_sig ℱ v u" unfolding * by auto
    then show ?thesis using st by auto
  qed
qed

lemma rstep_trancl_sig_step_left:
  assumes "(s, t) ∈ (rstep ℛ)⇧+" and "funas_rel ℛ ⊆ ℱ" and "funas_term t ⊆ ℱ"
  shows "(term_to_sig ℱ v s, t) ∈ (srstep ℱ ℛ)⇧+" using assms
proof (induct rule: converse_trancl_induct)
  case (base t)
  then show ?case using subsetD[OF fuans_term_term_to_sig, of _ ℱ v]
    by (auto simp: rstep_term_to_sig_left sig_step_def intro!: r_into_trancl)
next
  case (step s u)
  then have st: "(term_to_sig ℱ v u, t) ∈ (srstep ℱ ℛ)⇧+" by auto
  from step(1) obtain C l r σ where
    *: "s = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ" by auto
  show ?case
  proof (cases "ctxt_well_def_hole_path ℱ C")
    case True
    from *(3) step(4) have "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" by (auto simp: funas_rel_def)
    then have "(term_to_sig ℱ v s, term_to_sig ℱ v u) ∈ rstep ℛ"
      using True step(2) *(3) unfolding *
      by auto
    then have "(term_to_sig ℱ v s, term_to_sig ℱ v u) ∈ srstep ℱ ℛ"
      by (auto simp:_ sig_step_def)
    then show ?thesis using st by auto
  next
    case False
    then have "term_to_sig ℱ v s = term_to_sig ℱ v u" unfolding * by auto
    then show ?thesis using st by auto
  qed
qed

lemma sig_rrstepD:
  "(s, t) ∈ srrstep ℱ ℛ ⟹ (s, t) ∈ rrstep ℛ ∧ funas_tuple (s, t) ⊆ ℱ"
  by (auto simp: sig_step_def)

lemma sig_step_tranclD:
  "(s, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (s, t) ∈ (rstep ℛ)⇧+ ∧ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ"
  by (auto dest: subsetD[OF trancl_sig_subset])

lemma sig_step_rstep_trancl_conv:
  assumes "funas_rel ℛ ⊆ ℱ"
  shows "funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ ∧ (s, t) ∈ (rstep ℛ)⇧+ ⟷ (s, t) ∈ (srstep ℱ ℛ)⇧+"
  using assms rstep_trancl_sig_step_right[of s t ℛ ℱ]
  by (auto dest: sig_step_tranclD)

lemma sig_step_trancl_sig_trans:
  assumes "funas_rel ℛ ⊆ ℱ" "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "(s, t) ∈ (srstep 𝒢 ℛ)⇧+"
  shows "(s, t) ∈ (srstep ℱ ℛ)⇧+" using assms
  using sig_step_rstep_trancl_conv sig_step_tranclD by blast

lemma sig_step_rtranclD:
  "(s, t) ∈ (srstep ℱ ℛ)⇧* ⟹ s = t ∨ (s, t) ∈ (srstep ℱ ℛ)⇧+"
  by (auto simp: rtrancl_eq_or_trancl)

lemma sig_steps_subst_closed:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧*" "⋀ x. funas_term (σ x) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (srstep ℱ ℛ)⇧*" using assms(1)
proof (induct)
  case base then show ?case using assms(2)
    by (auto simp: sig_step_def funas_term_subst intro!: r_into_trancl)
next
  case (step t u)
  from step(2) have "(t ⋅ σ, u ⋅ σ) ∈ srstep ℱ ℛ" using assms(2)
    by (auto simp: sig_step_def funas_term_subst intro!: r_into_trancl)
  then show ?case using step(3) by auto
qed

(* replacing over variable positions by sub-term at given position returns original term *)

declare conj_cong [fundef_cong]
fun poss_of_term :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ pos set" where
  "poss_of_term u (Var x) = (if u = Var x then {[]} else {})" |
  "poss_of_term u (Fun f ss) = (if u = Fun f ss then {[]} else {i # p | i p. i < length ss ∧ p ∈ poss_of_term u (ss ! i)})"
declare conj_cong [fundef_cong del]

lemma poss_of_term_sound:
  "p ∈ poss_of_term u s ⟹ s |_ p = u"
  by (induct s arbitrary: p) (auto split!:if_splits)

lemma poss_of_term_in_poss:
  "poss_of_term u s ⊆ poss s"
  by (induct s) (auto, force)

lemma poss_of_term_possI [intro!]:
  "p ∈ poss s ⟹ s |_ p = u ⟹ p ∈ poss_of_term u s"
  by (induct s arbitrary: p)
    (auto, metis poss_Cons_poss subt_at.simps(2) subt_at_nepos_neq term.sel(4))

lemma poss_of_termE [elim!]:
  assumes "p ∈ poss_of_term u s"
    and "p ∈ poss s ⟹ s |_ p = u ⟹ P"
  shows "P" using assms(2) subsetD[OF poss_of_term_in_poss assms(1)] poss_of_term_sound[OF assms(1)]
  by blast

lemma possc_poss_of_term_conv:
  "hole_pos C ⊥ p ⟹ p ∈ poss_of_term u C⟨s⟩ ⟹ p ∈ poss_of_term u C⟨t⟩"
proof (induct C arbitrary: p)
  case (More f ss C ts)
  show ?case using More(1)[of "tl p"] More(2-)
    by (cases p) (auto simp: nth_append_Cons simp del: poss_of_term.simps, blast+)
qed (auto simp: parallel_pos)

locale rewrite_replace_const =
  fixes ℛ :: "('f, 'v) trs" and c :: 'f
  assumes linear: "∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r"
    and cons_nt_rewrite_rel: "(c, 0) ∉ funas_rel ℛ"
begin

lemma poss_of_term_ctxt_apply:
  "(c, 0) ∉ funas_term l ⟹ p ∈ poss_of_term (Fun c []) C⟨l ⋅ σ⟩ ⟹ hole_pos C ⊥ p ∨ hole_pos C ≤⇩p p"
proof (induct p arbitrary: C)
  case Nil then show ?case
    by (cases C) auto
next
  case (Cons i p) show ?case
  proof (cases C)
    case [simp]: (More f ss D ts)
    then show ?thesis using Cons(1)[of D] Cons(2-)
      by (cases "i = length ss") auto
  qed auto
qed

lemma poss_of_term_funas_term_ctxt:
  "(c, 0) ∉ funas_term C⟨r ⋅ σ⟩ ⟹ p ∈ poss_of_term (Fun c []) C⟨l ⋅ σ⟩ ⟹ hole_pos C ≤⇩p p"
proof (induct p arbitrary: C)
  case Nil then show ?case
    by (cases C) auto
next
  case (Cons i p)
  show ?case using Cons
  proof (cases C)
    case [simp]: (More f ss D ts)
    have "i ≠ length ss ⟹ (c, 0) ∈ funas_term C⟨r ⋅ σ⟩" using Cons(2-) possc_poss_of_term_conv[of C "i # p"]
      by (auto simp: nth_append_Cons simp del: poss_of_term.simps split!: if_splits)
        (simp add: funas_term_poss_conv)+
    then show ?thesis using Cons(1)[of D] Cons(2-)
      by (cases "i = length ss") auto
  qed auto
qed

lemma linear_term_subst_var:
  "linear_term l ⟹ (c, 0) ∉ funas_term l ⟹ q ∈ poss (l ⋅ σ) ⟹ l ⋅ σ |_ q = Fun c [] ⟹ ∃x∈vars_term l. the (first_varposs_of x l) ≤⇩p q"
proof (induct l arbitrary: q)
  case (Fun f ts)
  then show ?case
    by auto (metis Fun.prems(1) first_varposs_of.simps(2) less_eq_pos_simps(4) linear_term_fist_varposs_of_simp nth_mem)+
qed auto

abbreviation "step_subst_repl_upd C l σ u p ≡
   (let q = λ x. remove_prefix (hole_pos C @ the (first_varposs_of x l)) p in
   (λ x. if x ∈ vars_term l ∧ q x ≠ None then (σ x)[the (q x) ← u] else σ x))"

lemma step_subst_repl_upd:
  assumes "hole_pos C ≤⇩p p" and "p ∈ poss_of_term (Fun c []) C⟨l ⋅ σ⟩"
    and "linear_term l" "(c, 0) ∉ funas_term l"
  shows "C⟨l ⋅ σ⟩[p ← u] = C⟨l ⋅ step_subst_repl_upd C l σ u p⟩"
proof -
  from assms(1) obtain q where [simp]: "p = hole_pos C @ q" by (auto simp: less_eq_pos_def)
  from linear_term_subst_var[OF assms(3, 4), of q σ] obtain x where
    var: "x ∈ vars_term l" "the (first_varposs_of x l) ≤⇩p q"
    using assms(2) by auto
  then show ?thesis using assms(2-) first_varposs_of_neq_or_par[of x l]
    by (auto simp: first_varposs_of_varposs term_subst_eq_conv
        replace_term_under_subst[of _ "the (first_varposs_of x l)"])
qed

lemma replace_const_rewrite_step:
  fixes l r C σ u p
  defines "st ≡ Apply (l, r) C σ"
  defines "s ≡ apply_left st"
  defines "t ≡ apply_right st"
  defines "τ ≡ step_subst_repl_upd C l σ u p"
  assumes "st ∈ rewrite_step ℱ ℛ" "funas_term u ⊆ ℱ"
    and "(c, 0) ∉ funas_term C⟨r ⋅ σ⟩" and "p ∈ poss_of_term (Fun c []) C⟨l ⋅ σ⟩"
  shows "Apply (l, r) C τ ∈ rewrite_step ℱ ℛ ∧
    apply_left (Apply (l, r) C τ) = s[p ← u] ∧
    apply_right (Apply (l, r) C τ) = t"
proof -
  let ?t = "Apply (l, r) C (step_subst_repl_upd C l σ u p)"
  from assms(5) have fs: "funas_step (Apply (l, r) C σ) ⊆ ℱ"
    using funas_apply_step_funas_step funas_rewrite_step
    unfolding assms(1) by blast
  then have l: "funas_term (apply_left ?t) ⊆ ℱ" using assms(6) 
    by (auto simp: Let_def funas_step_def apply_left_def funas_term_subst dest!: subsetD[OF replace_term_funas])
  let ?q = "λ x. remove_prefix (hole_pos C @ the (first_varposs_of x l)) p"
  have "x ∈ vars_term l ⟹ ?q x ≠ None ⟹ (c, 0) ∈ funas_term (σ x)" for x
    using assms(5, 8) by (auto simp: apply_step_def funas_term_subst funas_term_poss_conv)
  from this assms(7) have "x ∈ vars_term l ⟹ x ∈ vars_term r ⟹ ?q x ≠ None ⟹ False" for x
    by (auto simp: funas_term_subst)
  then have r: "apply_right ?t = apply_right (Apply (l, r) C σ)"
    by (auto simp: apply_right_def intro!: term_subst_eq) blast
  from assms(5) have lf: "linear_term l" "(c, 0) ∉ funas_term l" using linear cons_nt_rewrite_rel
    by (auto simp: assms(1) funas_rel_def dest!: rewrite_step_rules)
  have "funas_term (apply_right ?t) ⊆ ℱ" unfolding r using fs
    by (auto simp: apply_right_def funas_apply_step_funas_step)
  then show ?thesis using r l rewrite_step_rules[OF assms(5)]
    using step_subst_repl_upd[OF poss_of_term_funas_term_ctxt[OF assms(7, 8)] assms(8) lf]
    by (auto simp: assms(1- 4) apply_left_def intro!: rewrite_stepI)
qed

lemma remove_const_lhs_seq_rule_pres:
  assumes "ss ∈ rewrite_steps ℱ ℛ" and "funas_term u ⊆ ℱ"
    and "start_t ss = s" and "end_t ss = t" and "(c, 0) ∉ funas_term t" and "p ∈ poss_of_term (Fun c []) s"
  shows "∃ ts ∈ rewrite_steps ℱ ℛ. start_t ts = s[p ← u] ∧ end_t ts = t ∧ map rules ts = map rules ss" using assms
proof (induct arbitrary: s p)
  case (base st)
  obtain C l r σ where st: "st = Apply (l, r) C σ" by (cases st) auto
  let ?τ = "step_subst_repl_upd C l σ u p"
  have step: "Apply (l, r) C ?τ ∈ rewrite_step ℱ ℛ ∧
    apply_left (Apply (l, r) C ?τ) = (apply_left st)[p ← u] ∧ 
    apply_right (Apply (l, r) C ?τ) = apply_right st"
    using base unfolding st
    by (intro replace_const_rewrite_step) (auto simp add: apply_left_def apply_right_def)
  then show ?case using base(1) conjunct2[OF step] base(3, 4)
    by (intro bexI[OF _ sequence.base[OF conjunct1[OF step]]]) (auto simp: st)
next
  case (trans_step st tu ys)
  obtain C l r σ where st: "st = Apply (l, r) C σ" by (cases st) auto
  have *: "s = C⟨l ⋅ σ⟩" "apply_right st = C⟨r ⋅ σ⟩" using trans_step(6) unfolding st
    by (simp_all add: apply_right_def apply_left_def)
  have [simp]: "start_t (tu # ys) = apply_right st" using trans_step(4) by (auto simp: stepsP_def')
  from trans_step(1) have rules: "(l, r) ∈ ℛ" and lf: "linear_term l" "(c, 0) ∉ funas_term l"
    and lr: "linear_term r" "(c, 0) ∉ funas_term r" using linear cons_nt_rewrite_rel unfolding st
    by (auto simp: funas_rel_def dest!: rewrite_step_rules)
  have IH: "q ∈ poss_of_term (Fun c []) C⟨r ⋅ σ⟩ ⟹
      ∃ ts ∈ rewrite_steps ℱ ℛ. start_t ts = C⟨r ⋅ σ⟩[q ← u] ∧ end_t ts = t ∧ map rules ts = map rules (tu # ys)" for q
    using trans_step(1, 4-) unfolding st *
    by (intro trans_step(3)) (auto simp: stepsP_def' apply_right_def)
  let ?τ = "step_subst_repl_upd C l σ u p"
  have step: "Apply (l, r) C ?τ ∈ rewrite_step ℱ ℛ"
    using trans_step(1, 5) funas_rewrite_step[OF trans_step(1)]
    by (intro rewrite_stepI) (auto simp: apply_left_def apply_right_def st funas_term_subst
        dest!: subsetD[OF replace_term_funas] rewrite_step_rules)
  consider (p) "hole_pos C ⊥ p" | (l) "hole_pos C ≤⇩p p" using trans_step(1, 9)
    using poss_of_term_ctxt_apply[OF lf(2), of p C σ]
    by (auto simp: st * )
  then show ?case
  proof cases
    case p
    have step: "Apply (l, r) (replace_term_at_ctxt C p u) σ ∈ rewrite_step ℱ ℛ"
      using funas_rewrite_step[OF trans_step(1)] trans_step(1) trans_step(5) unfolding st
      by (intro rewrite_stepI) (auto simp: apply_step_def dest: subsetD[OF replace_term_at_ctxt_funas] rewrite_step_rules)
    have "p ∈ poss_of_term (Fun c []) C⟨r ⋅ σ⟩" using possc_poss_of_term_conv[OF p] trans_step(4, 9)
      by (auto simp: apply_step_def st *)
    from IH[OF this] obtain ts where
      seq: "ts ∈ rewrite_steps ℱ ℛ" "start_t ts = (apply_right st)[p ← u]" "end_t ts = t" "map rules ts = map rules (tu # ys)"
      unfolding * by blast
    have **: "[Apply (l, r) (replace_term_at_ctxt C p u) σ] @ ts ∈ rewrite_steps ℱ ℛ"
      by (intro sequence_concat_onP[OF base[OF step] seq(1)]) (simp add: p apply_right_def st stepsP_def seq(2) *)
    show ?thesis using seq(2-)
      by (intro bexI[OF _ **]) (auto simp add: st * apply_left_def apply_right_def p)
  next
    case l
    then obtain q where [simp]: "p = hole_pos C @ q" by auto
    from linear_term_subst_var[OF lf, of q] obtain x where
      var: "x ∈ vars_term l" "the (first_varposs_of x l) ≤⇩p q"
      using trans_step(9) by (force simp: *)
    have lhs: "s[p ← u] = C⟨l ⋅ ?τ⟩" using var lf trans_step(9) unfolding *
      by (intro step_subst_repl_upd) auto
    show ?thesis
    proof (cases "x ∈ vars_term r")
      case True
      let ?q = "hole_pos C @ the (first_varposs_of x r) @ the (remove_prefix (the (first_varposs_of x l)) q)"
      from True have ap [simp]: "apply_right (Apply (l, r) C ?τ) = (apply_right st)[?q ← u]" using var lr l
        by (auto simp: apply_right_def st term_subst_eq_conv
            replace_term_under_subst[of _ "the (first_varposs_of x r)"] first_varposs_of_varposs)
      have "?q ∈ poss_of_term (Fun c []) C⟨r ⋅ σ⟩" using True l trans_step(9) lr var
        by (auto simp: * first_varposs_of_poss)
      from IH[OF this] obtain ts where seq: "ts ∈ rewrite_steps ℱ ℛ" "start_t ts = C⟨r ⋅ σ⟩[?q ← u]"
        "end_t ts = t" "map rules ts = map rules (tu # ys)" by blast
      have **: "[Apply (l, r) C ?τ] @ ts ∈ rewrite_steps ℱ ℛ" using seq(2) ap
        by (intro sequence_concat_onP[OF base[OF step] seq(1)]) (auto simp add: stepsP_def st apply_right_def)
      then show ?thesis using seq lhs
        by (intro bexI[OF _ **]) (auto simp: apply_left_def st)
    next
      case False
      then have ap [simp]: "apply_right (Apply (l, r) C ?τ) = apply_right st" using var
        by (auto simp: apply_right_def st term_subst_eq_conv)
      have **: "[Apply (l, r) C ?τ] @ tu # ys ∈ rewrite_steps ℱ ℛ" using trans_step(4) ap
        by (intro sequence_concat_onP[OF base[OF step] trans_step(2)])(simp add: stepsP_def')
      show ?thesis using trans_step(7) lhs
        by (intro bexI[OF _ **]) (auto simp: st * apply_left_def simp del: replace_term_below_hole)
    qed
  qed
qed

abbreviation "σ⇩c ≡ (λ x. Fun c [] :: ('f, 'v) term)"
lemma remove_const_subst_lhs_seq_rule_pres:
  assumes "ss ∈ rewrite_steps ℱ ℛ" and "start_t ss = s ⋅ σ⇩c" and "end_t ss = t" and "(c, 0) ∉ funas_term t"
  shows "∃ ts ∈ rewrite_steps ℱ ℛ. start_t ts = s ∧ end_t ts = t ∧ map rules ts = map rules ss"
  using assms
proof (induct "card (varposs s)" arbitrary: s)
  case (Suc n)
  obtain p ps where vl: "varposs s = insert p ps" "p ∉ ps" using Suc(2)
    by (metis card_le_Suc_iff dual_order.refl)
  let ?s = "s[p ← Fun c []]" have vp: "p ∈ varposs s" using vl by auto
  then have [simp]: "?s ⋅ σ⇩c = s ⋅ σ⇩c" by (induct s arbitrary: p) (auto simp: nth_list_update map_update intro!: nth_equalityI)
  have "varposs ?s = ps" using vl varposs_ground_replace[of p s "Fun c []"] by auto
  then have "n = card (varposs ?s)" using vl Suc(2) by (auto simp: card_insert_if finite_varposs)
  from Suc(1)[OF this] obtain ts where seq: "ts ∈ rewrite_steps ℱ ℛ" "start_t ts = s[p ← Fun c []]"
    "end_t ts = t" "map rules ts = map rules ss" using Suc(3-) vl
    by auto
  moreover have "funas_term (s |_ p) ⊆ ℱ" "p ∈ poss_of_term (Fun c []) s[p ← Fun c []]" using vp
    by (auto simp: varposs_iff replace_term_at_poss)
  ultimately show ?case using remove_const_lhs_seq_rule_pres[OF seq(1) _ seq(2, 3), of "s |_ p" p] vp Suc(6)
    by auto
qed (auto simp: ground_subst_apply card_eq_0_iff finite_varposs varposs_empty_gound)

end

abbreviation const_subt :: "'f ⇒ 'v ⇒ ('f, 'v) Term.term" where
  "const_subt c ≡ (λ x. Fun c [])"

lemma remove_const_substs_rule_pres:
  assumes "rewrite_replace_const ℛ c" "(d, 0) ∉ funas_rel ℛ"
    and "ss ∈ rewrite_steps ℱ ℛ" and "start_t ss = s ⋅ const_subt c" and "end_t ss = t ⋅ const_subt d"
    and funas: "c ≠ d" "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s"
  shows "∃ ts ∈ rewrite_steps ℱ ℛ. start_t ts = s ∧ end_t ts = t ∧ map rules ts = map rules ss"
proof -
  from funas(1, 2) have "(c, 0) ∉ funas_term (t ⋅ const_subt d)" by (auto simp: funas_term_subst)
  from this rewrite_replace_const.remove_const_subst_lhs_seq_rule_pres[OF assms(1, 3, 4, 5)]
  obtain ts where lhs: "ts ∈ rewrite_steps ℱ ℛ" "start_t ts = s" "end_t ts = t ⋅ const_subt d" "map rules ts = map rules ss"
    by auto
  have "rewrite_replace_const (ℛ¯) d" using assms(1, 2) by (auto simp: rewrite_replace_const_def funas_rel_def)
  from rewrite_replace_const.remove_const_subst_lhs_seq_rule_pres[OF this rewrite_steps_to_inv_steps[OF lhs(1)], of t s]
  obtain us where rhs: "us ∈ rewrite_steps_inv ℱ ℛ" "start_t us = t" "end_t us = s" "map rules us = map rules (rev (map rev_step ts))"
    using lhs(1- 3) funas(3) seq_not_NilD by force
  from rhs(4) lhs(4) have "map rules (rev (map rev_step us)) = map rules ss"
    by (auto simp: map_rules_rev_step_commute simp flip: rev_map map_map) auto
  then show ?thesis using rhs
    by (intro bexI[OF _ rewrite_steps_inv_to_steps[OF rhs(1)]]) (auto simp: rewrite_steps_inv_to_steps seq_not_NilD)
qed

abbreviation "linear_sys ℛ ≡ (∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r)"

lemma const_subt_eq_ground_eq:
  assumes "s ⋅ const_subt c = t ⋅ const_subt d" "c ≠ d"
    and "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s"
  shows "s = t" using assms
proof (induct s arbitrary: t)
  case (Var x) then show ?case by (cases t) auto
next
  case (Fun f ts)
  from Fun(2-) obtain g us where [simp]: "t = Fun g us" by (cases t) auto
  have [simp]: "g = f" and l: "length ts = length us" using Fun(2)
    by (auto intro: map_eq_imp_length_eq)
  have "i < length ts ⟹ ts ! i = us ! i" for i
    using Fun(1)[OF nth_mem, of i "us ! i" for i] Fun(2-) l
    by (auto simp: map_eq_conv')
  then show ?case using l
    by (auto intro: nth_equalityI)
qed

lemma remove_const_substs:
  assumes "linear_sys ℛ"
    and "(c, 0) ∉ funas_rel ℛ" "(d, 0) ∉ funas_rel ℛ"
    and "c ≠ d" "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s"
    and "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ ℛ)⇧*"
  shows "(s, t) ∈ (srstep ℱ ℛ)⇧*"
proof (cases "s ⋅ const_subt c = t ⋅ const_subt d")
  case True
  from const_subt_eq_ground_eq[OF this] assms(4 - 6) show ?thesis by auto
next
  case False
  then have step: "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ ℛ)⇧+" using assms(7)
    by (auto simp: rtrancl_eq_or_trancl)
  then show ?thesis using assms
    using remove_const_substs_rule_pres
      [unfolded rewrite_replace_const_def, where ?s = s and ?c = c and ?d = d
        and ?t = t and ?ℱ = ℱ and ?ℛ = ℛ]
    by (auto simp: funas_term_subst split!: if_splits)
      (metis Pair_inject rewrite_steps_impl_transcl_sig_rstep sig_rsteps_to_rewrite_steps trancl_into_rtrancl)
qed


lemma remove_const_substs_relcomp:
  assumes sys: "linear_sys ℛ" "linear_sys 𝒮"
    and fr: "(c, 0) ∉ funas_rel ℛ" "(d, 0) ∉ funas_rel ℛ"
    and fs:"(c, 0) ∉ funas_rel 𝒮" "(d, 0) ∉ funas_rel 𝒮"
    and diff: "c ≠ d" and funas: "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s"
    and seq: "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
  shows "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
proof (cases  "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ ℛ)⇧+ O (srstep ℱ 𝒮)⇧+")
  case True
  then obtain u where sp: "(s ⋅ const_subt c, u) ∈ (srstep ℱ ℛ)⇧+" "(u, t ⋅ const_subt d) ∈ (srstep ℱ 𝒮)⇧+"
    by auto
  from sig_rsteps_to_rewrite_steps[OF sp(1)] sig_rsteps_to_rewrite_steps[OF sp(2)] obtain rs ss
    where rs: "rs ∈ rewrite_steps ℱ ℛ" "(s ⋅ const_subt c, u) = steps_rel rs"
      and ss: "ss ∈ rewrite_steps ℱ 𝒮" "(u, t ⋅ const_subt d) = steps_rel ss"
    by blast+
  then have comp: "rs @ ss ∈ rewrite_steps ℱ (ℛ ∪ 𝒮)"
    by (intro compose_sequences_union) auto
  have rep: "rewrite_replace_const (ℛ ∪ 𝒮) c" using sys fr(1) fs(1)
    by (auto simp: rewrite_replace_const_def funas_rel_def)
  have "(d, 0) ∉ funas_rel (ℛ ∪ 𝒮)" using fr(2) fs(2) by (auto simp: funas_rel_def)
  from remove_const_substs_rule_pres[OF rep this comp _ _ diff funas] obtain
    ts where ts: "ts ∈ rewrite_steps ℱ (ℛ ∪ 𝒮)"
    "start_t ts = s ∧ end_t ts = t ∧ map rules ts = map rules (rs @ ss)"
    using rs ss by (cases rs; cases ss) auto
  from rs ss ts have ne: "rs ≠ []" "ss ≠ []" "ts ≠ []" and l: "length ts = length rs + length ss"
    by (auto simp flip: map_append dest!: map_eq_imp_length_eq)
  moreover have "rules ` set (take (length rs) ts) ⊆ ℛ" "rules ` set (drop (length rs) ts) ⊆ 𝒮"
    using conjunct2[OF conjunct2[OF ts(2)]] rs ss l
    by (auto 0 0 simp: map_nth_conv[of rules ts rules] nth_append rewrite_steps_rulesD
        simp del: map_append elim!: set_take_nth set_drop_nth)
  ultimately have seq: "take (length rs) ts ∈ rewrite_steps ℱ ℛ" "drop (length rs) ts ∈ rewrite_steps ℱ 𝒮"
    using rs ss ts
    using compose_sequences_split[of "take (length rs) ts" "drop (length rs) ts" ℱ ℛ 𝒮]
    by auto
  then have steps: "steps_rel (take (length rs) ts) ∈ (srstep ℱ ℛ)⇧+" "steps_rel (drop (length rs) ts) ∈ (srstep ℱ 𝒮)⇧+"
    by (auto dest!: rewrite_steps_impl_transcl_sig_rstep)
  moreover have "end_t (take (length rs) ts) = start_t (drop (length rs) ts)" using seq_property[OF ts(1)] ne l
    using last_conv_nth[OF seq_not_NilD[OF seq(1)]] hd_conv_nth[OF seq_not_NilD[OF seq(2)]]
    by (auto simp: min_def stepsP_def)
  ultimately show ?thesis using ts(2) l ne
    by auto
next
  case False
  from False seq have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ ℛ)⇧* ∨
    (s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℱ 𝒮)⇧*"
    by (auto simp: rtrancl_eq_or_trancl)
  then show ?thesis using remove_const_substs[OF sys(1) fr diff funas, of ℱ]
    using remove_const_substs[OF sys(2) fs diff funas, of ℱ]
    by auto
qed

― ‹Reducing commutation search space to sequences involving a root step›

lemma nsrsteps_with_root_step_step_on_args:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧+" "(s, t) ∉ srsteps_with_root_step ℱ ℛ"
  shows "∃ f ss ts. s = Fun f ss ∧ t = Fun f ts ∧ length ss = length ts ∧
    (∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*)" using assms
proof (induct)
  case (base t)
  obtain C l r σ where [simp]: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" and r: "(l, r) ∈ ℛ"
    using base(1) unfolding sig_step_def
    by blast
  then have funas: "funas_ctxt C ⊆ ℱ" "funas_term (l ⋅ σ) ⊆ ℱ" "funas_term (r ⋅ σ) ⊆ ℱ"
    using base(1) by (auto simp: sig_step_def)
  from funas(2-) r have "(l ⋅ σ, r ⋅ σ) ∈ sig_step ℱ (rrstep ℛ)"
    by (auto simp: sig_step_def rrstep_def')
  then have "C = Hole ⟹ False" using base(2) r
    by auto
  then obtain f ss D ts where [simp]: "C = More f ss D ts" by (cases C) auto
  have "(D⟨l ⋅ σ⟩, D⟨r ⋅ σ⟩) ∈ (srstep ℱ ℛ)" using base(1) r funas
    by (auto simp: sig_step_def)
  then show ?case using funas by (auto simp: nth_append_Cons)
next
  case (step t u) show ?case
  proof (cases "(s, t) ∈ srsteps_with_root_step ℱ ℛ ∨ (t, u) ∈ sig_step ℱ (rrstep ℛ)")
    case True then show ?thesis using step(1, 2, 4)
      by (auto simp add: relcomp3_I rtrancl.rtrancl_into_rtrancl)
  next
    case False
    obtain C l r σ where *[simp]: "t = C⟨l ⋅ σ⟩" "u = C⟨r ⋅ σ⟩" and r: "(l, r) ∈ ℛ"
      using step(2) unfolding sig_step_def by blast
    then have funas: "funas_ctxt C ⊆ ℱ" "funas_term (l ⋅ σ) ⊆ ℱ" "funas_term (r ⋅ σ) ⊆ ℱ"
      using step(2) by (auto simp: sig_step_def)
    from False have "C ≠ Hole" using funas r by (force simp: sig_step_def rrstep_def')
    then obtain f ss D ts where c[simp]: "C = More f ss D ts" by (cases C) auto
    from step(3, 1) False obtain g sss tss where
      **[simp]: "s = Fun g sss" "t = Fun g tss" and l: "length sss = length tss" and
      inv: "∀ i < length tss. (sss ! i, tss ! i) ∈ (srstep ℱ ℛ)⇧*"
      by auto
    have [simp]: "g = f" and lc: "Suc (length ss + length ts) = length sss"
      using l *(1) unfolding c using **(2) by auto
    then have "∀ i < Suc (length ss + length ts). ((ss @ D⟨l ⋅ σ⟩ # ts) ! i, (ss @ D⟨r ⋅ σ⟩ # ts) ! i) ∈ (srstep ℱ ℛ)⇧*"
      using * funas r by (auto simp: nth_append_Cons sig_step_def r_into_rtrancl rstep.intros)
    then have "i < length tss ⟹ (sss ! i, (ss @ D⟨r ⋅ σ⟩ # ts) ! i) ∈ (srstep ℱ ℛ)⇧*" for i
      using inv * l lc funas **
      by (auto simp: nth_append_Cons simp del: ** * split!: if_splits)
    then show ?thesis using inv l lc * unfolding c
      by auto
  qed
qed

lemma sig_step_rstep_split:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧*"
  shows "∃ D ss ts. num_holes D = length ss ∧ length ss = length ts ∧
    (∀ i < length ts. ss ! i = ts ! i ∨ (ss ! i, ts ! i) ∈ srsteps_with_root_step ℱ ℛ) ∧
    fill_holes D ss = s ∧ fill_holes D ts = t" using assms
proof (induct s arbitrary: t)
  case [simp]: (Var x) show ?case
  proof (cases "Var x = t")
    case True then show ?thesis
      by (rule_tac x = MHole in exI, rule_tac x = "[Var x]" in exI, rule_tac x = "[t]" in exI) auto
  next
    case False
    then obtain u where st: "(Var x, u) ∈ (srstep ℱ ℛ)" "(u, t) ∈ (srstep ℱ ℛ)⇧*"
      using Var unfolding rtrancl_eq_or_trancl by (metis converse_tranclE) 
    have "C⟨s⟩ = Var x ⟹ C = Hole" for C s by (cases C) auto
    then have "(Var x, u) ∈ (sig_step ℱ (rrstep ℛ))" using st
      by (force simp: sig_step_def rrstep_def' dest!: rstep_imp_C_s_r)
    then have "(Var x, t) ∈ srsteps_with_root_step ℱ ℛ" using st(2) by auto
    then show ?thesis
      by (rule_tac x = MHole in exI, rule_tac x = "[Var x]" in exI, rule_tac x = "[t]" in exI) auto
  qed
next
  case (Fun f ss) then show ?case
  proof (cases "Fun f ss = t")
    case True then show ?thesis
      by (rule_tac x = MHole in exI, rule_tac x = "[Fun f ss]" in exI, rule_tac x = "[t]" in exI) auto
  next
    case False note neq = this then show ?thesis
    proof (cases "(Fun f ss, t) ∈ srsteps_with_root_step ℱ ℛ")
      case True then show ?thesis
        by (rule_tac x = MHole in exI, rule_tac x = "[Fun f ss]" in exI, rule_tac x = "[t]" in exI) auto
    next
      case False
      from nsrsteps_with_root_step_step_on_args[OF _ False] obtain ts where
        *: "t = Fun f ts" and inv: "length ss = length ts" "∀i<length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*"
        using neq Fun(2) by (auto simp: rtrancl_eq_or_trancl)
      let ?P = "λ D sss tss i. num_holes D = length sss ∧ length sss = length tss ∧
         (∀i<length tss. sss ! i = tss ! i ∨ (sss ! i, tss ! i) ∈ (srstep ℱ ℛ)⇧* O sig_step ℱ (rrstep ℛ) O (srstep ℱ ℛ)⇧*) ∧
         fill_holes D sss = ss ! i ∧ fill_holes D tss = ts ! i"
      from Fun(1)[OF nth_mem, of i "ts ! i" for i] inv have "∀i < length ts. ∃x y z. ?P x y z i"
        by auto
      from Ex_list_of_length_P3[OF this] inv obtain Ds sss tss where
        size: "length Ds = length sss" "length sss = length tss" "length tss = length ts" and
        inn_sizes: "∀ i < length ts. num_holes (Ds ! i) = length (sss ! i)" "∀ i < length ts. length (sss ! i) = length (tss ! i)" and
        inv' : "∀ i < length tss. (∀ j < length (tss ! i). sss ! i ! j = tss ! i ! j ∨ (sss ! i ! j, tss  ! i ! j) ∈ (srstep ℱ ℛ)⇧* O sig_step ℱ (rrstep ℛ) O (srstep ℱ ℛ)⇧*)" and
        shap: "∀ i < length ts. fill_holes (Ds ! i) (sss ! i) = (ss ! i) ∧ fill_holes (Ds ! i) (tss ! i) = (ts ! i)"
        using inv(1) by auto
      from size(2-) inn_sizes(2-) inv' have "∀ i < length (concat tss). concat sss ! i = concat tss ! i ∨ (concat sss ! i, concat tss ! i) ∈ (srstep ℱ ℛ)⇧* O sig_step ℱ (rrstep ℛ) O (srstep ℱ ℛ)⇧*"
        by (intro concat_all_nth) auto
      moreover have "Fun f ss =⇩f (MFun f Ds, concat sss)" "Fun f ts =⇩f (MFun f Ds, concat tss)"
        using size inv(1) inn_sizes shap
        by (auto simp: inv intro!: eqf_MFunI)
      ultimately show ?thesis
        by (rule_tac x = "MFun f Ds" in exI, rule_tac x = "concat sss" in exI, rule_tac x = "concat tss" in exI)
          (auto simp add: eqf_Fun_MFun * simp del: fill_holes.simps dest: eqfE)
    qed
  qed
qed

lemma sig_step_rstep_comp_split:
  assumes "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
  shows "∃ D ss ts. num_holes D = length ss ∧ length ss = length ts ∧
    (∀ i < length ts. ss ! i = ts ! i ∨ (ss ! i, ts ! i) ∈ comp_rrstep_rel ℱ ℛ 𝒮) ∧ fill_holes D ss = s ∧ fill_holes D ts = t"
  using assms
proof (induct s arbitrary: t)
  case [simp]: (Var x) show ?case
  proof (cases "Var x = t")
    case True then show ?thesis
      by (rule_tac x = MHole in exI, rule_tac x = "[Var x]" in exI, rule_tac x = "[t]" in exI) auto
  next
    case False
    then obtain u where st: "Var x ≠ u ⟶ (Var x, u) ∈ (srstep ℱ ℛ)⇧+ ∧ (u, t) ∈ (sig_step ℱ (rstep 𝒮))⇧*"
      "Var x = u ⟶ (Var x, u) ∈ (srstep ℱ ℛ)⇧* ∧ (u, t) ∈ (sig_step ℱ (rstep 𝒮))⇧+"
      using Var.prems by (metis relcomp.cases rtranclD)
    then have "(Var x, u) ∈ (srstep ℱ ℛ)⇧+ ⟹ (Var x, u) ∈ srsteps_with_root_step ℱ ℛ"
      using st(2) nsrsteps_with_root_step_step_on_args by blast
    moreover have "(Var x, t) ∈ (sig_step ℱ (rstep 𝒮))⇧+ ⟹ (Var x, t) ∈ srsteps_with_root_step ℱ 𝒮"
      using st(2) nsrsteps_with_root_step_step_on_args by blast
    ultimately show ?thesis using st
      by (rule_tac x = MHole in exI, rule_tac x = "[Var x]" in exI, rule_tac x = "[t]" in exI) auto
  qed
next
  case (Fun f ss)
  obtain u where u: "(Fun f ss, u) ∈ (srstep ℱ ℛ)⇧*" "(u, t) ∈(sig_step ℱ (rstep 𝒮))⇧*" using Fun(2) by auto
  have D1: "(s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ 𝒮" for s t by auto
  have D2: "(s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ (s, t) ∈ srsteps_with_root_step ℱ ℛ O (sig_step ℱ (rstep 𝒮))⇧*" for s t by auto
  show ?case
  proof (cases "Fun f ss = u")
    case True then show ?thesis using u sig_step_rstep_split[of u t ℱ 𝒮]
      by auto (metis D1)
  next
    case False note neq_s = this then show ?thesis
    proof (cases "u = t")
      case True then show ?thesis using u sig_step_rstep_split[of "Fun f ss" u ℱ ℛ]
        by auto (metis D2) 
    next
      case False
      then have neq: "Fun f ss ≠ u" "u ≠ t" using neq_s by auto
      then show ?thesis
      proof (cases "(Fun f ss, u) ∈ srsteps_with_root_step ℱ ℛ")
        case True then show ?thesis using u
          by (rule_tac x = MHole in exI, rule_tac x = "[Fun f ss]" in exI, rule_tac x = "[t]" in exI) auto
      next
        case False note nsig_left = this show ?thesis
        proof (cases "(u, t) ∈ srsteps_with_root_step ℱ 𝒮")
          case True then show ?thesis using u
            by (rule_tac x = MHole in exI, rule_tac x = "[Fun f ss]" in exI, rule_tac x = "[t]" in exI)
              (auto simp add: relcomp.relcompI)
        next
          case False
          from nsrsteps_with_root_step_step_on_args[OF _ nsig_left]
          obtain us where *: "u = Fun f us ∧ length ss = length us ∧ (∀i<length us. (ss ! i, us ! i) ∈ (srstep ℱ ℛ)⇧*)"
            using neq u by (auto simp: rtrancl_eq_or_trancl)
          from nsrsteps_with_root_step_step_on_args[OF _ False] *
          obtain ts where [simp]: "t = Fun f ts" and **: "length us = length ts ∧ (∀i<length ts. (us ! i, ts ! i) ∈ (sig_step ℱ (rstep 𝒮))⇧*)"
            using neq u by (auto simp: rtrancl_eq_or_trancl)
          have inv: "length ss = length ts" "∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧* O (sig_step ℱ (rstep 𝒮))⇧*"
            using * ** by auto
          thm Fun
          let ?P = "λ D sss tss i. num_holes D = length sss ∧ length sss = length tss ∧
             (∀i<length tss. sss ! i = tss ! i ∨ (sss ! i, tss ! i) ∈ comp_rrstep_rel ℱ ℛ 𝒮) ∧
             fill_holes D sss = ss ! i ∧ fill_holes D tss = ts ! i"
          from Fun(1)[OF nth_mem, of i "ts ! i" for i] inv have "∀i < length ts. ∃x y z. ?P x y z i"
            by auto
          from Ex_list_of_length_P3[OF this] inv obtain Ds sss tss where
            size: "length Ds = length sss" "length sss = length tss" "length tss = length ts" and
            inn_sizes: "∀ i < length ts. num_holes (Ds ! i) = length (sss ! i)" "∀ i < length ts. length (sss ! i) = length (tss ! i)" and
            inv' : "∀ i < length tss. (∀ j < length (tss ! i). sss ! i ! j = tss ! i ! j ∨ (sss ! i ! j, tss  ! i ! j) ∈ comp_rrstep_rel ℱ ℛ 𝒮)" and
            shap: "∀ i < length ts. fill_holes (Ds ! i) (sss ! i) = (ss ! i) ∧ fill_holes (Ds ! i) (tss ! i) = (ts ! i)"
            using inv(1) by auto
          from size(2-) inn_sizes(2-) inv' have "∀ i < length (concat tss). concat sss ! i = concat tss ! i ∨ (concat sss ! i, concat tss ! i) ∈ comp_rrstep_rel ℱ ℛ 𝒮"
            by (intro concat_all_nth) auto
          moreover have "Fun f ss =⇩f (MFun f Ds, concat sss)" "Fun f ts =⇩f (MFun f Ds, concat tss)"
            using size inv(1) inn_sizes shap
            by (auto simp: inv intro!: eqf_MFunI)
          ultimately show ?thesis
            by (rule_tac x = "MFun f Ds" in exI, rule_tac x = "concat sss" in exI, rule_tac x = "concat tss" in exI)
              (auto simp add: eqf_Fun_MFun * simp del: fill_holes.simps dest: eqfE)
        qed
      qed
    qed
  qed
qed


lemma rrstep_converse: "rrstep (ℛ¯) = (rrstep ℛ)¯"
  by (auto simp: rrstep_def')

lemma partition_by_replicate_id:
  "i < n ⟹ length ss = n ⟹ partition_by ss (replicate n (Suc 0) @ ts) ! i = [ss ! i]"
proof (induct n arbitrary: i ss)
  case (Suc n) then show ?case
    by (auto simp: nth_Cons' take_Suc_conv_app_nth)
qed auto

lemma partition_by_replicate_end:
  "i = n ⟹ length ss = n ⟹ partition_by ss (replicate n (Suc 0) @ [0]) ! i = []"
proof (induct n arbitrary: i ss)
  case (Suc n) then show ?case
    by (auto simp: nth_Cons' take_Suc_conv_app_nth)
qed auto

lemma srstep_mctxt_cl:
  assumes "num_holes D = length ss" "length ss = length ts" 
    and funas: "funas_rel ℛ ⊆ ℱ" "funas_mctxt D ⊆ ℱ"
    "∀ i < length ts. funas_term (ss ! i) ⊆ ℱ" "∀ i < length ts. funas_term (ts ! i) ⊆ ℱ"
    and "∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*"
  shows "(fill_holes D ss, fill_holes D ts) ∈ (srstep ℱ ℛ)⇧*" using assms
proof (induct ss arbitrary: D ts rule: rev_induct)
  case Nil then show ?case
    by (cases ts) auto
next
  case (snoc s ss)
  from snoc(3) obtain t ts' where [simp]: "ts = ts' @ [t]"
    by (cases ts) (auto, metis append_butlast_last_id list.distinct(1))
  from snoc(3, 6, 7) have fn: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
    by (auto simp: nth_append split: if_splits)
  let ?C = "fill_holes_mctxt D ((replicate (length ts') MHole) @ [mctxt_of_term s])"
  let ?CM = "fill_holes_mctxt D (map mctxt_of_term ts' @ [MHole])"
  have [simp]: "⋃ (set (replicate (length ts') {})) = {}" by auto
  from snoc(1)[of ?C ts'] have steps: "(fill_holes ?C ss, fill_holes ?C ts') ∈ (srstep ℱ ℛ)⇧*"
    using snoc(2-) fn by (auto simp: num_holes_fill_holes_mctxt nth_append split: if_splits)
  have num: "num_holes ?C = length ts'" using snoc(2, 3) by (auto simp: num_holes_fill_holes_mctxt)
  have lhs [simp]: "fill_holes ?C ss = fill_holes D (ss @ [s])"  "fill_holes ?C ts' = fill_holes D (ts' @ [s])"
    using snoc(2, 3) fill_holes_mctxt_fill_holes num
    by (auto simp: fill_holes_mctxt_fill_holes nth_append
        partition_by_replicate_id partition_by_replicate_end
        intro!: arg_cong2[where ?f = fill_holes] nth_equalityI)
  have ctxt: "num_holes ?CM = Suc 0" using snoc(2, 3) by (auto simp: num_holes_fill_holes_mctxt)
  have [simp]: "fill_holes ?CM [s] = fill_holes D (ts' @ [s])" "fill_holes ?CM [t] = fill_holes D ts"
    using snoc(2, 3) fill_holes_mctxt_fill_holes num
    by (auto simp: fill_holes_mctxt_fill_holes nth_append num_holes_fill_holes_mctxt
        partition_by_replicate_id partition_by_replicate_end
        intro!: arg_cong2[where ?f = fill_holes] nth_equalityI)
  have "funas_term (fill_holes D (ts' @ [s])) ⊆ ℱ" "funas_term (fill_holes D ts) ⊆ ℱ" using snoc(2, 3, 5, 6, 7)
    by (auto simp: funas_mctxt_fill_holes nth_append split: if_splits)
      (metis in_mono in_set_conv_nth less_SucI)+
  from this ctxt rsteps_closed_ctxt[of s t ℛ "ctxt_of_mctxt ?CM"] have
    "(fill_holes D (ts' @ [s]), fill_holes D ts) ∈ (srstep ℱ ℛ)⇧*" using snoc(2-) fn
    using sig_step_rstep_trancl_conv[OF snoc(4)]
    by (cases "s = t") (auto simp: rtrancl_eq_or_trancl simp flip: fill_holes_apply_ctxt, metis lessI nth_append_length)
  then show ?case using steps by auto
qed

lemma srstep_relcomp_mctxt_cl:
  assumes "num_holes D = length ss" "length ss = length ts"
    and funas: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ" "funas_mctxt D ⊆ ℱ"
    "∀ i < length ts. funas_term (ss ! i) ⊆ ℱ" "∀ i < length ts. funas_term (ts ! i) ⊆ ℱ"
    and "∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
  shows "(fill_holes D ss, fill_holes D ts) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
  using assms
proof -
  from assms(2, 8) obtain us where us: "length us = length ts"
    "∀ i < length ts. (ss ! i, us ! i) ∈ (srstep ℱ ℛ)⇧*"
    "∀ i < length ts. (us ! i, ts ! i) ∈ (srstep ℱ 𝒮)⇧*"
    using Ex_list_of_length_P[of "length ts" "λ x i. (ss ! i, x) ∈ (srstep ℱ ℛ)⇧* ∧ (x, ts ! i) ∈ (srstep ℱ 𝒮)⇧*"]
    by auto
  from srstep_mctxt_cl[OF _ _ funas(1, 3)] srstep_mctxt_cl[OF _ _ funas(2, 3)] this
  have "(fill_holes D ss, fill_holes D us) ∈ (srstep ℱ ℛ)⇧*"
    "(fill_holes D us, fill_holes D ts) ∈ (srstep ℱ 𝒮)⇧*" using assms(1, 2) funas
    by auto (metis (no_types, lifting) rtrancl.simps sig_stepE)+
  then show ?thesis by auto
qed


lemma commute_rrstep:
  assumes "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
  shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮) ⟷
     comp_rrstep_rel ℱ (ℛ¯) 𝒮 ⊆ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*" (is "?Ls ⟷ ?Rs")
proof -
  have Drr: "(s :: ('a, 'b) term, t) ∈ sig_step ℱ ((rrstep ℒ)¯) ⟹ (s, t) ∈ sig_step ℱ ((rstep ℒ)¯)" for ℒ s t
    by (metis rrstep_converse rrstep_imp_rstep rstep_converse sig_stepE sig_stepI)
  have Drr2: "(s :: ('a, 'b) term, t) ∈ sig_step ℱ (rrstep ℒ) ⟹ (s, t) ∈ srstep ℱ ℒ" for ℒ s t
    by (metis rrstep_converse rrstep_imp_rstep rstep_converse sig_stepE sig_stepI)
  have "(s, t) ∈ srsteps_with_root_step ℱ (ℛ¯) ⟹ (s, t) ∈ (srstep ℱ (ℛ¯))⇧*" for s t
    by (auto simp: commute_def rtrancl_converse rrstep_converse rtrancl_eq_or_trancl dest!: Drr Drr2)
  moreover have "(s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ (s, t) ∈ (srstep ℱ 𝒮)⇧*" for s t
    by (auto simp: commute_def rtrancl_converse rrstep_converse rtrancl_eq_or_trancl dest!: Drr2)
  ultimately have fst: "?Ls ⟹ ?Rs" apply (auto simp: commute_def sig_step_restep_conv) apply blast
    by (fastforce simp add: relcomp.relcompI subset_iff)
  {fix s t assume ass: ?Rs "(s, t) ∈ (srstep ℱ (ℛ¯))⇧* O (srstep ℱ 𝒮)⇧*"
    from sig_step_rstep_comp_split[OF this(2)] obtain D ss ts where
      sizes: "num_holes D = length ss" "length ss = length ts"
      and inv: "∀ i < length ts. ss ! i = ts ! i ∨ (ss ! i, ts ! i) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮"
      and sha: "fill_holes D ss = s ∧ fill_holes D ts = t" by auto
    from ass inv have inv': "∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*"
      by auto (smt in_mono relcomp.simps rtrancl.rtrancl_refl)
    have "(s, t) ∈ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*"
    proof (cases "s = t")
      case False
      then have "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" using ass(2) assms
        by (auto simp: rtrancl_eq_or_trancl trancl_converse sig_step_restep_conv dest!: sig_step_tranclD)
      then show ?thesis using assms(1) sizes
        unfolding conjunct1[OF sha, symmetric] conjunct2[OF sha, symmetric]
        apply (intro srstep_relcomp_mctxt_cl[OF sizes assms(2) _ _ _ _ inv'])
           apply (auto simp: funas_rel_def funas_mctxt_fill_holes)
         apply (metis UN_iff UnCI in_set_conv_nth sup.orderE)+
        done
    qed auto}
  then have "?Rs ⟹ ?Ls" unfolding commute_def
    by (simp add: subrelI sig_step_restep_conv) 
  then show ?thesis using fst by blast
qed

(* LVTRS part *)

definition lvtrs where
  "lvtrs ℛ = (∀ (l, r) ∈ ℛ. vars_term l ∩ vars_term r = {} ∧ linear_term l ∧ linear_term r)"

lemma lvtrs_rrstpe_idep_subst_cl:
  assumes "lvtrs R" "(s, t) ∈ (rrstep R)"
  shows "(s ⋅ σ, t ⋅ τ) ∈ (rrstep R)"
proof -
  from assms(2) obtain l r σ' where r: "(l, r) ∈ R" and [simp]: "t = r ⋅ σ'" "s = l ⋅ σ'"
    by (auto simp: rrstep_def')
  let ?γ = "λ x. if x ∈ vars_term l then (σ' x) ⋅ σ else (σ' x) ⋅ τ"
  from assms(1) r have "x ∈ vars_term l ⟹ x ∈  vars_term r ⟹ False" for x unfolding lvtrs_def
    by auto
  then have "l ⋅ σ' ∘⇩s σ = l ⋅ ?γ"  "r ⋅ σ' ∘⇩s τ = r ⋅ ?γ"
    by (intro term_subst_eq, force simp add: subst_compose)+
  then show ?thesis using r
    by (auto simp: rrstep_def')
qed

lemma lvtrs_srrstpe_idep_subst_cl:
  assumes "lvtrs R" "(s, t) ∈ (srrstep ℱ R)" "⋀ t. funas_term (σ t) ⊆ ℱ" "⋀ t. funas_term (τ t) ⊆ ℱ"
  shows "(s ⋅ σ, t ⋅ τ) ∈ (srrstep ℱ R)"
  using lvtrs_rrstpe_idep_subst_cl[OF assms(1), of s t] assms(2-)
  by (auto simp: sig_step_def funas_term_subst) blast

locale steps_to_gsteps_ext = 
  fixes ℱ :: "('f × nat) set" and c d and v :: 'v and w :: 'v
  assumes fresh: "(c, 0) ∉ ℱ" "(d, 0) ∉ ℱ"
    and diff: "v ≠ w" "c ≠ d"
begin

abbreviation "ℋ ≡ ℱ ∪ {(c, 0), (d, 0)}"
lemma ext: "ℱ ⊆ ℋ" by auto

fun term_to_F where
  "term_to_F (Var x) = Var x"
| "term_to_F (Fun f ts) =
    (if f = c ∧ length ts = 0 then Var v else if f = d ∧ length ts = 0 then Var w else Fun f (map (term_to_F) ts))"

fun ctxt_to_F where
  "ctxt_to_F Hole = Hole"
| "ctxt_to_F (More f ss C ts) =
    (More f (map (term_to_F) ss) (ctxt_to_F C) (map (term_to_F) ts))"

lemma term_to_F_ctxt_dist [simp]:
  "term_to_F C⟨s⟩ = (ctxt_to_F C)⟨term_to_F s⟩"
  by (induct C) auto

lemma term_to_F_subst_dist [simp]:
  "funas_term l ⊆ ℱ ⟹ term_to_F (l ⋅ σ) = l ⋅ (λ x. term_to_F (σ x))" using fresh
  by (induct l) (auto simp: funas_rel_def)

lemma term_to_F_funas_reduction:
  "funas_term s ⊆ ℋ ⟹ funas_term (term_to_F s) ⊆ ℱ"
  unfolding ext by (induct s) auto

lemma ctxt_to_F_funas_reduction:
  "funas_ctxt C ⊆ ℋ ⟹ funas_ctxt (ctxt_to_F C) ⊆ ℱ"
  using subsetD[OF term_to_F_funas_reduction]
  by (induct C) (auto simp: ext SUP_le_iff)

lemma funas_rel_sig_rule:
  "funas_rel ℛ ⊆ ℱ ⟹ (l, r) ∈ ℛ ⟹ funas_tuple (l, r) ⊆ ℱ"
  by (auto simp: funas_rel_def)

lemma gext_step_to_step:
  "funas_rel ℛ ⊆ ℱ ⟹ (s, t) ∈ gsrstep ℋ ℛ ⟹ (term_to_F s, term_to_F t) ∈ srstep ℱ ℛ"
  using term_to_F_funas_reduction ctxt_to_F_funas_reduction
  by (auto simp: sig_step_def dest!: rstep_imp_C_s_r funas_rel_sig_rule)

lemma gext_steps_to_steps:
  assumes "(s, t) ∈ (gsrstep ℋ ℛ)⇧*" "funas_rel ℛ ⊆ ℱ" shows "(term_to_F s, term_to_F t) ∈ (srstep ℱ ℛ)⇧*" using assms(1)
proof (induct)
  case (step u t)
  from gext_step_to_step[OF assms(2) step(2)] have "(term_to_F u, term_to_F t) ∈ srstep ℱ ℛ" .
  then show ?case using step(3) by auto
qed auto

lemma extrstep_to_rstep:
  "funas_rel ℛ ⊆ ℱ ⟹ (s, t) ∈ srstep ℋ ℛ ⟹ (term_to_F s, term_to_F t) ∈ srstep ℱ ℛ"
  using term_to_F_funas_reduction ctxt_to_F_funas_reduction
  by (auto simp: sig_step_def dest!: rstep_imp_C_s_r funas_rel_sig_rule)

lemma extrsteps_to_rsteps:
  assumes "(s, t) ∈ (srstep ℋ ℛ)⇧*" "funas_rel ℛ ⊆ ℱ" shows "(term_to_F s, term_to_F t) ∈ (srstep ℱ ℛ)⇧*" using assms(1)
proof (induct)
  case (step u t)
  from extrstep_to_rstep[OF assms(2) step(2)] have "(term_to_F u, term_to_F t) ∈ srstep ℱ ℛ" .
  then show ?case using step(3) by auto
qed auto

abbreviation "rev_term_to ≡ λ x. if x = v then Fun c [] else Fun d []"

lemma revert_term_to_F:
  assumes "ground s" "funas_term s ⊆ ℋ"
  shows "(term_to_F s) ⋅ rev_term_to = s" using assms
proof (induct s)
  case (Fun f ts)
  have "i < length ts ⟹ term_to_F (ts ! i) ⋅ rev_term_to = ts ! i" for i
    using Fun(2-) by (intro Fun(1)[OF nth_mem]) (auto simp: SUP_le_iff)
  then show ?case using diff by (auto simp: comp_def intro: nth_equalityI)
qed auto

lemma rev_term_to_to_sig:
  "⋀x. funas_term (rev_term_to x) ⊆ ℋ"
  by auto

lemma grsterp_trancl_funasD:
  "(s, t) ∈ (gsrstep 𝒢 ℛ)⇧+ ⟹ funas_tuple (s, t) ⊆ 𝒢"
  by auto (meson in_mono inf_le1 sig_stepE tranclD tranclD2)+

lemma srstep_subst_gsrstep:
  defines "σ ≡ λ x. Fun c []"
  assumes "(s, t) ∈ (srstep ℋ ℛ)⇧*"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (gsrstep ℋ ℛ)⇧*" using assms(2) unfolding assms(1)
proof (induct)
  case (step t u)
  have "(t ⋅ (λ x. Fun c []), u ⋅ (λ x. Fun c [])) ∈ (gsrstep ℋ ℛ)" using step(2)
    by (auto simp: sig_step_def funas_term_subst)
  then show ?case using step(3)
    by (simp add: rtrancl.rtrancl_into_rtrancl)
qed auto

lemma srstep_trancl_gsrstep:
  assumes "ground s" "ground t" "(s, t) ∈ (srstep ℋ ℛ)⇧*"
  shows "(s, t) ∈ (gsrstep ℋ ℛ)⇧*"
  using srstep_subst_gsrstep[OF assms(3)] assms(1, 2)
  by (auto simp: ground_subst_apply)

lemma srstep_trancl_gsrstep_relcomp:
  assumes "ground s" "ground t" "(s, t) ∈ (srstep ℋ ℛ)⇧* O (srstep ℋ 𝒮)⇧*"
  shows "(s, t) ∈ (gsrstep ℋ ℛ)⇧* O (gsrstep ℋ 𝒮)⇧*"
  using srstep_subst_gsrstep assms
  apply (auto simp: ground_subst_apply)
  by (smt Un_empty_right Un_insert_right ground_subst_apply relcomp.relcompI srstep_subst_gsrstep)

lemma COM_to_GCOM:
  fixes ℛ :: "('f, 'v) term rel"
  assumes "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
    and "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  shows "commute (gsrstep ℋ ℛ) (gsrstep ℋ 𝒮)"
proof -
  from assms(1) have rel_conv: "funas_rel (ℛ¯) ⊆ ℱ" by (auto simp: funas_rel_def)
  {fix s t assume ass: "(s, t) ∈ ((gsrstep ℋ ℛ)¯)⇧* O (gsrstep ℋ 𝒮)⇧*"
    then have "(term_to_F s, term_to_F t) ∈ ((srstep ℱ ℛ)¯)⇧* O (srstep ℱ 𝒮)⇧*"
      using extrsteps_to_rsteps[OF _ assms(2)]
      using extrsteps_to_rsteps[OF _ rel_conv]
      by (auto simp flip: Restr_converse sig_step_restep_conv rstep_converse dest!: rtrancl_Restr) blast
    then have "(term_to_F s, term_to_F t) ∈ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*" using assms(3)
      by (auto simp: commute_def sig_step_restep_conv)
    then have step: "(term_to_F s, term_to_F t) ∈ (srstep ℋ 𝒮)⇧* O (srstep ℋ (ℛ¯))⇧*"
      using rtrancl_mono[OF sig_step_mono[OF ext]]
      by (auto simp flip: rstep_converse)
    have "(s, t) ∈ (gsrstep ℋ 𝒮)⇧* O (gsrstep ℋ (ℛ¯))⇧*"
    proof (cases "s = t")
      case False
      then have "ground s" "ground t"
        using ass by (auto simp: rtrancl_eq_or_trancl dest: tranclD tranclD2)
      moreover have "funas_term s ⊆ ℋ" "funas_term t ⊆ ℋ" using False ass
        by (auto simp: rtrancl_eq_or_trancl  simp flip: Restr_converse sig_step_restep_conv rstep_converse dest!: grsterp_trancl_funasD) blast+
      ultimately show ?thesis using step False
        using sig_steps_subst_closed[OF _ rev_term_to_to_sig, of "term_to_F s" _ 𝒮 id]
        using sig_steps_subst_closed[OF _ rev_term_to_to_sig, of _ "term_to_F t" "ℛ¯" id]
        apply (intro srstep_trancl_gsrstep_relcomp[of s t 𝒮 "ℛ¯"])
        apply (auto simp: revert_term_to_F simp flip: rstep_converse)
        apply blast
        done
    qed auto}
  then show ?thesis unfolding commute_def
    by (auto simp add: Restr_converse sig_step_restep_conv)
qed

lemma srsteps_to_gsrstep:
  assumes "lvtrs ℛ" "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
  shows "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ srsteps_with_root_step ℋ ℛ"
  using assms(2)
  using lvtrs_srrstpe_idep_subst_cl[OF assms(1), of _ _ ℋ "const_subt c" "const_subt d"]
  using sig_steps_subst_closed[of s _ ℋ ℛ "const_subt c"]
  using sig_steps_subst_closed[of _ t ℋ ℛ "const_subt d"]
  using rtrancl_mono[OF sig_step_mono[OF ext], of "rstep ℛ"] sig_step_mono[OF ext, of "rrstep ℛ"]
  by auto (meson relcomp3_I subset_iff)

lemma lvtrs_linear_system: "lvtrs ℛ ⟹ linear_sys ℛ"
  by (auto simp: lvtrs_def)

lemma GCOM_to_COM:
  fixes ℛ :: "('f, 'v) term rel"
  assumes "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
    and "lvtrs ℛ" "lvtrs 𝒮"
    and "commute (gsrstep ℋ ℛ) (gsrstep ℋ 𝒮)"
  shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
  from assms(3) have invR: "lvtrs (ℛ¯)" by (auto simp: lvtrs_def)
  from assms(1) have invF: "funas_rel (ℛ¯) ⊆ ℱ" by (auto simp: funas_rel_def)
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
      by (auto simp flip: rstep_converse simp: rtrancl_eq_or_trancl dest!: sig_rrstepD sig_step_tranclD)
    from ass have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ comp_rrstep_rel ℋ (ℛ¯) 𝒮"
      using srsteps_to_gsrstep[OF invR] srsteps_to_gsrstep[OF assms(4)]
      using sig_steps_subst_closed[of s _ ℋ "ℛ¯" "const_subt c"]
      using sig_steps_subst_closed[of _ t ℋ 𝒮 "const_subt d"]
      using rtrancl_mono[OF sig_step_mono[OF ext], of "rstep (ℛ¯)"]
      using rtrancl_mono[OF sig_step_mono[OF ext], of "rstep 𝒮"]
      by (auto simp flip: rstep_converse) (meson in_mono relcomp.relcompI)+
    then have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℋ (ℛ¯))⇧* O (srstep ℋ 𝒮)⇧*"
      using sig_step_mono2[OF rrstep_rstep_mono[of "ℛ¯"], of ℋ]
      using sig_step_mono2[OF rrstep_rstep_mono[of 𝒮], of ℋ]
      by (auto simp flip: rstep_converse)
         (meson in_mono r_into_rtrancl relcomp.simps rtrancl_trans)+
    then have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ 𝒮)⇧*"
      by (intro srstep_trancl_gsrstep_relcomp) auto
    then have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (gsrstep ℋ 𝒮)⇧* O (gsrstep ℋ (ℛ¯))⇧*"
      using assms(5) by (auto simp: commute_def sig_step_restep_conv Restr_converse)
    then have "(s ⋅ const_subt c, t ⋅ const_subt d) ∈ (srstep ℋ 𝒮)⇧* O (srstep ℋ (ℛ¯))⇧*"
      by auto (meson in_mono inf_le1 relcomp.simps rtrancl_mono)
    then have step: "(s, t) ∈ (srstep ℋ 𝒮)⇧* O (srstep ℋ (ℛ¯))⇧*"
      using assms(1 - 4) funas fresh diff
      by (intro remove_const_substs_relcomp[of 𝒮 "ℛ¯" c d t s ℋ])
         (auto simp: funas_rel_def dest: lvtrs_linear_system)
     from step have "(s, t) ∈ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*"
      using funas assms(1, 2)
      using sig_step_trancl_sig_trans[OF invF funas, of ℋ]
      using sig_step_trancl_sig_trans[OF assms(2) funas, of ℋ]
      using rstep_trancl_sig_step_right[of s _ _ _ v, OF _ assms(2) funas(1)]
      using rstep_trancl_sig_step_left[of _ t _ _ v, OF _ invF funas(2)]
      apply (auto simp: rtrancl_eq_or_trancl simp flip: rstep_converse)
      apply blast apply auto
      apply (meson relcomp.relcompI sig_stepE subsetD trancl_into_rtrancl trancl_sig_subset)
      done}
  then show ?thesis unfolding commute_rrstep[OF assms(1, 2)]
    by force
qed

lemma CR_to_GCR:
  fixes ℛ :: "('f, 'v) term rel"
  assumes "funas_rel ℛ ⊆ ℱ" and "CR (srstep ℱ ℛ)" shows "CR (gsrstep ℋ ℛ)"
  using COM_to_GCOM[OF assms(1) assms(1)] assms(2)
  by (auto simp: CR_iff_self_commute)

lemma GCR_to_CR:
  fixes ℛ :: "('f, 'v) term rel"
  assumes "funas_rel ℛ ⊆ ℱ" and "lvtrs ℛ" and "CR (gsrstep ℋ ℛ)" shows "CR (srstep ℱ ℛ)"
  using GCOM_to_COM[OF assms(1) assms(1) assms(2) assms(2)] assms(3)
  by (auto simp: CR_iff_self_commute)

end

end