Theory Conditional_Rewriting

theory Conditional_Rewriting
imports Reduction_Pair Renaming_Interpretations
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2012-2017)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2012-2015)
Author:  Sarah Winkler <sarah.winkler@uibk.ac.at> (2014, 2015)
Author:  Thomas Sternagel <thomas.sternagel@uibk.ac.at> (2015-2017)
License: LGPL (see file COPYING.LESSER)
*)
theory Conditional_Rewriting
imports
  QTRS.Trs
  "Check-NT.Reduction_Pair"
  QTRS.Renaming_Interpretations
begin

type_synonym ('f, 'v) condition = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) crule = "('f, 'v) rule × ('f, 'v) condition list"
type_synonym ('f, 'v) ctrs = "('f, 'v) crule set"

text ‹A conditional rewrite step of level @{term n}.›
fun cstep_n :: "('f, 'v) ctrs ⇒ nat ⇒ ('f, 'v) term rel"
where
  "cstep_n R 0 = {}" |
  cstep_n_Suc: "cstep_n R (Suc n) =
    {(C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) | C l r σ cs.
      ((l, r), cs) ∈ R ∧ (∀ (si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*)}"

definition conds_n_sat
where
  conds_n_sat_iff: "conds_n_sat R n cs σ ⟷ (∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*)"

lemma conds_n_satD:
  assumes "conds_n_sat R n cs σ" and "(s, t) ∈ set cs"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (cstep_n R n)*"
using assms by (auto simp: conds_n_sat_iff)

lemma conds_n_sat_append [simp]:
  "conds_n_sat R n (cs @ ds) σ ⟷ conds_n_sat R n cs σ ∧ conds_n_sat R n ds σ"
by (auto simp add: conds_n_sat_iff)

lemma conds_n_sat_Nil [simp]:
  "conds_n_sat R n [] σ"
by (simp add: conds_n_sat_iff)

lemma conds_n_sat_singleton [simp]:
  "conds_n_sat R n [c] σ ⟷ (fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep_n R n)*"
by (auto simp: conds_n_sat_iff)

lemma conds_n_sat_subst_list:
  "conds_n_sat R n (subst_list σ cs) τ = conds_n_sat R n cs (σ ∘s τ)"
by (auto simp: conds_n_sat_iff subst_set_def)

lemma cstep_n_SucI [Pure.intro?]:
  assumes "((l, r), cs) ∈ R"
    and "∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*"
    and "s = C⟨l ⋅ σ⟩"
    and "t = C⟨r ⋅ σ⟩"
  shows "(s, t) ∈ cstep_n R (Suc n)"
  using assms by (auto) blast

lemma cstep_nE:
  assumes "(s, t) ∈ cstep_n R n"
  obtains C l r σ cs n' where "((l, r), cs) ∈ R" and "n = Suc n'"
    and "∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n')*"
    and "s = C⟨l ⋅ σ⟩"
    and "t = C⟨r ⋅ σ⟩"
  using assms by (cases n) auto

lemma cstep_n_SucE:
  assumes "(s, t) ∈ cstep_n R (Suc n)"
  obtains C l r σ cs where "((l, r), cs) ∈ R"
    and "∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*"
    and "s = C⟨l ⋅ σ⟩"
    and "t = C⟨r ⋅ σ⟩"
  using assms by auto

declare cstep_n_Suc [simp del]

lemma cstep_n_Suc_mono:
  "cstep_n R n ⊆ cstep_n R (Suc n)"
proof (induct n)
  case (Suc n)
  show ?case
    using rtrancl_mono [OF Suc] by (auto elim!: cstep_n_SucE intro!: cstep_n_SucI)
qed simp

lemma cstep_n_mono:
  assumes "i ≤ n"
  shows "cstep_n R i ⊆ cstep_n R n"
using assms
proof (induct "n - i" arbitrary: i)
  case (Suc k)
  then have "k = n - Suc i" and "Suc i ≤ n" by arith+
  from Suc.hyps(1) [OF this] show ?case using cstep_n_Suc_mono by blast
qed simp

lemma csteps_n_mono:
  assumes "m ≤ n"
  shows "(cstep_n R m)* ⊆ (cstep_n R n)*"
using assms by (intro rtrancl_mono cstep_n_mono)

lemma conds_n_sat_mono:
  "m ≤ n ⟹ conds_n_sat R m cs σ ⟹ conds_n_sat R n cs σ"
using csteps_n_mono [of m n R]
by (auto simp: conds_n_sat_iff)

lemma cstep_n_mono':
  "cstep_n R m ⊆ cstep_n R (m + k)"
  using cstep_n_mono [of "m" "m + k"] by simp

lemma cstep_n_ctxt:
  assumes "(s, t) ∈ cstep_n R n"
  shows "(C⟨s⟩, C⟨t⟩) ∈ cstep_n R n"
  using assms by (cases n) (auto elim!: cstep_n_SucE intro: cstep_n_SucI [where C = "C ∘c D" for D])

lemma all_ctxt_closed_csteps_n [intro]:
  "all_ctxt_closed UNIV ((cstep_n R n)*)"
by (rule trans_ctxt_imp_all_ctxt_closed)
   (auto simp: ctxt.closed_def elim!: ctxt.closure.cases intro: trans_rtrancl refl_rtrancl cstep_n_ctxt [THEN rtrancl_map])

lemma cstep_n_subst:
  assumes "(s, t) ∈ cstep_n R n"
  shows "(s ⋅ σ, t ⋅ σ) ∈ cstep_n R n"
using assms
proof (induct n arbitrary: s t σ)
  case (Suc n)
  from ‹(s, t) ∈ cstep_n R (Suc n)› obtain C l r cs τ
    where "((l, r), cs) ∈ R" and "∀(si, ti) ∈ set cs. (si ⋅ τ, ti ⋅ τ) ∈ (cstep_n R n)*"
    and "s = C⟨l ⋅ τ⟩" and "t = C⟨r ⋅ τ⟩" by (rule cstep_n_SucE)
  then show ?case
    using Suc.hyps and rtrancl_map [of "cstep_n R n" "λt. t ⋅ σ"]
    by (auto intro!: cstep_n_SucI [of l r cs R "τ ∘s σ" _ _ "C ⋅c σ"])
qed simp

lemma cstep_n_ctxt_subst:
  assumes "(s, t) ∈ cstep_n R n"
  shows "(D ⟨s ⋅ σ⟩, D ⟨t ⋅ σ⟩) ∈ cstep_n R n"
  by (intro cstep_n_ctxt cstep_n_subst) fact

definition "cstep R = (⋃n. cstep_n R n)"

lemma cstep_iff:
  "(s, t) ∈ cstep R ⟷ (∃n. (s, t) ∈ cstep_n R n)"
  by (auto simp: cstep_def)

definition conds_sat
where
  conds_sat_iff: "conds_sat R cs σ ⟷ (∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep R)*)"

lemma conds_sat_subst_list:
  "conds_sat R (subst_list σ cs) τ = conds_sat R cs (σ ∘s τ)"
by (auto simp: conds_sat_iff subst_set_def)

lemma conds_sat_append [simp]:
  "conds_sat R (cs1 @ cs2) σ ⟷ conds_sat R cs1 σ ∧ conds_sat R cs2 σ"
by (auto simp: conds_sat_iff)
  
lemma NF_cstep_subterm:
  assumes "t ∈ NF (cstep R)" and "t ⊵ s"
  shows "s ∈ NF (cstep R)"
proof (rule ccontr)  
  assume "¬ ?thesis"
  then obtain u where "(s, u) ∈ cstep R" by auto
  from ‹t ⊵ s› obtain C where "t = C⟨s⟩" by auto
  with ‹(s, u) ∈ cstep R› have "(t, C⟨u⟩) ∈ cstep R"
    using cstep_iff cstep_n_ctxt by blast
  hence "t ∉ NF (cstep R)" by auto
  with assms show False by simp
qed

lemma cstep_n_empty [simp]: "cstep_n {} n = {}"
  by (induct n) (auto simp: cstep_n_Suc)

lemma cstep_empty [simp]: "cstep {} = {}"
  unfolding cstep_def by simp

lemma csteps_n_trans:
  assumes "(s, t) ∈ (cstep_n R m)*" and "(t, u) ∈ (cstep_n R n)*"
  shows "(s, u) ∈ (cstep_n R (max m n))*"
  using assms
    and cstep_n_mono [of m "max m n" R, THEN rtrancl_mono]
    and cstep_n_mono [of n "max m n" R, THEN rtrancl_mono]
    by (auto dest!: set_mp)

lemma csteps_imp_csteps_n:
  assumes "(s, t) ∈ (cstep R)*"
  shows "∃n. (s, t) ∈ (cstep_n R n)*"
  using assms by (induct) (auto intro: csteps_n_trans simp: cstep_iff)

lemma cstep_n_imp_cstep:
  assumes "(s, t) ∈ cstep_n R n"
  shows "(s, t) ∈ cstep R"
using assms by (auto simp: cstep_iff)

lemma csteps_n_imp_csteps:
  assumes "(s, t) ∈ (cstep_n R n)*"
  shows "(s, t) ∈ (cstep R)*"
using assms by (induct; auto dest: cstep_n_imp_cstep)

lemma csteps_n_subset_csteps:
  "(cstep_n R n)* ⊆ (cstep R)*"
by (auto dest: csteps_n_imp_csteps)

lemma all_cstep_imp_cstep_n:
  assumes "∀i < (k::nat). (si i, ti i) ∈ (cstep R)*"
  shows "∃n. ∀i < k. (si i, ti i) ∈ (cstep_n R n)*" (is "∃n. ∀i < k. ?P i n")
proof -
  have "∀i < k. ∃ni. ?P i ni"
    using assms by (auto intro: csteps_imp_csteps_n)
  then obtain f where *: "∀i < k. ?P i (f i)" by metis
  define n where "n ≡ Max (set (map f [0 ..< k]))"
  have "∀i < k. f i ≤ n" by (auto simp: n_def)
  then have "∀i < k. ?P i n"
    using cstep_n_mono [of "f i" n R for i, THEN rtrancl_mono] and * by blast
  then show ?thesis ..
qed

lemma cstepI:
  assumes "((l, r), cs) ∈ R"
    and conds: "∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep R)*"
    and "s = C⟨l ⋅ σ⟩"
    and "t = C⟨r ⋅ σ⟩"
  shows "(s, t) ∈ cstep R"
proof -
  obtain n where "∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*"
  using all_cstep_imp_cstep_n[of "length cs" "λi. fst (cs ! i) ⋅ σ" "λi. snd (cs ! i) ⋅ σ" R]
  and conds
    by (auto simp: all_set_conv_all_nth split_beta')
  then have "(s, t) ∈ cstep_n R (Suc n)" using assms by (intro cstep_n_SucI) (assumption)+
  then show ?thesis using cstep_iff by auto
qed

lemma cstepE [elim]:
  assumes "(s, t) ∈ cstep R"
    and imp: "⋀C σ l r cs. ⟦((l, r), cs) ∈ R; ∀(si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep R)*; s = C⟨l ⋅ σ⟩; t = C⟨r ⋅ σ⟩⟧ ⟹ P"
  shows "P"
proof -
  obtain n where *: "(s, t) ∈ cstep_n R n" using assms by (auto simp: cstep_iff)
  then show ?thesis
  proof (cases n)
    case (Suc n')
    have **: "(cstep_n R n')* ⊆ (cstep R)*" by (rule rtrancl_mono) (auto simp: cstep_iff)
    show ?thesis
      by (rule cstep_n_SucE [OF * [unfolded Suc]], rule imp, insert **) auto
  qed simp
qed

lemma Var_NF_cstep:
  assumes "∀ ((l, r), cs) ∈ R. is_Fun l"
  shows "Var x ∈ NF (cstep R)"
proof
  fix s
  show "(Var x, s) ∉ cstep R"
  proof
    assume "(Var x, s) ∈ cstep R"
    then show "False" using assms supteq_var_imp_eq by fastforce
  qed
qed

lemma cstep_ctxt_closed:
  "ctxt.closed (cstep R)"
  by (rule ctxt.closedI) (auto intro: cstep_n_ctxt simp: cstep_iff)

lemma csteps_all_ctxt_closed[intro]: "all_ctxt_closed UNIV ((cstep r)^*)"
  using  cstep_ctxt_closed by (blast intro: trans_ctxt_imp_all_ctxt_closed trans_rtrancl refl_rtrancl)

lemma join_csteps_all_ctxt_closed: "all_ctxt_closed UNIV ((cstep r))" 
proof -
 have var:"∀x. (Var x, Var x) ∈ (cstep r)" by fast
 { fix f ss ts
   assume a:"length ts = length ss" "∀i<length ts. (ts ! i, ss ! i) ∈ (cstep r)"
   from a(2) have "∀i<length ts. ∃ ui. (ts ! i, ui)∈ (cstep r)^* ∧  (ss ! i, ui) ∈ (cstep r)^*" by blast
   with choice have "∃ui. ∀i<length ts. (ts ! i, ui i)∈ (cstep r)^* ∧  (ss ! i, ui i) ∈ (cstep r)^*" by meson
   then obtain ui where ui:"⋀i. i<length ts ⟹ (ts ! i, ui i)∈ (cstep r)^* ∧  (ss ! i, ui i) ∈ (cstep r)^*" by blast
   let ?us = "map ui [0 ..<length ts]"
   have lus: "length ts = length ?us" by simp
   from ui have uss:"⋀j. j < length ts ⟹ (ss ! j, ?us ! j) ∈ (cstep r)^*" by auto
   from ui have ust:"⋀j. j < length ts ⟹ (ts ! j, ?us ! j) ∈ (cstep r)^*" by auto
   note acc = conjunct1[OF csteps_all_ctxt_closed[unfolded all_ctxt_closed_def], rule_format]
   from acc[OF _ lus ust] have tseq:"(Fun f ts, Fun f ?us) ∈ (cstep r)*" by blast
   from acc[OF _ lus[unfolded a(1)] uss[unfolded a(1)]] a(1) have sseq:"(Fun f ss, Fun f ?us) ∈ (cstep r)*" by force
   with tseq have "(Fun f ts, Fun f ss) ∈ (cstep r)" by blast
 }
 with var show ?thesis  unfolding all_ctxt_closed_def by auto
qed

abbreviation clhs :: "('f, 'v) crule ⇒ ('f, 'v) term"
where
  "clhs ρ ≡ fst (fst ρ)"

abbreviation crhs :: "('f, 'v) crule ⇒ ('f, 'v) term"
where
  "crhs ρ ≡ snd (fst ρ)"

definition X_vars :: "('f, 'v) crule ⇒ nat ⇒ 'v set"
where
  "X_vars ρ i = vars_term (clhs ρ) ∪ ⋃(vars_term ` rhss (set (take i (snd ρ))))"

lemma X_vars_mono:
  "i ≤ j ⟹ X_vars ρ i ⊆ X_vars ρ j"
by (fastforce simp: X_vars_def dest: set_take_subset_set_take)

definition Y_vars ::"('f, 'v) crule ⇒ nat ⇒ 'v set"
where
  "Y_vars ρ i =
    vars_term (crhs ρ) ∪ vars_term (snd (snd ρ ! i)) ∪ (vars_trs (set (drop (Suc i) (snd ρ))))"

lemma X_vars_alt : 
  assumes "i ≤ length (snd ρ)"
  shows "X_vars ρ i = vars_term (clhs ρ) ∪ ⋃((λj. vars_term (snd (snd ρ ! j))) ` {j. j < i})"
proof -
  let ?L = "⋃(vars_term ` (rhss (set (List.take i (snd ρ)))))"
  let ?R = "⋃((λj. vars_term (snd (snd ρ ! j))) ` {j. j < i})"
  { fix x
   assume "x ∈ ?L" 
   hence "∃j. j < i ∧ x ∈ vars_term (snd ((snd ρ) ! j))" unfolding set_conv_nth using nth_take[of _ i "snd ρ"] by fastforce
   then obtain j where j:"j < i" and x:"x ∈ vars_term (snd (snd ρ ! j))" by blast
   hence "x ∈ ?R"  by blast
  } hence *: "?L ⊆ ?R" by auto
  { fix x
   assume "x ∈ ?R"
   hence "∃j. j < i ∧ x ∈ vars_term (snd ((snd ρ) ! j))" by blast
   then obtain j where  j:"j < i" and x:"x ∈ vars_term (snd (snd ρ ! j))" by blast
   hence "x ∈ vars_term (snd (take i (snd ρ) ! j))"  using nth_take[OF j(1)] by force
   with j(1)  have "x ∈ ?L" unfolding set_conv_nth length_take min_absorb2[OF assms] by blast
  } hence "?R ⊆ ?L" by auto
  with * have *:"?L = ?R" by blast
  show ?thesis unfolding X_vars_def * by blast
qed

lemma set_drop_nth: "set (drop i xs) = {xs ! j | j. j ≥ i ∧ j < length xs}"
proof -
  {
    fix j
    have "i ≤ j ⟹ j < length xs ⟹ ∃ia. xs ! j = drop i xs ! ia ∧ ia < length xs - i"
      by (metis diff_less_mono le_add_diff_inverse less_or_eq_imp_le nth_drop)
  }
  thus ?thesis unfolding set_conv_nth by auto
qed

lemma Y_vars_alt : 
  assumes i: "i < length (snd ρ)"
  shows "Y_vars ρ i = vars_term (crhs ρ) ∪ 
    ⋃ {vars_term (fst (snd ρ ! j)) | j. i < j ∧ j < length (snd ρ)} ∪
    ⋃ {vars_term (snd (snd ρ ! j)) | j. i ≤ j ∧ j < length (snd ρ)}"
    (is "_ = ?A ∪ ?B ∪ ?C")
proof -  
  {
    fix x
    have "(x ∈ Y_vars ρ i) = (x ∈ ?A ∨ x ∈ vars_term (snd (snd ρ ! i)) 
      ∨ x ∈ vars_trs (set (drop (Suc i) (snd ρ))))" (is "_ = (_ ∨ x ∈ ?B' ∨ x ∈ ?C')") 
      unfolding Y_vars_def by auto
    also have "?C' = UNION (set (drop (Suc i) (snd ρ))) vars_rule" unfolding vars_trs_def by auto
    also have "set (drop (Suc i) (snd ρ)) = {snd ρ ! j | j. j ≥ Suc i ∧ j < length (snd ρ)}"
      (is "_ = ?C''") unfolding set_drop_nth ..
    also have "(x ∈ ?B' ∨ x ∈ UNION ?C'' vars_rule) = (x ∈ ?B ∪ ?C)" 
    proof -
      {
        assume "x ∈ ?B'"
        hence "x ∈ ?C" using i by auto
      } moreover {
        assume "x ∈ UNION ?C'' vars_rule"
        then obtain j where "x ∈ vars_rule (snd ρ ! j)" 
          and *: "j > i" "j ≥ i" "j < length (snd ρ)" by auto
        hence "x ∈ vars_term (fst (snd ρ ! j)) ∪ vars_term (snd (snd ρ ! j))" 
          by (auto simp: vars_rule_def)
        with * have "x ∈ ?B ∪ ?C" by blast
      } moreover {
        assume "x ∈ ?B"
        then obtain j where "x ∈ vars_term (fst (snd ρ ! j))" 
          and *: "Suc i ≤ j" "j < length (snd ρ)" by auto
        hence "x ∈ vars_rule (snd ρ ! j)" 
          by (auto simp: vars_rule_def)
        with * have "x ∈ UNION ?C'' vars_rule" by blast
      } moreover {
        assume "x ∈ ?C"
        then obtain j where xx: "x ∈ vars_term (snd (snd ρ ! j))" 
          and *: "i ≤ j" "j < length (snd ρ)" by auto
        hence x: "x ∈ vars_rule (snd ρ ! j)" 
          by (auto simp: vars_rule_def)
        have "x ∈ ?B' ∪ UNION ?C'' vars_rule"
        proof (cases "j = i")
          case False
          with * have "Suc i ≤ j" by auto
          with * x show ?thesis by blast
        qed (insert xx, auto)
      }
      ultimately show ?thesis by blast
    qed
    finally have "(x ∈ Y_vars ρ i) = (x ∈ ?A ∪ ?B ∪ ?C)" by auto
  }
  thus ?thesis by blast
qed
   
definition type3 :: "('f, 'v) ctrs ⇒ bool"
where
  "type3 R ⟷ (∀ ρ ∈ R. vars_term (crhs ρ) ⊆ (vars_term (clhs ρ) ∪ vars_trs (set (snd ρ))))"

definition dctrs :: "('f, 'v) ctrs ⇒ bool"
where
  "dctrs R ⟷ (∀ ρ ∈ R. ∀ i < length (snd ρ). vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i)"

definition wf_ctrs :: "('f, 'v) ctrs ⇒ bool"
where
  "wf_ctrs R ⟷ (∀((l, r), cs) ∈ R. is_Fun l) ∧ type3 R ∧ dctrs R"

definition funs_crule :: "('f, 'v) crule ⇒ 'f set"
where
  "funs_crule ρ = funs_rule (fst ρ) ∪ funs_trs (set (snd ρ))"

definition funas_crule :: "('f, 'v) crule ⇒ ('f × nat) set"
where
  "funas_crule ρ = funas_rule (fst ρ) ∪ funas_trs (set (snd ρ))"

definition funs_ctrs :: "('f, 'v) ctrs ⇒ 'f set"
where
  "funs_ctrs R = ⋃(funs_crule ` R)"

definition funas_ctrs :: "('f, 'v) ctrs ⇒ ('f × nat) set"
where
  "funas_ctrs R = ⋃(funas_crule ` R)"

definition vars_crule :: "('f, 'v) crule ⇒ 'v set"
where
  "vars_crule ρ = vars_rule (fst ρ) ∪ vars_trs (set (snd ρ))"

definition vars_ctrs :: "('f, 'v) ctrs ⇒ 'v set"
where
  "vars_ctrs R = ⋃(vars_crule ` R)"

text ‹The underlying unconditional TRS›
definition Ru :: "('f, 'v) ctrs ⇒ ('f, 'v) trs"
where
  "Ru R = fst ` R"

lemma defined_R_imp_Ru: "root l = Some fn ⟹ ((l, r), cs) ∈ R ⟹ defined (Ru R) fn"
  by (force simp: Ru_def defined_def)
  
lemma cstep_imp_Ru_step: "(cstep R) ⊆ (rstep (Ru R))"
proof
 fix s t
 assume "(s,t) ∈ cstep R"
 with cstep_iff cstep_n.simps(1) obtain n where n:"(s,t) ∈ cstep_n R (Suc n)"
  by (metis empty_iff not0_implies_Suc)
 hence "∃C l r σ cs. (s,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∧ ((l,r),cs) ∈ R" unfolding Ru_def cstep_n.simps(2) by fast
 hence *:"∃C l r σ. (s,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∧ (l,r) ∈ Ru R" unfolding Ru_def by force
 with rule rstep_r_p_s_imp_rstep * rstep_r_p_s_def show "(s,t) ∈ rstep (Ru R)" by fast
qed

lemma Ru_NF_imp_R_NF: "t ∈ NF (rstep (Ru R)) ⟹ t ∈ NF (cstep R)"
using NF_anti_mono [OF cstep_imp_Ru_step] by blast

lemma funas_ctrs_cond:
 assumes rho:"ρ ∈ R" and i:"i < length (snd ρ)" shows "funas_rule (snd ρ ! i) ⊆ funas_ctrs R"
   using assms funas_crule_def unfolding funas_ctrs_def funas_trs_def set_conv_nth by blast

lemma wf_ctrs_steps_preserves_funas:
 assumes wf: "wf_ctrs R" and s: "funas_term s ⊆ F" and R: "funas_ctrs R ⊆ F"
   and st:"(s, t) ∈ (cstep R)*"
 shows "funas_term t ⊆ F"
proof- 
 from wf[unfolded wf_ctrs_def] have t3:"type3 R" and dctrs:"dctrs R" by auto
 let ?rfuns = "λ v. funas_term v ⊆ F"
 from rtrancl_power csteps_imp_csteps_n[OF st]  obtain n k where st':"(s,t) ∈ (cstep_n R n) ^^ k" by blast
 let ?P = "λ (n,k). ∀ s t. ?rfuns s ⟶ (s,t) ∈ (cstep_n R n) ^^ k ⟶ ?rfuns t"
 have "?P (n,k)" proof(induct rule: wf_induct[OF wf_measures, of "[fst, snd]" ?P])
  case (1 nk) note ind = this
   obtain n k where nk: "nk = (n,k)" by force
   { fix s t
     assume s:"?rfuns s" and st:"(s, t) ∈ (cstep_n R n) ^^ k"
     hence "?rfuns t" proof(cases k)
      case 0
       with s st show ?thesis by simp
      next
      case (Suc m)
       from relpow_Suc_E[OF st[unfolded Suc]] obtain u where u:"(s,u) ∈ (cstep_n R n) ^^ m" "(u,t) ∈ cstep_n R n" by blast 
       have "((n,m), nk) ∈ measures [fst, snd]" unfolding nk Suc by auto
       from ind[rule_format, OF this, unfolded split, rule_format, OF s u(1)] have fu:"?rfuns u" by auto
       show ?thesis proof (cases n)
        case 0
         from u(2)[unfolded 0 cstep_n.simps] show ?thesis by auto
        next
        case (Suc n)
          from u(2)[unfolded Suc cstep_n.simps] obtain C l r σ cs where step:"(u,t) = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩)"
           "((l, r), cs) ∈ R" "∀(si, ti)∈set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*" by force
          from this(1) fu have fl:"?rfuns (l ⋅ σ)" by auto
          with supteq_imp_funas_term_subset supteq_Var
            have fx:"⋀x. x ∈ vars_term l ⟹ ?rfuns (σ x)" by fastforce
          { fix i
            assume i:"i < length cs"
            let ?stm = " λ m. (fst (cs ! m) ⋅ σ, snd (cs ! m) ⋅ σ)"
            from i have "funas_rule (?stm i) ⊆ F" proof (induct i rule:nat_less_induct)
             fix i
             assume ind2:"∀m<i. (m < length cs ⟶ funas_rule (?stm m) ⊆ F)" and i:"i < length cs"
             from dctrs[unfolded dctrs_def, rule_format, OF step(2), of i] i have 
              vs:"vars_term (fst (cs ! i)) ⊆ vars_term l ∪ X_vars ((l, r), cs) i" by auto
             { fix j x
               assume "x ∈ ⋃(vars_term ` rhss (set (take i cs)))" 
               hence "∃j. j < i ∧ x ∈ vars_term (snd (cs ! j))" unfolding set_conv_nth using nth_take[of _ i cs] by fastforce
               then obtain j where j:"j < i" and x:"x ∈ vars_term (snd (cs ! j))" by blast
               from ind2[rule_format, OF j] i j have "funas_term (snd (cs ! j) ⋅ σ) ⊆ F" unfolding funas_rule_def by auto
               with x supteq_imp_funas_term_subset supteq_Var have "?rfuns (σ x)" by fastforce
             } note vt = this
             { fix x assume "x ∈ vars_term (fst (cs ! i))"
               with vs[unfolded X_vars_def] fx vt have "?rfuns (σ x)" by auto
             }
             with funas_ctrs_cond[OF step(2), unfolded snd_conv, OF i] R have lhs:"?rfuns (fst (cs ! i) ⋅ σ)" 
              unfolding funas_term_subst funas_rule_def by blast
             from i have "(fst (cs ! i), snd (cs ! i)) ∈ set cs" by auto
             from  step(3)[rule_format, OF this, unfolded split] obtain l where 
              st:"(fst (cs ! i) ⋅ σ, snd (cs ! i) ⋅ σ) ∈ (cstep_n R n) ^^ l" unfolding rtrancl_power by blast
             have "((n,l), nk) ∈ measures [fst, snd]" unfolding nk Suc by auto
             from ind[rule_format, OF this, unfolded split, rule_format, OF lhs st]
               have rhs:"funas_term (snd (cs ! i) ⋅ σ) ⊆ F" by auto
             from lhs rhs show "funas_rule (?stm i) ⊆ F" unfolding funas_rule_def by auto
            qed
          } note aux = this
          from t3[unfolded type3_def, rule_format, OF step(2)] 
           have vr:"vars_term r ⊆ vars_term l ∪ vars_trs (set cs )" by auto
           from funas_rule_def[of "(l,r)"] have "funas_term r ⊆ funas_crule ((l, r), cs)" unfolding funas_crule_def by auto
           with  step(2) have fr:"funas_term r ⊆ funas_ctrs R" unfolding funas_ctrs_def by auto
          { fix j x
            assume j:"j < length cs" and "x ∈ vars_rule (cs ! j)"
            with supteq_Var have "fst (cs ! j) ⊵ Var x ∨ snd (cs ! j) ⊵ Var x" unfolding vars_rule_def by fastforce
            hence x:"fst (cs ! j) ⋅ σ ⊵ Var x ⋅ σ ∨ snd (cs ! j) ⋅ σ ⊵ Var x ⋅ σ" by auto
            from aux j have "funas_rule (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ⊆ F" unfolding funas_rule_def by auto
            with x supteq_imp_funas_term_subset  have "?rfuns (σ x)" unfolding funas_rule_def by force
          }
          with vr[unfolded set_conv_nth vars_trs_def] fx have "⋀x. x ∈ vars_term r ⟹ ?rfuns (σ x)" by blast
          with step(2) fr R have lhs:"?rfuns (r ⋅ σ)" unfolding funas_term_subst funas_rule_def by blast
          from step(1) have t:"t = C⟨r ⋅ σ⟩" and u:"u = C⟨l ⋅ σ⟩" by (fast,fast)
          from lhs fu show "?rfuns t" unfolding t u by auto
         qed
      qed
   }
   thus ?case unfolding nk split by blast
 qed
 from this[unfolded split, rule_format, OF s st'] show ?thesis by auto
qed

lemma funs_crule_funas_crule:
  "funs_crule r = fst ` funas_crule r" 
  unfolding funs_crule_def funas_crule_def  funs_trs_funas_trs funs_rule_funas_rule by blast

lemma funs_ctrs_funas_ctrs:
  "funs_ctrs R = fst ` funas_ctrs R" 
proof -
 from funs_crule_funas_crule have "⋃(funs_crule ` R) = ⋃(((λx. fst ` x) ∘ funas_crule) ` R)" by (metis comp_apply)
 thus ?thesis unfolding funs_ctrs_def funas_ctrs_def image_Union by force
qed

lemma wf_ctrs_steps_preserves_funs:
  assumes wf: "wf_ctrs R" and s: "funs_term s ⊆ F"
    and R: "funs_ctrs R ⊆ F" and st: "(s, t) ∈ (cstep R)*"
  shows "funs_term t ⊆ F"
proof -
  from s R wf_ctrs_steps_preserves_funas[OF wf _ _ st, of "F × UNIV"]
  show ?thesis unfolding funs_term_funas_term funs_ctrs_funas_ctrs by fastforce
qed

lemma cstep_map_funs_term:
  assumes R: "⋀ f. f ∈ funs_ctrs R ⟹ h f = f" and "(s, t) ∈ cstep R"
  shows "(map_funs_term h s, map_funs_term h t) ∈ cstep R"
proof -
  let ?h = "map_funs_term h"
  from assms[unfolded cstep_def] obtain n where "(s,t) ∈ cstep_n R n" by auto
  hence "(?h s, ?h t) ∈ cstep_n R n"
  proof (induct n arbitrary: s t)
    case (Suc n)
    from cstep_n_SucE[OF Suc(2)]
      obtain C l r σ cs
      where rule: "((l,r), cs) ∈ R" and cs: "∀(si, ti)∈set cs. (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*" 
      and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" . 
    let  = "map_funs_subst h σ"
    note funs_defs = funs_ctrs_def funs_crule_def[abs_def] funs_rule_def[abs_def] funs_trs_def
    from rule have lr: "funs_term l ∪ funs_term r ⊆ funs_ctrs R" unfolding funs_defs
      by auto
    have hl: "?h l = l"
      by (rule funs_term_map_funs_term_id[OF R], insert lr, auto)
    have hr: "?h r = r"
      by (rule funs_term_map_funs_term_id[OF R], insert lr, auto)
    show ?case unfolding s t
      unfolding map_funs_subst_distrib map_funs_term_ctxt_distrib hl hr
    proof (rule cstep_n_SucI[OF rule _ refl refl], rule)
      fix si ti
      assume in_cs: "(si,ti) ∈ set cs"
      from in_cs rule have st: "funs_term si ∪ funs_term ti ⊆ funs_ctrs R" unfolding funs_defs by force
      have hs: "?h si = si"
        by (rule funs_term_map_funs_term_id[OF R], insert st, auto)
      have ht: "?h ti = ti"
        by (rule funs_term_map_funs_term_id[OF R], insert st, auto)
      from in_cs cs have steps: "(si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)*" by auto
      have "(?h (si ⋅ σ), ?h (ti ⋅ σ)) ∈ (cstep_n R n)*"
        by (rule rtrancl_map[OF Suc(1) steps])
      thus "(si ⋅ ?σ, ti ⋅ ?σ) ∈ (cstep_n R n)*" unfolding map_funs_subst_distrib hs ht .
    qed
  qed simp
  thus ?thesis unfolding cstep_def by auto
qed

definition normalized :: "('f, 'v) ctrs ⇒ ('f, 'v) subst ⇒ bool"
where
  "normalized R σ ⟷ (∀x. σ x ∈ NF (cstep R))"

lemma empty_subst_normalized:
  assumes "∀((l, r), cs) ∈ R. is_Fun l"
  shows "normalized R Var"
  by (simp add: Var_NF_cstep assms normalized_def)
  
definition "strongly_irreducible R t ⟷ (∀σ. normalized R σ ⟶ t ⋅ σ ∈ NF (cstep R))"

lemma strongly_irreducible_I [Pure.intro?]:
  assumes "⋀σ. normalized R σ ⟹ t ⋅ σ ∈ NF (cstep R)"
  shows "strongly_irreducible R t"
using assms by (auto simp add: strongly_irreducible_def)

lemma Var_strongly_irreducible_cstep:
  "∀ ((l, r), cs) ∈ R. is_Fun l ⟹ strongly_irreducible R (Var x)"
by (rule strongly_irreducible_I) (simp add: normalized_def)

lemma constructor_term_imp_strongly_irreducible:
  fixes t R
  assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
    and constr: "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f }"
  shows "strongly_irreducible R t"
using constr
proof (induction t)
  case (Var x)
  show ?case using varcond Var_strongly_irreducible_cstep[of R x] by simp
next
  case (Fun f ts)
  show ?case
  proof
    fix σ
    assume norm: "normalized R σ"
    show "Fun f ts ⋅ σ ∈ NF (cstep R)"
    proof
      fix s
      show "(Fun f ts ⋅ σ, s) ∉ cstep R"
      proof
        assume "(Fun f ts ⋅ σ, s) ∈ cstep R"
        with cstepE [of "Fun f ts ⋅ σ" s "R"] obtain C τ l r cs
        where "((l, r), cs) ∈ R" and "Fun f ts ⋅ σ = C⟨l ⋅ τ⟩" and "s = C⟨r ⋅ τ⟩"
        and "∀(si, ti)∈set cs. (si ⋅ τ, ti ⋅ τ) ∈ (cstep R)*" by auto
        from varcond ‹((l, r), cs) ∈ R› Ru_def have "is_Fun l" by fastforce
        show "False"
        proof (cases C)
          case (Hole)
          with ‹Fun f ts ⋅ σ = C⟨l ⋅ τ⟩› have "Fun f ts ⋅ σ = l ⋅ τ" by auto
          with ‹is_Fun l› ‹((l, r), cs) ∈ R›
            have "(f, length ts) ∈ {f. defined (Ru R) f}"
            using map_eq_imp_length_eq [of "λt. t ⋅ σ" ts]
            by (cases l) (force intro: defined_R_imp_Ru)+
          with Fun.prems show "False" by auto
        next
          case (More g lts D rts)
          {
            fix u
            assume "u ∈ set ts"
            then have "funas_term u ⊆ funas_term (Fun f ts)" by auto
            with Fun.prems have "funas_term u ⊆ funas_ctrs R - {f. defined (Ru R) f}" by auto
          }
          note * = this
          {
            fix u
            assume "u ∈ set ts"
            from * [OF this] and Fun.IH[OF this]
            have "strongly_irreducible R u" by auto
          }
          note IH = this
          from More ‹Fun f ts ⋅ σ = C⟨l ⋅ τ⟩› have "map (λt. t ⋅ σ) ts = lts @ D⟨l ⋅ τ⟩ # rts" by simp
          then obtain u where u: "u ∈ set ts" and "u ⋅ σ = D⟨l ⋅ τ⟩"
            by (induct ts arbitrary: lts rts) (auto simp: Cons_eq_append_conv)
          then have "u ⋅ σ ⊵ l ⋅ τ" by simp
          then show "False"
          proof (cases rule: supteq_subst_cases)
            note supteq_imp_funas_term_subset [simp del]
            case (in_term v)
            with ‹is_Fun l› and * [OF u] and defined_R_imp_Ru[OF _ ‹((l, r), cs) ∈ R›]
            show ?thesis
            using supteq_imp_funas_term_subset [OF ‹u ⊵ v›] and map_eq_imp_length_eq
            by (cases l; cases v) (fastforce)+
          next
            have "(l ⋅ τ, r ⋅ τ) ∈ cstep R" by (rule cstepI [of _ _ _ _ _ _ ], fact+) (simp_all)
            moreover
            case (in_subst x)
            ultimately show ?thesis using norm NF_cstep_subterm[of "σ x" R "l ⋅ τ"]
              by (auto simp: normalized_def)
          qed
        qed
      qed
    qed
  qed
qed

lemma strongly_irreducible_imp_NF:
  assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
    and si: "strongly_irreducible R t"
  shows "t ∈ NF (cstep R)"
by (metis empty_subst_normalized si strongly_irreducible_def subst_apply_term_empty vc)

lemma constructor_term_NF_cstep:
  assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
    and  constr: "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f}"
  shows "t ∈ NF (cstep R)"
by (auto simp: assms constructor_term_imp_strongly_irreducible strongly_irreducible_imp_NF)

lemma ground_Ru_NF_imp_strongly_irreducible:
  assumes varcond: "∀((l, r), cs) ∈ R. is_Fun l"
    and ground: "ground t"
    and ru_nf: "t ∈ NF (rstep (Ru R))"
  shows "strongly_irreducible R t"
using ground ru_nf
proof (induction t)
  case (Fun f ts)
  from Fun.prems(1) have "∀σ. Fun f ts ⋅ σ = Fun f ts"
  using ground_subst_apply by blast
  then show ?case
    using Fun.prems(2) Ru_NF_imp_R_NF [of "Fun f ts" R] strongly_irreducible_I[of R "Fun f ts"]
    by fastforce
qed simp

context
  fixes R :: "('f, 'v) ctrs"
  assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
begin

lemma syntactic_det_imp_strong_det:
  assumes "(∀ ((l, r), cs) ∈ R. ∀ (si, ti) ∈ set cs.
    ((funas_term ti ⊆ ((funas_ctrs R) - { f. defined (Ru R) f }) ∨
    (ground ti ∧ ti ∈ NF (rstep (Ru R))))))"
  shows str_det: "(∀ ((l, r), cs) ∈ R. ∀ (si, ti) ∈ set cs. strongly_irreducible R ti)"
proof -
  {
    fix l r cs si ti
    assume "((l, r), cs) ∈ R" and "(si, ti) ∈ set cs"
    moreover
    {
      assume *: "funas_term ti ⊆ funas_ctrs R - { f. defined (Ru R) f }"
      from vc have **: "∀((l, r), cs) ∈ R. is_Fun l" by auto
      have "strongly_irreducible R ti"
        using constructor_term_imp_strongly_irreducible [OF ** *] by auto
    }
    moreover
    {
      assume "ground ti ∧ ti ∈ NF (rstep (Ru R))"
      then have "strongly_irreducible R ti"
        using ground_Ru_NF_imp_strongly_irreducible
        by (simp add: Ru_NF_imp_R_NF ground_subst_apply strongly_irreducible_I)
    }
    ultimately
    have "strongly_irreducible R ti" using assms by fastforce
  }
  then show ?thesis by force
qed

end

lemma Var_cstep_n [dest]:
  assumes "(Var x, t) ∈ cstep_n R n"
    and "∀((l, r), cs) ∈ R. is_Fun l"
  shows "False"
using assms by (auto simp: elim!: cstep_nE) (case_tac C; case_tac l; force)

lemma Var_rtrancl_cstep_n [dest]:
  assumes "(Var x, t) ∈ (cstep_n R n)*"
    and "∀((l, r), cs) ∈ R. is_Fun l"
  shows "t = Var x"
using assms by (induct) auto


subsection ‹TRS for level @{term n}.›

fun trs_n :: "('f, 'v) ctrs ⇒ nat ⇒ ('f, 'v) trs"
where
  "trs_n R 0 = {}" |
  "trs_n R (Suc n) =
    {(l ⋅ σ, r ⋅ σ) | l r σ cs.
      ((l, r), cs) ∈ R ∧ (∀ (si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (rstep (trs_n R n))*)}"

lemma trs_n_SucI:
  assumes "((l, r), cs) ∈ R"
    and "⋀si ti. (si, ti) ∈ set cs ⟹ (si ⋅ σ, ti ⋅ σ) ∈ (rstep (trs_n R n))*"
  shows "(l ⋅ σ, r ⋅ σ) ∈ trs_n R (Suc n)"
  using assms by (simp) blast

lemma trs_nE:
  assumes "(s, t) ∈ trs_n R n"
  obtains l r σ cs n' where "n = Suc n'" and "s = l ⋅ σ" and "t = r ⋅ σ" and "((l, r), cs) ∈ R"
    and "∀ (si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (rstep (trs_n R n'))*"
  using assms by (cases n; simp) blast

lemma trs_n_SucE:
  assumes "(s, t) ∈ trs_n R (Suc n)"
  obtains l r σ cs where "s = l ⋅ σ" and "t = r ⋅ σ" and "((l, r), cs) ∈ R"
    and "∀ (si, ti) ∈ set cs. (si ⋅ σ, ti ⋅ σ) ∈ (rstep (trs_n R n))*"
  using assms by (simp) blast

declare trs_n.simps(2) [simp del]

lemma trs_n_subst:
  assumes "(l, r) ∈ trs_n R n"
  shows "(l ⋅ σ, r ⋅ σ) ∈ trs_n R n"
using assms
proof (induction n)
  case (Suc n)
  from Suc.prems obtain l' r' σ' cs
    where [simp]: "l = l' ⋅ σ'" "r = r' ⋅ σ'" and "((l', r'), cs) ∈ R"
    and "∀(si, ti) ∈ set cs. (si ⋅ σ', ti ⋅ σ') ∈ (rstep (trs_n R n))*"
    by (auto elim: trs_n_SucE)
  moreover then have "∀(si, ti) ∈ set cs.
    (si ⋅ (σ' ∘s σ), ti ⋅ (σ' ∘s σ)) ∈ (rstep (trs_n R n))*" by (auto intro: rsteps_closed_subst)
  ultimately have "(l' ⋅ (σ' ∘s σ), r' ⋅ (σ' ∘s σ)) ∈ trs_n R (Suc n)"
    by (blast intro: trs_n_SucI)
  then show ?case by simp
qed simp

lemma no_step_from_constructor:
  assumes vc: "∀((l, r), cs) ∈ R. is_Fun l"
    and "funas_term t ⊆ funas_ctrs R - { f. defined (Ru R) f }"
    and fp: "p ∈ funposs t"
  shows "(t ⋅ σ |_ p, u) ∉ trs_n R n"
proof
  assume "(t ⋅ σ |_ p, u) ∈ trs_n R n"
  from trs_nE [OF this] obtain l r τ cs where *: "((l, r), cs) ∈ R" and **: "t ⋅ σ |_ p = l ⋅ τ"
    by metis
  then obtain f ts where [simp]: "l = Fun f ts" using vc by (cases l, auto)
  have "defined (Ru R) (f, length ts)" using * by (intro defined_R_imp_Ru) (auto)
  moreover from fp ** have "(f, length ts) ∈ funas_term t"
  proof -
    from funposs_fun_conv [OF fp] obtain g ss where ***: "t |_ p = Fun g ss" by blast
    with funposs_imp_poss [OF fp] have "t ⋅ σ |_ p = Fun g (map (λx. x ⋅ σ) ss)" by auto
    then have [simp]: "g = f" "length ts = length ss" using ** map_eq_imp_length_eq by (force)+
    from *** funposs_imp_poss [OF fp] show ?thesis by (auto simp add: funas_term_poss_conv)   
  qed
  ultimately show "False" using assms(2) by blast
qed

lemma cstep_n_rstep_trs_n_conv:
  "cstep_n R n = rstep (trs_n R n)"
proof (induction n)
  case (Suc n)
  { fix s t
    assume "(s, t) ∈ cstep_n R (Suc n)"
    then have "(s, t) ∈ rstep (trs_n R (Suc n))"
      by (auto elim!: cstep_n_SucE simp: Suc split: prod.splits)
         (metis rstep.ctxt rstep.rule trs_n_SucI) }
  moreover
  { fix s t
    assume "(s, t) ∈ rstep (trs_n R (Suc n))"
    then obtain u v C σ where "(u, v) ∈ trs_n R (Suc n)"
      and [simp]: "s = C⟨u ⋅ σ⟩""t = C⟨v ⋅ σ⟩" ..
    then obtain l r cs τ where "((l, r), cs) ∈ R"
      and [simp]: "u = l ⋅ τ" "v = r ⋅ τ"
      and "∀(si, ti) ∈ set cs. (si ⋅ τ, ti ⋅ τ) ∈ (rstep (trs_n R n))*"
      by (auto elim: trs_n_SucE)
    moreover then have "∀(si, ti) ∈ set cs. (si ⋅ (τ ∘s σ), ti ⋅ (τ ∘s σ)) ∈ (cstep_n R n)*"
      by (auto intro: rsteps_closed_subst simp: Suc)
    ultimately have "(C⟨l ⋅ (τ ∘s σ)⟩, C⟨r ⋅ (τ ∘s σ)⟩) ∈ cstep_n R (Suc n)" by (blast intro: cstep_n_SucI)
    then have "(s, t) ∈ cstep_n R (Suc n)" by simp }
  ultimately show ?case by auto
qed simp

lemma trs_n_Suc_mono:
  "trs_n R n ⊆ trs_n R (Suc n)"
proof (induct n)
  case (Suc n)
  then have "rstep (trs_n R n) ⊆ rstep (trs_n R (Suc n))" by (metis rstep_mono)
  from rtrancl_mono [OF this]
    show ?case by (auto elim!: trs_n_SucE intro!: trs_n_SucI)
qed simp

lemma rrstep_trs_n [simp]:
  "rrstep (trs_n R n) = trs_n R n"
  by (auto simp: CS_rrstep_conv [symmetric]
    elim: subst.closure.cases intro: subst.closureI2 [of _ _ _ _ Var] trs_n_subst)

lemma cstep_rstep_UN_trs_n_conv: "cstep R = rstep (⋃n. trs_n R n)"
by (auto simp: cstep_def cstep_n_rstep_trs_n_conv rstep_UN)

lemma Var_trs_n [dest]:
  assumes "(Var x, t) ∈ trs_n R n"
    and "∀((l, r), cs) ∈ R. is_Fun l"
  shows "False"
using assms by (induct n) (force elim!: trs_n_SucE split: prod.splits)+

lemma linear_term_cstep_n_cases':
  assumes "linear_term s"
    and cstep: "(s ⋅ σ, u) ∈ cstep_n R n"
  shows "(∃τ. s ⋅ τ = u ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)*)) ∨
    (∃p ∈ funposs s. (s ⋅ σ |_ p, u |_ p) ∈ trs_n R n)"
proof -
  from cstep [THEN cstep_nE] obtain C l r σ' cs k
    where rule: "((l, r), cs) ∈ R" and [simp]: "n = Suc k"
    and conds: "conds_n_sat R k cs σ'"
    and s_σ: "s ⋅ σ = C⟨l ⋅ σ'⟩" and u: "u = C⟨r ⋅ σ'⟩"
    unfolding conds_n_sat_iff by metis (*only metis works; investigate!*)
  define p where "p ≡ hole_pos C"
  have *: "p ∈ poss (s ⋅ σ)" by (simp add: assms s_σ p_def)
  show ?thesis
  proof (cases "p ∈ funposs s")
    case False
    with * obtain q1 q2 x
      where p: "p = q1 <#> q2" and q1: "q1 ∈ poss s"
      and lq1: "s |_ q1 = Var x" and q2: "q2 ∈ poss (σ x)"
        by (rule poss_subst_apply_term)
    moreover
    have [simp]: "s ⋅ σ |_ p = l ⋅ σ'" using assms p_def s_σ by auto 
    ultimately
    have [simp]: "σ x |_ q2 = l ⋅ σ'" by simp
    
    define τ where "τ ≡ λy. if y = x then replace_at (σ x) q2 (r ⋅ σ') else σ y"
    have τ_x: "τ x = replace_at (σ x) q2 (r ⋅ σ')" by (simp add: τ_def)
    have [simp]: "⋀y. y ≠ x ⟹ τ y = σ y" by (simp add: τ_def)
    have "(σ x, τ x) ∈ cstep_n R n"
    proof -
      let ?C = "ctxt_of_pos_term q2 (σ x)"
      have "(?C⟨l ⋅ σ'⟩, ?C⟨r ⋅ σ'⟩) ∈ cstep_n R n"
        using conds by (auto intro!: cstep_n_SucI rule simp: conds_n_sat_iff)
      then show ?thesis using q2 by (simp add: τ_def replace_at_ident)
    qed
    then have "∀x. (σ x, τ x) ∈ (cstep_n R n)*" by (auto simp: τ_def)
    moreover have "s ⋅ τ = u"
    proof -
      have [simp]: "ctxt_of_pos_term p (s ⋅ σ) = C" by (simp add: assms s_σ p_def)
      have "s ⋅ σ |_ q1 = σ x" by (simp add: lq1 q1)
      from linear_term_replace_in_subst [OF ‹linear_term s› q1 lq1, of σ τ, OF _ τ_x, folded ctxt_ctxt_compose]
        and q1 and ctxt_of_pos_term_append [of q1 "s ⋅ σ" q2, folded p, unfolded this, symmetric]
        show "s ⋅ τ = u" by (simp add: u)
    qed
    ultimately show ?thesis by blast
  next
    case True
    moreover have "(s ⋅ σ |_ p, u |_ p) ∈ trs_n R (Suc k)"
      using conds
      by (auto simp: conds_n_sat_iff p_def s_σ u
               intro: trs_n_SucI [OF rule] simp: cstep_n_rstep_trs_n_conv)
    ultimately show ?thesis by auto
  qed
qed

lemma linear_term_cstep_n_cases [consumes 2]:
  assumes "linear_term s"
    and "(s ⋅ σ, u) ∈ cstep_n R n"
  obtains (varposs) τ where "s ⋅ τ = u"
    and "∀x. (σ x, τ x) ∈ (cstep_n R n)*"
  | (funposs) p where "p ∈ funposs s" and "(s ⋅ σ |_ p, u |_ p) ∈ trs_n R n"
using linear_term_cstep_n_cases' [OF assms] by blast

lemma linear_term_rtrancl_cstep_n_cases':
  assumes "linear_term s"
    and "(s ⋅ σ, t) ∈ (cstep_n R n)*"
  shows "(∃τ. s ⋅ τ = t ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)*)) ∨
    (∃τ p u. (∀x. (σ x, τ x) ∈ (cstep_n R n)*) ∧
      p ∈ funposs s ∧ (s ⋅ τ |_ p, u) ∈ trs_n R n)"
using assms(2)
proof (induct)
  case base
  let  = "σ"
  have "s ⋅ σ = s ⋅ ?τ" using coincidence_lemma by blast
  moreover have "∀x. (σ x, ?τ x) ∈ (cstep_n R n)*" by auto
  ultimately show ?case by auto
next
  case (step t u)
  show ?case using step(3)
  proof
    assume "∃τ. s ⋅ τ = t ∧ (∀x. (σ x, τ x) ∈ (cstep_n R n)*)"
    then obtain τ where t: "t = s ⋅ τ" and *: "∀x. (σ x, τ x) ∈ (cstep_n R n)*" by blast
    then have "(s ⋅ τ, u) ∈ cstep_n R n" using ‹(t, u) ∈ cstep_n R n› by auto
    with ‹linear_term s›
      show ?thesis
      using * by (cases rule: linear_term_cstep_n_cases; blast dest: rtrancl_trans)
  qed blast
qed

lemma linear_term_rtrancl_cstep_n_cases [consumes 2]:
  assumes "linear_term s"
    and "(s ⋅ σ, t) ∈ (cstep_n R n)*"
  obtains (varposs) τ where "s ⋅ τ = t" and "∀x. (σ x, τ x) ∈ (cstep_n R n)*"
  | (funposs) τ p u where "∀x. (σ x, τ x) ∈ (cstep_n R n)*"
    and "p ∈ funposs s" and "(s ⋅ τ |_ p, u) ∈ trs_n R n"
using linear_term_rtrancl_cstep_n_cases' [OF assms] by blast

definition properly_oriented
where
  "properly_oriented R ⟷ (∀ρ ∈ R.
    vars_term (crhs ρ) ⊆ vars_term (clhs ρ) ∨
    (∀i < length (snd ρ). vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i))"

definition extended_properly_oriented
where
 "extended_properly_oriented R ⟷ (∀ρ ∈ R. vars_term (crhs ρ) ⊆ vars_term (clhs ρ) ∨
    (∃m ≤ length (snd ρ).
      (∀i < m. vars_term (fst (snd ρ ! i)) ⊆ X_vars ρ i) ∧
      (∀i∈{m ..< length (snd ρ)}. vars_term (crhs ρ) ∩ vars_rule (snd ρ ! i) ⊆ X_vars ρ m)))"

definition right_stable :: "('f, 'v) ctrs ⇒ bool"
where
  "right_stable R ⟷ (∀ ρ ∈ R. ∀ i < length (snd ρ).
    let ti = snd (snd ρ ! i) in
    (vars_term (clhs ρ) ∪ ⋃(vars_term ` lhss (set (take (Suc i) (snd ρ)))) ∪
    ⋃(vars_term ` (rhss (set (take i (snd ρ)))))) ∩ vars_term ti = {} ∧
    (linear_term ti ∧ funas_term ti ⊆ funas_ctrs R - { f. defined (Ru R) f } ∨
    ground ti ∧ ti ∈ NF (rstep (Ru R))))"

lemma right_stable_rhsD:
  assumes "right_stable R" and "ρ ∈ R" and "i < length (snd ρ)"
  shows "(vars_term (clhs ρ) ∪ ⋃(vars_term ` lhss (set (take (Suc i) (snd ρ)))) ∪
    ⋃(vars_term ` (rhss (set (take i (snd ρ)))))) ∩ vars_term (snd (snd ρ ! i)) = {}"
using assms by (auto simp: right_stable_def Let_def)

lemma right_stable_rhs_cases [consumes 3, case_names lct [linear cterm] gnf [ground nf]]:
  assumes "right_stable R" and "ρ ∈ R"
    and "t ∈ rhss (set (snd ρ))"
  obtains
    (lct) "linear_term t" and "funas_term t ⊆ funas_ctrs R - {f. defined (Ru R) f}" |
    (gnf) "ground t" and "t ∈ NF (rstep (Ru R))"
proof -
  obtain i where "i < length (snd ρ)" and "t = snd (snd ρ ! i)"
    using assms(3) by (auto dest: in_set_idx)
  with assms(1, 2) show ?thesis using lct and gnf by (auto simp: right_stable_def Let_def)
qed

lemma crule_cases:
  assumes "⋀l r cs. ρ = ((l, r), cs) ⟹ P"
  shows "P"
using assms by (cases ρ; auto)

lemma cstep_subst:
  assumes "(s, t) ∈ cstep R"
  shows "(s ⋅ σ, t ⋅ σ) ∈ cstep R"
using assms
by (auto simp: cstep_def dest: cstep_n_subst)

lemma subst_closed_cstep [intro]:
  "subst.closed (cstep R)"
using cstep_subst subst.closedI by blast

lemma cstep_ctxt:
  assumes "(s, t) ∈ cstep R"
  shows "(C⟨s⟩, C⟨t⟩) ∈ cstep R"
using assms
by (simp add: cstep_ctxt_closed ctxt.closedD)

lemma csteps_ctxt:
  assumes "(s, t) ∈ (cstep R)*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (cstep R)*"
using assms
by (simp add: cstep_ctxt_closed ctxt.closedD ctxt.closed_rtrancl)

abbreviation conds :: "('f, 'v) crule ⇒ ('f, 'v) rule list"
where
  "conds ρ ≡ snd ρ"

lemma conds_n_sat_mono':
  assumes "conds_n_sat R n cs σ"
    and "set ds ⊆ set cs"
  shows "conds_n_sat R n ds σ"
using assms by (auto simp: conds_n_sat_iff)

definition evars_crule :: "('f, 'v) crule ⇒ 'v set"
where "evars_crule ρ = vars_trs (set (conds ρ)) - vars_term (clhs ρ)"

lemmas args_csteps_imp_csteps = args_steps_imp_steps [OF cstep_ctxt_closed]

lemma substs_csteps:
  assumes "⋀x. (σ x, τ x) ∈ (cstep R)*"
  shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)*"
proof (induct t)
  case (Var y)
  show ?case using assms by simp_all
next
  case (Fun f ts)
  then have "∀i<length (map (λt. t ⋅ σ) ts).
    (map (λt. t ⋅ σ ) ts ! i, map (λt. t ⋅ τ) ts ! i) ∈ (cstep R)*" by auto
  from args_csteps_imp_csteps [OF _ this] show ?case by simp
qed

lemma term_subst_cstep:
  assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ cstep R" 
  shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)*"
using assms
proof (induct t)
  case (Fun f ts)
  { fix ti
    assume ti: "ti ∈ set ts"
    with Fun(2) have "⋀x. x ∈ vars_term ti ⟹ (σ x, τ x) ∈ cstep R" by auto
    from Fun(1) [OF ti this] have "(ti ⋅ σ, ti ⋅ τ) ∈ (cstep R)*" by blast
  }
  then show ?case by (simp add: args_csteps_imp_csteps) 
qed (auto)

lemma term_subst_csteps:
  assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ (cstep R)*" 
  shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)*"
using assms
proof (induct t)
  case (Fun f ts)
  { fix ti
    assume ti: "ti ∈ set ts"
    with Fun(2) have "⋀x. x ∈ vars_term ti ⟹ (σ x, τ x) ∈ (cstep R)*" by auto
    from Fun(1) [OF ti this] have "(ti ⋅ σ, ti ⋅ τ) ∈ (cstep R)*" by blast
  }
  then show ?case by (simp add: args_csteps_imp_csteps) 
qed (auto)

lemma term_subst_csteps_join:
  assumes "⋀y. y ∈ vars_term u ⟹ (σ1 y, σ2 y) ∈ (cstep R)"
  shows "(u ⋅ σ1, u ⋅ σ2) ∈ (cstep R)"
using assms
proof -
  { fix x
    assume "x ∈ vars_term u"
    from assms [OF this] have "∃σ. (σ1 x, σ x) ∈ (cstep R)* ∧ (σ2 x, σ x) ∈ (cstep R)*" by auto
  }
  then have "∀x ∈ vars_term u. ∃σ. (σ1 x, σ x) ∈ (cstep R)* ∧ (σ2 x, σ x) ∈ (cstep R)*" by blast
  then obtain s where "∀x ∈ vars_term u. (σ1 x, (s x) x) ∈ (cstep R)* ∧ (σ2 x, (s x) x) ∈ (cstep R)*" by metis
  then obtain σ where "∀x ∈ vars_term u. (σ1 x, σ x) ∈ (cstep R)* ∧ (σ2 x, σ x) ∈ (cstep R)*" by fast
  then have "(u ⋅ σ1, u ⋅ σ) ∈ (cstep R)* ∧ (u ⋅ σ2, u ⋅ σ) ∈ (cstep R)*" using term_subst_csteps by metis
  then show ?thesis by blast 
qed

lemma subst_csteps_imp_csteps:
  fixes σ :: "('f, 'v) subst"
  assumes "∀x∈vars_term t. (σ x, τ x) ∈ (cstep R)*"
  shows "(t ⋅ σ, t ⋅ τ) ∈ (cstep R)*"
  by (rule all_ctxt_closed_subst_step)
     (insert assms, auto)

lemma replace_at_subst_csteps:
  fixes σ τ :: "('f, 'v) subst"
  assumes *: "⋀x. (σ x, τ x) ∈ (cstep R)*"
    and "p ∈ poss t"
    and "t |_ p = Var x"
  shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ (cstep R)*"
using assms(2-)
proof (induction t arbitrary: p)
  case (Fun f ts)
  then obtain i q where [simp]: "p = i <# q" and i: "i < length ts"
    and q: "q ∈ poss (ts ! i)" and [simp]: "ts ! i |_ q = Var x" by (cases p) auto
  let ?C = "ctxt_of_pos_term q (ts ! i ⋅ σ)"
  let ?ts = "map (λt. t ⋅ τ) ts"
  let ?ss = "take i (map (λt. t ⋅ σ) ts) @ ?C⟨τ x⟩ # drop (Suc i) (map (λt. t ⋅ σ) ts)"
  have "∀j<length ts. (?ss ! j, ?ts ! j) ∈ (cstep R)*"
  proof (intro allI impI)
    fix j
    assume j: "j < length ts"
    moreover
    { assume [simp]: "j = i"
      have "?ss ! j = ?C⟨τ x⟩" using i by (simp add: nth_append_take)
      with Fun.IH [of "ts ! i" q]
      have "(?ss ! j, ?ts ! j) ∈ (cstep R)*" using q and i by simp }
    moreover
    { assume "j < i"
      with i have "?ss ! j = ts ! j ⋅ σ"
        and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_take_is_nth_conv)
      then have "(?ss ! j, ?ts ! j) ∈ (cstep R)*" by (auto simp: * subst_csteps_imp_csteps) }
    moreover
    { assume "j > i"
      with i and j have "?ss ! j = ts ! j ⋅ σ"
        and "?ts ! j = ts ! j ⋅ τ" by (simp_all add: nth_append_drop_is_nth_conv)
      then have "(?ss ! j, ?ts ! j) ∈ (cstep R)*" by (auto simp: * subst_csteps_imp_csteps) }
    ultimately show "(?ss ! j, ?ts ! j) ∈ (cstep R)*" by arith
  qed
  moreover have "i < length ts" by fact
  ultimately show ?case
    by (simp add: args_csteps_imp_csteps)
qed simp

fun map_funs_crule :: "('f ⇒ 'g) ⇒ ('f, 'v) crule ⇒ ('g, 'v) crule"
where
  "map_funs_crule f r = ((map_funs_term f (clhs r), map_funs_term f (crhs r)), map (map_funs_rule f) (conds r))"

lemma map_funs_crule_id [simp]: "map_funs_crule id = id" by auto

fun map_funs_ctrs :: "('f ⇒ 'g) ⇒ ('f, 'v) ctrs ⇒ ('g, 'v) ctrs"
where
  "map_funs_ctrs f R = map_funs_crule f ` R"

lemma conds_sat_Cons:
  "conds_sat R (c # cs) σ ⟷ (fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep R)* ∧ conds_sat R cs σ"
by (auto simp: conds_sat_iff)

lemma conds_n_sat_Cons:
  "conds_n_sat R n (c # cs) σ ⟷
    (fst c ⋅ σ, snd c ⋅ σ) ∈ (cstep_n R n)* ∧ conds_n_sat R n cs σ"
by (auto simp: conds_n_sat_iff)

lemma conds_sat_conds_n_sat:
  "conds_sat R cs σ ⟷ (∃n. conds_n_sat R n cs σ)" (is "?P = ?Q")
proof
  assume "?Q" then show "?P"
    by (auto simp: conds_sat_iff conds_n_sat_iff dest: csteps_n_imp_csteps)
next
  assume "?P" then show "?Q"
  proof (induct cs)
    case (Cons c cs)
    then show ?case
      apply (auto simp: conds_sat_Cons conds_n_sat_Cons dest!: csteps_imp_csteps_n)
      apply (rule_tac x = "max n na" in exI)
      apply (auto simp: max_def conds_n_sat_iff conds_sat_iff
        dest!: csteps_n_mono)
      apply (rule_tac m1 = na and n1 = n in csteps_n_mono [THEN subsetD])
      apply force+
      done
  qed simp
qed

subsection ‹Permutation Types for Conditional Rules and CTRSs›

interpretation crule_pt: prod_pt rule_pt.permute_prod rules_pt.permute_list ..

adhoc_overloading
  PERMUTE crule_pt.permute_prod and
  FRESH crule_pt.fresh crule_pt.fresh_set

interpretation ctrs_pt: set_pt crule_pt.permute_prod ..

adhoc_overloading
  PERMUTE ctrs_pt.permute_set and
  FRESH ctrs_pt.fresh

lemma finite_crule_supp:
  "finite (crule_pt.supp ((l, r), cs))"
  by (simp add: finite_term_supp rule_fs.finite_supp)

interpretation crule_fs: finitely_supported crule_pt.permute_prod
  by standard (auto simp: finite_rule_supp finite_term_supp)

lemma conds_n_sat_perm_shift:
  "conds_n_sat R n (π ∙ cs) σ = conds_n_sat R n cs (σ ∘ Rep_perm π)"
by (auto simp: conds_n_sat_iff permute_term_subst_apply_term eqvt split: prod.splits)

lemma supp_vars_crule_eq:
  fixes r :: "('f, 'v :: infinite) crule"
  shows "crule_pt.supp r = vars_crule r"
by (cases r; auto simp: vars_crule_def vars_trs_def supp_vars_term_eq vars_rule_def)

lemma vars_crule_disjoint:
  fixes l r u v :: "('f, 'v :: infinite) term"
    and cs ds :: "('f, 'v) rule list"
  shows "∃p. vars_crule (p ∙ ((l, r), cs)) ∩ vars_crule ((u, v), ds) = {}"
proof -
  from crule_fs.supp_fresh_set obtain p
    where "crule_pt.supp (p ∙ ((l, r), cs)) ♯ ((u, v), ds)" by blast
  from crule_pt.fresh_set_disjoint [OF this]
    show ?thesis
    by (auto simp: supp_vars_crule_eq vars_rule_def)
qed

lemma X_vars_eqvt [eqvt]:
  "p ∙ X_vars r i = X_vars (p ∙ r) i"
proof -
  have "take i (snd (p ∙ r)) = p ∙ take i (snd r)"
    by (metis (no_types, hide_lams) crule_pt.snd_eqvt rules_pt.permute_list_def take_map)
  then show ?thesis
    by (simp_all add: X_vars_def eqvt)
qed

lemma variant_conds_n_sat_cstep_n:
  assumes "π ∙ ρ ∈ R"
    and "conds_n_sat R n (conds ρ) σ"
  shows "(clhs ρ ⋅ σ, crhs ρ ⋅ σ) ∈ cstep_n R (Suc n)"
proof -
  from assms(1) have r: "((π ∙ clhs ρ, π ∙ crhs ρ), π ∙ conds ρ) ∈ R"
    by (simp add: eqvt split: prod.split)
       (metis crule_pt.snd_eqvt prod.collapse rules_pt.permute_list_def)
  from assms(2) have "conds_n_sat R n (- π ∙ π ∙ conds ρ) σ"
    by (metis rules_pt.permute_minus_cancel(2))
  from conds_n_sat_perm_shift [THEN iffD1, OF this]
    have "conds_n_sat R n (π ∙ conds ρ) (σ ∘ Rep_perm (- π))" (is "conds_n_sat _ _ _ ?τ") by auto
  from conds_n_sat_iff [THEN iffD1, OF this]
    have "∀(si, ti)∈set (π ∙ conds ρ). (si ⋅ ?τ, ti ⋅ ?τ) ∈ (cstep_n R n)*" .
  from cstep_n_SucI [OF r this, of _ ]
    have "(π ∙ clhs ρ ⋅ ?τ, π ∙ crhs ρ ⋅ ?τ) ∈ cstep_n R (Suc n)" by force
  then have "(clhs ρ ⋅ (sop π ∘s ?τ), crhs ρ ⋅ (sop π ∘s ?τ)) ∈ cstep_n R (Suc n)" by simp
  then show ?thesis
    by (metis (no_types, lifting) permute_term_subst_apply_term subst_subst
        term_apply_subst_Var_Rep_perm term_pt.permute_minus_cancel(2))
qed

lemma variant_conds_sat_cstep:
  assumes "π ∙ ρ ∈ R"
    and "conds_sat R (conds ρ) σ"
  shows "(clhs ρ ⋅ σ, crhs ρ ⋅ σ) ∈ cstep R"
using assms conds_sat_conds_n_sat cstep_n_imp_cstep variant_conds_n_sat_cstep_n by blast

lemma rsteps_eqvt:
  "π ∙ (rstep R)* = (rstep (π ∙ R))*"
using rstep_eqvt [of π R]
by (metis permute_rstep rstep_rtrancl_idemp)

lemma trs_n_eqvt_aux:
  "π ∙ (trs_n (-π ∙ R) n) = trs_n R n"
proof (induct n)
  case (Suc n)
  then have IH: "π ∙ (trs_n (-π ∙ R) n) = trs_n R n" by blast
  show ?case
  proof (intro equalityI subrelI, goal_cases)
    case (1 s t)
    then have "(-π ∙ s, -π ∙ t) ∈ trs_n (-π ∙ R) (Suc n)"
      using inv_rule_mem_trs_simps(1) by blast
    then show ?case unfolding trs_n.simps apply (simp add: IH [symmetric])
      apply auto
      apply (rule_tac x = "π ∙ l" in exI)
      apply (rule_tac x = "π ∙ r" in exI)
      apply (rule_tac x = "sop (-π) ∘s σ ∘s sop π" in exI)
      apply (auto simp:)
      apply (metis term_pt.permute_minus_cancel(1))
      apply (metis term_pt.permute_minus_cancel(1))
      apply (rule_tac x = "π ∙ cs" in exI)
      apply (auto simp: eqvt)
      by (metis (no_types, lifting) case_prodD rstep_imp_perm_rstep rstep_rtrancl_idemp term_apply_subst_eqvt)
  next
    case (2 s t)
    then have "(-π ∙ s, -π ∙ t) ∈ trs_n (-π ∙ R) (Suc n)"
      apply (auto simp: trs_n.simps(2))
      apply (rule_tac x = "-π ∙ l" in exI)
      apply (rule_tac x = "-π ∙ r" in exI)
      apply (rule_tac x = "sop π ∘s σ ∘s sop (-π)" in exI)
      apply auto
      apply (rule_tac x = "-π ∙ cs" in exI)
      apply (auto simp: eqvt map_idI rsteps_eqvt IH)
      by force
    then show ?case using inv_rule_mem_trs_simps(1) by blast
  qed
qed simp

lemma rstep_perm_trs_n:
  shows "rstep (π ∙ (trs_n R n)) = rstep (trs_n (π ∙ R) n)"
using trs_n_eqvt_aux [of "-π" R n]
apply (simp)
by (metis rstep_permute)

lemma cstep_permute:
  "cstep (π ∙ R) = cstep R"
proof -
  have "cstep (π ∙ R) = (⋃n. rstep (trs_n (π ∙ R) n))"
    by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
  also have "… = (⋃n. rstep (π ∙ (trs_n R n)))" unfolding rstep_perm_trs_n ..
  also have "… = (⋃n. rstep (trs_n R n))" unfolding rstep_permute ..
  also have "… = cstep R" by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
  finally show ?thesis .
qed

lemma cstep_eqvt [eqvt]:
  "π ∙ cstep R = cstep (π ∙ R)"
proof -
  have "π ∙ cstep R = π ∙ (⋃n. rstep (trs_n R n))"
    by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
  also have "… = (⋃n. rstep (π ∙ (trs_n R n)))" by (auto simp: eqvt)
  also have "… = (⋃n. rstep (trs_n (π ∙ R) n))" unfolding rstep_perm_trs_n ..
  also have "… = cstep (π ∙ R)" by (auto simp: cstep_def cstep_n_rstep_trs_n_conv)
  finally show ?thesis .
qed

lemma permute_cstep [simp]:
  "π ∙ cstep R = cstep R"
by (simp add: eqvt cstep_permute)

lemma csteps_eqvt:
  "π ∙ (cstep R)* = (cstep (π ∙ R))*"
proof (intro equalityI subrelI)
  fix s t assume "(s, t) ∈ π ∙ (cstep R)*"
  then have "(-π ∙ s, -π ∙ t) ∈ (cstep R)*" by auto
  then show "(s, t) ∈ (cstep (π ∙ R))*"
    apply (induct "-π ∙ s" "-π ∙ t" arbitrary: t)
    apply auto
    by (metis (no_types, lifting) cstep_eqvt inv_rule_mem_trs_simps(2) minus_minus rtrancl.rtrancl_into_rtrancl term_pt.permute_minus_cancel(1))
next
  fix s t assume "(s, t) ∈ (cstep (π ∙ R))*"
  then show "(s, t) ∈ π ∙ (cstep R)*"
    apply (induct)
    using inv_rule_mem_trs_simps(1) apply blast
    by (metis cstep_eqvt inv_rule_mem_trs_simps(1) rtrancl.rtrancl_into_rtrancl)
qed

lemma cstep_n_permute_iff:
  "(π ∙ s, π ∙ t) ∈ cstep_n R n ⟷ (s, t) ∈ cstep_n R n"
by (auto simp: cstep_n_rstep_trs_n_conv split: prod.splits)

lemma subst_compose_o_assoc:
  "(σ ∘s τ) ∘ f = (σ ∘ f) ∘s τ"
by (rule ext) (simp add: subst_compose)

lemma perm_csteps_n_perm:
  assumes "(π ∙ s, t) ∈ (cstep_n R n)*"
  shows "∃u. t = π ∙ u"
  using assms by (metis term_pt.permute_minus_cancel(1))

lemma subst_list_subst_compose:
  "subst_list (σ ∘s τ) xs = subst_list τ (subst_list σ xs)"
by (simp add: subst_list_def)

lemma subst_list_Rep_perm:
  "subst_list (σ ∘ Rep_perm π) xs = subst_list σ (π ∙ xs)"
  by (auto simp: subst_list_def permute_term_subst_apply_term [symmetric] eqvt)


lemma finite_vars_crule: "finite (vars_crule r)"
by (auto simp: vars_crule_def vars_defs)

lemma nth_subst_list [simp]:
  "i < length ts ⟹ subst_list σ ts ! i = (fst (ts ! i) ⋅ σ, snd (ts ! i) ⋅ σ)"
by (auto simp: subst_list_def)

lemma length_subst_list [simp]:
  "length (subst_list σ ts) = length ts"
by (auto simp: subst_list_def)

lemma vars_conds_vars_crule_subset:
  "x ∈ vars_term (fst (conds r ! i)) ⟹ i < length (conds r) ⟹ x ∈ vars_crule r"
  "x ∈ vars_term (snd (conds r ! i)) ⟹ i < length (conds r) ⟹ x ∈ vars_crule r"
by (auto simp: vars_crule_def vars_defs)

lemma permute_conds_set [simp]:
  fixes cs :: "('f, 'v::infinite) rule list"
  shows "π ∙ set cs = set (π ∙ cs)"
by (induct cs) (auto simp: eqvt)

lemma cstep_imp_map_cstep:
  assumes "(s, t) ∈ cstep R"
  shows "(map_funs_term h s, map_funs_term h t) ∈ cstep (map_funs_ctrs h R)"
    (is "(?h s, ?h t) ∈ cstep (?H R)")
proof -
  obtain n where "(s, t) ∈ cstep_n R n" using assms by (auto simp: cstep_iff)
  then have "(?h s, ?h t) ∈ cstep_n (?H R) n"
  proof (induct n arbitrary: s t)
    case (Suc n)
    then obtain C σ l r cs where rule: "((l, r), cs) ∈ R"
      and *: "∀(u, v) ∈ set cs. (u ⋅ σ, v ⋅ σ) ∈ (cstep_n R n)*"
      and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by (auto elim: cstep_n_SucE)
    let  = "?h ∘ σ"
    let ?C = "map_funs_ctxt h C"
    let ?cs = "map (map_funs_rule h) cs"
    have "((?h l, ?h r), ?cs) ∈ ?H R" using rule by force
    moreover have "?h s = ?C⟨?h l ⋅ ?σ⟩" and "?h t = ?C⟨?h r ⋅ ?σ⟩" by (auto simp: s t o_def)
    moreover have "∀(u, v) ∈ set ?cs. (u ⋅ ?σ, v ⋅ ?σ) ∈ (cstep_n (?H R) n)*"
      using rtrancl_map [where f = ?h and r = "cstep_n R n", OF Suc.hyps]
        and * by (auto simp: o_def) force
    ultimately show ?case by (blast intro: cstep_n_SucI)
  qed simp
  then show ?thesis by (auto simp: cstep_iff)
qed

definition "trs2ctrs R = { (r, []) | r. r ∈ R }"

lemma cstep_n_subset:
  assumes "R ⊆ S"
  shows "cstep_n R n ⊆ cstep_n S n"
  using assms and rtrancl_mono [of "cstep_n R n" "cstep_n S n" for n]
  by (induct n) (auto elim!: cstep_n_SucE intro!: cstep_n_SucI split: prod.splits, blast)

lemma cstep_subset:
  assumes "R ⊆ S"
  shows "cstep R ⊆ cstep S"
  using cstep_n_subset [OF assms] by (force simp: cstep_iff)
  
lemma conds_sat_mono:
  assumes "R ⊆ S"
  shows "conds_sat R cs σ ⟹ conds_sat S cs σ"
  using rtrancl_mono [OF cstep_subset [OF assms]] by (auto simp: conds_sat_iff)

end