Theory Trs

section ‹Term Rewrite Systems›

theory Trs
  imports
    Relation_Closure
    First_Order_Terms.Term_More
    "Abstract-Rewriting.Relative_Rewriting"
begin

text ‹
  A rewrite rule is a pair of terms. A term rewrite system (TRS) is a set of rewrite rules.
›
type_synonym ('f, 'v) rule = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) trs  = "('f, 'v) rule set"

inductive_set rstep :: "_ ⇒ ('f, 'v) term rel" for R :: "('f, 'v) trs"
  where
    rstep: "⋀C σ l r. (l, r) ∈ R ⟹ s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep R"

lemma rstep_induct_rule [case_names IH, induct set: rstep]:
  assumes "(s, t) ∈ rstep R"
    and "⋀C σ l r. (l, r) ∈ R ⟹ P (C⟨l ⋅ σ⟩) (C⟨r ⋅ σ⟩)"
  shows "P s t"
  using assms by (induct) simp

text ‹
  An alternative induction scheme that treats the rule-case, the
  substition-case, and the context-case separately.
›
lemma rstep_induct [consumes 1, case_names rule subst ctxt]:
  assumes "(s, t) ∈ rstep R"
    and rule: "⋀l r. (l, r) ∈ R ⟹ P l r"
    and subst: "⋀s t σ. P s t ⟹ P (s ⋅ σ) (t ⋅ σ)"
    and ctxt: "⋀s t C. P s t ⟹ P (C⟨s⟩) (C⟨t⟩)"
  shows "P s t"
  using assms by (induct) auto

lemmas rstepI = rstep.intros [intro]

lemmas rstepE = rstep.cases [elim]

lemma rstep_ctxt [intro]: "(s, t) ∈ rstep R ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep R"
  by (force simp flip: ctxt_ctxt_compose)

lemma rstep_rule [intro]: "(l, r) ∈ R ⟹ (l, r) ∈ rstep R"
  using rstep.rstep [where C = □ and σ = Var and R = R] by simp

lemma rstep_subst [intro]: "(s, t) ∈ rstep R ⟹ (s ⋅ σ, t ⋅ σ) ∈ rstep R"
  by (force simp flip: subst_subst_compose)

lemma rstep_empty [simp]: "rstep {} = {}"
  by auto

lemma rstep_mono: "R ⊆ S ⟹ rstep R ⊆ rstep S"
  by force

lemma rstep_union: "rstep (R ∪ S) = rstep R ∪ rstep S"
  by auto

lemma rstep_converse [simp]: "rstep (R¯) = (rstep R)¯"
  by auto

interpretation subst: rel_closure "λσ t. t ⋅ σ" Var "λx y. y ∘⇩s x" by (standard) auto
declare subst.closure.induct [consumes 1, case_names subst, induct pred: subst.closure]
declare subst.closure.cases [consumes 1, case_names subst, cases pred: subst.closure]

interpretation ctxt: rel_closure "ctxt_apply_term" □ "(∘⇩c)" by (standard) auto
declare ctxt.closure.induct [consumes 1, case_names ctxt, induct pred: ctxt.closure]
declare ctxt.closure.cases [consumes 1, case_names ctxt, cases pred: ctxt.closure]

lemma rstep_eq_closure: "rstep R = ctxt.closure (subst.closure R)"
  by (force elim: ctxt.closure.cases subst.closure.cases)

lemma ctxt_closed_rstep [intro]: "ctxt.closed (rstep R)"
  by (simp add: rstep_eq_closure ctxt.closed_closure)

lemma ctxt_closed_one:
  "ctxt.closed r ⟹ (s, t) ∈ r ⟹ (Fun f (ss @ s # ts), Fun f (ss @ t # ts)) ∈ r"
  using ctxt.closedD [of r s t "More f ss □ ts"] by auto

subsection‹Well-formed TRSs›

definition
  wf_trs :: "('f, 'v) trs ⇒ bool"
  where
    "wf_trs R = (∀l r. (l,r) ∈ R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l)"

lemma wf_trs_imp_lhs_Fun:
  "wf_trs R ⟹ (l,r) ∈ R ⟹ ∃f ts. l = Fun f ts"
  unfolding wf_trs_def by blast

lemma rstep_imp_Fun:
  assumes "wf_trs R"
  shows "(s, t) ∈ rstep R ⟹ ∃f ss. s = Fun f ss"
proof -
  assume "(s, t) ∈ rstep R"
  then obtain C l r σ where lr: "(l,r) ∈ R" and s: "s = C ⟨ l ⋅ σ ⟩" by auto
  with wf_trs_imp_lhs_Fun[OF assms lr] show ?thesis by (cases C, auto)
qed

lemma SN_Var:
  assumes "wf_trs R" shows "SN_on (rstep R) {Var x}"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain S where [symmetric]: "S 0 = Var x"
    and chain: "chain (rstep R) S" by auto
  then have "(Var x, S (Suc 0)) ∈ rstep R" by force
  then obtain C l r σ where "(l, r) ∈ R" and "Var x = C⟨l ⋅ σ⟩" by best
  then have "Var x = l ⋅ σ" by (induct C) simp_all
  then obtain y where "l = Var y" by (induct l) simp_all
  with assms and ‹(l, r) ∈ R› show False unfolding wf_trs_def by blast
qed

subsection ‹Function Symbols and Variables of Rules and TRSs›

definition
  vars_rule :: "('f, 'v) rule ⇒ 'v set"
  where
    "vars_rule r = vars_term (fst r) ∪ vars_term (snd r)"

lemma finite_vars_rule:
  "finite (vars_rule r)"
  by (auto simp: vars_rule_def)

definition vars_trs :: "('f, 'v) trs ⇒ 'v set" where
  "vars_trs R = (⋃r∈R. vars_rule r)"

lemma vars_trs_union: "vars_trs (R ∪ S) = vars_trs R ∪ vars_trs S"
  unfolding vars_trs_def by auto

lemma finite_trs_has_finite_vars:
  assumes "finite R" shows "finite (vars_trs R)"
  using assms unfolding vars_trs_def vars_rule_def [abs_def] by simp

lemmas vars_defs = vars_trs_def vars_rule_def

definition funs_rule :: "('f, 'v) rule ⇒ 'f set" where
  "funs_rule r = funs_term (fst r) ∪ funs_term (snd r)"


text ‹The same including arities.›
definition funas_rule :: "('f, 'v) rule ⇒ 'f sig" where
  "funas_rule r = funas_term (fst r) ∪ funas_term (snd r)"

definition funs_trs :: "('f, 'v) trs ⇒ 'f set" where
  "funs_trs R = (⋃r∈R. funs_rule r)"

definition funas_trs :: "('f, 'v) trs ⇒ 'f sig" where
  "funas_trs R = (⋃r∈R. funas_rule r)"

lemma funs_rule_funas_rule: "funs_rule rl = fst ` funas_rule rl"
  using funs_term_funas_term unfolding funs_rule_def funas_rule_def image_Un by metis

lemma funs_trs_funas_trs:"funs_trs R = fst ` funas_trs R"
  unfolding funs_trs_def funas_trs_def image_UN using funs_rule_funas_rule by metis

lemma finite_funas_rule: "finite (funas_rule lr)"
  unfolding funas_rule_def
  using finite_funas_term by auto

lemma finite_funas_trs:
  assumes "finite R"
  shows "finite (funas_trs R)"
  unfolding funas_trs_def
  using assms finite_funas_rule by auto

lemma funas_empty[simp]: "funas_trs {} = {}" unfolding funas_trs_def by simp

lemma funas_trs_union[simp]: "funas_trs (R ∪ S) = funas_trs R ∪ funas_trs S"
  unfolding funas_trs_def by blast

definition funas_args_rule :: "('f, 'v) rule ⇒ 'f sig" where
  "funas_args_rule r = funas_args_term (fst r) ∪ funas_args_term (snd r)"

definition funas_args_trs :: "('f, 'v) trs ⇒ 'f sig" where
  "funas_args_trs R = (⋃r∈R. funas_args_rule r)"

lemmas funas_args_defs =
  funas_args_trs_def funas_args_rule_def funas_args_term_def

definition roots_rule :: "('f, 'v) rule ⇒ 'f sig"
  where
    "roots_rule r = set_option (root (fst r)) ∪ set_option (root (snd r))"

definition roots_trs :: "('f, 'v) trs ⇒ 'f sig" where
  "roots_trs R = (⋃r∈R. roots_rule r)"

lemmas roots_defs =
  roots_trs_def roots_rule_def

definition funas_head :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ 'f sig" where
  "funas_head P R = funas_trs P - (funas_trs R ∪ funas_args_trs P)"

lemmas funs_defs = funs_trs_def funs_rule_def
lemmas funas_defs =
  funas_trs_def funas_rule_def
  funas_args_defs
  funas_head_def
  roots_defs

text ‹A function symbol is said to be \emph{defined} (w.r.t.\ to a given
TRS) if it occurs as root of some left-hand side.›
definition
  defined :: "('f, 'v) trs ⇒ ('f × nat) ⇒ bool"
  where
    "defined R fn ⟷ (∃l r. (l, r) ∈ R ∧ root l = Some fn)"

lemma defined_funas_trs: assumes d: "defined R fn" shows "fn ∈ funas_trs R"
proof -
  from d [unfolded defined_def] obtain l r
    where "(l, r) ∈ R" and "root l = Some fn" by auto
  then show ?thesis
    unfolding funas_trs_def funas_rule_def [abs_def] by (cases l) force+
qed

fun root_list :: "('f, 'v) term ⇒ ('f × nat) list"
  where
    "root_list (Var x) = []" |
    "root_list (Fun f ts) = [(f, length ts)]"

definition vars_rule_list :: "('f, 'v) rule ⇒ 'v list"
  where
    "vars_rule_list r = vars_term_list (fst r) @ vars_term_list (snd r)"

definition funs_rule_list :: "('f, 'v) rule ⇒ 'f list"
  where
    "funs_rule_list r = funs_term_list (fst r) @ funs_term_list (snd r)"

definition funas_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
  where
    "funas_rule_list r = funas_term_list (fst r) @ funas_term_list (snd r)"

definition roots_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
  where
    "roots_rule_list r = root_list (fst r) @ root_list (snd r)"

definition funas_args_rule_list :: "('f, 'v) rule ⇒ ('f × nat) list"
  where
    "funas_args_rule_list r = funas_args_term_list (fst r) @ funas_args_term_list (snd r)"

lemma set_vars_rule_list [simp]:
  "set (vars_rule_list r) = vars_rule r"
  by (simp add: vars_rule_list_def vars_rule_def)

lemma set_funs_rule_list [simp]:
  "set (funs_rule_list r) = funs_rule r"
  by (simp add: funs_rule_list_def funs_rule_def)

lemma set_funas_rule_list [simp]:
  "set (funas_rule_list r) = funas_rule r"
  by (simp add: funas_rule_list_def funas_rule_def)

lemma set_roots_rule_list [simp]:
  "set (roots_rule_list r) = roots_rule r"
  by (cases "fst r" "snd r" rule: term.exhaust [case_product term.exhaust])
    (auto simp: roots_rule_list_def roots_rule_def ac_simps)

lemma set_funas_args_rule_list [simp]:
  "set (funas_args_rule_list r) = funas_args_rule r"
  by (simp add: funas_args_rule_list_def funas_args_rule_def)

definition vars_trs_list :: "('f, 'v) rule list ⇒ 'v list"
  where
    "vars_trs_list trs = concat (map vars_rule_list trs)"

definition funs_trs_list :: "('f, 'v) rule list ⇒ 'f list"
  where
    "funs_trs_list trs = concat (map funs_rule_list trs)"

definition funas_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
  where
    "funas_trs_list trs = concat (map funas_rule_list trs)"

definition roots_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
  where
    "roots_trs_list trs = remdups (concat (map roots_rule_list trs))"

definition funas_args_trs_list :: "('f, 'v) rule list ⇒ ('f × nat) list"
  where
    "funas_args_trs_list trs = concat (map funas_args_rule_list trs)"

lemma set_vars_trs_list [simp]:
  "set (vars_trs_list trs) = vars_trs (set trs)"
  by (simp add: vars_trs_def vars_trs_list_def)

lemma set_funs_trs_list [simp]:
  "set (funs_trs_list R) = funs_trs (set R)"
  by (simp add: funs_trs_def funs_trs_list_def)

lemma set_funas_trs_list [simp]:
  "set (funas_trs_list R) = funas_trs (set R)"
  by (simp add: funas_trs_def funas_trs_list_def)

lemma set_roots_trs_list [simp]:
  "set (roots_trs_list R) = roots_trs (set R)"
  by (simp add: roots_trs_def roots_trs_list_def)

lemma set_funas_args_trs_list [simp]:
  "set (funas_args_trs_list R) = funas_args_trs (set R)"
  by (simp add: funas_args_trs_def funas_args_trs_list_def)

lemmas vars_list_defs = vars_trs_list_def vars_rule_list_def
lemmas funs_list_defs = funs_trs_list_def funs_rule_list_def
lemmas funas_list_defs = funas_trs_list_def funas_rule_list_def
lemmas roots_list_defs = roots_trs_list_def roots_rule_list_def
lemmas funas_args_list_defs = funas_args_trs_list_def funas_args_rule_list_def

lemma vars_trs_list_Nil [simp]:
  "vars_trs_list [] = []" unfolding vars_trs_list_def by simp

context
  fixes R :: "('f, 'v) trs"
  assumes "wf_trs R"
begin

lemma funas_term_subst_rhs:
  assumes "funas_trs R ⊆ F" and "(l, r) ∈ R" and "funas_term (l ⋅ σ) ⊆ F"
  shows "funas_term (r ⋅ σ) ⊆ F"
proof -
  have "vars_term r ⊆ vars_term l"  using ‹wf_trs R› and ‹(l, r) ∈ R› by (auto simp: wf_trs_def)
  moreover have "funas_term l ⊆ F" and "funas_term r ⊆ F"
    using ‹funas_trs R ⊆ F› and ‹(l, r) ∈ R› by (auto simp: funas_defs) force+
  ultimately show ?thesis
    using ‹funas_term (l ⋅ σ) ⊆ F› by (force simp: funas_term_subst)
qed

lemma vars_rule_lhs:
  "r ∈ R ⟹ vars_rule r = vars_term (fst r)"
  using ‹wf_trs R› by (cases r) (auto simp: wf_trs_def vars_rule_def)

end

subsection‹Closure Properties›

lemma ctxt_closed_R_imp_supt_R_distr:
  assumes "ctxt.closed R" and "s ⊳ t" and "(t, u) ∈ R" shows "∃t. (s, t) ∈ R ∧ t ⊳ u"
proof -
  from ‹s ⊳ t› obtain C where "C ≠ □" and "C⟨t⟩ = s" by auto
  from ‹ctxt.closed R› and ‹(t,u) ∈ R›
  have RCtCu: "(C⟨t⟩,C⟨u⟩) ∈ R" by (rule ctxt.closedD)
  from ‹C ≠ □› have "C⟨u⟩ ⊳ u" by auto
  from RCtCu have "(s,C⟨u⟩) ∈ R" unfolding ‹C⟨t⟩ = s› .
  from this and ‹C⟨u⟩ ⊳ u› show ?thesis by auto
qed

lemma ctxt_closed_imp_qc_supt: "ctxt.closed R ⟹ {⊳} O R ⊆ R O (R ∪ {⊳})⇧*" by blast

text ‹Let~$R$ be a relation on terms that is closed under contexts. If~$R$
is well-founded then $R \cup \rhd$ is well-founed.›
lemma SN_imp_SN_union_supt:
  assumes "SN R" and "ctxt.closed R"
  shows "SN (R ∪ {⊳})"
proof -
  from ‹ctxt.closed R› have "quasi_commute R {⊳}"
    unfolding quasi_commute_def by (rule ctxt_closed_imp_qc_supt)
  have "SN {⊳}" by (rule SN_supt)
  from ‹SN R› and ‹SN {⊳}› and ‹quasi_commute R {⊳}›
  show ?thesis by (rule quasi_commute_imp_SN)
qed

lemma stable_loop_imp_not_SN:
  assumes stable: "subst.closed r" and steps: "(s, s ⋅ σ) ∈ r⇧+"
  shows "¬ SN_on r {s}"
proof -
  let ?f =  "λ i. s ⋅ (power.power Var (∘⇩s) σ i)"
  have main: "⋀ i. (?f i, ?f (Suc i)) ∈ r⇧+"
  proof -
    fix i
    show "(?f i, ?f (Suc i)) ∈ r⇧+"
    proof (induct i)
      case (Suc i)
      from Suc subst.closed_trancl[OF stable] have step: "(?f i ⋅ σ, ?f (Suc i) ⋅ σ) ∈ r⇧+" by auto
      let ?σg = "power.power Var (∘⇩s) σ i"
      let ?σgs = "power.power Var (∘⇩s) σ (Suc i)"
      have idi: "?σg ∘⇩s σ = σ ∘⇩s ?σg" by (rule subst_monoid_mult.power_commutes)
      have idsi: "?σgs ∘⇩s σ = σ ∘⇩s ?σgs" by (rule subst_monoid_mult.power_commutes)
      have "?f i ⋅ σ = s ⋅ ?σg  ∘⇩s σ" by simp
      also have "… = ?f (Suc i)" unfolding idi by simp
      finally have one: "?f i ⋅ σ = ?f (Suc i)" .
      have "?f (Suc i) ⋅ σ = s ⋅ ?σgs ∘⇩s σ" by simp
      also have "… = ?f (Suc (Suc i))" unfolding idsi by simp
      finally have two: "?f (Suc i) ⋅ σ = ?f (Suc (Suc i))" by simp
      show ?case using one two step by simp
    qed (auto simp: steps)
  qed
  then have "¬ SN_on (r⇧+) {?f 0}" unfolding SN_on_def by best
  then show ?thesis using SN_on_trancl by force
qed

lemma subst_closed_supteq: "subst.closed {⊵}" by blast

lemma subst_closed_supt: "subst.closed {⊳}" by blast

lemma ctxt_closed_supt_subset: "ctxt.closed R ⟹ {⊳} O R ⊆ R O {⊳}" by blast

subsection‹Properties of Rewrite Steps›

lemma rstep_relcomp_idemp1 [simp]:
  "rstep (rstep R O rstep S) = rstep R O rstep S"
proof -
  { fix s t
    assume "(s, t) ∈ rstep (rstep R O rstep S)"
    then have "(s, t) ∈ rstep R O rstep S"
      by (induct) blast+ }
  then show ?thesis by auto
qed

lemma rstep_relcomp_idemp2 [simp]:
  "rstep (rstep R O rstep S O rstep T) = rstep R O rstep S O rstep T"
proof -
  { fix s t
    assume "(s, t) ∈ rstep (rstep R O rstep S O rstep T)"
    then have "(s, t) ∈ rstep R O rstep S O rstep T"
      by (induct) blast+ }
  then show ?thesis by auto
qed

lemma ctxt_closed_rsteps [intro]: "ctxt.closed ((rstep R)⇧*)" by blast

lemma subset_rstep: "R ⊆ rstep R" by auto

lemma subst_closure_rstep_subset: "subst.closure (rstep R) ⊆ rstep R"
  by (auto elim: subst.closure.cases)

lemma subst_closed_rstep [intro]: "subst.closed (rstep R)" by blast

lemma subst_closed_rsteps: "subst.closed ((rstep R)⇧*)" by blast

lemmas supt_rsteps_subset = ctxt_closed_supt_subset [OF ctxt_closed_rsteps]

lemma supteq_rsteps_subset:
  "{⊵} O (rstep R)⇧* ⊆ (rstep R)⇧* O {⊵}" (is "?S ⊆ ?T")
  using supt_rsteps_subset [of R] by (auto simp: supt_supteq_set_conv)

lemma quasi_commute_rsteps_supt:
  "quasi_commute ((rstep R)⇧*) {⊳}"
  unfolding quasi_commute_def using supt_rsteps_subset [of R] by auto

lemma rstep_UN:
  "rstep (⋃i∈A. R i) = (⋃i∈A. rstep (R i))"
  by (force)

definition
  rstep_r_p_s :: "('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) subst ⇒ ('f, 'v) trs"
  where
    "rstep_r_p_s R r p σ = {(s, t).
    let C = ctxt_of_pos_term p s in p ∈ poss s ∧ r ∈ R ∧ (C⟨fst r ⋅ σ⟩ = s) ∧ (C⟨snd r ⋅ σ⟩ = t)}"

lemma rstep_r_p_s_def':
  "rstep_r_p_s R r p σ = {(s, t).
    p ∈ poss s ∧ r ∈ R ∧ s |_ p = fst r ⋅ σ ∧ t = replace_at s p (snd r ⋅ σ)}" (is "?l = ?r")
proof -
  { fix s t
    have "((s,t) ∈ ?l) = ((s,t) ∈ ?r)"
      unfolding rstep_r_p_s_def Let_def
      using ctxt_supt_id [of p s] and subt_at_ctxt_of_pos_term [of p s "fst r ⋅ σ"] by auto }
  then show ?thesis by auto
qed

lemma parallel_steps:
  fixes p⇩1 :: pos
  assumes "(s, t) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
    and "(s, u) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2"
    and par: "p⇩1 ⊥ p⇩2"
  shows "(t, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2 ∧
         (u, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
proof -
  have p1: "p⇩1 ∈ poss s" and lr1: "(l⇩1, r⇩1) ∈ R⇩1" and σ1: "s |_ p⇩1 = l⇩1 ⋅ σ⇩1"
    and t: "t = replace_at s p⇩1 (r⇩1 ⋅ σ⇩1)"
    and p2: "p⇩2 ∈ poss s" and lr2: "(l⇩2, r⇩2) ∈ R⇩2" and σ2: "s |_ p⇩2 = l⇩2 ⋅ σ⇩2"
    and u: "u = replace_at s p⇩2 (r⇩2 ⋅ σ⇩2)" using assms by (auto simp: rstep_r_p_s_def')

  have "replace_at t p⇩2 (r⇩2 ⋅ σ⇩2) = replace_at u p⇩1 (r⇩1 ⋅ σ⇩1)"
    using t and u and parallel_replace_at [OF ‹p⇩1 ⊥ p⇩2› p1 p2] by auto
  moreover
  have "(t, (ctxt_of_pos_term p⇩2 t)⟨r⇩2 ⋅ σ⇩2⟩) ∈ rstep_r_p_s R⇩2 (l⇩2, r⇩2) p⇩2 σ⇩2"
  proof -
    have "t |_ p⇩2 = l⇩2 ⋅ σ⇩2" using σ2 and parallel_replace_at_subt_at [OF par p1 p2] and t by auto
    moreover have "p⇩2 ∈ poss t" using parallel_poss_replace_at [OF par p1] and t and p2 by auto
    ultimately show ?thesis using lr2 and ctxt_supt_id [of p⇩2 t] by (simp add: rstep_r_p_s_def)
  qed
  moreover
  have "(u, (ctxt_of_pos_term p⇩1 u)⟨r⇩1 ⋅ σ⇩1⟩) ∈ rstep_r_p_s R⇩1 (l⇩1, r⇩1) p⇩1 σ⇩1"
  proof -
    have par': "p⇩2 ⊥ p⇩1" using parallel_pos_sym [OF par] .
    have "u |_ p⇩1 = l⇩1 ⋅ σ⇩1" using σ1 and parallel_replace_at_subt_at [OF par' p2 p1] and u by auto
    moreover have "p⇩1 ∈ poss u" using parallel_poss_replace_at [OF par' p2] and u and p1 by auto
    ultimately show ?thesis using lr1 and ctxt_supt_id [of p⇩1 u] by (simp add: rstep_r_p_s_def)
  qed
  ultimately show ?thesis by auto
qed

lemma rstep_iff_rstep_r_p_s:
  "(s, t) ∈ rstep R ⟷ (∃l r p σ. (s, t) ∈ rstep_r_p_s R (l, r) p σ)" (is "?lhs = ?rhs")
proof
  assume "(s, t) ∈ rstep R"
  then obtain C σ l r where s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and "(l, r) ∈ R" by auto
  let ?p = "hole_pos C"
  let ?C = "ctxt_of_pos_term ?p s"
  have C: "ctxt_of_pos_term ?p s = C" unfolding s by (induct C) simp_all
  have "?p ∈ poss s" unfolding s by simp
  moreover have "(l, r) ∈ R" by fact
  moreover have "?C⟨l ⋅ σ⟩ = s" unfolding C by (simp add: s)
  moreover have "?C⟨r ⋅ σ⟩ = t" unfolding C by (simp add: t)
  ultimately show "?rhs" unfolding rstep_r_p_s_def Let_def by auto
next
  assume "?rhs"
  then obtain l r p σ where "p ∈ poss s"
    and "(l, r) ∈ R"
    and s[symmetric]: "(ctxt_of_pos_term p s)⟨l ⋅ σ⟩ = s"
    and t[symmetric]: "(ctxt_of_pos_term p s)⟨r ⋅ σ⟩ = t"
    unfolding rstep_r_p_s_def Let_def by auto
  then show "?lhs" by auto
qed

lemma rstep_r_p_s_imp_rstep:
  assumes "(s, t) ∈ rstep_r_p_s R r p σ"
  shows "(s, t) ∈ rstep R"
  using assms by (cases r) (auto simp: rstep_iff_rstep_r_p_s)

text ‹Rewriting steps below the root position.›
definition
  nrrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs"
  where
    "nrrstep R = {(s,t). ∃r i ps σ. (s,t) ∈ rstep_r_p_s R r (i#ps) σ}"

text ‹An alternative characterisation of non-root rewrite steps.›
lemma nrrstep_def':
  "nrrstep R = {(s, t). ∃l r C σ. (l, r) ∈ R ∧ C ≠ □ ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩}"
  (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
  proof (rule subrelI)
    fix s t assume "(s, t) ∈ nrrstep R"
    then obtain l r i ps σ where step: "(s, t) ∈ rstep_r_p_s R (l, r) (i # ps) σ"
      unfolding nrrstep_def by best
    let ?C = "ctxt_of_pos_term (i # ps) s"
    from step have"i # ps ∈ poss s" and "(l, r) ∈ R" and "s = ?C⟨l⋅σ⟩" and "t = ?C⟨r⋅σ⟩"
      unfolding rstep_r_p_s_def Let_def by auto
    moreover from ‹i # ps ∈ poss s› have "?C ≠ □" by (induct s) auto
    ultimately show "(s, t) ∈ ?rhs" by auto
  qed
next
  show "?rhs ⊆ ?lhs"
  proof (rule subrelI)
    fix s t assume "(s, t) ∈ ?rhs"
    then obtain l r C σ where in_R: "(l, r) ∈ R" and "C ≠ □"
      and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
    from ‹C ≠ □› obtain i p where ip: "hole_pos C = i # p" by (induct C) auto
    have "i # p ∈ poss s" using hole_pos_poss[of C] unfolding s ip by simp
    then have C: "C = ctxt_of_pos_term (i # p) s"
      unfolding s ip[symmetric] by simp
    from ‹i # p ∈ poss s› in_R s t have "(s, t) ∈ rstep_r_p_s R (l, r) (i # p) σ"
      unfolding rstep_r_p_s_def C by simp
    then show "(s, t) ∈ nrrstep R" unfolding nrrstep_def by best
  qed
qed

lemma nrrstepI: "(l,r) ∈ R ⟹ s = C⟨l⋅σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ C ≠ □ ⟹ (s,t) ∈ nrrstep R" unfolding nrrstep_def' by auto

lemma nrrstep_union: "nrrstep (R ∪ S) = nrrstep R ∪ nrrstep S"
  unfolding nrrstep_def' by blast

lemma nrrstep_empty[simp]: "nrrstep {} = {}" unfolding nrrstep_def' by blast

text ‹Rewriting step at the root position.›
definition
  rrstep :: "('f, 'v) trs ⇒ ('f, 'v) trs"
  where
    "rrstep R = {(s,t). ∃r σ. (s,t) ∈ rstep_r_p_s R r [] σ}"

text ‹An alternative characterisation of root rewrite steps.›
lemma rrstep_def': "rrstep R = {(s, t). ∃l r σ. (l, r) ∈ R ∧ s = l⋅σ ∧ t = r⋅σ}"
  (is "_ = ?rhs")
  by (auto simp: rrstep_def rstep_r_p_s_def)

lemma rules_subset_rrstep [simp]: "R ⊆ rrstep R"
  by (force simp: rrstep_def' intro: exI [of _ Var])

lemma rrstep_union: "rrstep (R ∪ S) = rrstep R ∪ rrstep S" unfolding rrstep_def' by blast

lemma rrstep_empty[simp]: "rrstep {} = {}"
  unfolding rrstep_def' by auto

lemma subst_closed_rrstep: "subst.closed (rrstep R)"
  unfolding subst.closed_def
proof
  fix ss ts
  assume "(ss,ts) ∈ subst.closure (rrstep R)"
  then show "(ss,ts) ∈ rrstep R"
  proof
    fix s t σ
    assume ss: "ss = s ⋅ σ" and ts: "ts = t ⋅ σ" and step: "(s,t) ∈ rrstep R"
    from step obtain l r δ where lr: "(l,r) ∈ R" and s: "s = l ⋅ δ" and t: "t = r ⋅ δ" unfolding rrstep_def' by auto
    obtain sig where "sig = δ ∘⇩s σ" by auto
    with ss s ts t have "ss = l ⋅ sig" and "ts = r ⋅ sig" by simp+
    with lr show "(ss,ts) ∈ rrstep R" unfolding rrstep_def' by (auto simp: Let_def)
  qed
qed

lemma rstep_iff_rrstep_or_nrrstep: "rstep R = (rrstep R ∪ nrrstep R)"
proof
  show "rstep R ⊆ rrstep R ∪ nrrstep R"
  proof (rule subrelI)
    fix s t assume "(s,t) ∈ rstep R"
    then obtain l r p σ where rstep_rps: "(s,t) ∈ rstep_r_p_s R (l,r) p σ"
      by (auto simp: rstep_iff_rstep_r_p_s)
    then show "(s,t) ∈ rrstep R ∪ nrrstep R" unfolding rrstep_def nrrstep_def by (cases p) auto
  qed
next
  show "rrstep R ∪ nrrstep R ⊆ rstep R"
  proof (rule subrelI)
    fix s t assume "(s,t) ∈ rrstep R ∪ nrrstep R"
    then show "(s,t) ∈ rstep R" by (auto simp: rrstep_def nrrstep_def rstep_iff_rstep_r_p_s)
  qed
qed

lemma rstep_i_pos_imp_rstep_arg_i_pos:
  assumes nrrstep: "(Fun f ss,t) ∈ rstep_r_p_s R (l,r) (i#ps) σ"
  shows "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) ps σ"
proof -
  from nrrstep obtain C where C:"C = ctxt_of_pos_term (i#ps) (Fun f ss)"
    and pos: "(i#ps) ∈ poss (Fun f ss)"
    and Rlr: "(l,r) ∈ R"
    and Fun: "C⟨l⋅σ⟩ = Fun f ss"
    and t: "C⟨r⋅σ⟩ = t" unfolding rstep_r_p_s_def Let_def by auto
  then obtain D where C':"C = More f (take i ss) D (drop (Suc i) ss)" by auto
  then have CFun: "C⟨l⋅σ⟩ = Fun f (take i ss @ (D⟨l⋅σ⟩) # drop (Suc i) ss)" by auto
  from pos have len: "i < length ss" by auto
  from len
  have "(take i ss @ (D⟨l⋅σ⟩) # drop (Suc i) ss)!i = D⟨l⋅σ⟩" by (auto simp: nth_append)
  with C Fun CFun have ssi: "ss!i = D⟨l⋅σ⟩" by auto
  from C' t have t': "t = Fun f (take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)" by auto
  from len
  have "(take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)!i = D⟨r⋅σ⟩" by (auto simp: nth_append)
  with t' have "t|_[i] = (D⟨r⋅σ⟩)|_[]" by auto
  then have subt_at: "t|_[i] = D⟨r⋅σ⟩" by simp
  from C C' have "D = ctxt_of_pos_term ps (ss!i)" by auto
  with pos Rlr ssi[symmetric] subt_at[symmetric]
  show ?thesis unfolding rstep_r_p_s_def Let_def by auto
qed

lemma ctxt_closure_rstep_eq [simp]: "ctxt.closure (rstep R) = rstep R"
  by (rule ctxt.closure_id) blast

lemma subst_closure_rstep_eq [simp]: "subst.closure (rstep R) = rstep R"
  by (rule subst.closure_id) blast

lemma supt_rstep_subset:
  "{⊳} O rstep R ⊆ rstep R O {⊳}"
proof (rule subrelI)
  fix s t assume "(s,t) ∈ {⊳} O rstep R" then show "(s,t) ∈ rstep R O {⊳}"
  proof (induct s)
    case (Var x)
    then have "∃u. Var x ⊳ u ∧ (u,t) ∈ rstep R" by auto
    then obtain u where "Var x ⊳ u" and "(u,t) ∈ rstep R" by auto
    from ‹Var x ⊳ u› show ?case by (cases rule: supt.cases)
  next
    case (Fun f ss)
    then obtain u where "Fun f ss ⊳ u" and "(u,t) ∈ rstep R" by auto
    from ‹Fun f ss ⊳ u› obtain C
      where "C ≠ □" and "C⟨u⟩ = Fun f ss" by auto
    from ‹C ≠ □› have "C⟨t⟩ ⊳ t" by (rule nectxt_imp_supt_ctxt)
    from ‹(u,t) ∈ rstep R› have "(C⟨u⟩,C⟨t⟩) ∈ rstep R" ..
    then have "(Fun f ss,C⟨t⟩) ∈ rstep R" unfolding ‹C⟨u⟩ = Fun f ss› .
    with ‹C⟨t⟩ ⊳ t› show ?case by auto
  qed
qed

lemma ne_rstep_seq_imp_list_of_terms:
  assumes "(s,t) ∈ (rstep R)⇧+"
  shows "∃ts. length ts > 1 ∧ ts!0 = s ∧ ts!(length ts - 1) = t ∧
         (∀i<length ts - 1. (ts!i,ts!(Suc i)) ∈ (rstep R))" (is "∃ts. _ ∧ _ ∧ _ ∧ ?P ts")
  using assms
proof (induct rule: trancl.induct)
  case (r_into_trancl x y)
  let ?ts = "[x,y]"
  have "length ?ts > 1" by simp
  moreover have "?ts!0 = x" by simp
  moreover have "?ts!(length ?ts - 1) = y" by simp
  moreover from r_into_rtrancl r_into_trancl have "?P ?ts" by auto
  ultimately show ?case by fast
next
  case (trancl_into_trancl x y z)
  then obtain ts where "length ts > 1" and "ts!0 = x"
    and last1: "ts!(length ts - 1) = y" and "?P ts" by auto
  let ?ts = "ts@[z]"
  have len: "length ?ts = length ts + 1" by simp
  from ‹length ts > 1› have "length ?ts > 1" by auto
  moreover with ‹ts!0 = x› have "?ts!0 = x" by (induct ts) auto
  moreover have last2: "?ts!(length ?ts - 1) = z" by simp
  moreover have "?P ?ts"
  proof (intro allI impI)
    fix i assume A: "i < length ?ts - 1"
    show "(?ts!i,?ts!(Suc i)) ∈ rstep R"
    proof (cases "i < length ts - 1")
      case True with ‹?P ts› A show ?thesis unfolding len unfolding nth_append by auto
    next
      case False with A have "i = length ts - 1" by simp
      with last1 ‹length ts > 1› have "?ts!i = y" unfolding nth_append by auto
      have "Suc i = length ?ts - 1" using ‹i = length ts - 1› using ‹length ts > 1› by auto
      with last2 have "?ts!(Suc i) = z" by auto
      from ‹(y,z) ∈ rstep R› show ?thesis unfolding ‹?ts!(Suc i) = z› ‹?ts!i = y› .
    qed
  qed
  ultimately show ?case by fast
qed


locale E_compatible =
  fixes R :: "('f,'v)trs" and E :: "('f,'v)trs"
  assumes E: "E O R = R" "Id ⊆ E"
begin

definition restrict_SN_supt_E :: "('f, 'v) trs" where
  "restrict_SN_supt_E = restrict_SN R R ∪ restrict_SN (E O {⊳} O E) R"

lemma ctxt_closed_R_imp_supt_restrict_SN_E_distr:
  assumes "ctxt.closed R"
    and "(s,t) ∈ (restrict_SN (E O {⊳}) R)"
    and "(t,u) ∈ restrict_SN R R"
  shows "(∃t. (s,t) ∈ restrict_SN R R ∧ (t,u) ∈ restrict_SN (E O {⊳}) R)" (is "∃ t. _ ∧ (t,u) ∈ ?snSub")
proof -
  from ‹(s,t) ∈ ?snSub› obtain v where "SN_on R {s}" and ac: "(s,v) ∈ E" and "v ⊳ t" unfolding restrict_SN_def supt_def by auto
  from ‹v ⊳ t› obtain C where "C ≠ Hole" and v: "C⟨t⟩ = v" by best
  from ‹(t,u) ∈ restrict_SN R R› have "(t,u) ∈ R" unfolding restrict_SN_def by auto
  from ‹ctxt.closed R› and this have RCtCu: "(C⟨t⟩,C⟨u⟩) ∈ R" by (rule ctxt.closedD)
  with v ac have "(s,C⟨u⟩) ∈ E O R" by auto
  then have sCu: "(s,C⟨u⟩) ∈ R" using E by simp
  with ‹SN_on R {s}› have one: "SN_on R {C⟨u⟩}"
    using step_preserves_SN_on[of "s" "C⟨u⟩" R] by blast
  from ‹C ≠ □› have "C⟨u⟩ ⊳ u" by auto
  with one E have "(C⟨u⟩,u) ∈ ?snSub" unfolding restrict_SN_def supt_def by auto
  from sCu and ‹SN_on R {s}› and ‹(C⟨u⟩,u) ∈ ?snSub› show ?thesis unfolding restrict_SN_def by auto
qed

lemma ctxt_closed_R_imp_restrict_SN_qc_E_supt:
  assumes ctxt: "ctxt.closed R"
  shows "quasi_commute (restrict_SN R R) (restrict_SN (E O {⊳} O E) R)" (is "quasi_commute ?r ?s")
proof -
  have "?s O ?r ⊆ ?r O (?r ∪ ?s)⇧*"
  proof (rule subrelI)
    fix x y
    assume "(x,y) ∈ ?s O ?r"
    from this obtain z where "(x,z) ∈ ?s" and "(z,y) ∈ ?r" by best
    then obtain v w where ac: "(x,v) ∈ E" and vw: "v ⊳ w" and wz: "(w,z) ∈ E" and zy: "(z,y) ∈ R" and "SN_on R {x}" unfolding restrict_SN_def supt_def
      using E(2) by auto
    from wz zy have "(w,y) ∈ E O R" by auto
    with E have wy: "(w,y) ∈ R" by auto
    from ctxt_closed_R_imp_supt_R_distr[OF ctxt vw wy] obtain w where "(v,w) ∈ R" and "w ⊳ y" using ctxt_closed_R_imp_supt_R_distr[where R = R and s = v and t = z and u = y] by auto
    with ac E have "(x,w) ∈ R" and "w ⊳ y" by auto
    from this and ‹SN_on R {x}› have "SN_on R {w}" using step_preserves_SN_on
      unfolding supt_supteq_conv by auto
    with ‹w ⊳ y› E have "(w,y) ∈ ?s" unfolding restrict_SN_def supt_def by force
    with ‹(x,w) ∈ R› ‹SN_on R {x}› show "(x,y) ∈ ?r O (?r ∪ ?s)⇧*" unfolding restrict_SN_def by auto
  qed
  then show ?thesis unfolding quasi_commute_def .
qed

lemma ctxt_closed_imp_SN_restrict_SN_E_supt:
  assumes "ctxt.closed R"
    and SN: "SN (E O {⊳} O E)"
  shows "SN restrict_SN_supt_E"
proof -
  let ?r = "restrict_SN R R"
  let ?s = "restrict_SN (E O {⊳} O E) R"
  from ‹ctxt.closed R› have "quasi_commute ?r ?s"
    by (rule ctxt_closed_R_imp_restrict_SN_qc_E_supt)
  from SN have "SN ?s" by (rule SN_subset, auto simp: restrict_SN_def)
  have "SN ?r" by (rule SN_restrict_SN_idemp)
  from ‹SN ?r› and ‹SN ?s› and ‹quasi_commute ?r ?s›
  show ?thesis unfolding restrict_SN_supt_E_def by (rule quasi_commute_imp_SN)
qed
end

lemma E_compatible_Id: "E_compatible R Id"
  by standard auto

definition restrict_SN_supt :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
  "restrict_SN_supt R = restrict_SN R R ∪ restrict_SN {⊳} R"

lemma ctxt_closed_SN_on_subt:
  assumes "ctxt.closed R" and "SN_on R {s}" and "s ⊵ t"
  shows "SN_on R {t}"
proof (rule ccontr)
  assume "¬ SN_on R {t}"
  then obtain A where "A 0 = t" and "∀i. (A i,A (Suc i)) ∈ R"
    unfolding SN_on_def by best
  from ‹s ⊵ t› obtain C where "s = C⟨t⟩" by auto
  let ?B = "λi. C⟨A i⟩"
  have "∀i. (?B i,?B(Suc i)) ∈ R"
  proof
    fix i
    from ‹∀i. (A i,A(Suc i)) ∈ R› have "(?B i,?B(Suc i)) ∈ ctxt.closure(R)" by fast
    then show "(?B i,?B(Suc i)) ∈ R" using ‹ctxt.closed R› by auto
  qed
  with ‹A 0 = t› have "?B 0 = s ∧ (∀i. (?B i,?B(Suc i)) ∈ R)" unfolding ‹s = C⟨t⟩› by auto
  then have "¬ SN_on R {s}" unfolding SN_on_def by auto
  with assms show "False" by simp
qed

lemma ctxt_closed_R_imp_supt_restrict_SN_distr:
  assumes R: "ctxt.closed R"
    and st: "(s,t) ∈ (restrict_SN {⊳} R)"
    and tu: "(t,u) ∈ restrict_SN R R"
  shows "(∃t. (s,t) ∈ restrict_SN R R ∧ (t,u) ∈ restrict_SN {⊳} R)" (is "∃ t. _ ∧ (t,u) ∈ ?snSub")
  using E_compatible.ctxt_closed_R_imp_supt_restrict_SN_E_distr[OF E_compatible_Id R _ tu, of s]
    st by auto

lemma ctxt_closed_R_imp_restrict_SN_qc_supt:
  assumes "ctxt.closed R"
  shows "quasi_commute (restrict_SN R R) (restrict_SN supt R)" (is "quasi_commute ?r ?s")
  using E_compatible.ctxt_closed_R_imp_restrict_SN_qc_E_supt[OF E_compatible_Id assms] by auto

lemma ctxt_closed_imp_SN_restrict_SN_supt:
  assumes "ctxt.closed R"
  shows "SN (restrict_SN_supt R)"
  using E_compatible.ctxt_closed_imp_SN_restrict_SN_E_supt[OF E_compatible_Id assms]
  unfolding E_compatible.restrict_SN_supt_E_def[OF E_compatible_Id] restrict_SN_supt_def
  using SN_supt by auto

lemma SN_restrict_SN_supt_rstep:
  shows "SN (restrict_SN_supt (rstep R))"
proof -
  have "ctxt.closed (rstep R)" by (rule ctxt_closed_rstep)
  then show ?thesis by (rule ctxt_closed_imp_SN_restrict_SN_supt)
qed

lemma nrrstep_imp_pos_term:
  "(Fun f ss,t) ∈ nrrstep R ⟹
    ∃i s. t = Fun f (ss[i:=s]) ∧ (ss!i,s) ∈ rstep R ∧ i < length ss"
proof -
  assume "(Fun f ss,t) ∈ nrrstep R"
  then obtain l r i ps σ where rstep_rps:"(Fun f ss,t) ∈ rstep_r_p_s R (l,r) (i#ps) σ"
    unfolding nrrstep_def by auto
  then obtain C
    where "(l,r) ∈ R"
      and pos: "(i#ps) ∈ poss (Fun f ss)"
      and C: "C = ctxt_of_pos_term (i#ps) (Fun f ss)"
      and "C⟨l⋅σ⟩ = Fun f ss"
      and t: "C⟨r⋅σ⟩ = t"
    unfolding rstep_r_p_s_def Let_def by auto
  then obtain D where "C = More f (take i ss) D (drop (Suc i) ss)" by auto
  with t have t': "t = Fun f (take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)" by auto
  from rstep_rps have "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) ps σ"
    by (rule rstep_i_pos_imp_rstep_arg_i_pos)
  then have rstep:"(ss!i,t|_[i]) ∈ rstep R" by (auto simp: rstep_iff_rstep_r_p_s)
  then have "(C⟨ss!i⟩,C⟨t|_[i]⟩) ∈ rstep R" ..
  from pos have len: "i < length ss" by auto
  from len
  have "(take i ss @ (D⟨r⋅σ⟩) # drop (Suc i) ss)!i = D⟨r⋅σ⟩" by (auto simp: nth_append)
  with C t' have "t|_[i] = D⟨r⋅σ⟩" by auto
  with t' have "t = Fun f (take i ss @ (t|_[i]) # drop (Suc i) ss)" by auto
  with len have "t = Fun f (ss[i:=t|_[i]])" by (auto simp: upd_conv_take_nth_drop)
  with rstep len show "∃i s. t = Fun f (ss[i:=s]) ∧ (ss!i,s) ∈ rstep R ∧ i < length ss" by auto
qed


lemma rstep_cases[consumes 1, case_names root nonroot]:
  "⟦(s,t) ∈ rstep R; (s,t) ∈ rrstep R ⟹ P; (s,t) ∈ nrrstep R ⟹ P⟧ ⟹ P"
  by (auto simp: rstep_iff_rrstep_or_nrrstep)

lemma nrrstep_imp_rstep: "(s,t) ∈ nrrstep R ⟹ (s,t) ∈ rstep R"
  by (auto simp: rstep_iff_rrstep_or_nrrstep)

lemma nrrstep_imp_Fun: "(s,t) ∈ nrrstep R ⟹ ∃f ss. s = Fun f ss"
proof -
  assume "(s,t) ∈ nrrstep R"
  then obtain i ps where "i#ps ∈ poss s"
    unfolding nrrstep_def rstep_r_p_s_def Let_def by auto
  then show "∃f ss. s = Fun f ss" by (cases s) auto
qed

lemma nrrstep_imp_subt_rstep:
  assumes "(s,t) ∈ nrrstep R"
  shows "∃i. i < num_args s ∧ num_args s = num_args t ∧ (s|_[i],t|_[i]) ∈ rstep R ∧ (∀j. i ≠ j ⟶ s|_[j] = t|_[j])"
proof -
  from ‹(s,t) ∈ nrrstep R› obtain f ss where "s = Fun f ss" using nrrstep_imp_Fun by blast
  with ‹(s,t) ∈ nrrstep R› have "(Fun f ss,t) ∈ nrrstep R" by simp
  then obtain i u where "t = Fun f (ss[i := u])" and "(ss!i,u) ∈ rstep R" and "i < length ss"
    using nrrstep_imp_pos_term by best
  from ‹s = Fun f ss› and ‹t = Fun f (ss[i := u])› have "num_args s = num_args t" by auto
  from ‹i < length ss› and ‹s = Fun f ss› have "i < num_args s" by auto
  from ‹s = Fun f ss› have "s|_[i] = (ss!i)" by auto
  from ‹t = Fun f (ss[i := u])› and ‹i < length ss› have "t|_[i] = u" by auto
  from ‹s = Fun f ss› and ‹t = Fun f (ss[i := u])›
  have  "∀j. j ≠ i ⟶ s|_[j] = t|_[j]" by auto
  with ‹(ss!i,u) ∈ rstep R›
    and ‹i < num_args s›
    and ‹num_args s = num_args t›
    and ‹s|_[i] = (ss!i)›[symmetric] and ‹t|_[i] = u›[symmetric]
  show ?thesis by (auto)
qed

lemma nrrstep_subt: assumes "(s, t) ∈ nrrstep R" shows "∃u⊲s. ∃v⊲t. (u, v) ∈ rstep R"
proof -
  from assms obtain l r C σ where "(l, r) ∈ R" and "C ≠ □"
    and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" unfolding nrrstep_def' by best
  from ‹C ≠ □› s have "s ⊳ l⋅σ" by auto
  moreover from ‹C ≠ □› t have "t ⊳ r⋅σ" by auto
  moreover from ‹(l, r) ∈ R› have "(l⋅σ, r⋅σ) ∈ rstep R" by auto
  ultimately show ?thesis by auto
qed

lemma nrrstep_args:
  assumes "(s, t) ∈ nrrstep R"
  shows "∃f ss ts. s = Fun f ss ∧ t = Fun f ts ∧ length ss = length ts
    ∧ (∃j<length ss. (ss!j, ts!j) ∈ rstep R ∧ (∀i<length ss. i ≠ j ⟶ ss!i = ts!i))"
proof -
  from assms obtain l r C σ where "(l, r) ∈ R" and "C ≠ □"
    and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" unfolding nrrstep_def' by best
  from ‹C ≠ □› obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
  have "s = Fun f (ss1 @ D⟨l⋅σ⟩ # ss2)" (is "_ = Fun f ?ss") by (simp add: s C)
  moreover have "t = Fun f (ss1 @ D⟨r⋅σ⟩ # ss2)" (is "_ = Fun f ?ts") by (simp add: t C)
  moreover have "length ?ss = length ?ts" by simp
  moreover have "∃j<length ?ss.
    (?ss!j, ?ts!j) ∈ rstep R ∧ (∀i<length ?ss. i ≠ j ⟶ ?ss!i = ?ts!i)"
  proof -
    let ?j = "length ss1"
    have "?j < length ?ss" by simp
    moreover have "(?ss!?j, ?ts!?j) ∈ rstep R"
    proof -
      from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
      then show ?thesis by auto
    qed
    moreover have "∀i<length ?ss. i ≠ ?j ⟶ ?ss!i = ?ts!i" (is "∀i<length ?ss. _ ⟶ ?P i")
    proof (intro allI impI)
      fix i assume "i < length ?ss" and "i ≠ ?j"
      then have "i < length ss1 ∨ length ss1 < i" by auto
      then show "?P i"
      proof
        assume "i < length ss1" then show "?P i" by (auto simp: nth_append)
      next
        assume "i > length ss1" then show "?P i"
          using ‹i < length ?ss› by (auto simp: nth_Cons' nth_append)
      qed
    qed
    ultimately show ?thesis by best
  qed
  ultimately show ?thesis by auto
qed

lemma nrrstep_iff_arg_rstep:
  "(s,t) ∈ nrrstep R ⟷
   (∃f ss i t'. s = Fun f ss ∧ i < length ss ∧ t = Fun f (ss[i:=t']) ∧ (ss!i,t') ∈ rstep R)"
  (is "?L ⟷ ?R")
proof
  assume L: ?L
  from nrrstep_args[OF this]
  obtain f ss ts where "s = Fun f ss" "t = Fun f ts" by auto
  with nrrstep_imp_pos_term[OF L[unfolded this]]
  show ?R by auto
next assume R: ?R
  then obtain f i ss t'
    where s: "s = Fun f ss" and t: "t = Fun f (ss[i:=t'])"
      and i: "i < length ss" and st': "(ss ! i, t') ∈ rstep R" by auto
  from st' obtain C l r σ where lr: "(l, r) ∈ R" and s': "ss!i = C⟨l ⋅ σ⟩" and t': "t' = C⟨r ⋅ σ⟩" by auto
  let ?D = "More f (take i ss) C (drop (Suc i) ss)"
  have "s = ?D⟨l ⋅ σ⟩" "t = ?D⟨r ⋅ σ⟩" unfolding s t
    using id_take_nth_drop[OF i] upd_conv_take_nth_drop[OF i] s' t' by auto
  with lr show ?L apply(rule nrrstepI) using t' by auto
qed


lemma subterms_NF_imp_SN_on_nrrstep:
  assumes "∀s⊲t. s ∈ NF (rstep R)" shows "SN_on (nrrstep R) {t}"
proof
  fix S assume "S 0 ∈ {t}" and "∀i. (S i, S (Suc i)) ∈ nrrstep R"
  then have "(t, S (Suc 0)) ∈ nrrstep R" by auto
  then obtain l r C σ where "(l, r) ∈ R" and "C ≠ □" and t: "t = C⟨l⋅σ⟩" unfolding nrrstep_def' by auto
  then obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
  have "t ⊳ D⟨l⋅σ⟩" unfolding t C by auto
  moreover have "D⟨l⋅σ⟩ ∉ NF (rstep R)"
  proof -
    from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
    then show ?thesis by auto
  qed
  ultimately show False using assms by simp
qed

lemma args_NF_imp_SN_on_nrrstep:
  assumes "∀t∈set ts. t ∈ NF (rstep R)" shows "SN_on (nrrstep R) {Fun f ts}"
proof
  fix S assume "S 0 ∈ {Fun f ts}" and "∀i. (S i, S (Suc i)) ∈ nrrstep R"
  then have "(Fun f ts, S (Suc 0)) ∈ nrrstep R"
    unfolding singletonD[OF ‹S 0 ∈ {Fun f ts}›, symmetric] by simp
  then obtain l r C σ where "(l, r) ∈ R" and "C ≠ □" and "Fun f ts = C⟨l⋅σ⟩"
    unfolding nrrstep_def' by auto
  then obtain ss1 D ss2 where C: "C = More f ss1 D ss2" by (induct C) auto
  with ‹Fun f ts = C⟨l⋅σ⟩› have "D⟨l⋅σ⟩ ∈ set ts" by auto
  moreover have "D⟨l⋅σ⟩ ∉ NF (rstep R)"
  proof -
    from ‹(l, r) ∈ R› have "(D⟨l⋅σ⟩, D⟨r⋅σ⟩) ∈ rstep R" by auto
    then show ?thesis by auto
  qed
  ultimately show False using assms by simp
qed

lemma rrstep_imp_rule_subst:
  assumes "(s,t) ∈ rrstep R"
  shows "∃l r σ. (l,r) ∈ R ∧ (l⋅σ) = s ∧ (r⋅σ) = t"
proof -
  have "ctxt_of_pos_term [] s = Hole" by auto
  obtain l r σ where "(s,t) ∈ rstep_r_p_s R (l,r) [] σ" using assms unfolding rrstep_def by best
  then have "let C = ctxt_of_pos_term [] s in [] ∈ poss s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = s ∧ C⟨r⋅σ⟩ = t" unfolding rstep_r_p_s_def by simp
  with ‹ctxt_of_pos_term [] s = Hole› have "(l,r) ∈ R" and "l⋅σ = s" and "r⋅σ = t" unfolding Let_def by auto
  then show ?thesis by auto
qed

lemma nrrstep_preserves_root:
  assumes "(Fun f ss,t) ∈ nrrstep R" (is "(?s,t) ∈ nrrstep R") shows "∃ts. t = (Fun f ts)"
  using assms unfolding nrrstep_def rstep_r_p_s_def Let_def by auto

lemma nrrstep_equiv_root: assumes "(s,t) ∈ nrrstep R" shows "∃f ss ts. s = Fun f ss ∧ t = Fun f ts"
proof -
  from assms obtain f ss where "s = Fun f ss" using nrrstep_imp_Fun by best
  with assms obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
  from ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by best
qed

lemma nrrstep_reflects_root:
  assumes "(s,Fun g ts) ∈ nrrstep R" (is "(s,?t) ∈ nrrstep R")
  shows "∃ss. s = (Fun g ss)"
proof -
  from assms obtain f ss ts' where "s = Fun f ss" and "Fun g ts = Fun f ts'" using nrrstep_equiv_root by best
  then have "f = g" by simp
  with ‹s = Fun f ss› have "s = Fun g ss" by simp
  then show ?thesis by auto
qed

lemma nrrsteps_preserve_root:
  assumes "(Fun f ss,t) ∈ (nrrstep R)⇧*"
  shows "∃ts. t = (Fun f ts)"
  using assms by induct (auto simp: nrrstep_preserves_root)

lemma nrrstep_Fun_imp_arg_rsteps:
  assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R") and "i < length ss"
  shows "(ss!i,ts!i) ∈ (rstep R)⇧*"
proof -
  from assms have "[i] ∈ poss ?s" using empty_pos_in_poss by simp
  from ‹(?s,?t) ∈ nrrstep R›
  obtain l r j ps σ
    where A: "let C = ctxt_of_pos_term (j#ps) ?s in (j#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" unfolding nrrstep_def rstep_r_p_s_def by force
  let ?C = "ctxt_of_pos_term (j#ps) ?s"
  from A have "(j#ps) ∈ poss ?s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = ?s" and "?C⟨r⋅σ⟩ = ?t" using Let_def by auto
  have C: "?C = More f (take j ss) (ctxt_of_pos_term ps (ss!j)) (drop (Suc j) ss)" (is "?C = More f ?ss1 ?D ?ss2") by auto
  from ‹?C⟨l⋅σ⟩ = ?s› have "?D⟨l⋅σ⟩ = (ss!j)" by (auto simp: take_drop_imp_nth)
  from ‹(l,r) ∈ R› have "(l⋅σ,r⋅σ) ∈ (subst.closure R)" by auto
  then have "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))"
    and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" by (auto simp only: ctxt.closure.intros)
  then have D_rstep: "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ rstep R" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ rstep R"
    unfolding rstep_eq_closure by auto
  from ‹?C⟨r⋅σ⟩ = ?t› and C have "?t = Fun f (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
  then have ts: "ts = (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
  have "j = i ∨ j ≠ i" by simp
  from ‹j#ps ∈ poss ?s› have "j < length ss" by simp
  then have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! j = ?D⟨r⋅σ⟩" by (auto simp: nth_append_take)
  with ts have "ts!j = ?D⟨r⋅σ⟩" by auto
  have "j = i ∨ j ≠ i" by simp
  then show "(ss!i,ts!i) ∈ (rstep R)⇧*"
  proof
    assume "j = i"
    with ‹ts!j = ?D⟨r⋅σ⟩› and ‹?D⟨l⋅σ⟩ = ss!j› and D_rstep show ?thesis by auto
  next
    assume "j ≠ i"
    with ‹i < length ss› and ‹j < length ss› have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! i = ss!i" by (auto simp: nth_append_take_drop_is_nth_conv)
    with ts have "ts!i = ss!i" by auto
    then show ?thesis by auto
  qed
qed

lemma nrrstep_imp_arg_rsteps:
  assumes "(s,t) ∈ nrrstep R" and "i < num_args s" shows "(args s!i,args t!i) ∈ (rstep R)⇧*"
proof (cases s)
  fix x assume "s = Var x" then show ?thesis using assms by auto
next
  fix f ss assume "s = Fun f ss"
  then have "(Fun f ss,t) ∈ nrrstep R" using assms by simp
  then obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
  with ‹(s,t) ∈ nrrstep R› and ‹s = Fun f ss› have "(Fun f ss,Fun f ts) ∈ nrrstep R" by simp
  from  ‹s = Fun f ss› and ‹i < num_args s› have "i < length ss" by simp
  with ‹(Fun f ss,Fun f ts) ∈ nrrstep R›
  have "(ss!i,ts!i) ∈ (rstep R)⇧*" by (rule nrrstep_Fun_imp_arg_rsteps)
  with ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by simp
qed

lemma nrrsteps_imp_rsteps: "(s,t) ∈ (nrrstep R)⇧* ⟹ (s,t) ∈ (rstep R)⇧*"
proof (induct rule: rtrancl.induct)
  case (rtrancl_refl a) then show ?case by simp
next
  case (rtrancl_into_rtrancl a b c)
  then have IH: "(a,b) ∈ (rstep R)⇧*" and nrrstep: "(b,c) ∈ nrrstep R" by auto
  from nrrstep have "(b,c) ∈ rstep R" using nrrstep_imp_rstep by auto
  with IH show ?case by auto
qed

lemma nrrstep_Fun_preserves_num_args:
  assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R")
  shows "length ss = length ts"
proof -
  from assms obtain l r i ps σ
    where "let C = ctxt_of_pos_term (i#ps) ?s in (i#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" (is "let C = ?C in _")
    unfolding nrrstep_def rstep_r_p_s_def by force
  then have "(l,r) ∈ R" and Cl: "?C⟨l⋅σ⟩ = ?s" and Cr: "?C⟨r⋅σ⟩ = ?t" unfolding Let_def by auto
  have C: "?C = More f (take i ss) (ctxt_of_pos_term ps (ss!i)) (drop (Suc i) ss)" (is "?C = More f ?ss1 ?D ?ss2") by simp
  from C and Cl have s: "?s = Fun f (take i ss @ ?D⟨l⋅σ⟩ # drop (Suc i) ss)" (is "?s = Fun f ?ss") by simp
  from C and Cr have t: "?t = Fun f (take i ss @ ?D⟨r⋅σ⟩ # drop (Suc i) ss)" (is "?t = Fun f ?ts") by simp
  from s and t have ss: "ss = ?ss" and ts: "ts = ?ts" by auto
  have "length ?ss = length ?ts" by auto
  with ss and ts show ?thesis by simp
qed

lemma nrrstep_equiv_num_args:
  assumes "(s,t) ∈ nrrstep R" shows "num_args s = num_args t"
proof -
  from assms obtain f ss ts where s:"s = Fun f ss" and t:"t = Fun f ts" using nrrstep_equiv_root by best
  with assms have "(Fun f ss,Fun f ts) ∈ nrrstep R" by simp
  then have "length ss = length ts" by (rule nrrstep_Fun_preserves_num_args)
  with s and t show ?thesis by auto
qed

lemma nrrsteps_equiv_num_args:
  assumes "(s,t) ∈ (nrrstep R)⇧*" shows "num_args s = num_args t"
  using assms by (induct, auto simp: nrrstep_equiv_num_args)

lemma nrrstep_preserves_num_args:
  assumes "(s,t) ∈ nrrstep R" and "i < num_args s" shows "i < num_args t"
proof (cases s)
  fix x assume "s = Var x" then show ?thesis using assms by auto
next
  fix f ss assume "s = Fun f ss"
  with assms obtain ts where "t = Fun f ts" using nrrstep_preserves_root by best
  from ‹(s,t) ∈ nrrstep R› have "length ss = length ts" unfolding ‹s = Fun f ss› and ‹t = Fun f ts› by (rule nrrstep_Fun_preserves_num_args)
  with assms and ‹s = Fun f ss› and ‹t = Fun f ts› show ?thesis by auto
qed

lemma nrrstep_reflects_num_args:
  assumes "(s,t) ∈ nrrstep R" and "i < num_args t" shows "i < num_args s"
proof (cases t)
  fix x assume "t = Var x" then show ?thesis using assms by auto
next
  fix g ts assume "t = Fun g ts"
  with assms obtain ss where "s = Fun g ss" using nrrstep_reflects_root by best
  from ‹(s,t) ∈ nrrstep R› have "length ss = length ts" unfolding ‹s = Fun g ss› and ‹t = Fun g ts› by (rule nrrstep_Fun_preserves_num_args)
  with assms and ‹s = Fun g ss› and ‹t = Fun g ts› show ?thesis by auto
qed

lemma nrrsteps_imp_arg_rsteps:
  assumes "(s,t) ∈ (nrrstep R)⇧*" and "i < num_args s"
  shows "(args s!i,args t!i) ∈ (rstep R)⇧*"
  using assms
proof (induct rule: rtrancl.induct)
  case (rtrancl_refl a) then show ?case by auto
next
  case (rtrancl_into_rtrancl a b c)
  then have IH: "(args a!i,args b!i) ∈ (rstep R)⇧*" by auto
  from ‹(a,b) ∈ (nrrstep R)⇧*› and ‹i < num_args a› have "i < num_args b" by induct (auto simp: nrrstep_preserves_num_args)
  with ‹(b,c) ∈ nrrstep R›
  have "(args b!i,args c!i) ∈ (rstep R)⇧*" by (rule nrrstep_imp_arg_rsteps)
  with IH show ?case by simp
qed

lemma nrrsteps_imp_eq_root_arg_rsteps:
  assumes steps: "(s,t) ∈ (nrrstep R)⇧*"
  shows "root s = root t ∧ (∀i<num_args s. (s |_ [i], t |_ [i] ) ∈ (rstep R)⇧*)"
proof (cases s)
  case (Var x)
  have "s = t" using steps unfolding Var
  proof (induct)
    case (step y z)
    from nrrstep_imp_Fun[OF step(2)] step(3) have False by auto
    then show ?case ..
  qed simp
  then show ?thesis by auto
next
  case (Fun f ss)
  from nrrsteps_equiv_num_args[OF steps]
    nrrsteps_imp_arg_rsteps[OF steps]
    nrrsteps_preserve_root[OF steps[unfolded Fun]]
  show ?thesis unfolding Fun by auto
qed

lemma SN_on_imp_SN_on_subt:
  assumes "SN_on (rstep R) {t}" shows "∀s⊴t. SN_on (rstep R) {s}"
proof (rule ccontr)
  assume "¬(∀s⊴t. SN_on (rstep R) {s})"
  then obtain s where "t ⊵ s" and "¬ SN_on (rstep R) {s}" by auto
  then obtain S where "S 0 = s" and chain: "chain (rstep R) S" by auto
  from ‹t ⊵ s› obtain C where t: "t = C⟨s⟩" by auto
  let ?S = "λi. C⟨S i⟩"
  from ‹S 0 = s› have "?S 0 = t" by (simp add: t)
  moreover from chain have "chain (rstep R) ?S" by blast
  ultimately have "¬ SN_on (rstep R) {t}" by best
  with assms show False by simp
qed

lemma not_SN_on_subt_imp_not_SN_on:
  assumes "¬ SN_on (rstep R) {t}" and "s ⊵ t"
  shows "¬ SN_on (rstep R) {s}"
  using assms SN_on_imp_SN_on_subt by blast

lemma SN_on_instance_imp_SN_on_var:
  assumes "SN_on (rstep R) {t ⋅ σ}" and "x ∈ vars_term t"
  shows "SN_on (rstep R) {Var x ⋅ σ}"
proof -
  from assms have "t ⊵ Var x" by auto
  then have "t⋅σ ⊵ (Var x)⋅σ" by (rule supteq_subst)
  with SN_on_imp_SN_on_subt and assms show ?thesis by best
qed

lemma var_imp_var_of_arg:
  assumes "x ∈ vars_term (Fun f ss)" (is "x ∈ vars_term ?s")
  shows "∃i < num_args (Fun f ss). x ∈ vars_term (ss!i)"
proof -
  from assms have "x ∈ ⋃(set (map vars_term ss))" by simp
  then have "x ∈ (⋃i<length ss. vars_term(ss!i))" unfolding set_conv_nth by auto
  then have "∃i<length ss. x ∈ vars_term(ss!i)" using UN_iff by best
  then obtain i where "i < length ss" and "x ∈ vars_term(ss!i)" by auto
  then have "i < num_args ?s" by simp
  with ‹x ∈ vars_term(ss!i)› show ?thesis by auto
qed

lemma subt_instance_and_not_subst_imp_subt:
  "s⋅σ ⊵ t ⟹ ∀x ∈ vars_term s. ¬((Var x)⋅σ ⊵ t) ⟹ ∃u. s ⊵ u ∧ t = u⋅σ"
proof (induct s arbitrary: t rule: term.induct)
  case (Var x) then show ?case by auto
next
  case (Fun f ss)
  from ‹Fun f ss⋅σ ⊵ t› have "(Fun f ss⋅σ = t) ∨ (Fun f ss⋅σ ⊳ t)" by auto
  then show ?case
  proof
    assume "Fun f ss⋅σ = t" with Fun show ?thesis by auto
  next
    assume "Fun f ss⋅σ ⊳ t"
    then have "Fun f (map (λt. t⋅σ) ss) ⊳ t" by simp
    then have "∃s ∈ set (map (λt. t⋅σ) ss). s ⊵ t" (is "∃s ∈ set ?ss'. s ⊵ t") by (rule supt_Fun_imp_arg_supteq)
    then obtain s' where "s' ∈ set ?ss'" and "s' ⊵ t" by best
    then have "∃i < length ?ss'. ?ss'!i = s'" using in_set_conv_nth[where ?x = "s'"] by best
    then obtain i where "i < length ?ss'" and "?ss'!i = s'" by best
    then have "?ss'!i = (ss!i)⋅σ" by auto
    from ‹?ss'!i = s'› have "s' = (ss!i)⋅σ" unfolding ‹?ss'!i = (ss!i)⋅σ› by simp
    from ‹s' ⊵ t› have "(ss!i)⋅σ ⊵ t" unfolding ‹s' = (ss!i)⋅σ› by simp
    with ‹i < length ?ss'› have "(ss!i) ∈ set ss" by auto
    with ‹(ss!i)⋅σ ⊵ t› have "∃s ∈ set ss. s⋅σ ⊵ t" by best
    then obtain s where "s ∈ set ss" and "s⋅σ ⊵ t" by best
    with Fun have "∀x ∈ vars_term s. ¬((Var x)⋅σ ⊵ t)" by force
    from Fun
    have IH: "s ∈ set ss ⟶ (∀v. s⋅σ ⊵ v ⟶ (∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ v) ⟶ (∃u. s ⊵ u ∧ v = u⋅σ))"
      by auto
    with ‹s ∈ set ss› have "!!v. s⋅σ ⊵ v ⟹ (∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ v) ⟶ (∃u. s ⊵ u ∧ v = u⋅σ)"
      by simp
    with ‹s⋅σ ⊵ t› have "(∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ t) ⟶ (∃u. s ⊵ u ∧ t = u⋅σ)" by simp
    with ‹∀x ∈ vars_term s. ¬ Var x⋅σ ⊵ t› obtain u where "s ⊵ u" and "t = u⋅σ" by best
    with ‹s ∈ set ss› have "Fun f ss ⊵ u" by auto
    with ‹t = u⋅σ› show ?thesis by best
  qed
qed

lemma SN_imp_SN_subt:
  "SN_on (rstep R) {s} ⟹ s ⊵ t ⟹ SN_on (rstep R) {t}"
  by (rule ctxt_closed_SN_on_subt[OF ctxt_closed_rstep])

lemma subterm_preserves_SN_gen:
  assumes ctxt: "ctxt.closed R"
    and SN: "SN_on R {t}" and supt: "t ⊳ s"
  shows "SN_on R {s}"
proof -
  from supt have "t ⊵ s" by auto
  then show ?thesis using ctxt_closed_SN_on_subt[OF ctxt SN, of s] by simp
qed

context E_compatible
begin

lemma SN_on_step_E_imp_SN_on: assumes "SN_on R {s}"
  and "(s,t) ∈ E"
shows "SN_on R {t}"
  using assms E(1) unfolding SN_on_all_reducts_SN_on_conv[of _ t] SN_on_all_reducts_SN_on_conv[of _ s]
  by blast

lemma SN_on_step_REs_imp_SN_on:
  assumes R: "ctxt.closed R"
    and st: "(s,t) ∈ (R ∪ E O {⊳} O E)"
    and SN: "SN_on R {s}"
  shows "SN_on R {t}"
proof (cases "(s,t) ∈ R")
  case True
  from step_preserves_SN_on[OF this SN] show ?thesis .
next
  case False
  with st obtain u v where su: "(s,u) ∈ E" and uv: "u ⊳ v" and vt: "(v,t) ∈ E" by auto
  have u: "SN_on R {u}" by (rule SN_on_step_E_imp_SN_on[OF SN su])
  with uv R have "SN_on R {v}" by (metis subterm_preserves_SN_gen)
  then show ?thesis by (rule SN_on_step_E_imp_SN_on[OF _ vt])
qed

lemma restrict_SN_supt_E_I:
  "ctxt.closed R ⟹ SN_on R {s} ⟹ (s,t) ∈ R ∪ E O {⊳} O E ⟹ (s,t) ∈ restrict_SN_supt_E"
  unfolding restrict_SN_supt_E_def restrict_SN_def
  using SN_on_step_REs_imp_SN_on[of s t] E(2) by auto

lemma ctxt_closed_imp_SN_on_E_supt:
  assumes R: "ctxt.closed R"
    and SN: "SN (E O {⊳} O E)"
  shows "SN_on (R ∪ E O {⊳} O E) {t. SN_on R {t}}"
proof -
  {
    fix f
    assume f0: "SN_on R {f 0}" and f: "⋀ i. (f i, f (Suc i)) ∈ R ∪ E O {⊳} O E"
    from ctxt_closed_imp_SN_restrict_SN_E_supt[OF assms]
    have SN: "SN restrict_SN_supt_E" .
    {
      fix i
      have "SN_on R {f i}"
        by (induct i, rule f0, rule SN_on_step_REs_imp_SN_on[OF R f])
    } note fi = this
    {
      fix i
      from f[of i] fi[of i]
      have "(f i, f (Suc i)) ∈ restrict_SN_supt_E" by (metis restrict_SN_supt_E_I[OF R])
    }
    with SN have False by auto
  }
  then show ?thesis unfolding SN_on_def by blast
qed
end

lemma subterm_preserves_SN:
  "SN_on (rstep R) {t} ⟹ t ⊳ s ⟹ SN_on (rstep R) {s}"
  by (rule subterm_preserves_SN_gen[OF ctxt_closed_rstep])

lemma SN_on_r_imp_SN_on_supt_union_r:
  assumes ctxt: "ctxt.closed R"
    and "SN_on R T"
  shows "SN_on (supt ∪ R) T" (is "SN_on ?S T")
proof (rule ccontr)
  assume "¬ SN_on ?S T"
  then obtain s where ini: "s 0 : T" and chain: "chain ?S s"
    unfolding SN_on_def by auto
  have SN: "∀i. SN_on R {s i}"
  proof
    fix i show "SN_on R {s i}"
    proof (induct i)
      case 0 show ?case using assms using ‹s 0 ∈ T› and SN_on_subset2[of "{s 0}" T R] by simp
    next
      case (Suc i)
      from chain have "(s i, s (Suc i)) ∈ ?S" by simp
      then show ?case
      proof
        assume "(s i, s (Suc i)) ∈ supt"
        from subterm_preserves_SN_gen[OF ctxt Suc this] show ?thesis .
      next
        assume "(s i, s (Suc i)) ∈ R"
        from step_preserves_SN_on[OF this Suc] show ?thesis .
      qed
    qed
  qed
  have "¬ (∃S. ∀i. (S i, S (Suc i)) ∈ restrict_SN_supt R)"
    using ctxt_closed_imp_SN_restrict_SN_supt[OF ctxt] unfolding SN_defs by auto
  moreover have "∀i. (s i, s (Suc i)) ∈ restrict_SN_supt R"
  proof
    fix i
    from SN have SN: "SN_on R {s i}" by simp
    from chain have "(s i, s (Suc i)) ∈ supt ∪ R" by simp
    then show "(s i, s (Suc i)) ∈ restrict_SN_supt R"
      unfolding restrict_SN_supt_def restrict_SN_def using SN by auto
  qed
  ultimately show False by auto
qed

lemma SN_on_rstep_imp_SN_on_supt_union_rstep:
  "SN_on (rstep R) T ⟹ SN_on (supt ∪ rstep R) T"
  by (rule SN_on_r_imp_SN_on_supt_union_r[OF ctxt_closed_rstep])

lemma SN_supt_r_trancl:
  assumes ctxt: "ctxt.closed R"
    and a: "SN R"
  shows "SN ((supt ∪ R)⇧+)"
proof -
  have "SN (supt ∪ R)"
    using SN_on_r_imp_SN_on_supt_union_r[OF ctxt, of UNIV]
      and a by force
  then show "SN ((supt ∪ R)⇧+)" by (rule SN_imp_SN_trancl)
qed

lemma SN_supt_rstep_trancl:
  "SN (rstep R) ⟹ SN ((supt ∪ rstep R)⇧+)"
  by (rule SN_supt_r_trancl[OF ctxt_closed_rstep])

lemma SN_imp_SN_arg_gen:
  assumes ctxt: "ctxt.closed R"
    and SN: "SN_on R {Fun f ts}" and arg: "t ∈ set ts" shows "SN_on R {t}"
proof -
  from arg have "Fun f ts ⊵ t" by auto
  with SN show ?thesis by (rule ctxt_closed_SN_on_subt[OF ctxt])
qed

lemma SN_imp_SN_arg:
  "SN_on (rstep R) {Fun f ts} ⟹ t ∈ set ts ⟹ SN_on (rstep R) {t}"
  by (rule SN_imp_SN_arg_gen[OF ctxt_closed_rstep])

lemma SNinstance_imp_SN:
  assumes "SN_on (rstep R) {t ⋅ σ}"
  shows "SN_on (rstep R) {t}"
proof
  fix f
  assume prem: "f 0 ∈ {t}" "∀i. (f i, f (Suc i)) ∈ rstep R" 
  let ?g = "λ i. (f i) ⋅ σ"
  from prem have "?g 0 = t ⋅ σ ∧ (∀ i. (?g i, ?g (Suc i)) ∈ rstep R)" using subst_closed_rstep
    by auto
  then have "¬ SN_on (rstep R) {t ⋅ σ}" by auto
  with assms show False by blast
qed

lemma rstep_imp_C_s_r:
  assumes "(s,t) ∈ rstep R"
  shows "∃C σ l r. (l,r) ∈ R ∧ s = C⟨l⋅σ⟩ ∧ t = C⟨r⋅σ⟩"
proof -
  from assms obtain l r p σ where step:"(s,t) ∈ rstep_r_p_s R (l,r) p σ"
    unfolding rstep_iff_rstep_r_p_s by best
  let ?C = "ctxt_of_pos_term p s"
  from step have "p ∈ poss s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = s" and "?C⟨r⋅σ⟩ = t"
    unfolding rstep_r_p_s_def Let_def by auto
  then have "(l,r) ∈ R ∧ s = ?C⟨l⋅σ⟩ ∧ t = ?C⟨r⋅σ⟩" by auto
  then show ?thesis by force
qed

fun map_funs_rule :: "('f ⇒ 'g) ⇒ ('f, 'v) rule ⇒ ('g, 'v) rule"
  where
    "map_funs_rule fg lr = (map_funs_term fg (fst lr), map_funs_term fg (snd lr))"

fun map_funs_trs :: "('f ⇒ 'g) ⇒ ('f, 'v) trs ⇒ ('g, 'v) trs"
  where
    "map_funs_trs fg R = map_funs_rule fg ` R"

lemma map_funs_trs_union: "map_funs_trs fg (R ∪ S) = map_funs_trs fg R ∪ map_funs_trs fg S"
  unfolding map_funs_trs.simps by auto

lemma rstep_map_funs_term: assumes R: "⋀ f. f ∈ funs_trs R ⟹ h f = f" and step: "(s,t) ∈ rstep R"
  shows "(map_funs_term h s, map_funs_term h t) ∈ rstep R"
proof -
  from step obtain C l r σ where s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and rule: "(l,r) ∈ R" by auto
  let ?σ = "map_funs_subst h σ"
  let ?h = "map_funs_term h"
  note funs_defs = funs_rule_def[abs_def] funs_trs_def
  from rule have lr: "funs_term l ∪ funs_term r ⊆ funs_trs 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 ?thesis unfolding s t
    unfolding map_funs_subst_distrib map_funs_term_ctxt_distrib hl hr
    by (rule rstepI[OF rule refl refl])
qed

lemma wf_trs_map_funs_trs[simp]: "wf_trs (map_funs_trs f R) = wf_trs R"
  unfolding wf_trs_def
proof (rule iffI, intro allI impI)
  fix l r
  assume "∀l r. (l, r) ∈ map_funs_trs f R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l" and "(l, r) ∈ R"
  then show "(∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l" by (cases l, force+)
next
  assume ass: " ∀l r. (l, r) ∈ R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
  show "∀l r. (l, r) ∈ map_funs_trs f R ⟶ (∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
  proof (intro allI impI)
    fix l r
    assume "(l, r) ∈ map_funs_trs f R"
    with ass
    show "(∃f ts. l = Fun f ts) ∧ vars_term r ⊆ vars_term l"
      by (cases l, force+)
  qed
qed

lemma map_funs_trs_comp: "map_funs_trs fg (map_funs_trs gh R) = map_funs_trs (fg o gh) R"
proof -
  have mr: "map_funs_rule (fg o gh) = map_funs_rule fg o map_funs_rule gh"
    by (rule ext, auto simp: map_funs_term_comp)
  then show ?thesis
    by (auto simp: map_funs_term_comp image_comp mr)
qed

lemma map_funs_trs_mono: assumes "R ⊆ R'" shows "map_funs_trs fg R ⊆ map_funs_trs fg R'"
  using assms by auto

lemma map_funs_trs_power_mono:
  fixes R R' :: "('f,'v)trs" and fg :: "'f ⇒ 'f"
  assumes "R ⊆ R'" shows "((map_funs_trs fg)^^n) R ⊆ ((map_funs_trs fg)^^n) R'"
  using assms by (induct n, simp, auto)

declare map_funs_trs.simps[simp del]

lemma rstep_imp_map_rstep:
  assumes "(s, t) ∈ rstep R"
  shows "(map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
  using assms
proof (induct)
  case (IH C σ l r)
  then have "(map_funs_term fg l, map_funs_term fg r) ∈ map_funs_trs fg R" (is "(?l, ?r) ∈ ?R")
    unfolding map_funs_trs.simps by force
  then have "(?l, ?r) ∈ rstep ?R" ..
  then have "(?l ⋅ map_funs_subst fg σ, ?r ⋅ map_funs_subst fg σ) ∈ rstep ?R" ..
  then show ?case by auto
qed

lemma rsteps_imp_map_rsteps: assumes "(s,t) ∈ (rstep R)⇧*"
  shows "(map_funs_term fg s, map_funs_term fg t) ∈ (rstep (map_funs_trs fg R))⇧*"
  using assms
proof (induct, clarify)
  case (step y z)
  then have "(map_funs_term fg y, map_funs_term fg z) ∈ rstep (map_funs_trs fg R)" using rstep_imp_map_rstep
    by (auto simp: map_funs_trs.simps)
  with step show ?case by auto
qed

lemma SN_map_imp_SN:
  assumes SN: "SN_on (rstep (map_funs_trs fg R)) {map_funs_term fg t}"
  shows "SN_on (rstep R) {t}"
proof (rule ccontr)
  assume "¬ SN_on (rstep R) {t}"
  from this obtain f where cond: "f 0 = t ∧ (∀ i. (f i, f (Suc i)) ∈ rstep R)"
    unfolding SN_on_def by auto
  obtain g where g: "g = (λ i. map_funs_term fg (f i))" by auto
  with cond have cond2: "g 0 = map_funs_term fg t ∧ (∀ i. (g i, g (Suc i)) ∈ rstep (map_funs_trs fg R))"
    using rstep_imp_map_rstep[where fg = fg] by blast
  from SN
  have "¬ (∃ g. (g 0 = map_funs_term fg t ∧ (∀ i. (g i, g (Suc i)) ∈ rstep (map_funs_trs fg R))))"
    unfolding SN_on_def by auto
  with cond2 show False  by auto
qed

lemma rstep_iff_map_rstep:
  assumes "inj fg"
  shows "(s, t) ∈ rstep R ⟷ (map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
proof
  assume "(s,t) ∈ rstep R"
  then show "(map_funs_term fg s, map_funs_term fg t) ∈ rstep(map_funs_trs fg R)"
    by (rule rstep_imp_map_rstep)
next
  assume "(map_funs_term fg s, map_funs_term fg t) ∈ rstep (map_funs_trs fg R)"
  then have "(map_funs_term fg s, map_funs_term fg t) ∈ ctxt.closure(subst.closure(map_funs_trs fg R))"
    by (simp add: rstep_eq_closure)
  then obtain C u v where "(u,v) ∈ subst.closure(map_funs_trs fg R)" and "C⟨u⟩ = map_funs_term fg s"
    and "C⟨v⟩ = map_funs_term fg t"
    by (cases rule: ctxt.closure.cases) force
  then obtain σ w x where "(w,x) ∈ map_funs_trs fg R" and "w⋅σ = u" and "x⋅σ = v"
    by (cases rule: subst.closure.cases) force
  then obtain l r where "w = map_funs_term fg l" and "x = map_funs_term fg r"
    and "(l,r) ∈ R" by (auto simp: map_funs_trs.simps)
  have ps: "C⟨map_funs_term fg l ⋅ σ⟩ = map_funs_term fg s" and pt: "C⟨map_funs_term fg r ⋅ σ⟩ = map_funs_term fg t"
    unfolding ‹w = map_funs_term fg l›[symmetric] ‹x = map_funs_term fg r›[symmetric] ‹w⋅σ = u› ‹x⋅σ = v›
      ‹C⟨u⟩ = map_funs_term fg s› ‹C⟨v⟩ = map_funs_term fg t› by auto
  let ?gf = "the_inv fg"
  let ?C = "map_funs_ctxt ?gf C"
  let ?σ = "map_funs_subst ?gf σ"
  have gffg: "?gf ∘ fg = id" using the_inv_f_f[OF assms] by (intro ext, auto)
  from ps and pt have "s = map_funs_term ?gf (C⟨map_funs_term fg l ⋅ σ⟩)"
    and "t = map_funs_term ?gf (C⟨map_funs_term fg r ⋅ σ⟩)" by (auto simp: map_funs_term_comp gffg)
  then have s: "s = ?C⟨map_funs_term ?gf (map_funs_term fg l ⋅ σ)⟩"
    and t: "t = ?C⟨map_funs_term ?gf (map_funs_term fg r ⋅ σ)⟩" using map_funs_term_ctxt_distrib by auto
  from s have "s = ?C⟨l⋅?σ⟩" by (simp add: map_funs_term_comp gffg)
  from t have "t = ?C⟨r⋅?σ⟩" by (simp add: map_funs_term_comp gffg)
  from ‹(l, r) ∈ R› have "(l⋅?σ, r⋅?σ) ∈ subst.closure R" by blast
  then have "(?C⟨l⋅?σ⟩,?C⟨r⋅?σ⟩) ∈ ctxt.closure(subst.closure R)" by blast
  then show "(s,t) ∈ rstep R" unfolding ‹s = ?C⟨l⋅?σ⟩› ‹t = ?C⟨r⋅?σ⟩› by (simp add: rstep_eq_closure)
qed

lemma rstep_map_funs_trs_power_mono:
  fixes R R' :: "('f,'v)trs" and fg :: "'f ⇒ 'f"
  assumes subset: "R ⊆ R'" shows "rstep (((map_funs_trs fg)^^n) R) ⊆ rstep (((map_funs_trs fg)^^n) R')"
  by (rule rstep_mono, rule map_funs_trs_power_mono, rule subset)

lemma subsetI3: "(⋀x y z. (x, y, z) ∈ A ⟹ (x, y, z) ∈ B) ⟹ A ⊆ B" by auto

lemma aux: "(⋃a∈P. {(x,y,z). x = fst a ∧ y = snd a ∧ Q a z}) = {(x,y,z). (x,y) ∈ P ∧ Q (x,y) z}" (is "?P = ?Q")
proof
  show "?P ⊆ ?Q"
  proof
    fix x assume "x ∈ ?P"
    then obtain a where "a ∈ P" and "x ∈ {(x,y,z). x = fst a ∧ y = snd a ∧ Q a z}" by auto
    then obtain b where "Q (fst x, fst (snd x)) (snd (snd x))" and "(fst x, fst (snd x)) = a" and "snd (snd x) = b" by force
    from ‹a ∈ P› have "(fst a,snd a) ∈ P" unfolding split_def by simp
    from ‹Q (fst x, fst (snd x)) (snd (snd x))› have "Q a b" unfolding ‹(fst x, fst (snd x)) = a› ‹snd (snd x) = b› .
    from ‹(fst a,snd a) ∈ P› and ‹Q a b› show "x ∈ ?Q" unfolding split_def ‹(fst x, fst (snd x)) = a›[symmetric] ‹snd (snd x) = b›[symmetric] by simp
  qed
next
  show "?Q ⊆ ?P"
  proof (rule subsetI3)
    fix x y z assume "(x,y,z) ∈ ?Q"
    then have "(x,y) ∈ P" and "Q (x,y) z" by auto
    then have "x = fst(x,y) ∧ y = snd(x,y) ∧ Q (x,y) z" by auto
    then have "(x,y,z) ∈ {(x,y,z). x = fst(x,y) ∧ y = snd(x,y) ∧ Q (x,y) z}" by auto
    then have "∃p∈P. (x,y,z) ∈ {(x,y,z). x = fst p ∧ y = snd p ∧ Q p z}" using ‹(x,y) ∈ P› by blast
    then show "(x,y,z) ∈ ?P" unfolding UN_iff[symmetric] by simp
  qed
qed

lemma finite_imp_finite_DP_on':
  assumes "finite R"
  shows "finite {(l, r, u).
    ∃h us. u = Fun h us ∧ (l, r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬ (l ⊳ u)}"
proof -
  have "⋀l r. (l, r) ∈ R ⟹ finite {u. r ⊵ u}"
  proof -
    fix l r
    assume "(l, r) ∈ R"
    show "finite {u. r ⊵ u}" by (rule finite_subterms)
  qed
  with ‹finite R› have "finite(⋃(l, r) ∈ R. {u. r ⊵ u})" by auto
  have "finite(⋃lr∈R. {(l, r, u). l = fst lr ∧ r = snd lr ∧ snd lr ⊵ u})"
  proof (rule finite_UN_I)
    show "finite R" by (rule ‹finite R›)
  next
    fix lr
    assume "lr ∈ R"
    have "finite {u. snd lr ⊵ u}" by (rule finite_subterms)
    then show "finite {(l,r,u). l = fst lr ∧ r = snd lr ∧ snd lr ⊵ u}" by auto
  qed
  then have "finite {(l,r,u). (l,r) ∈ R ∧ r ⊵ u}" unfolding aux by auto
  have "{(l,r,u). (l,r) ∈ R ∧ r ⊵ u} ⊇ {(l,r,u). (∃h us. u = Fun h us ∧ (l,r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬(l ⊳ u))}" by auto
  with ‹finite {(l,r,u). (l,r) ∈ R ∧ r ⊵ u}› show ?thesis using finite_subset by fast
qed

lemma card_image_le':
  assumes "finite S"
  shows "card (⋃y∈S.{x. x = f y}) ≤ card S"
proof -
  have A:"(⋃y∈S. {x. x = f y}) = f ` S" by auto
  from assms show ?thesis unfolding A using card_image_le by auto
qed

lemma subteq_of_map_imp_map: "map_funs_term g s ⊵ t ⟹ ∃u. t = map_funs_term g u"
proof (induct s arbitrary: t)
  case (Var x)
  then have "map_funs_term g (Var x) ⊳ t ∨ map_funs_term g (Var x) = t" by auto
  then show ?case
  proof
    assume "map_funs_term g (Var x) ⊳ t" then show ?thesis by (cases rule: supt.cases) auto
  next
    assume "map_funs_term g (Var x) = t" then show ?thesis by best
  qed
next
  case (Fun f ss)
  then have "map_funs_term g (Fun f ss) ⊳ t ∨ map_funs_term g (Fun f ss) = t" by auto
  then show ?case
  proof
    assume "map_funs_term g (Fun f ss) ⊳ t"
    then show ?case using Fun by (cases rule: supt.cases) (auto simp: supt_supteq_conv)
  next
    assume "map_funs_term g (Fun f ss) = t" then show ?thesis by best
  qed
qed

lemma map_funs_term_inj:
  assumes "inj (fg :: ('f ⇒ 'g))"
  shows "inj (map_funs_term fg)"
proof -
  {
    fix s t :: "('f,'v)term"
    assume "map_funs_term fg s = map_funs_term fg t"
    then have "s = t"
    proof (induct s arbitrary: t)
      case (Var x) with assms show ?case by (induct t) auto
    next
      case (Fun f ss) then show ?case
      proof (induct t)
        case (Var y) then show ?case by auto
      next
        case (Fun g ts)
        then have A: "map (map_funs_term fg) ss = map (map_funs_term fg) ts" by simp
        then have len_eq:"length ss = length ts" by (rule map_eq_imp_length_eq)
        from A have "!!i. i < length ss ⟹ (map (map_funs_term fg) ss)!i = (map (map_funs_term fg) ts)!i" by auto
        with len_eq have eq: "!!i. i < length ss ⟹ map_funs_term fg  (ss!i) = map_funs_term fg (ts!i)" using nth_map by auto
        have in_set: "!!i. i < length ss ⟹ (ss!i) ∈ set ss" by auto
        from Fun have "∀i < length ss. (ss!i) = (ts!i)" using in_set eq by auto
        with len_eq have "ss = ts" using nth_equalityI[where xs = ss and ys = ts] by simp
        have "f = g" using Fun ‹inj fg› unfolding inj_on_def by auto
        with ‹ss = ts› show ?case by simp
      qed
    qed
  }
  then show ?thesis unfolding inj_on_def by auto
qed

lemma rsteps_closed_ctxt:
  assumes "(s, t) ∈ (rstep R)⇧*"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧*"
proof -
  from assms obtain n where "(s,t) ∈ (rstep R)^^n"
    using rtrancl_is_UN_relpow by auto
  then show ?thesis
  proof (induct n arbitrary: s)
    case 0 then show ?case by auto
  next
    case (Suc n)
    from relpow_Suc_D2[OF ‹(s,t) ∈ (rstep R)^^Suc n›] obtain u
      where "(s,u) ∈ (rstep R)" and "(u,t) ∈ (rstep R)^^n" by auto
    from ‹(s,u) ∈ (rstep R)› have "(C⟨s⟩,C⟨u⟩) ∈ (rstep R)" ..
    from Suc and ‹(u,t) ∈ (rstep R)^^n› have "(C⟨u⟩,C⟨t⟩) ∈ (rstep R)⇧*" by simp
    with ‹(C⟨s⟩,C⟨u⟩) ∈ (rstep R)› show ?case by auto
  qed
qed

lemma one_imp_ctxt_closed: assumes one: "⋀ f bef s t aft. (s,t) ∈ r ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r"
  shows "ctxt.closed r"
proof
  fix s t C
  assume st: "(s,t) ∈ r"
  show "(C⟨s⟩, C⟨t⟩) ∈ r"
  proof (induct C)
    case (More f bef C aft)
    from one[OF More] show ?case by auto
  qed (insert st, auto)
qed

lemma ctxt_closed_nrrstep [intro]: "ctxt.closed (nrrstep R)"
proof (rule one_imp_ctxt_closed)
  fix f bef s t aft
  assume "(s,t) ∈ nrrstep R"
  from this[unfolded nrrstep_def'] obtain l r C σ
    where lr: "(l,r) ∈ R" and C: "C ≠ □"
      and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
  show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ nrrstep R"
  proof (rule nrrstepI[OF lr])
    show "More f bef C aft ≠ □" by simp
  qed (insert s t, auto)
qed

definition all_ctxt_closed :: "'f sig ⇒ ('f, 'v) trs ⇒ bool" where
  "all_ctxt_closed F r ⟷ (∀f ts ss. (f, length ss) ∈ F ⟶ length ts = length ss ⟶
    (∀i. i < length ts ⟶ (ts ! i, ss ! i) ∈ r) ⟶ (∀ i. i < length ts ⟶ funas_term (ts ! i) ∪ funas_term (ss ! i) ⊆ F) ⟶ (Fun f ts, Fun f ss) ∈ r) ∧ (∀ x. (Var x, Var x) ∈ r)"

lemma all_ctxt_closedD: "all_ctxt_closed F r ⟹ (f,length ss) ∈ F ⟹ length ts = length ss
  ⟹ ⟦⋀ i. i < length ts ⟹ (ts ! i, ss ! i) ∈ r ⟧
  ⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ts ! i) ⊆ F ⟧
  ⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ss ! i) ⊆ F ⟧
  ⟹ (Fun f ts, Fun f ss) ∈ r"
  unfolding all_ctxt_closed_def by auto

lemma all_ctxt_closed_sig_reflE: assumes all: "all_ctxt_closed F r"
  shows "funas_term t ⊆ F ⟹ (t,t) ∈ r"
proof (induct t)
  case (Var x)
  from all[unfolded all_ctxt_closed_def] show ?case by auto
next
  case (Fun f ts)
  show ?case
    by (rule all_ctxt_closedD[OF all _ _ Fun(1)], insert Fun(2), force+)
qed

lemma all_ctxt_closed_reflE: assumes all: "all_ctxt_closed UNIV r"
  shows "(t,t) ∈ r"
  by (rule all_ctxt_closed_sig_reflE[OF all], auto)

lemma all_ctxt_closed_relcomp: assumes "all_ctxt_closed UNIV R" "all_ctxt_closed UNIV S"
  shows "all_ctxt_closed UNIV (R O S)"
  unfolding all_ctxt_closed_def
proof (intro allI impI conjI)
  show "(Var x, Var x) ∈ R O S" for x using assms unfolding all_ctxt_closed_def by auto
  fix f ts ss
  assume len: "length ts = length ss" 
    and steps: "∀i<length ts. (ts ! i, ss ! i) ∈ R O S" 
  hence "∀ i. ∃ us. i < length ts ⟶ (ts ! i, us) ∈ R ∧ (us, ss ! i) ∈ S" by blast
  from choice[OF this] obtain us where steps: "⋀ i. i<length ts ⟹ (ts ! i, us i) ∈ R ∧ (us i, ss ! i) ∈ S" 
    by blast
  let ?us = "map us [0..<length ss]" 
  from all_ctxt_closedD[OF assms(2)] steps len have us: "(Fun f ?us, Fun f ss) ∈ S" by auto
  from all_ctxt_closedD[OF assms(1)] steps len have tu: "(Fun f ts, Fun f ?us) ∈ R" by force
  from tu us 
  show "(Fun f ts, Fun f ss) ∈ R O S" by auto
qed

lemma all_ctxt_closed_relpow:
  assumes acc:"all_ctxt_closed UNIV Q"
  shows "all_ctxt_closed UNIV (Q ^^ n)"
proof (induct n)
  case 0
  thus ?case by (auto simp: all_ctxt_closed_def nth_equalityI)
next
  case (Suc n)
  from all_ctxt_closed_relcomp[OF this acc]
  show ?case by simp
qed


lemma all_ctxt_closed_subst_step_sig:
  fixes r :: "('f, 'v) trs" and t :: "('f, 'v) term"
  assumes all: "all_ctxt_closed F r"
    and sig: "funas_term t ⊆ F"
    and steps: "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r"
    and sig_subst: "⋀ x. x ∈ vars_term t ⟹ funas_term (σ x) ∪ funas_term (τ x) ⊆ F"
  shows "(t ⋅ σ, t ⋅ τ) ∈ r"
  using sig steps sig_subst
proof (induct t)
  case (Var x)
  then show ?case by auto
next
  case (Fun f ts)
  {
    fix t
    assume t: "t ∈ set ts"
    with Fun(2-3) have "funas_term t ⊆ F" "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r" by auto
    from Fun(1)[OF t this Fun(4)] t have step: "(t ⋅ σ, t ⋅ τ) ∈ r" by auto
    from Fun(4) t have "⋀ x. x ∈ vars_term t ⟹ funas_term (σ x) ∪ funas_term (τ x) ⊆ F" by auto
    with ‹funas_term t ⊆ F› have "funas_term (t ⋅ σ) ∪ funas_term (t ⋅ τ) ⊆ F" unfolding funas_term_subst by auto
    note step this
  }
  then have steps: "⋀ i. i < length ts ⟹ (ts ! i ⋅ σ, ts ! i ⋅ τ) ∈ r ∧ funas_term (ts ! i ⋅ σ) ∪ funas_term (ts ! i ⋅ τ) ⊆ F" unfolding set_conv_nth by auto
  with all_ctxt_closedD[OF all, of f "map (λ t. t ⋅ τ) ts" "map (λ t. t ⋅ σ) ts"] Fun(2)
  show ?case by auto
qed

lemma all_ctxt_closed_subst_step:
  fixes r :: "('f, 'v) trs" and t :: "('f, 'v) term"
  assumes all: "all_ctxt_closed UNIV r"
    and steps: "⋀ x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ r"
  shows "(t ⋅ σ, t ⋅ τ) ∈ r"
  by (rule all_ctxt_closed_subst_step_sig[OF all _ steps], auto)

lemma all_ctxt_closed_ctxtE: assumes all: "all_ctxt_closed F R"
  and Fs: "funas_term s ⊆ F"
  and Ft: "funas_term t ⊆ F"
  and step: "(s,t) ∈ R"
shows "funas_ctxt C ⊆ F ⟹ (C ⟨ s ⟩, C ⟨ t ⟩) ∈ R"
proof(induct C)
  case Hole
  from step show ?case by auto
next
  case (More f bef C aft)
  let ?n = "length bef"
  let ?m = "Suc (?n + length aft)"
  show ?case unfolding intp_actxt.simps
  proof (rule all_ctxt_closedD[OF all])
    fix i
    let ?t = "λ s. (bef @ C ⟨ s ⟩ # aft) ! i"
    assume "i < length (bef @ C⟨s⟩ # aft)"
    then have i: "i < ?m" by auto
    then have mem: "⋀ s. ?t s ∈ set (bef @ C ⟨ s ⟩ # aft)" unfolding set_conv_nth by auto
    from mem[of s] More Fs show "funas_term (?t s) ⊆ F" by auto
    from mem[of t] More Ft show "funas_term (?t t) ⊆ F" by auto
    from More have step: "(C ⟨ s ⟩, C ⟨ t ⟩) ∈ R" by auto
    {
      fix s
      assume "s ∈ set bef ∪ set aft"
      with More have "funas_term s ⊆ F" by auto
      from all_ctxt_closed_sig_reflE[OF all this] have "(s,s) ∈ R" by auto
    } note steps = this
    show "(?t s, ?t t) ∈ R"
    proof (cases "i = ?n")
      case True
      then show ?thesis using step by auto
    next
      case False
      show ?thesis
      proof (cases "i < ?n")
        case True
        then show ?thesis unfolding append_Cons_nth_left[OF True] using steps by auto
      next
        case False
        with ‹i ≠ ?n› i have "∃ k. k < length aft ∧ i = Suc ?n + k" by presburger
        then obtain k where k: "k < length aft" and i: "i = Suc ?n + k" by auto
        from k show ?thesis using steps unfolding i by (auto simp: nth_append)
      qed
    qed
  qed (insert More, auto)
qed

lemma trans_ctxt_sig_imp_all_ctxt_closed: assumes tran: "trans r"
  and refl: "⋀ t. funas_term t ⊆ F ⟹ (t,t) ∈ r"
  and ctxt: "⋀ C s t. funas_ctxt C ⊆ F ⟹ funas_term s ⊆ F ⟹ funas_term t ⊆ F ⟹ (s,t) ∈ r ⟹ (C ⟨ s ⟩, C ⟨ t ⟩) ∈ r"
shows "all_ctxt_closed F r"
  unfolding all_ctxt_closed_def
proof (intro conjI, intro allI impI)
  fix f ts ss
  assume f: "(f,length ss) ∈ F" and
    l: "length ts = length ss" and
    steps: "∀ i < length ts. (ts ! i, ss ! i) ∈ r" and
    sig: "∀ i < length ts. funas_term (ts ! i) ∪  funas_term (ss ! i) ⊆ F"
  from sig have sig_ts: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ F"  unfolding set_conv_nth by auto
  let ?p = "λ ss. (Fun f ts, Fun f ss) ∈ r ∧ funas_term (Fun f ss) ⊆ F"
  let ?r = "λ xsi ysi. (xsi, ysi) ∈ r ∧ funas_term ysi ⊆ F"
  have init: "?p ts" by (rule conjI[OF refl], insert f sig_ts l, auto)
  have "?p ss"
  proof (rule parallel_list_update[where p = ?p and r = ?r, OF _ HOL.refl init l[symmetric]])
    fix xs i y
    assume len: "length xs = length ts"
      and i: "i < length ts"
      and r: "?r (xs ! i) y"
      and p: "?p xs"
    let ?C = "More f (take i xs) Hole (drop (Suc i) xs)"
    have id1: "Fun f xs = ?C ⟨ xs ! i⟩" using id_take_nth_drop[OF i[folded len]] by simp
    have id2: "Fun f (xs[i := y]) = ?C ⟨ y ⟩" using upd_conv_take_nth_drop[OF i[folded len]] by simp
    from p[unfolded id1] have C: "funas_ctxt ?C ⊆ F" and xi: "funas_term (xs ! i) ⊆ F" by auto
    from r have "funas_term y ⊆ F" "(xs ! i, y) ∈ r" by auto
    with ctxt[OF C xi this] C have r: "(Fun f xs, Fun f (xs[i := y])) ∈ r"
      and f: "funas_term (Fun f (xs[i := y])) ⊆ F" unfolding id1 id2 by auto
    from p r tran have "(Fun f ts, Fun f (xs[i := y])) ∈ r" unfolding trans_def by auto
    with f
    show "?p (xs[i := y])"  by auto
  qed (insert sig steps, auto)
  then show "(Fun f ts, Fun f ss) ∈ r" ..
qed (insert refl, auto)

lemma trans_ctxt_imp_all_ctxt_closed: assumes tran: "trans r"
  and refl: "refl r"
  and ctxt: "ctxt.closed r"
shows "all_ctxt_closed F r"
  by (rule trans_ctxt_sig_imp_all_ctxt_closed[OF tran _ ctxt.closedD[OF ctxt]], insert refl[unfolded refl_on_def], auto)

lemma all_ctxt_closed_rsteps[intro]: "all_ctxt_closed F ((rstep r)⇧*)"
  by (blast intro: trans_ctxt_imp_all_ctxt_closed trans_rtrancl refl_rtrancl)

lemma subst_rsteps_imp_rsteps:
  fixes σ :: "('f, 'v) subst"
  assumes "⋀ x. x∈vars_term t ⟹ (σ x, τ x) ∈ (rstep R)⇧*"
  shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep R)⇧*"
  by (rule all_ctxt_closed_subst_step)
    (insert assms, auto)

lemma rtrancl_trancl_into_trancl:
  assumes len: "length ts = length ss"
    and steps: "∀ i < length ts. (ts ! i, ss ! i) ∈ R⇧*"
    and i: "i < length ts"
    and step: "(ts ! i, ss ! i) ∈ R⇧+"
    and ctxt: "ctxt.closed R"
  shows "(Fun f ts, Fun f ss) ∈ R⇧+"
proof -
  from ctxt have ctxt_rt: "ctxt.closed (R⇧*)" by blast
  from ctxt have ctxt_t: "ctxt.closed (R⇧+)" by blast
  from id_take_nth_drop[OF i] have ts: "ts = take i ts @ ts ! i # drop (Suc i) ts" (is "_ = ?ts") by auto
  from id_take_nth_drop[OF i[simplified len]] have ss: "ss = take i ss @ ss ! i # drop (Suc i) ss" (is "_ = ?ss") by auto
  let ?mid = "take i ss @ ts ! i # drop (Suc i) ss"
  from trans_ctxt_imp_all_ctxt_closed[OF trans_rtrancl refl_rtrancl ctxt_rt] have all: "all_ctxt_closed UNIV (R⇧*)" .
  from ctxt_closed_one[OF ctxt_t step] have "(Fun f ?mid, Fun f ?ss) ∈ R⇧+" .
  then have part1: "(Fun f ?mid, Fun f ss) ∈ R⇧+" unfolding ss[symmetric] .
  from ts have lents: "length ts =  length ?ts" by simp
  have "(Fun f ts, Fun f ?mid) ∈ R⇧*"
  proof (rule all_ctxt_closedD[OF all])
    fix j
    assume jts: "j < length ts"
    from i len have i: "i < length ss" by auto
    show "(ts ! j, ?mid ! j) ∈ R⇧*"
    proof (cases "j < i")
      case True
      with i have j: "j < length ss" by auto
      with True have id: "?mid ! j = ss ! j" by (simp add: nth_append)
      from steps len j have "(ts ! j, ss ! j) ∈ R⇧*" by auto
      then show ?thesis using id by simp
    next
      case False
      show ?thesis
      proof (cases "j = i")
        case True
        then have "?mid ! j = ts ! j" using i by (simp add: nth_append)
        then show ?thesis by simp
      next
        case False
        from i have min: "min (length ss) i = i" by simp
        from False ‹¬ j < i› have "j > i" by arith
        then obtain k where k: "j - i = Suc k" by (cases "j - i", auto)
        then have j: "j = Suc (i+k)" by auto
        with jts len have ss: "Suc i + k ≤ length ss" and jlen: "j < length ts" by auto
        then have "?mid ! j = ss ! j" using j i by (simp add: nth_append min ‹¬ j < i› nth_drop[OF ss])
        with steps jlen show ?thesis by auto
      qed
    qed
  qed (insert lents[symmetric] len, auto)
  with part1 show ?thesis by auto
qed

lemma SN_ctxt_apply_imp_SN_ctxt_to_term_list_gen:
  assumes ctxt: "ctxt.closed r"
  assumes SN: "SN_on r {C⟨t⟩}"
  shows "SN_on r (set (ctxt_to_term_list C))"
proof -
  {
    fix u
    assume "u ∈ set (ctxt_to_term_list C)"
    from ctxt_to_term_list_supt[OF this, of t] have "C⟨t⟩ ⊵ u"
      by (rule supt_imp_supteq)
    from ctxt_closed_SN_on_subt[OF ctxt, OF SN this]
    have "SN_on r {u}" by auto
  }
  then show ?thesis
    unfolding SN_on_def by auto
qed

lemma rstep_subset: "ctxt.closed R' ⟹ subst.closed R' ⟹ R ⊆ R' ⟹ rstep R ⊆ R'" by fast

lemma trancl_rstep_ctxt:
  "(s,t) ∈ (rstep R)⇧+ ⟹ (C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧+"
  by (rule ctxt.closedD, blast)

lemma args_steps_imp_steps_gen:
  assumes ctxt: "⋀ bef s t aft. (s, t) ∈ r (length bef) ⟹
    length ts = Suc (length bef + length aft) ⟹
    (Fun f (bef @ (s :: ('f, 'v) term) # aft), Fun f (bef @ t # aft)) ∈ R⇧*"
    and len: "length ss = length ts"
    and args: "⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ (r i)⇧*"
  shows "(Fun f ss, Fun f ts) ∈ R⇧*"
proof -
  let ?tss = "λi. take i ts @ drop i ss"
  {
    fix bef :: "('f,'v)term list" and s t and  aft :: "('f,'v)term list"
    assume "(s,t) ∈ (r (length bef))⇧*" and len: "length ts = Suc (length bef + length aft)"
    then have "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ R⇧*"
    proof (induct)
      case (step t u)
      from step(3)[OF len] ctxt[OF step(2) len] show ?case by auto
    qed simp
  }
  note one = this
  have a:"∀i ≤ length ts. (Fun f ss,Fun f (?tss i)) ∈ R⇧*"
  proof (intro allI impI)
    fix i assume "i ≤ length ts" then show "(Fun f ss,Fun f (?tss i)) ∈ R⇧*"
    proof (induct i)
      case 0
      then show ?case by simp
    next
      case (Suc i)
      then have IH: "(Fun f ss,Fun f (?tss i)) ∈ R⇧*"
        and i: "i < length ts" by auto
      have si: "?tss (Suc i) = take i ts @ ts ! i # drop (Suc i) ss"
        unfolding take_Suc_conv_app_nth[OF i] by simp
      have ii: "?tss i = take i ts @ ss ! i # drop (Suc i) ss"
        unfolding Cons_nth_drop_Suc[OF i[unfolded len[symmetric]]] ..
      from i have i': "length (take i ts) < length ts"  and len': "length (take i ts) = i" by auto
      from len i have len'': "length ts = Suc (length (take i ts) + length (drop (Suc i) ss))" by simp
      from one[OF args[OF i'] len''] IH
      show ?case unfolding si ii len' by auto
    qed
  qed
  from this[THEN spec, THEN mp[OF _ le_refl]]
  show ?thesis using len by auto
qed

lemma args_steps_imp_steps:
  assumes ctxt: "ctxt.closed R"
    and len: "length ss = length ts" and args: "∀i<length ss. (ss!i, ts!i) ∈ R⇧*"
  shows "(Fun f ss, Fun f ts) ∈ R⇧*"
proof (rule args_steps_imp_steps_gen[OF _ len])
  fix i
  assume "i < length ts" then show "(ss ! i, ts ! i) ∈ R⇧*" using args len by auto
qed (insert ctxt_closed_one[OF ctxt], auto)

lemmas args_rsteps_imp_rsteps = args_steps_imp_steps [OF ctxt_closed_rstep]

lemma replace_at_subst_steps:
  fixes σ τ :: "('f, 'v) subst"
  assumes acc: "all_ctxt_closed UNIV r"
    and refl: "refl r"
    and *: "⋀x. (σ x, τ x) ∈ r"
    and "p ∈ poss t"
    and "t |_ p = Var x"
  shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ r"
  using assms(4-)
proof (induction t arbitrary: p)
  case (Var x)
  then show ?case using refl by (simp add: refl_on_def)
next
  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) ∈ 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) ∈ 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) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
    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) ∈ r" by (auto simp: * all_ctxt_closed_subst_step [OF acc]) }
    ultimately show "(?ss ! j, ?ts ! j) ∈ r" by arith
  qed
  moreover have "i < length ts" by fact
  ultimately show ?case
    by (auto intro: all_ctxt_closedD [OF acc])
qed

lemma replace_at_subst_rsteps:
  fixes σ τ :: "('f, 'v) subst"
  assumes *: "⋀x. (σ x, τ x) ∈ (rstep R)⇧*"
    and "p ∈ poss t"
    and "t |_ p = Var x"
  shows "(replace_at (t ⋅ σ) p (τ x), t ⋅ τ) ∈ (rstep R)⇧*"
  by (intro replace_at_subst_steps[OF _ _ assms], auto simp: refl_on_def)

lemma substs_rsteps:
  assumes "⋀x. (σ x, τ x) ∈ (rstep R)⇧*"
  shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep 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) ∈ (rstep R)⇧*" by auto
  from args_rsteps_imp_rsteps [OF _ this] show ?case by simp
qed

lemma nrrstep_Fun_imp_arg_rstep:
  fixes ss :: "('f,'v)term list"
  assumes "(Fun f ss,Fun f ts) ∈ nrrstep R" (is "(?s,?t) ∈ nrrstep R")
  shows "∃C i. i < length ss ∧ (ss!i,ts!i) ∈ rstep R ∧ C⟨ss!i⟩ = Fun f ss ∧ C⟨ts!i⟩ = Fun f ts"
proof -
  from ‹(?s,?t) ∈ nrrstep R›
  obtain l r j ps σ where A: "let C = ctxt_of_pos_term (j#ps) ?s in (j#ps) ∈ poss ?s ∧ (l,r) ∈ R ∧ C⟨l⋅σ⟩ = ?s ∧ C⟨r⋅σ⟩ = ?t" unfolding nrrstep_def rstep_r_p_s_def by force
  let ?C = "ctxt_of_pos_term (j#ps) ?s"
  from A have "(j#ps) ∈ poss ?s" and "(l,r) ∈ R" and "?C⟨l⋅σ⟩ = ?s" and "?C⟨r⋅σ⟩ = ?t" using Let_def by auto
  have C: "?C = More f (take j ss) (ctxt_of_pos_term ps (ss!j)) (drop (Suc j) ss)" (is "?C = More f ?ss1 ?D ?ss2") by auto
  from ‹?C⟨l⋅σ⟩ = ?s› have "?D⟨l⋅σ⟩ = (ss!j)" by (auto simp: take_drop_imp_nth)
  from ‹(l,r) ∈ R› have "(l⋅σ,r⋅σ) ∈ (subst.closure R)" by auto
  then have "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ (ctxt.closure(subst.closure R))" by (auto simp only: ctxt.closure.intros)
  then have D_rstep: "(?D⟨l⋅σ⟩,?D⟨r⋅σ⟩) ∈ rstep R" and "(?C⟨l⋅σ⟩,?C⟨r⋅σ⟩) ∈ rstep R"
    by (auto simp: rstep_eq_closure)
  from ‹?C⟨r⋅σ⟩ = ?t› and C have "?t = Fun f (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
  then have ts: "ts = (take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss)" by auto
  from ‹j#ps ∈ poss ?s› have r0: "j < length ss" by simp
  then have "(take j ss @ ?D⟨r⋅σ⟩ # drop (Suc j) ss) ! j = ?D⟨r⋅σ⟩" by (auto simp: nth_append_take)
  with ts have "ts!j = ?D⟨r⋅σ⟩" by auto
  let ?C' = "More f (take j ss) □ (drop (Suc j) ss)"
  from D_rstep have r1: "(ss!j,ts!j) ∈ rstep R" unfolding ‹ts!j = ?D⟨r⋅σ⟩› ‹?D⟨l⋅σ⟩ = ss!j› by simp
  have "?s = ?C⟨l⋅σ⟩" unfolding ‹?C⟨l⋅σ⟩ = ?s› by simp
  also have "… = ?C'⟨?D⟨l⋅σ⟩⟩" unfolding C by simp
  finally have r2:"?C'⟨ss!j⟩ = ?s" unfolding ‹?D⟨l⋅σ⟩ = ss!j› by simp
  have "?t = ?C⟨r⋅σ⟩" unfolding ‹?C⟨r⋅σ⟩ = ?t› by simp
  also have "… = ?C'⟨?D⟨r⋅σ⟩⟩" unfolding C by simp
  finally have r3:"?C'⟨ts!j⟩ = ?t" unfolding ‹ts!j = ?D⟨r⋅σ⟩› by simp
  from r0 r1 r2 r3 show ?thesis by best
qed

lemma pair_fun_eq[simp]:
  fixes f :: "'a ⇒ 'b" and g :: "'b ⇒ 'a"
  shows "((λ(x,y). (x,f y)) ∘ (λ(x,y). (x,g y))) = (λ(x,y). (x,(f ∘ g) y))" (is "?f = ?g")
proof (rule ext)
  fix ab :: "'c * 'b"
  obtain a b where "ab = (a,b)" by force
  have "((λ(x,y). (x,f y))∘(λ(x,y). (x,g y))) (a,b) = (λ(x,y). (x,(f∘g) y)) (a,b)" by simp
  then show "?f ab = ?g ab" unfolding ‹ab = (a,b)› by simp
qed

lemma restrict_singleton:
  assumes "x ∈ subst_domain σ" shows "∃t. σ |s {x} = (λy. if y = x then t else Var y)"
proof -
  have "σ |s {x} = (λy. if y = x then σ y else Var y)" by (simp add: subst_restrict_def)
  then have "σ |s {x} = (λy. if y = x then σ x else Var y)" by (simp cong: if_cong)
  then show ?thesis by (rule exI[of _ "σ x"])
qed

definition rstep_r_c_s :: "('f,'v)rule ⇒ ('f,'v)ctxt ⇒ ('f,'v)subst ⇒ ('f,'v)term rel"
  where "rstep_r_c_s r C σ = {(s,t) | s t. s = C⟨fst r ⋅ σ⟩ ∧ t = C⟨snd r ⋅ σ⟩}"

lemma rstep_iff_rstep_r_c_s: "((s,t) ∈ rstep R) = (∃ l r C σ. (l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ)" (is "?left = ?right")
proof
  assume ?left
  then obtain l r p σ where step: "(s,t) ∈ rstep_r_p_s R (l,r) p σ"
    unfolding rstep_iff_rstep_r_p_s by blast
  obtain D where D: "D = ctxt_of_pos_term p s" by auto
  with step have Rrule: "(l,r) ∈ R" and s: "s = D⟨l ⋅ σ⟩" and t: "t = D⟨r ⋅ σ⟩"
    unfolding rstep_r_p_s_def by (force simp: Let_def)+
  then show ?right unfolding rstep_r_c_s_def by auto
next
  assume ?right
  from this obtain l r C σ where "(l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ" by auto
  then have rule: "(l,r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
    unfolding rstep_r_c_s_def by auto
  show ?left unfolding rstep_eq_closure by (auto simp: s t intro: rule)
qed

lemma rstep_subset_characterization:
  "(rstep R ⊆ rstep S) = (∀ l r. (l,r) ∈ R ⟶ (∃ l' r' C σ . (l',r') ∈ S ∧ l = C⟨l' ⋅ σ⟩ ∧ r = C⟨r' ⋅ σ⟩))" (is "?left = ?right")
proof
  assume ?right
  show ?left
  proof 
    fix s t
    assume "(s,t) ∈ rstep R"
    then obtain l r C σ where step: "(l,r) ∈ R ∧ (s,t) ∈ rstep_r_c_s (l,r) C σ"
      unfolding rstep_iff_rstep_r_c_s by best
    then have Rrule: "(l,r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
      unfolding rstep_r_c_s_def by (force)+
    from Rrule ‹?right› obtain l' r' C' σ' where Srule: "(l',r') ∈ S" and l: "l = C'⟨l' ⋅ σ'⟩" and r: "r = C'⟨r' ⋅ σ'⟩"
      by (force simp: Let_def)+
    let ?D = "C ∘⇩c (C' ⋅⇩c σ)"
    let ?sig = "σ' ∘⇩s σ"
    have s2: "s = ?D⟨l' ⋅ ?sig⟩" by (simp add: s l)
    have t2: "t = ?D⟨r' ⋅ ?sig⟩" by (simp add: t r)
    from s2 t2 have sStep: "(s,t) ∈ rstep_r_c_s (l',r') ?D ?sig" unfolding rstep_r_c_s_def by force
    with Srule show "(s,t) ∈ rstep S" by (simp only: rstep_iff_rstep_r_c_s, blast)
  qed
next
  assume ?left
  show ?right
  proof (rule ccontr)
    assume "¬ ?right"
    from this obtain l r where "(l,r) ∈ R" and cond: "∀ l' r' C σ. (l',r') ∈ S ⟶ (l ≠ C⟨l' ⋅ σ⟩ ∨ r ≠ C⟨r' ⋅ σ⟩)" by blast
    then have "(l,r) ∈ rstep R" by blast
    with ‹?left› have "(l,r) ∈ rstep S" by auto
    with cond show False by (simp only: rstep_iff_rstep_r_c_s, unfold rstep_r_c_s_def, force)
  qed
qed

lemma rstep_preserves_funas_terms_var_cond:
  assumes "funas_trs R ⊆ F" and "funas_term s ⊆ F" and "(s,t) ∈ rstep R"
    and wf: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
  shows "funas_term t ⊆ F"
proof -
  from ‹(s,t) ∈ rstep R› obtain l r C σ where R: "(l,r) ∈ R"
    and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
  from ‹funas_trs R ⊆ F› and R have "funas_term r ⊆ F"
    unfolding funas_defs [abs_def] by force
  with wf[OF R] ‹funas_term s ⊆ F› show ?thesis unfolding s t by (force simp: funas_term_subst)
qed

lemma rstep_preserves_funas_terms:
  assumes "funas_trs R ⊆ F" and "funas_term s ⊆ F" and "(s,t) ∈ rstep R"
    and wf: "wf_trs R"
  shows "funas_term t ⊆ F"
  by (rule rstep_preserves_funas_terms_var_cond[OF assms(1-3)], insert wf[unfolded wf_trs_def], auto)

lemma rsteps_preserve_funas_terms_var_cond:
  assumes F: "funas_trs R ⊆ F" and s: "funas_term s ⊆ F" and steps: "(s,t) ∈ (rstep R)⇧*"
    and wf: "⋀ l r. (l,r) ∈ R ⟹ vars_term r ⊆ vars_term l"
  shows "funas_term t ⊆ F"
  using steps
proof (induct)
  case base then show ?case by (rule s)
next
  case (step t u)
  show ?case by (rule rstep_preserves_funas_terms_var_cond[OF F step(3) step(2) wf])
qed

lemma rsteps_preserve_funas_terms:
  assumes F: "funas_trs R ⊆ F" and s: "funas_term s ⊆ F"
    and steps: "(s,t) ∈ (rstep R)⇧*" and wf: "wf_trs R"
  shows "funas_term t ⊆ F"
  by (rule rsteps_preserve_funas_terms_var_cond[OF assms(1-3)], insert wf[unfolded wf_trs_def], auto)

lemma no_Var_rstep [simp]:
  assumes "wf_trs R" and "(Var x, t) ∈ rstep R" shows "False"
  using rstep_imp_Fun[OF assms] by auto

lemma lhs_wf:
  assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
  shows "funas_term l ⊆  F"
  using assms by (force simp: funas_trs_def funas_rule_def)

lemma rhs_wf:
  assumes R: "(l, r) ∈ R" and "funas_trs R ⊆ F"
  shows "funas_term r ⊆ F"
  using assms by (force simp: funas_trs_def funas_rule_def)

lemma supt_map_funs_term [intro]:
  assumes "t ⊳ s"
  shows "map_funs_term fg t ⊳ map_funs_term fg s"
  using assms
proof (induct)
  case (arg s ss f)
  then have "map_funs_term fg s ∈ set(map (map_funs_term fg) ss)" by simp
  then show ?case unfolding term.map by (rule supt.arg)
next
  case (subt s ss u f)
  then have "map_funs_term fg s ∈ set(map (map_funs_term fg) ss)" by simp
  with ‹map_funs_term fg s ⊳ map_funs_term fg u› show ?case
    unfolding term.map by (metis supt.subt)
qed

lemma nondef_root_imp_arg_step:
  assumes "(Fun f ss, t) ∈ rstep R"
    and wf: "∀(l, r)∈R. is_Fun l"
    and ndef: "¬ defined R (f, length ss)"
  shows "∃i<length ss. (ss ! i, t |_ [i]) ∈ rstep R
    ∧ t = Fun f (take i ss @ (t |_ [i]) # drop (Suc i) ss)"
proof -
  from assms obtain l r p σ
    where rstep_r_p_s: "(Fun f ss, t) ∈ rstep_r_p_s R (l, r) p σ"
    unfolding rstep_iff_rstep_r_p_s by auto
  let ?C = "ctxt_of_pos_term p (Fun f ss)"
  from rstep_r_p_s have "p ∈ poss (Fun f ss)" and "(l, r) ∈ R"
    and "?C⟨l ⋅ σ⟩ = Fun f ss" and "?C⟨r ⋅ σ⟩ = t" unfolding rstep_r_p_s_def Let_def by auto
  have "∃i q. p = i#q"
  proof (cases p)
    case Cons then show ?thesis by auto
  next
    case Nil
    have "?C = □" unfolding Nil by simp
    with ‹?C⟨l⋅σ⟩ = Fun f ss› have "l⋅σ = Fun f ss" by simp
    have "∀(l,r)∈R. ∃f ss. l = Fun f ss"
    proof (intro ballI impI)
      fix lr assume "lr ∈ R"
      with wf have "∀x. fst lr ≠ Var x" by auto
      then have "∃f ss. (fst lr) = Fun f ss" by (cases "fst lr") auto
      then show "(λ(l,r). ∃f ss. l = Fun f ss) lr" by auto
    qed
    with ‹(l,r) ∈ R› obtain g ts where "l = Fun g ts" unfolding wf_trs_def by best
    with ‹l⋅σ = Fun f ss› ‹l = Fun g ts› and ‹(l, r) ∈ R› ndef
    show ?thesis unfolding defined_def by auto
  qed
  then obtain i q where "p = i#q" by auto
  from ‹p ∈ poss(Fun f ss)› have "i < length ss" and "q ∈ poss(ss!i)" unfolding ‹p = i#q› by auto
  let ?D = "ctxt_of_pos_term q (ss!i)"
  have C: "?C = More f (take i ss) ?D (drop (Suc i) ss)" unfolding ‹p = i#q› by auto
  from ‹?C⟨l⋅σ⟩ = Fun f ss› have "take i ss@?D⟨l⋅σ⟩#drop (Suc i) ss = ss" unfolding C by auto
  then have "(take i ss@?D⟨l⋅σ⟩#drop (Suc i) ss)!i = ss!i" by simp
  with ‹i < length ss› have "?D⟨l⋅σ⟩ = ss!i" using nth_append_take[where xs = ss and i = i] by auto
  have t: "t = Fun f (take i ss@?D⟨r⋅σ⟩#drop (Suc i) ss)" unfolding ‹?C⟨r⋅σ⟩ = t›[symmetric] C by simp
  from ‹i < length ss› have "t|_[i] = ?D⟨r⋅σ⟩" unfolding t unfolding subt_at.simps using nth_append_take[where xs = ss and i = i] by auto
  from ‹q ∈ poss(ss!i)› and ‹(l,r) ∈ R›
    and ‹?D⟨l⋅σ⟩ = ss!i› and ‹t|_[i] = ?D⟨r⋅σ⟩›[symmetric]
  have "(ss!i,t|_[i]) ∈ rstep_r_p_s R (l,r) q σ" unfolding rstep_r_p_s_def Let_def by auto
  then have "(ss!i,t|_[i]) ∈ rstep R" unfolding rstep_iff_rstep_r_p_s by auto
  from ‹i < length ss› and this and t show ?thesis unfolding ‹t|_[i] = ?D⟨r⋅σ⟩›[symmetric] by auto
qed

lemma nondef_root_imp_arg_steps:
  assumes "(Fun f ss,t) ∈ (rstep R)⇧*"
    and wf: "∀(l, r)∈R. is_Fun l"
    and "¬ defined R (f,length ss)"
  shows "∃ts. length ts = length ss ∧ t = Fun f ts ∧ (∀i<length ss. (ss!i,ts!i) ∈ (rstep R)⇧*)"
proof -
  from assms obtain n where "(Fun f ss,t) ∈ (rstep R)^^n"
    using rtrancl_imp_relpow by best
  then show ?thesis
  proof (induct n arbitrary: t)
    case 0 then show ?case by auto
  next
    case (Suc n)
    then obtain u where "(Fun f ss,u) ∈ (rstep R)^^n" and "(u,t) ∈ rstep R" by auto
    with Suc obtain ts where IH1: "length ts = length ss" and IH2: "u = Fun f ts" and IH3: "∀i<length ss. (ss!i,ts!i) ∈ (rstep R)⇧*" by auto
    from ‹(u,t) ∈ rstep R› have "(Fun f ts,t) ∈ rstep R" unfolding ‹u = Fun f ts› .
    from nondef_root_imp_arg_step[OF this wf ‹¬ defined R (f,length ss)›[simplified IH1[symmetric]]]
    obtain j where "j < length ts"
      and "(ts!j,t|_[j]) ∈ rstep R"
      and B: "t = Fun f (take j ts@(t|_[j])#drop (Suc j) ts)" (is "t = Fun f ?ts") by auto
    from ‹j < length ts› have "length ?ts = length ts" by auto
    then have A: "length ?ts = length ss" unfolding ‹length ts = length ss› .
    have C: "∀i<length ss. (ss!i,?ts!i) ∈ (rstep R)⇧*"
    proof (intro allI, intro impI)
      fix i assume "i < length ss"
      from ‹i < length ss› and IH3 have "(ss!i,ts!i) ∈ (rstep R)⇧*" by auto
      have "i = j ∨ i ≠ j" by auto
      then show "(ss!i,?ts!i) ∈ (rstep R)⇧*"
      proof
        assume "i = j"
        from ‹j < length ts› have "j ≤ length ts" by simp
        from nth_append_take[OF this] have "?ts!j = t|_[j]" by simp
        from ‹(ts!j,t|_[j]) ∈ rstep R› have "(ts!i,t|_[i]) ∈ rstep R" unfolding ‹i = j› .
        with ‹(ss!i,ts!i) ∈ (rstep R)⇧*› show ?thesis unfolding ‹i = j› unfolding ‹?ts!j = t|_[j]› by auto
      next
        assume "i ≠ j"
        from ‹i < length ss› have "i ≤ length ts" unfolding ‹length ts = length ss› by simp
        from ‹j < length ts› have "j ≤ length ts" by simp
        from nth_append_take_drop_is_nth_conv[OF ‹i ≤ length ts› ‹j ≤ length ts› ‹i ≠ j›]
        have "?ts!i = ts!i" by simp
        with ‹(ss!i,ts!i) ∈ (rstep R)⇧*› show ?thesis by auto
      qed
    qed
    from A and B and C show ?case by blast
  qed
qed

lemma rstep_imp_nrrstep:
  assumes "is_Fun s" and "¬ defined R (the (root s))" and "∀(l,r)∈R. is_Fun l"
    and "(s, t) ∈ rstep R"
  shows "(s, t) ∈ nrrstep R"
proof -
  from ‹is_Fun s› obtain f ss where s: "s = Fun f ss" by (cases s) auto
  with assms have undef: "¬ defined R (f, length ss)" by simp
  from assms have non_var: "∀(l, r)∈R. is_Fun l" by auto
  from nondef_root_imp_arg_step[OF ‹(s, t) ∈ rstep R›[unfolded s] non_var undef]
  obtain i where "i < length ss" and step: "(ss ! i, t |_ [i]) ∈ rstep R"
    and t: "t = Fun f (take i ss @ (t |_ [i]) # drop (Suc i) ss)" by auto
  from step obtain C l r σ where "(l, r) ∈ R" and lhs: "ss ! i = C⟨l ⋅ σ⟩"
    and rhs: "t |_ [i] = C⟨r ⋅ σ⟩" by auto
  let ?C = "More f (take i ss) C (drop (Suc i) ss)"
  have "(l, r) ∈ R" by fact
  moreover have "?C ≠ □" by simp
  moreover have "s = ?C⟨l ⋅ σ⟩"
  proof -
    have "s = Fun f (take i ss @ ss!i # drop (Suc i) ss)"
      using id_take_nth_drop[OF ‹i < length ss›] unfolding s by simp
    also have "… = ?C⟨l ⋅ σ⟩" by (simp add: lhs)
    finally show ?thesis .
  qed
  moreover have "t = ?C⟨r ⋅ σ⟩"
  proof -
    have "t = Fun f (take i ss @ t |_ [i] # drop (Suc i) ss)" by fact
    also have "… = Fun f (take i ss @ C⟨r ⋅ σ⟩ # drop (Suc i) ss)" by (simp add: rhs)
    finally show ?thesis by simp
  qed
  ultimately show "(s, t) ∈ nrrstep R" unfolding nrrstep_def' by blast
qed

lemma rsteps_imp_nrrsteps:
  assumes "is_Fun s" and "¬ defined R (the (root s))"
    and no_vars: "∀(l, r)∈R. is_Fun l"
    and "(s, t) ∈ (rstep R)⇧*"
  shows "(s, t) ∈ (nrrstep R)⇧*"
  using ‹(s, t) ∈ (rstep R)⇧*›
proof (induct)
  case base show ?case by simp
next
  case (step u v)
  from assms obtain f ss where s: "s = Fun f ss" by (induct s) auto
  from nrrsteps_preserve_root[OF ‹(s, u) ∈ (nrrstep R)⇧*›[unfolded s]]
  obtain ts where u: "u = Fun f ts" by auto
  from nrrsteps_equiv_num_args[OF ‹(s, u) ∈ (nrrstep R)⇧*›[unfolded s]]
  have len: "length ss = length ts" unfolding u by simp
  have "is_Fun u" by (simp add: u)
  have undef: "¬ defined R (the (root u))"
    using ‹¬ defined R (the (root s))›
    unfolding s u by (simp add: len)
  have "(u, v) ∈ nrrstep R"
    using rstep_imp_nrrstep[OF ‹is_Fun u› undef no_vars] step
    by simp
  with step show ?case by auto
qed

lemma left_var_imp_not_SN:
  fixes R :: "('f,'v)trs" and t :: "('f, 'v) term"
  assumes "(Var y, r) ∈ R" (is "(?y, _) ∈ _")
  shows "¬ (SN_on (rstep R) {t})"
proof (rule steps_imp_not_SN_on)
  fix t :: "('f,'v)term"
  let ?yt = "subst y t"
  show "(t, r ⋅ ?yt) ∈ rstep R"
    by (rule rstepI[OF assms, where C = □ and σ = ?yt], auto simp: subst_def)
qed

lemma not_SN_subt_imp_not_SN:
  assumes ctxt: "ctxt.closed R" and SN: "¬ SN_on R {t}" and sub: "s ⊵ t"
  shows "¬ SN_on R {s}"
  using ctxt_closed_SN_on_subt[OF ctxt _ sub] SN
  by auto

lemma root_Some:
  assumes "root t = Some fn"
  obtains ss where "length ss = snd fn" and "t = Fun (fst fn) ss"
  using assms by (induct t) auto

lemma map_funs_rule_power:
  fixes f :: "'f ⇒ 'f"
  shows "((map_funs_rule f) ^^ n) = map_funs_rule (f ^^ n)"
proof (rule sym, intro ext, clarify)
  fix  l r :: "('f,'v)term"
  show "map_funs_rule (f ^^ n) (l,r) = (map_funs_rule f ^^ n) (l,r)"
  proof (induct n)
    case 0
    show ?case by (simp add: term.map_ident)
  next
    case (Suc n)
    have "map_funs_rule (f ^^ Suc n) (l,r) = map_funs_rule f (map_funs_rule (f ^^ n) (l,r))"
      by (simp add: map_funs_term_comp)
    also have "… = map_funs_rule f ((map_funs_rule f ^^ n) (l,r))" unfolding Suc ..
    also have "… = (map_funs_rule f ^^ (Suc n)) (l,r)" by simp
    finally show ?case .
  qed
qed

lemma map_funs_trs_power:
  fixes f :: "'f ⇒ 'f"
  shows "map_funs_trs f ^^ n = map_funs_trs (f ^^ n)"
proof
  fix R :: "('f, 'v) trs"
  have "map_funs_rule (f ^^ n) ` R = (map_funs_rule f ^^ n) ` R" unfolding map_funs_rule_power ..
  also have "… = ((λ R. map_funs_trs f R) ^^ n) R" unfolding map_funs_trs.simps
    apply (induct n)
     apply simp
    by (metis comp_apply funpow.simps(2) image_comp)
  finally have "map_funs_rule (f ^^ n) ` R = (map_funs_trs f ^^ n) R" .
  then show "(map_funs_trs f ^^ n) R = map_funs_trs (f ^^ n) R"
    by (simp add: map_funs_trs.simps)
qed

text ‹The set of minimally nonterminating terms with respect to a relation @{term "R"}.›
definition Tinf :: "('f, 'v) trs ⇒ ('f, 'v) terms"
  where
    "Tinf R = {t. ¬ SN_on R {t} ∧ (∀s ⊲ t. SN_on R {s})}"

lemma not_SN_imp_subt_Tinf:
  assumes "¬ SN_on R {s}" shows "∃t⊴s. t ∈ Tinf R"
proof -
  let ?S = "{t | t. s ⊵ t ∧ ¬ SN_on R {t}}"
  from assms have s: "s ∈ ?S" by auto
  from mp[OF spec[OF spec[OF SN_imp_minimal[OF SN_supt]]] s]
  obtain t where st: "s ⊵ t" and nSN: "¬ SN_on R {t}"
    and min: "∀ u. (t,u) ∈ supt ⟶ u ∉ ?S" by auto
  have "t ∈ Tinf R" unfolding Tinf_def
  proof (intro CollectI allI impI conjI nSN)
    fix u
    assume u: "t ⊳ u"
    from u st have "s ⊳ u" using supteq_supt_trans by auto
    with min u show "SN_on R {u}" by auto
  qed
  with st show ?thesis by auto
qed

lemma not_SN_imp_Tinf:
  assumes "¬ SN R" shows "∃t. t ∈ Tinf R"
  using assms not_SN_imp_subt_Tinf unfolding SN_on_def by blast

lemma ctxt_of_pos_term_map_funs_term_conv [iff]:
  assumes "p ∈ poss s"
  shows "map_funs_ctxt fg (ctxt_of_pos_term p s) = (ctxt_of_pos_term p (map_funs_term fg s))"
  using assms
proof (induct s arbitrary: p)
  case (Var x) then show ?case by simp
next
  case (Fun f ss) then show ?case
  proof (cases p)
    case Nil then show ?thesis by simp
  next
    case (Cons i q)
    with ‹p ∈ poss(Fun f ss)› have "i < length ss" and "q ∈ poss(ss!i)" unfolding Cons poss.simps by auto
    then have "ss!i ∈ set ss" by simp
    with Fun and ‹q ∈ poss(ss!i)›
    have IH: "map_funs_ctxt fg(ctxt_of_pos_term q (ss!i)) = ctxt_of_pos_term q (map_funs_term fg (ss!i))" by simp
    have "map_funs_ctxt fg(ctxt_of_pos_term p (Fun f ss)) = map_funs_ctxt fg(ctxt_of_pos_term (i#q) (Fun f ss))" unfolding Cons by simp
    also have "… = map_funs_ctxt fg(More f (take i ss) (ctxt_of_pos_term q (ss!i)) (drop (Suc i) ss))" by simp
    also have "… = More (fg f) (map (map_funs_term fg) (take i ss)) (map_funs_ctxt fg(ctxt_of_pos_term q (ss!i))) (map (map_funs_term fg) (drop (Suc i) ss))" by simp
    also have "… = More (fg f) (map (map_funs_term fg) (take i ss)) (ctxt_of_pos_term q (map_funs_term fg (ss!i))) (map (map_funs_term fg) (drop (Suc i) ss))" unfolding IH by simp
    also have "… = More (fg f) (take i (map (map_funs_term fg) ss)) (ctxt_of_pos_term q (map (map_funs_term fg) ss!i)) (drop (Suc i) (map (map_funs_term fg) ss))" unfolding nth_map[OF ‹i < length ss›,symmetric] take_map drop_map nth_map by simp
    finally show ?thesis unfolding Cons by simp
  qed
qed

lemma var_rewrite_imp_not_SN:
  assumes sn: "SN_on (rstep R) {u}" and step: "(t, s) ∈ rstep R"
  shows "is_Fun t"
  using assms
proof (cases t)
  case (Fun f ts) then show ?thesis by simp
next
  case (Var x)
  from step obtain l r p σ where "(Var x, s) ∈ rstep_r_p_s R (l,r) p σ" unfolding Var rstep_iff_rstep_r_p_s by best
  then have "l ⋅ σ = Var x" and rule: "(l,r) ∈ R" unfolding rstep_r_p_s_def by (auto simp: Let_def)
  from this obtain y where "l = Var y" (is "_ = ?y") by (cases l, auto)
  with rule have "(?y, r) ∈ R" by auto
  then have "¬ (SN_on (rstep R) {u})" by (rule left_var_imp_not_SN)
  with sn show ?thesis by blast
qed

lemma rstep_id: "rstep Id = Id" by auto

lemma map_funs_rule_id [simp]: "map_funs_rule id = id"
  by (intro ext, auto)

lemma map_funs_trs_id [simp]: "map_funs_trs id = id"
  by (intro ext, auto simp: map_funs_trs.simps)

definition sig_step :: "'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs" where
  "sig_step F R = {(a, b). (a, b) ∈ R ∧ funas_term a ⊆ F ∧ funas_term b ⊆ F}"

lemma sig_step_union: "sig_step F (R ∪ S) = sig_step F R ∪ sig_step F S"
  unfolding sig_step_def by auto

lemma sig_step_UNIV: "sig_step UNIV R = R" unfolding sig_step_def by simp

lemma sig_stepI[intro]: "(a,b) ∈ R ⟹ funas_term a ⊆ F ⟹ funas_term b ⊆ F ⟹ (a,b) ∈ sig_step F R" unfolding sig_step_def by auto

lemma sig_stepE[elim,consumes 1]: "(a,b) ∈ sig_step F R ⟹ ⟦(a,b) ∈ R ⟹ funas_term a ⊆ F ⟹ funas_term b ⊆ F ⟹ P⟧ ⟹ P" unfolding sig_step_def by auto

lemma all_ctxt_closed_sig_rsteps [intro]:
  fixes R :: "('f, 'v) trs"
  shows "all_ctxt_closed F ((sig_step F (rstep R))⇧*)" (is "all_ctxt_closed _ (?R⇧*)")
proof (rule trans_ctxt_sig_imp_all_ctxt_closed)
  fix C :: "('f,'v)ctxt" and s t :: "('f,'v)term"
  assume C: "funas_ctxt C ⊆ F"
    and s: "funas_term s ⊆ F"
    and t: "funas_term t ⊆ F"
    and steps: "(s,t) ∈ ?R⇧*"
  from steps
  show "(C ⟨ s ⟩, C ⟨ t ⟩) ∈ ?R⇧*"
  proof (induct)
    case (step t u)
    from step(2) have tu: "(t,u) ∈ rstep R" and t: "funas_term t ⊆ F" and u: "funas_term u ⊆ F" by auto
    have "(C ⟨ t ⟩, C ⟨ u ⟩) ∈ ?R" by (rule sig_stepI[OF rstep_ctxt[OF tu]], insert C t u, auto)
    with step(3) show ?case by auto
  qed auto
qed (auto intro: trans_rtrancl)

lemma wf_loop_imp_sig_ctxt_rel_not_SN:
  assumes R: "(l,C⟨l⟩) ∈ R" and wf_l: "funas_term l ⊆ F"
    and wf_C: "funas_ctxt C ⊆ F"
    and ctxt: "ctxt.closed R"
  shows "¬ SN_on (sig_step F R) {l}"
proof -
  let ?t = "λ i. (C^i)⟨l⟩"
  have "∀i. funas_term (?t i) ⊆ F"
  proof
    fix i show "funas_term (?t i) ⊆ F" unfolding funas_term_ctxt_apply
      by (rule Un_least[OF _ wf_l], induct i, insert wf_C, auto)
  qed
  moreover have "∀i. (?t i,?t(Suc i)) ∈ R"
  proof
    fix i
    show "(?t i, ?t (Suc i)) ∈ R"
    proof (induct i)
      case 0 with R show ?case by auto
    next
      case (Suc i)
      from ctxt.closedD[OF ctxt Suc, of C]
      show ?case by simp
    qed
  qed
  ultimately have steps: "∀i. (?t i,?t(Suc i)) ∈ sig_step F R" unfolding sig_step_def by blast
  show ?thesis unfolding SN_defs
    by (simp, intro exI[of _ ?t], simp only: steps, simp)
qed

lemma lhs_var_imp_sig_step_not_SN_on:
  assumes x: "(Var x, r) ∈ R" and F: "funas_trs R ⊆ F"
  shows "¬ SN_on (sig_step F (rstep R)) {Var x}"
proof -
  let ?σ = "(λx. r)"
  let ?t = "λi. (?σ ^^ i) x"
  obtain t where t: "t = ?t" by auto
  from rhs_wf[OF x F] have wf_r: "funas_term r ⊆ F" .
  {
    fix i
    have "funas_term (?t i) ⊆ F"
    proof (induct i)
      case 0 show ?case using wf_r by auto
    next
      case (Suc i)
      have "?t (Suc i) = ?t i ⋅ ?σ" unfolding subst_power_Suc subst_compose_def by simp
      also have "funas_term ... ⊆ F" unfolding funas_term_subst[of "?t i"]
        using Suc wf_r by auto
      finally show ?case .
    qed
  } note wf_t = this
  {
    fix i
    have "(t i, t (Suc i)) ∈ (sig_step F (rstep R))" unfolding t
      by (rule sig_stepI[OF rstepI[OF x, of _ □ "?σ ^^ i"] wf_t wf_t], auto simp: subst_compose_def)
  } note steps = this
  have x: "t 0 = Var x" unfolding t by simp
  with steps show ?thesis unfolding SN_defs not_not
    by (intro exI[of _ t], auto)
qed

lemma rhs_free_vars_imp_sig_step_not_SN:
  assumes R: "(l,r) ∈ R" and free: "¬ vars_term r ⊆ vars_term l"
    and F: "funas_trs R ⊆ F"
  shows "¬ SN_on (sig_step F (rstep R)) {l}"
proof -
  from free obtain x where x: "x ∈ vars_term r - vars_term l" by auto
  then have "x ∈ vars_term r" by simp
  from supteq_Var[OF this] have "r ⊵ Var x" .
  then obtain C where r: "C⟨Var x⟩ = r" by auto
  let ?σ = "λy. if y = x then l else Var y"
  let ?t = "λi. ((C ⋅⇩c ?σ)^i)⟨l⟩"
  from rhs_wf[OF R] F have wf_r: "funas_term r ⊆ F" by fast
  from lhs_wf[OF R] F have wf_l: "funas_term l ⊆ F" by fast
  from wf_r[unfolded r[symmetric]]
  have wf_C: "funas_ctxt C ⊆ F" by simp
  from x have neq: "∀y∈vars_term l. y ≠ x" by auto
  have "l⋅?σ = l ⋅ Var"
    by (rule term_subst_eq, insert neq, auto)
  then have l: "l ⋅ ?σ = l" by simp
  have wf_C: "funas_ctxt (C ⋅⇩c ?σ) ⊆ F" using wf_C wf_l
    by simp
  have rsigma: "r⋅?σ = (C ⋅⇩c ?σ)⟨l⟩" unfolding r[symmetric] by simp
  from R have lr: "(l ⋅ ?σ, r ⋅ ?σ) ∈ rstep R" by auto
  then have lr: "(l,(C ⋅⇩c ?σ)⟨l⟩) ∈ rstep R" unfolding l unfolding rsigma .
  show ?thesis
    by (rule wf_loop_imp_sig_ctxt_rel_not_SN[OF lr wf_l wf_C ctxt_closed_rstep])
qed

lemma lhs_var_imp_rstep_not_SN: assumes "(Var x,r) ∈ R" shows "¬ SN(rstep R)"
  using lhs_var_imp_sig_step_not_SN_on[OF assms subset_refl] unfolding sig_step_def SN_defs by blast

lemma rhs_free_vars_imp_rstep_not_SN:
  assumes "(l,r) ∈ R" and "¬ vars_term r ⊆ vars_term l"
  shows "¬ SN_on (rstep R) {l}"
  using rhs_free_vars_imp_sig_step_not_SN[OF assms subset_refl] unfolding sig_step_def SN_defs by blast

lemma free_right_rewrite_imp_not_SN:
  assumes step: "(t,s) ∈ rstep_r_p_s R (l,r) p σ"
    and vars: "¬ vars_term l ⊇ vars_term r"
  shows "¬ SN_on (rstep R) {t}"
proof
  assume SN: "SN_on (rstep R) {t}"
  let ?C = "ctxt_of_pos_term p t"
  from step have left: "?C⟨l ⋅ σ⟩ = t" (is "?t = t") and right: "?C⟨r ⋅ σ⟩ = s" and pos: "p ∈ poss t"
    and rule: "(l,r) ∈ R"
    unfolding rstep_r_p_s_def by (auto simp: Let_def)
  from rhs_free_vars_imp_rstep_not_SN[OF rule vars] have nSN:"¬ SN_on (rstep R) {l}" by simp
  from SN_imp_SN_subt[OF SN ctxt_imp_supteq[of ?C "l ⋅ σ", simplified left]]
  have SN: "SN_on (rstep R) {l ⋅ σ}" .
  from SNinstance_imp_SN[OF SN] nSN show False by simp
qed

lemma not_SN_on_rstep_subst_apply_term[intro]:
  assumes "¬ SN_on (rstep R) {t}" shows "¬ SN_on (rstep R) {t ⋅ σ}"
  using assms unfolding SN_on_def by best

lemma SN_rstep_imp_wf_trs: assumes "SN (rstep R)" shows "wf_trs R"
proof (rule ccontr)
  assume "¬ wf_trs R"
  then obtain l r where R: "(l,r) ∈ R"
    and not_wf: "(∀f ts. l ≠ Fun f ts) ∨ ¬(vars_term r ⊆ vars_term l)" unfolding wf_trs_def
    by auto
  from not_wf have "¬ SN (rstep R)"
  proof
    assume free: "¬ vars_term r ⊆ vars_term l"
    from rhs_free_vars_imp_rstep_not_SN[OF R free] show ?thesis unfolding SN_defs by auto
  next
    assume "∀f ts. l ≠ Fun f ts"
    then obtain x where l:"l = Var x" by (cases l) auto
    with R have "(Var x,r) ∈ R" unfolding l by simp
    from lhs_var_imp_rstep_not_SN[OF this] show ?thesis by simp
  qed
  with assms show False by blast
qed

lemma SN_sig_step_imp_wf_trs: assumes SN: "SN (sig_step F (rstep R))" and F: "funas_trs R ⊆ F" shows "wf_trs R"
proof (rule ccontr)
  assume "¬ wf_trs R"
  then obtain l r where R: "(l,r) ∈ R"
    and not_wf: "(∀f ts. l ≠ Fun f ts) ∨ ¬(vars_term r ⊆ vars_term l)" unfolding wf_trs_def
    by auto
  from not_wf have "¬ SN (sig_step F (rstep R))"
  proof
    assume free: "¬ vars_term r ⊆ vars_term l"
    from rhs_free_vars_imp_sig_step_not_SN[OF R free F] show ?thesis unfolding SN_on_def by auto
  next
    assume "∀f ts. l ≠ Fun f ts"
    then obtain x where l:"l = Var x" by (cases l) auto
    with R have "(Var x,r) ∈ R" unfolding l by simp
    from lhs_var_imp_sig_step_not_SN_on[OF this F] show ?thesis
      unfolding SN_on_def by auto
  qed
  with assms show False by blast
qed

lemma rhs_free_vars_imp_rstep_not_SN':
  assumes "(l, r) ∈ R" and "¬ vars_term r ⊆ vars_term l"
  shows "¬ SN (rstep R)"
  using rhs_free_vars_imp_rstep_not_SN [OF assms] by (auto simp: SN_defs)

lemma SN_imp_variable_condition:
  assumes "SN (rstep R)"
  shows "∀(l, r) ∈ R. vars_term r ⊆ vars_term l"
  using assms and rhs_free_vars_imp_rstep_not_SN' [of _ _ R] by blast

lemma rstep_cases'[consumes 1, case_names root nonroot]:
  assumes rstep: "(s, t) ∈ rstep R"
    and root: "⋀l r σ. (l, r) ∈ R ⟹ l ⋅ σ = s ⟹ r ⋅ σ = t ⟹ P"
    and nonroot: "⋀f ss1 u ss2 v. s = Fun f (ss1 @ u # ss2) ⟹ t = Fun f (ss1 @ v # ss2) ⟹ (u, v) ∈ rstep R ⟹ P"
  shows "P"
proof -
  from rstep_imp_C_s_r[OF rstep] obtain C σ l r
    where R: "(l,r) ∈ R" and s: "C⟨l⋅σ⟩ = s" and t: "C⟨r⋅σ⟩ = t" by fast
  show ?thesis proof (cases C)
    case Hole
    from s t have "l⋅σ = s" and "r⋅σ = t" by (auto simp: Hole)
    with R show ?thesis by (rule root)
  next
    case (More f ss1 D ss2)
    let ?u = "D⟨l⋅σ⟩"
    let ?v  = "D⟨r⋅σ⟩"
    have "s = Fun f (ss1 @ ?u # ss2)" by (simp add: More s[symmetric])
    moreover have "t = Fun f (ss1 @ ?v # ss2)" by (simp add: More t[symmetric])
    moreover have "(?u,?v) ∈ rstep R" using R by auto
    ultimately show ?thesis by (rule nonroot)
  qed
qed

lemma NF_Var: assumes wf: "wf_trs R" shows "(Var x, t) ∉ rstep R"
proof
  assume "(Var x, t) ∈ rstep R"
  from rstep_imp_C_s_r[OF this] obtain C l r σ
    where R: "(l,r) ∈ R" and lhs: "Var x = C⟨l⋅σ⟩" by fast
  from lhs have "Var x = l⋅σ" by (induct C) auto
  then obtain y where l: "l = Var y" by (induct l) auto
  from wf R obtain f ss where "l = Fun f ss" unfolding wf_trs_def by best
  with l show False by simp
qed

lemma rstep_cases_Fun'[consumes 2, case_names root nonroot]:
  assumes wf: "wf_trs R"
    and rstep: "(Fun f ss,t) ∈ rstep R"
    and root': "⋀ls r σ. (Fun f ls,r) ∈ R ⟹ map (λt. t⋅σ) ls = ss ⟹ r⋅σ = t ⟹ P"
    and nonroot': "⋀i u. i < length ss ⟹ t = Fun f (take i ss@u#drop (Suc i) ss) ⟹ (ss!i,u) ∈ rstep R ⟹ P"
  shows "P"
  using rstep proof (cases rule: rstep_cases')
  case (root l r σ)
  with wf obtain g ls where l: "l = Fun g ls" unfolding wf_trs_def by best
  from root have [simp]: "g = f" unfolding l by simp
  from root have "(Fun f ls,r) ∈ R" and "map (λt. t⋅σ) ls = ss" and "r⋅σ = t" unfolding l by auto
  then show ?thesis by (rule root')
next
  case (nonroot g ss1 u ss2 v)
  then have [simp]: "g = f" and args: "ss = ss1 @ u # ss2" by auto
  let ?i = "length ss1"
  from args have ss1: "take ?i ss = ss1" by simp
  from args have "drop ?i ss = u # ss2" by simp
  then have "drop (Suc 0) (drop ?i ss) = ss2" by simp
  then have ss2: "drop (Suc ?i) ss = ss2" by simp
  from args have len: "?i < length ss" by simp
  from id_take_nth_drop[OF len] have "ss = take ?i ss @ ss!?i # drop (Suc ?i) ss" by simp
  then have u: "ss!?i = u" unfolding args unfolding ss1[unfolded args] ss2[unfolded args] by simp
  from nonroot have "t = Fun f (take ?i ss@v#drop (Suc ?i) ss)" unfolding ss1 ss2 by simp
  moreover from nonroot have "(ss!?i,v) ∈ rstep R" unfolding u by simp
  ultimately show ?thesis by (rule nonroot'[OF len])
qed

lemma rstep_preserves_undefined_root:
  assumes "wf_trs R" and "¬ defined R (f, length ss)" and "(Fun f ss, t) ∈ rstep R"
  shows "∃ts. length ts = length ss ∧ t = Fun f ts"
proof -
  from ‹wf_trs R› and ‹(Fun f ss, t) ∈ rstep R› show ?thesis
  proof (cases rule: rstep_cases_Fun')
    case (root ls r σ)
    then have "defined R (f, length ss)" by (auto simp: defined_def)
    with ‹¬ defined R (f, length ss)› show ?thesis by simp
  next
    case (nonroot i u) then show ?thesis by simp
  qed
qed

lemma rstep_ctxt_imp_nrrstep: assumes step: "(s,t) ∈ rstep R" and C: "C ≠ □" shows "(C⟨s⟩,C⟨t⟩) ∈ nrrstep R"
proof -
  from step obtain l r D σ where "(l,r) ∈ R" "s = D⟨l ⋅ σ⟩" "t = D⟨r ⋅ σ⟩" by auto
  thus ?thesis unfolding nrrstep_def' using C
    by (intro CollectI, unfold split, intro exI[of _ "C ∘⇩c D"] exI conjI, auto) (cases C, auto)
qed

lemma rsteps_ctxt_imp_nrrsteps: assumes steps: "(s,t) ∈ (rstep R)⇧*" and C: "C ≠ □" shows "(C⟨s⟩,C⟨t⟩) ∈ (nrrstep R)⇧*"
  using steps 
proof (induct)
  case (step t u)
  from rstep_ctxt_imp_nrrstep[OF step(2) C] step(3) show ?case by simp
qed simp

lemma nrrstep_mono:
  assumes "R ⊆ R'"
  shows "nrrstep R ⊆ nrrstep R'"
  using assms by (force simp: nrrstep_def rstep_r_p_s_def Let_def)

lemma rrstepE:
  assumes "(s, t) ∈ rrstep R"
  obtains l and r and σ where "(l, r) ∈ R" and "s = l ⋅ σ" and "t = r ⋅ σ"
  using assms by (auto simp: rrstep_def rstep_r_p_s_def)

lemma nrrstepE:
  assumes "(s, t) ∈ nrrstep R"
  obtains C and l and r and σ where "C ≠ □" and "(l, r) ∈ R"
    and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩"
  using assms by (auto simp: nrrstep_def rstep_r_p_s_def Let_def)
    (metis ctxt.cop_nil list.discI poss_Cons_poss replace_at_subt_at subt_at_id_imp_eps)


lemma singleton_subst_restrict [simp]:
  "subst x s |s {x} = subst x s"
  unfolding subst_def subst_restrict_def by (rule ext) simp

lemma singleton_subst_map [simp]:
  "f ∘ subst x s = (f ∘ Var)(x := f s)" by (intro ext, auto simp: subst_def)

lemma subst_restrict_vars [simp]:
  "(λz. if z ∈ V then f z else g z) |s V = f |s V"
  unfolding subst_restrict_def
proof (intro ext)
  fix x
  show "(if x ∈ V then if x ∈ V then f x else g x else Var x)
    = (if x ∈ V then f x else Var x)" by simp
qed

lemma subst_restrict_restrict [simp]:
  assumes "V ∩ W = {}"
  shows "((λz. if z ∈ V then f z else g z) |s W) = g |s W"
  unfolding subst_restrict_def
proof (intro ext)
  fix x
  show "(if x ∈ W then if x ∈ V then f x else g x else Var x)
    = (if x ∈ W then g x else Var x)" using assms by auto
qed

lemma rstep_rstep: "rstep (rstep R) = rstep R"
proof -
  have "ctxt.closure (subst.closure (rstep R)) = rstep R" by (simp only: subst_closure_rstep_eq ctxt_closure_rstep_eq)
  then show ?thesis unfolding rstep_eq_closure .
qed

lemma rstep_trancl_distrib: "rstep (R⇧+) ⊆ (rstep R)⇧+"
proof
  fix s t
  assume "(s,t) ∈ rstep (R⇧+)"
  then show "(s,t) ∈ (rstep R)⇧+"
  proof
    fix l r C σ
    presume lr: "(l,r) ∈ R⇧+" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
    from lr have "(C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∈ (rstep R)⇧+"
    proof(induct)
      case (base r)
      then show ?case by auto
    next
      case (step r rr)
      from step(2) have "(C⟨r ⋅ σ⟩, C⟨rr ⋅ σ⟩) ∈ (rstep R)" by auto
      with step(3) show ?case by auto
    qed
    then show "(s,t) ∈ (rstep R)⇧+" unfolding s t .
  qed auto
qed

lemma rsteps_closed_subst:
  assumes "(s, t) ∈ (rstep R)⇧*"
  shows "(s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧*"
  using assms and subst.closed_rtrancl [OF subst_closed_rstep] by (auto simp: subst.closed_def)

lemma join_subst:
  "subst.closed r ⟹ (s, t) ∈ r⇧↓ ⟹ (s ⋅ σ, t ⋅ σ) ∈ r⇧↓"
  by (simp add: join_def subst.closedD subst.closed_comp subst.closed_converse subst.closed_rtrancl)


lemma join_subst_rstep [intro]:
  "(s, t) ∈ (rstep R)⇧↓ ⟹ (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧↓"
  by (intro join_subst, auto)

lemma join_ctxt [intro]:
  assumes "(s, t) ∈ (rstep R)⇧↓"
  shows "(C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧↓"
proof -
  from assms obtain u where "(s, u) ∈ (rstep R)⇧*" and "(t, u) ∈ (rstep R)⇧*" by auto
  then have "(C⟨s⟩, C⟨u⟩) ∈ (rstep R)⇧*" and "(C⟨t⟩, C⟨u⟩) ∈ (rstep R)⇧*" by (auto intro: rsteps_closed_ctxt)
  then show ?thesis by blast
qed

lemma rstep_simps:
  "rstep (R⇧=) = (rstep R)⇧="
  "rstep (rstep R) = rstep R"
  "rstep (R ∪ S) = rstep R ∪ rstep S"
  "rstep Id = Id"
  "rstep (R⇧↔) = (rstep R)⇧↔"
  by auto

lemma rstep_rtrancl_idemp [simp]:
  "rstep ((rstep R)⇧*) = (rstep R)⇧*"
proof -
  { fix s t
    assume "(s, t) ∈ rstep ((rstep R)⇧*)"
    then have "(s, t) ∈ (rstep R)⇧*"
      by (induct) (metis rsteps_closed_ctxt rsteps_closed_subst) }
  then show ?thesis by auto
qed

lemma all_ctxt_closed_rstep_conversion: 
  "all_ctxt_closed UNIV ((rstep R)⇧↔⇧*)" 
  unfolding conversion_def rstep_simps(5)[symmetric] by blast


definition instance_rule :: "('f, 'v) rule ⇒ ('f, 'w) rule ⇒ bool" where
  [code del]: "instance_rule lr st ⟷ (∃ σ. fst lr = fst st ⋅ σ ∧ snd lr = snd st ⋅ σ)"
  (* instance rule has implementation in Substitution.thy *)

definition eq_rule_mod_vars :: "('f, 'v) rule ⇒ ('f, 'v) rule ⇒ bool" where
  "eq_rule_mod_vars lr st ⟷ instance_rule lr st ∧ instance_rule st lr"

notation eq_rule_mod_vars ("(_/ =⇩v _)" [51,51] 50)

lemma instance_rule_var_cond: assumes eq: "instance_rule (s,t) (l,r)"
  and vars: "vars_term r ⊆ vars_term l"
shows "vars_term t ⊆ vars_term s"
proof -
  from eq[unfolded instance_rule_def]
  obtain τ where s: "s = l ⋅ τ" and t: "t = r ⋅ τ" by auto
  show ?thesis
  proof
    fix x
    assume "x ∈ vars_term t"
    from this[unfolded t] have "x ∈ vars_term (l ⋅ τ)" using vars unfolding vars_term_subst by auto
    then show "x ∈ vars_term s" unfolding s by auto
  qed
qed

lemma instance_rule_rstep: assumes step: "(s,t) ∈ rstep {lr}"
  and bex: "Bex R (instance_rule lr)"
shows "(s,t) ∈ rstep R"
proof -
  from bex obtain lr' where inst: "instance_rule lr lr'" and R: "lr' ∈ R" by auto
  obtain l r where lr: "lr = (l,r)" by force
  obtain l' r' where lr': "lr' = (l',r')" by force
  note inst = inst[unfolded lr lr']
  note R = R[unfolded lr']
  from inst[unfolded instance_rule_def] obtain σ where l: "l = l' ⋅ σ" and r: "r = r' ⋅ σ" by auto
  from step[unfolded lr] obtain C τ where "s = C ⟨l ⋅ τ⟩" "t = C ⟨r ⋅ τ⟩" by auto
  with l r have s: "s = C⟨l' ⋅ (σ ∘⇩s τ)⟩" and t: "t = C⟨r' ⋅ (σ ∘⇩s τ)⟩" by auto
  from rstepI[OF R s t] show ?thesis .
qed

lemma eq_rule_mod_vars_var_cond: assumes eq: "(l,r) =⇩v (s,t)"
  and vars: "vars_term r ⊆ vars_term l"
shows "vars_term t ⊆ vars_term s"
  by (rule instance_rule_var_cond[OF _ vars], insert eq[unfolded eq_rule_mod_vars_def], auto)

lemma eq_rule_mod_varsE[elim]: fixes l :: "('f,'v)term" 
  assumes "(l,r) =⇩v (s,t)"
  shows "∃ σ τ. l = s ⋅ σ ∧ r = t ⋅ σ ∧ s = l ⋅ τ ∧ t = r ⋅ τ ∧ range σ ⊆ range Var ∧ range τ ⊆ range Var"
proof -
  from assms[unfolded eq_rule_mod_vars_def instance_rule_def fst_conv snd_conv]
  obtain σ τ where l: "l = s ⋅ σ" and r: "r = t ⋅ σ" and s: "s = l ⋅ τ" and t: "t = r ⋅ τ" by blast+
  obtain f :: 'f where True by auto
  let ?vst = "vars_term (Fun f [s,t])"
  let ?vlr = "vars_term (Fun f [l,r])"
  define σ' where "σ' ≡ λ x. if x ∈ ?vst then σ x else Var x"
  define τ' where "τ' ≡ λ x. if x ∈ ?vlr then τ x else Var x"
  show ?thesis
  proof (intro exI conjI)
    show l: "l = s ⋅ σ'" unfolding l σ'_def
      by (rule term_subst_eq, auto)
    show r: "r = t ⋅ σ'" unfolding r σ'_def
      by (rule term_subst_eq, auto)
    show s: "s = l ⋅ τ'" unfolding s τ'_def
      by (rule term_subst_eq, auto)
    show t: "t = r ⋅ τ'" unfolding t τ'_def
      by (rule term_subst_eq, auto)
    have "Fun f [s,t] ⋅ Var = Fun f [l, r] ⋅ τ'" unfolding s t by simp
    also have "… = Fun f [s,t] ⋅ (σ' ∘⇩s τ')" unfolding l r by simp
    finally have "Fun f [s,t] ⋅ (σ' ∘⇩s τ') = Fun f [s,t] ⋅ Var" by simp
    from term_subst_eq_rev[OF this] have vst: "⋀ x. x ∈ ?vst ⟹ σ' x ⋅ τ' = Var x" unfolding subst_compose_def by auto
    have "Fun f [l,r] ⋅ Var = Fun f [s, t] ⋅ σ'" unfolding l r by simp
    also have "… = Fun f [l,r] ⋅ (τ' ∘⇩s σ')" unfolding s t by simp
    finally have "Fun f [l,r] ⋅ (τ' ∘⇩s σ') = Fun f [l,r] ⋅ Var" by simp
    from term_subst_eq_rev[OF this] have vlr: "⋀ x. x ∈ ?vlr ⟹ τ' x ⋅ σ' = Var x" unfolding subst_compose_def by auto
    {
      fix x
      have "σ' x ∈ range Var"
      proof (cases "x ∈ ?vst")
        case True
        from vst[OF this] show ?thesis by (cases "σ' x", auto)
      next
        case False
        then show ?thesis unfolding σ'_def by auto
      qed
    }
    then show "range σ' ⊆ range Var" by auto
    {
      fix x
      have "τ' x ∈ range Var"
      proof (cases "x ∈ ?vlr")
        case True
        from vlr[OF this] show ?thesis by (cases "τ' x", auto)
      next
        case False
        then show ?thesis unfolding τ'_def by auto
      qed
    }
    then show "range τ' ⊆ range Var" by auto
  qed
qed

subsection‹Linear and Left-Linear TRSs›

definition
  linear_trs :: "('f, 'v) trs ⇒ bool"
  where
    "linear_trs R ≡ ∀(l, r)∈R. linear_term l ∧ linear_term r"

lemma linear_trsE[elim,consumes 1]: "linear_trs R ⟹ (l,r) ∈ R ⟹ linear_term l ∧ linear_term r"
  unfolding linear_trs_def by auto

lemma linear_trsI[intro]: "⟦ ⋀ l r. (l,r) ∈ R ⟹ linear_term l ∧ linear_term r⟧ ⟹ linear_trs R"
  unfolding linear_trs_def by auto

definition
  left_linear_trs :: "('f, 'v) trs ⇒ bool"
  where
    "left_linear_trs R ⟷ (∀(l, r)∈R. linear_term l)"

lemma left_linear_trs_union: "left_linear_trs (R ∪ S) = (left_linear_trs R ∧ left_linear_trs S)"
  unfolding left_linear_trs_def by auto

lemma left_linear_mono: assumes "left_linear_trs S" and "R ⊆ S" shows "left_linear_trs R"
  using assms unfolding left_linear_trs_def by auto

lemma left_linear_map_funs_trs[simp]:  "left_linear_trs (map_funs_trs f R) = left_linear_trs R"
  unfolding left_linear_trs_def by (auto simp: map_funs_trs.simps)

lemma left_linear_weak_match_rstep:
  assumes rstep: "(u, v) ∈ rstep R"
    and weak_match: "weak_match s u"
    and ll: "left_linear_trs R"
  shows "∃t. (s, t) ∈ rstep R ∧ weak_match t v"
  using weak_match
proof (induct rule: rstep_induct_rule [OF rstep])
  case (1 C sig l r)
  from 1(2) show ?case
  proof (induct C arbitrary: s)
    case (More f bef C aft s)
    let ?n = "Suc (length bef + length aft)"
    let ?m = "length bef"
    from More(2) obtain ss where s: "s = Fun f ss" and lss: "?n = length ss" and wm: "(∀i<length ss. weak_match (ss ! i) ((bef @ C⟨l ⋅ sig⟩ # aft) ! i))"  by (cases s, auto)
    from lss wm[THEN spec, of ?m] have "weak_match (ss ! ?m) C⟨l ⋅ sig⟩" by auto
    from More(1)[OF this] obtain t where wmt:  "weak_match t C⟨r ⋅ sig⟩" and step: "(ss ! ?m,t) ∈ rstep R" by auto
    from lss have mss: "?m < length ss" by simp
    let ?tsi = "λ t. take ?m ss @ t # drop (Suc ?m) ss"
    let ?ts = "?tsi t"
    let ?ss = "?tsi (ss ! ?m)"
    from id_take_nth_drop[OF mss]
    have lts: "length ?ts = ?n" using lss by auto
    show ?case
    proof (rule exI[of _ "Fun f ?ts"], intro conjI)
      have "weak_match (Fun f ?ts) (More f bef C aft)⟨r ⋅ sig⟩ =
        weak_match (Fun f ?ts) (Fun f (bef @ C⟨r ⋅ sig⟩ # aft))" by simp
      also have "…" proof (unfold weak_match.simps lts, intro conjI refl allI impI)
        fix i
        assume i: "i < ?n"
        show "weak_match (?ts ! i) ((bef @ C⟨r ⋅ sig⟩ # aft) ! i)"
        proof (cases "i = ?m")
          case True
          have "weak_match (?ts ! i) ((bef @ C⟨r ⋅ sig⟩ # aft) ! i) = weak_match t C⟨r ⋅ sig⟩"
            using True mss by (simp add: nth_append)
          then show ?thesis using wmt by simp
        next
          case False
          have eq: "?ts ! i = ss ! i ∧ (bef @ C⟨r ⋅ sig⟩ # aft) ! i = (bef @ C⟨l ⋅ sig⟩ # aft) ! i"
          proof (cases "i < ?m")
            case True
            then show ?thesis by (simp add: nth_append lss[symmetric])
          next
            case False
            with ‹i ≠ ?m› i have "∃ j. i = Suc (?m + j) ∧ j < length aft" by presburger
            then obtain j where i: "i = Suc (?m + j)" and j: "j < length aft" by auto
            then have id: " (Suc (length bef + j) - min (Suc (length bef + length aft)) (length bef)) = Suc j" by simp
            from j show ?thesis by (simp add: nth_append i id lss[symmetric])
          qed
          then show ?thesis using wm[THEN spec, of i] i[unfolded lss] by (simp)
        qed
      qed simp
      finally show "weak_match (Fun f ?ts) (More f bef C aft)⟨r ⋅ sig⟩" by simp
    next
      have "s = Fun f ?ss" unfolding s using id_take_nth_drop[OF mss, symmetric] by simp
      also have "… = (More f (take ?m ss) □ (drop (Suc ?m) ss))⟨(ss ! ?m)⟩" (is "_ = ?C⟨_⟩") by simp
      finally have s: "s = ?C⟨ss ! ?m⟩" .
      have t: "Fun f ?ts = ?C⟨t⟩" by simp
      from rstep_ctxt[OF step]
      show "(s, Fun f ?ts) ∈ rstep R"
        unfolding s t .
    qed
  next
    case (Hole s)
    from ll 1(1) have "linear_term l" unfolding left_linear_trs_def by auto
    from linear_weak_match[OF this Hole[simplified] refl] obtain τ where
      "s = l ⋅ τ" and "(∀ x ∈ vars_term l . weak_match (Var x ⋅ τ) (Var x ⋅ sig))"
      by auto
    then obtain tau where s: "s = l ⋅ tau" and wm: "(∀ x ∈ vars_term l . weak_match (tau x) (Var x ⋅ sig))"
      by (auto)
    let ?delta = "(λ x. if x ∈ vars_term l then tau x else Var x ⋅ sig)"
    show ?case
    proof (rule exI[of _ "r ⋅ ?delta"], rule conjI)
      have "s = l ⋅ (tau |s (vars_term l))" unfolding s by (rule coincidence_lemma)
      also have "… = l ⋅ (?delta  |s (vars_term l))" by simp
      also have "… = l ⋅ ?delta" by (rule coincidence_lemma[symmetric])
      finally have s: "s = l ⋅ ?delta" .
      from 1(1) have step: "(l ⋅ ?delta, r ⋅ ?delta) ∈ rstep R" by auto
      then show "(s, r ⋅ ?delta) ∈ rstep R" unfolding s .
    next
      have "weak_match (r ⋅ ?delta) (r ⋅ sig)"
      proof (induct r)
        case (Fun f ss)
        from this[unfolded set_conv_nth]
        show ?case by (force)
      next
        case (Var x)
        show ?case
        proof (cases "x ∈ vars_term l")
          case True
          with wm Var show ?thesis by simp
        next
          case False
          show ?thesis by (simp add: Var False weak_match_refl)
        qed
      qed
      then show "weak_match (r ⋅ ?delta) (□ ⟨(r ⋅ sig)⟩)" by simp
    qed
  qed
qed

context
begin

private fun S where
  "S R s t 0 = s"
| "S R s t (Suc i) = (SOME u. (S R s t i,u) ∈ rstep R ∧ weak_match u (t(Suc i)))"

lemma weak_match_SN:
  assumes wm: "weak_match s t"
    and ll: "left_linear_trs R"
    and SN: "SN_on (rstep R) {s}"
  shows "SN_on (rstep R) {t}"
proof
  fix f
  assume t0: "f 0 ∈ {t}" and chain: "chain (rstep R) f"
  let ?s = "S R s f"
  let ?P = "λi u. (?s i, u) ∈ rstep R ∧ weak_match u (f (Suc i))"
  have "∀i. (?s i, ?s (Suc i)) ∈ rstep R ∧ weak_match (?s (Suc i)) (f (Suc i))"
  proof
    fix i show "(?s i, ?s (Suc i)) ∈ rstep R ∧ weak_match (?s (Suc i)) (f (Suc i))"
    proof (induct i)
      case 0
      from chain have ini: "(f 0, f (Suc 0)) ∈ rstep R" by simp
      then have "(t, f (Suc 0)) ∈ rstep R" unfolding singletonD[OF t0, symmetric] .
      from someI_ex[OF left_linear_weak_match_rstep[OF this wm ll]]
      show ?case by simp
    next
      case (Suc i)
      then have IH1: "(?s i, ?s (Suc i)) ∈ rstep R"
        and IH2: "weak_match (?s (Suc i)) (f (Suc i))" by auto
      from chain have nxt: "(f (Suc i), f (Suc (Suc i))) ∈ rstep R" by simp
      from someI_ex[OF left_linear_weak_match_rstep[OF this IH2 ll]]
      have "∃u. ?P (Suc i) u" by auto
      from someI_ex[OF this]
      show ?case by simp
    qed
  qed
  moreover have "?s 0 = s" by simp
  ultimately have "¬ SN_on (rstep R) {s}" by best
  with SN show False by simp
qed
end

lemma lhs_notin_NF_rstep: "(l, r) ∈ R ⟹ l ∉ NF (rstep R)" by auto

lemma NF_instance:
  assumes "(t ⋅ σ) ∈ NF (rstep R)" shows "t ∈ NF (rstep R)"
  using assms by auto

lemma NF_subterm:
  assumes "t ∈ NF (rstep R)" and "t ⊵ s"
  shows "s ∈ NF (rstep R)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain u where "(s, u) ∈ rstep R" by auto
  from ‹t ⊵ s› obtain C where "t = C⟨s⟩" by auto
  with ‹(s, u) ∈ rstep R› have "(t, C⟨u⟩) ∈ rstep R" by auto
  then have "t ∉ NF (rstep R)" by auto
  with assms show False by simp
qed

abbreviation
  lhss :: "('f, 'v) trs ⇒ ('f, 'v) terms"
  where
    "lhss R ≡ fst ` R"

abbreviation
  rhss :: "('f, 'v) trs ⇒ ('f, 'v) terms"
  where
    "rhss R ≡ snd ` R"


definition map_funs_trs_wa :: "('f × nat ⇒ 'g) ⇒ ('f, 'v) trs ⇒ ('g, 'v) trs" where
  "map_funs_trs_wa fg R = (λ(l, r). (map_funs_term_wa fg l, map_funs_term_wa fg r)) ` R"

lemma map_funs_trs_wa_union: "map_funs_trs_wa fg (R ∪ S) = map_funs_trs_wa fg R ∪ map_funs_trs_wa fg S"
  unfolding map_funs_trs_wa_def by auto

lemma map_funs_term_wa_compose: "map_funs_term_wa gh (map_funs_term_wa fg t) = map_funs_term_wa (λ (f,n). gh (fg (f,n), n)) t"
  by (induct t, auto)

lemma map_funs_trs_wa_compose: "map_funs_trs_wa gh (map_funs_trs_wa fg R) = map_funs_trs_wa (λ (f,n). gh (fg (f,n), n)) R" (is "?L = map_funs_trs_wa ?fgh R")
proof -
  have "map_funs_trs_wa ?fgh R = {(map_funs_term_wa ?fgh l, map_funs_term_wa ?fgh r)| l r. (l,r) ∈ R}" unfolding map_funs_trs_wa_def by auto
  also have "… = {(map_funs_term_wa gh (map_funs_term_wa fg l), map_funs_term_wa gh (map_funs_term_wa fg r)) | l r. (l,r) ∈ R}" unfolding map_funs_term_wa_compose ..
  finally show ?thesis unfolding map_funs_trs_wa_def by force
qed

lemma map_funs_trs_wa_funas_trs_id: assumes R: "funas_trs R ⊆ F"
  and id: "⋀ g n. (g,n) ∈ F ⟹ f (g,n) = g"
shows "map_funs_trs_wa f R = R"
proof -
  {
    fix l r
    assume "(l,r) ∈ R"
    with R have l: "funas_term l ⊆ F" and r: "funas_term r ⊆ F" unfolding funas_trs_def
      by (force simp: funas_rule_def)+
    from map_funs_term_wa_funas_term_id[OF l id] map_funs_term_wa_funas_term_id[OF r id]
    have "map_funs_term_wa f l = l" "map_funs_term_wa f r = r" by auto
  } note main = this
  have "map_funs_trs_wa f R = {(map_funs_term_wa f l, map_funs_term_wa f r) | l r. (l,r) ∈ R}"
    unfolding map_funs_trs_wa_def by force
  also have "… = R" using main by force
  finally show ?thesis .
qed

lemma map_funs_trs_wa_rstep: assumes step:"(s,t) ∈ rstep R"
  shows "(map_funs_term_wa fg s,map_funs_term_wa fg t) ∈ rstep (map_funs_trs_wa fg R)"
  using step
proof (induct)
  case (IH C σ l r)
  show ?case unfolding map_funs_trs_wa_def
    by (rule rstepI[where l = "map_funs_term_wa fg l" and r = "map_funs_term_wa fg r" and C = "map_funs_ctxt_wa fg C"], auto simp: IH)
qed

lemma map_funs_trs_wa_rsteps: assumes step:"(s,t) ∈ (rstep R)⇧*"
  shows "(map_funs_term_wa fg s,map_funs_term_wa fg t) ∈ (rstep (map_funs_trs_wa fg R))⇧*"
  using step
proof (induct)
  case (step a b)
  from map_funs_trs_wa_rstep[OF step(2), of fg] step(3) show ?case by auto
qed auto

lemma rstep_ground:
  assumes wf_trs: "⋀l r. (l, r) ∈ R ⟹ vars_term r ⊆ vars_term l"
    and ground: "ground s"
    and step: "(s, t) ∈ rstep R"
  shows "ground t"
  using step ground
proof (induct)
  case (IH C σ l r)
  from wf_trs[OF IH(1)] IH(2)
  show ?case by auto
qed

lemma rsteps_ground:
  assumes wf_trs: "⋀l r. (l, r) ∈ R ⟹ vars_term r ⊆ vars_term l"
    and ground: "ground s"
    and steps: "(s, t) ∈ (rstep R)⇧*"
  shows "ground t"
  using steps ground
  by (induct, insert rstep_ground[OF wf_trs], auto)

definition locally_terminating :: "('f,'v)trs ⇒ bool"
  where "locally_terminating R ≡ ∀ F. finite F ⟶ SN (sig_step F (rstep R))"

definition "non_collapsing R ⟷ (∀ lr ∈ R. is_Fun (snd lr))"

lemma supt_rstep_stable:
  assumes "(s, t) ∈ {⊳} ∪ rstep R"
  shows "(s ⋅ σ, t ⋅ σ) ∈ {⊳} ∪ rstep R"
  using assms proof
  assume "s ⊳ t" show ?thesis
  proof (rule UnI1)
    from ‹s ⊳ t› show "s ⋅ σ ⊳ t ⋅ σ" by (rule supt_subst)
  qed
next
  assume "(s, t) ∈ rstep R" show ?thesis
  proof (rule UnI2)
    from ‹(s, t) ∈ rstep R› show "(s ⋅ σ, t ⋅ σ) ∈ rstep R" ..
  qed
qed

lemma supt_rstep_trancl_stable:
  assumes "(s, t) ∈ ({⊳} ∪ rstep R)⇧+"
  shows "(s ⋅ σ, t ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧+"
  using assms proof (induct)
  case (base u)
  then have "(s ⋅ σ, u ⋅ σ) ∈ {⊳} ∪ rstep R" by (rule supt_rstep_stable)
  then show ?case ..
next
  case (step u v)
  from ‹(s ⋅ σ, u ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧+›
    and supt_rstep_stable[OF ‹(u, v) ∈ {⊳} ∪ rstep R›, of "σ"]
  show ?case ..
qed

lemma supt_rsteps_stable:
  assumes "(s, t) ∈ ({⊳} ∪ rstep R)⇧*"
  shows "(s ⋅ σ, t ⋅ σ) ∈ ({⊳} ∪ rstep R)⇧*"
  using assms
proof (induct)
  case base then show ?case ..
next
  case (step u v)
  from ‹(s, u) ∈ ({⊳} ∪ rstep R)⇧*› and ‹(u, v) ∈ {⊳} ∪ rstep R›
  have "(s, v) ∈ ({⊳} ∪ rstep R)⇧+" by (rule rtrancl_into_trancl1)
  from trancl_into_rtrancl[OF supt_rstep_trancl_stable[OF this]]
  show ?case .
qed

lemma eq_rule_mod_vars_refl[simp]: "r =⇩v r"
proof (cases r)
  case (Pair l r)
  {
    have "fst (l, r) = fst (l, r) ⋅ Var ∧ snd (l, r) = snd (l, r) ⋅ Var" by auto
  }
  then show ?thesis unfolding Pair eq_rule_mod_vars_def instance_rule_def by best
qed

lemma instance_rule_refl[simp]: "instance_rule r r"
  using eq_rule_mod_vars_refl[of r] unfolding eq_rule_mod_vars_def by simp

lemma is_Fun_Fun_conv: "is_Fun t = (∃f ts. t = Fun f ts)" by auto

lemma wf_trs_def':
  "wf_trs R = (∀(l, r)∈R. is_Fun l ∧ vars_term r ⊆ vars_term l)"
  by (rule iffI) (auto simp: wf_trs_def is_Fun_Fun_conv)

definition wf_rule :: "('f, 'v) rule ⇒ bool" where
  "wf_rule r ⟷ is_Fun (fst r) ∧ vars_term (snd r) ⊆ vars_term (fst r)"

definition wf_rules :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
  "wf_rules R = {r. r ∈ R ∧ wf_rule r}"

lemma wf_trs_wf_rules[simp]: "wf_trs (wf_rules R)"
  unfolding wf_trs_def' wf_rules_def wf_rule_def split_def by simp

lemma wf_rules_subset[simp]: "wf_rules R ⊆ R"
  unfolding wf_rules_def by auto

fun wf_reltrs :: "('f, 'v) trs ⇒ ('f, 'v) trs  ⇒ bool" where
  "wf_reltrs R S = (
    wf_trs R ∧ (R ≠ {} ⟶ (∀l r. (l, r) ∈ S ⟶ vars_term r ⊆ vars_term l)))"

lemma SN_rel_imp_wf_reltrs:
  assumes SN_rel: "SN_rel (rstep R) (rstep S)"
  shows "wf_reltrs R S"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain l r where "¬ wf_trs R ∨ R ≠ {} ∧ (l,r) ∈ S ∧ ¬ vars_term r ⊆ vars_term l" (is "_ ∨ ?two") by auto
  then show False
  proof
    assume "¬ wf_trs R"
    with SN_rstep_imp_wf_trs[OF SN_rel_imp_SN[OF assms]]
    show False by simp
  next
    assume ?two
    then obtain ll rr x where lr: "(l,r) ∈ S" and llrr: "(ll,rr) ∈ R" and x: "x ∈ vars_term r" and nx: "x ∉ vars_term l" by auto
    obtain f and σ
      where sigma: "σ = (λy. if x = y then Fun f [ll,l] else Var y)" by auto
    have id: "σ |s (vars_term l) = Var" unfolding sigma
      by (simp add: subst_restrict_def, rule ext, auto simp: nx)
    have l: "l = l ⋅ σ"  by (simp add: coincidence_lemma[of l σ] id)
    have "(l ⋅ σ, r ⋅ σ) ∈ rstep S" using lr by auto
    with l have sstep: "(l, r ⋅ σ) ∈ rstep S" by simp
    from supteq_subst[OF supteq_Var[OF x], of σ] have
      "r ⋅ σ ⊵ Fun f [ll,l]" unfolding sigma by auto
    then obtain C where "C⟨Fun f [ll, l]⟩ = r ⋅ σ" by auto
    with sstep have sstep: "(l,C⟨Fun f [ll, l]⟩) ∈ rstep S" by simp
    obtain r where r: "r = relto (rstep R) (rstep S) ∪ {⊳}" by auto
    have "(C⟨Fun f [ll,l]⟩, C⟨Fun f [rr,l]⟩) ∈ rstep R"
      by (intro rstepI[OF llrr, of _ "C ∘⇩c More f [] □ [l]" Var], auto)
    with sstep have relto: "(l,C⟨Fun f [rr,l]⟩) ∈ r" unfolding  r by auto
    have "C⟨Fun f [rr,l]⟩ ⊵ Fun f [rr,l]" using ctxt_imp_supteq by auto
    also have "Fun f [rr,l] ⊳ l" by auto
    finally have supt: "C⟨Fun f [rr,l]⟩ ⊳ l" unfolding supt_def by simp
    then have "(C⟨Fun f [rr,l]⟩, l) ∈ r" unfolding r by auto
    with relto have loop: "(l, l) ∈ r⇧+" by auto
    have "SN r" unfolding r
      by (rule SN_imp_SN_union_supt[OF SN_rel[unfolded SN_rel_defs]], blast)
    then have "SN (r⇧+)" by (rule SN_imp_SN_trancl)
    with loop show False unfolding SN_on_def by auto
  qed
qed

lemmas rstep_wf_rules_subset = rstep_mono[OF wf_rules_subset]

definition map_vars_trs :: "('v ⇒ 'w) ⇒ ('f, 'v) trs ⇒ ('f, 'w) trs" where
  "map_vars_trs f R = (λ (l, r). (map_vars_term f l, map_vars_term f r)) ` R"

lemma map_vars_trs_rstep:
  assumes "(s, t) ∈ rstep (map_vars_trs f R)" (is "_ ∈ rstep ?R")
  shows "(s ⋅ τ, t ⋅ τ) ∈ rstep R"
  using assms
proof
  fix ml mr C σ
  presume mem: "(ml,mr) ∈ ?R" and s: "s = C⟨ml ⋅ σ⟩" and t: "t = C⟨mr ⋅ σ⟩"
  let ?m = "map_vars_term f"
  from mem obtain l r where mem: "(l,r) ∈ R" and id: "ml = ?m l" "mr = ?m r"
    unfolding map_vars_trs_def by auto
  have id: "s ⋅ τ = (C ⋅⇩c τ)⟨?m l ⋅ σ ∘⇩s τ⟩" "t ⋅ τ = (C ⋅⇩c τ)⟨?m r ⋅ σ ∘⇩s τ⟩" by (auto simp: s t id)
  then show "(s ⋅ τ, t ⋅ τ) ∈ rstep R"
    unfolding id apply_subst_map_vars_term
    using mem by auto
qed auto

lemma map_vars_rsteps:
  assumes "(s,t) ∈ (rstep (map_vars_trs f R))⇧*" (is "_ ∈ (rstep ?R)⇧*")
  shows "(s ⋅ τ, t ⋅ τ) ∈ (rstep R)⇧*"
  using assms
proof (induct)
  case base then show ?case by simp
next
  case (step t u)
  from map_vars_trs_rstep[OF step(2), of τ] step(3) show ?case by auto
qed

lemma rsteps_subst_closed: "(s,t) ∈ (rstep R)⇧+ ⟹ (s ⋅ σ, t ⋅ σ) ∈ (rstep R)⇧+"
proof -
  let ?R = "rstep R"
  assume steps: "(s,t) ∈ ?R⇧+"
  have subst: "subst.closed (?R⇧+)" by (rule subst.closed_trancl[OF subst_closed_rstep])
  from this[unfolded subst.closed_def] steps show ?thesis by auto
qed

lemma supteq_rtrancl_supt:
  "(R⇧+ O {⊵}) ⊆ ({⊳} ∪ R)⇧+" (is "?l ⊆ ?r")
proof
  fix x z
  assume "(x,z) ∈ ?l"
  then obtain y where xy: "(x,y) ∈ R⇧+" and yz: "y ⊵ z" by auto
  from xy have xy: "(x,y) ∈ ?r" by (rule trancl_mono, simp)
  show "(x,z) ∈ ?r"
  proof (cases "y = z")
    case True
    with xy show ?thesis by simp
  next
    case False
    with yz have yz: "(y,z) ∈ {⊳} ∪ R" by auto
    with xy have xz: "(x,z) ∈ ?r O ({⊳} ∪ R)" by auto
    then show ?thesis by (metis UnCI trancl_unfold)
  qed
qed

lemma rrstepI[intro]: "(l, r) ∈ R ⟹ s = l ⋅ σ ⟹ t = r ⋅ σ ⟹ (s, t) ∈ rrstep R"
  unfolding rrstep_def' by auto

lemma CS_rrstep_conv: "subst.closure = rrstep"
  apply (intro ext)
  apply (unfold rrstep_def')
  apply (intro subset_antisym)
  by (insert subst.closure.cases, blast, auto)

text ‹Rewrite steps at a fixed position›

inductive_set rstep_pos :: "('f, 'v) trs ⇒ pos ⇒ ('f, 'v) term rel" for R and p
  where
    rule [intro]:"(l, r) ∈ R ⟹ p ∈ poss s ⟹ s |_ p = l ⋅ σ ⟹
    (s, replace_at s p (r ⋅ σ)) ∈ rstep_pos R p"

lemma rstep_pos_subst:
  assumes "(s, t) ∈ rstep_pos R p"
  shows "(s ⋅ σ, t ⋅ σ) ∈ rstep_pos R p"
  using assms
proof (cases)
  case (rule l r σ')
  with rstep_pos.intros [OF this(2), of p "s ⋅ σ" "σ' ∘⇩s σ"]
  show ?thesis by (auto simp: ctxt_of_pos_term_subst)
qed

lemma rstep_pos_rule:
  assumes "(l, r) ∈ R"
  shows "(l, r) ∈ rstep_pos R []"
  using rstep_pos.intros [OF assms, of "[]" l Var] by simp

lemma rstep_pos_rstep_r_p_s_conv:
  "rstep_pos R p = {(s, t) | s t r σ. (s, t) ∈ rstep_r_p_s R r p σ}"
  by (auto simp: rstep_r_p_s_def Let_def subt_at_ctxt_of_pos_term
      intro: replace_at_ident
      elim!: rstep_pos.cases)

lemma rstep_rstep_pos_conv:
  "rstep R = {(s, t) | s t p. (s, t) ∈ rstep_pos R p}"
  by (force simp: rstep_pos_rstep_r_p_s_conv rstep_iff_rstep_r_p_s)

lemma rstep_pos_supt:
  assumes "(s, t) ∈ rstep_pos R p"
    and q: "q ∈ poss u" and u: "u |_ q = s"
  shows "(u, (ctxt_of_pos_term q u)⟨t⟩) ∈ rstep_pos R (q @ p)"
  using assms
proof (cases)
  case (rule l r σ)
  with q and u have "(q @ p) ∈ poss u" and "u |_ (q @ p) = l ⋅ σ" by auto
  with rstep_pos.rule [OF rule(2) this] show ?thesis
    unfolding rule by (auto simp: ctxt_of_pos_term_append u)
qed

lemma rrstep_rstep_pos_conv:
  "rrstep R = rstep_pos R []"
  by (auto simp: rrstep_def rstep_pos_rstep_r_p_s_conv)

lemma rrstep_imp_rstep:
  assumes "(s, t) ∈ rrstep R"
  shows "(s, t) ∈ rstep R"
  using assms by (auto simp: rrstep_def rstep_iff_rstep_r_p_s)

lemma not_NF_rstep_imp_subteq_not_NF_rrstep:
  assumes "s ∉ NF (rstep R)"
  shows "∃t ⊴ s. t ∉ NF (rrstep R)"
proof -
  from assms obtain u where "(s, u) ∈ rstep R" by auto
  then obtain l r C σ where "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and u: "u = C⟨r ⋅ σ⟩" by auto
  then have "(l ⋅ σ, r ⋅ σ) ∈ rrstep R" and "l ⋅ σ ⊴ s" by auto
  then show ?thesis by blast
qed

lemma all_subt_NF_rrstep_iff_all_subt_NF_rstep:
  "(∀s ⊲ t. s ∈ NF (rrstep R)) ⟷ (∀s ⊲ t. s ∈ NF (rstep R))"
  by (auto dest: rrstep_imp_rstep supt_supteq_trans not_NF_rstep_imp_subteq_not_NF_rrstep)

lemma not_in_poss_imp_NF_rstep_pos [simp]:
  assumes "p ∉ poss s"
  shows "s ∈ NF (rstep_pos R p)"
  using assms by (auto simp: NF_def elim: rstep_pos.cases)

lemma Var_rstep_imp_rstep_pos_Empty:
  assumes "(Var x, t) ∈ rstep R"
  shows "(Var x, t) ∈ rstep_pos R []"
  using assms by (metis Var_supt nrrstep_subt rrstep_rstep_pos_conv rstep_cases)

lemma rstep_args_NF_imp_rrstep:
  assumes "(s, t) ∈ rstep R"
    and "∀u ⊲ s. u ∈ NF (rstep R)"
  shows "(s, t) ∈ rrstep R"
  using assms by (metis NF_iff_no_step nrrstep_subt rstep_cases)

lemma rstep_pos_imp_rstep_pos_Empty:
  assumes "(s, t) ∈ rstep_pos R p"
  shows "(s |_ p, t |_ p) ∈ rstep_pos R []"
  using assms by (cases) (auto simp: replace_at_subt_at intro: rstep_pos_rule rstep_pos_subst)

lemma rstep_pos_arg:
  assumes "(s, t) ∈ rstep_pos R p"
    and "i < length ss" and "ss ! i = s"
  shows "(Fun f ss, (ctxt_of_pos_term [i] (Fun f ss))⟨t⟩) ∈ rstep_pos R (i # p)"
  using assms
  by cases (auto simp: rstep_pos.simps)

lemma rstep_imp_max_pos:
  assumes "(s, t) ∈ rstep R"
  shows "∃u. ∃p∈poss s. (s, u) ∈ rstep_pos R p ∧ (∀v ⊲ s |_ p. v ∈ NF (rstep R))"
  using assms
proof (induction s arbitrary: t)
  case (Var x)
  from Var_rstep_imp_rstep_pos_Empty [OF this] show ?case by auto
next
  case (Fun f ss)
  show ?case
  proof (cases "∀v ⊲ Fun f ss |_ []. v ∈ NF (rstep R)")
    case True
    moreover with Fun.prems
    have "(Fun f ss, t) ∈ rstep_pos R []"
      by (auto dest: rstep_args_NF_imp_rrstep simp: rrstep_rstep_pos_conv)
    ultimately show ?thesis by auto
  next
    case False
    then obtain v where "v ⊲ Fun f ss" and "v ∉ NF (rstep R)" by auto
    then obtain s and w where "s ∈ set ss" and "s ⊵ v" and "(s, w) ∈ rstep R"
      by (auto simp: NF_def) (metis NF_iff_no_step NF_subterm supt_Fun_imp_arg_supteq)
    from Fun.IH [OF this(1, 3)] obtain u and p
      where "p ∈ poss s" and *: "(s, u) ∈ rstep_pos R p"
        and **: "∀v ⊲ s |_ p. v ∈ NF (rstep R)" by blast
    from ‹s ∈ set ss› obtain i
      where "i < length ss" and [simp]:"ss ! i = s" by (auto simp: in_set_conv_nth)
    with ‹p ∈ poss s› have "i # p ∈ poss (Fun f ss)" by auto
    moreover with ** have "∀v ⊲ Fun f ss |_ (i # p). v ∈ NF (rstep R)" by auto
    moreover from rstep_pos_arg [OF * ‹i < length ss› ‹ss ! i = s›]
    have "(Fun f ss, (ctxt_of_pos_term [i] (Fun f ss))⟨u⟩) ∈ rstep_pos R (i # p)" .
    ultimately show ?thesis by blast
  qed
qed

subsection‹Normal Forms›

abbreviation NF_trs :: "('f, 'v) trs ⇒ ('f, 'v) terms" where
  "NF_trs R ≡ NF (rstep R)"

lemma NF_trs_mono: "r ⊆ s ⟹ NF_trs s ⊆ NF_trs r"
  by (rule NF_anti_mono[OF rstep_mono])

lemma NF_trs_union: "NF_trs (R ∪ S) = NF_trs R ∩ NF_trs S"
  unfolding rstep_union using NF_anti_mono[of _ "rstep R ∪ rstep S"] by auto

abbreviation NF_terms :: "('f, 'v) terms ⇒ ('f, 'v) terms" where
  "NF_terms Q ≡ NF (rstep (Id_on Q))"

lemma NF_terms_anti_mono:
  "Q ⊆ Q' ⟹ NF_terms Q' ⊆ NF_terms Q"
  by (rule NF_trs_mono, auto)

lemma lhs_var_not_NF:
  assumes "l ∈ T" and "is_Var l" shows "t ∉ NF_terms T"
proof -
  from assms obtain x where l: "l = Var x" by (cases l, auto)
  let ?σ = "subst x t"
  from assms have "l ∉ NF_terms T" by auto
  with NF_instance[of l "?σ" "Id_on T"]
  have "l ⋅ ?σ ∉ NF_terms T" by auto
  then show ?thesis by (simp add: l subst_def)
qed

lemma not_NF_termsE[elim]:
  assumes "s ∉ NF_terms Q"
  obtains l C σ where "l ∈ Q" and "s = C⟨l ⋅ σ⟩"
proof -
  from assms obtain t where "(s, t) ∈ rstep (Id_on Q)" by auto
  with ‹⋀l C σ. ⟦l ∈ Q; s = C⟨l ⋅ σ⟩⟧ ⟹ thesis› show ?thesis by auto
qed

lemma notin_NF_E [elim]:
  fixes R :: "('f, 'v) trs"
  assumes "t ∉ NF_trs R"
  obtains C l and σ :: "('f, 'v) subst" where "l ∈ lhss R" and "t = C⟨l ⋅ σ⟩"
proof -
  assume 1: "⋀l C (σ::('f, 'v) subst). l ∈ lhss R ⟹ t = C⟨l ⋅ σ⟩ ⟹ thesis"
  from assms obtain u where "(t, u) ∈ rstep R" by (auto simp: NF_def)
  then obtain C σ l r where "(l, r) ∈ R" and "t = C⟨l ⋅ σ⟩" by blast
  with 1 show ?thesis by force
qed

lemma NF_ctxt_subst: "NF_terms Q = {t. ¬ (∃ C q σ. t = C⟨q⋅σ⟩ ∧ q ∈ Q)}" (is "_ = ?R")
proof -
  {
    fix t
    assume "t ∉ ?R"
    then obtain C q σ where t: "t = C⟨q⋅σ⟩" and q: "q ∈ Q" by auto
    have "(t,t) ∈ rstep (Id_on Q)"
      unfolding t using q by auto
    then have "t ∉ NF_terms Q" by auto
  }
  moreover
  {
    fix t
    assume "t ∉ NF_terms Q"
    then obtain C q σ where t: "t = C⟨q⋅σ⟩" and q: "q ∈ Q" by auto
    then have "t ∉ ?R" by auto
  }
  ultimately show ?thesis by auto
qed

lemma some_NF_imp_no_Var:
  assumes "t ∈ NF_terms Q"
  shows "Var x ∉ Q"
proof
  assume "Var x ∈ Q"
  with assms[unfolded NF_ctxt_subst] have "⋀ σ C. t ≠ C ⟨ σ x ⟩" by force
  from this[of Hole "λ _. t"] show False by simp
qed

lemma NF_map_vars_term_inj:
  assumes inj: "⋀ x. n (m x) = x" and NF: "t ∈ NF_terms Q"
  shows "(map_vars_term m t) ∈ NF_terms (map_vars_term m ` Q)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then obtain u where "(map_vars_term m t, u) ∈ rstep (Id_on (map_vars_term m ` Q))" by blast
  then obtain ml mr C σ where in_mR: "(ml, mr) ∈ Id_on (map_vars_term m ` Q)"
    and mt: "map_vars_term m t = C⟨ml ⋅ σ⟩" by best
  let ?m = n
  from in_mR obtain l r where "(l, r) ∈ Id_on Q" and ml: "ml = map_vars_term m l" by auto
  have "t = map_vars_term ?m (map_vars_term m t)" by (simp add: map_vars_term_inj_compose[of n m, OF inj])
  also have "… = map_vars_term ?m (C⟨ml ⋅ σ⟩)" by (simp add: mt)
  also have "… = (map_vars_ctxt ?m C)⟨map_vars_term ?m (map_vars_term m l ⋅ σ)⟩"
    by (simp add: map_vars_term_ctxt_commute ml)
  also have "… = (map_vars_ctxt ?m C)⟨l ⋅ (map_vars_subst_ran ?m (σ ∘ m))⟩"
    by (simp add: apply_subst_map_vars_term map_vars_subst_ran)
  finally show False using NF and ‹(l, r) ∈ Id_on Q› by auto
qed

lemma notin_NF_terms: "t ∈ Q ⟹ t ∉ NF_terms Q"
  using lhs_notin_NF_rstep[of t t "Id_on Q"] by (simp add: Id_on_iff)

lemma NF_termsI [intro]:
  assumes NF: "⋀ C l σ. t = C ⟨l ⋅ σ⟩ ⟹ l ∈ Q ⟹ False"
  shows "t ∈ NF_terms Q"
  by (rule ccontr, rule not_NF_termsE [OF _ NF])

lemma NF_args_imp_NF:
  assumes ss: "⋀ s. s ∈ set ss ⟹ s ∈ NF_terms Q"
    and someNF: "t ∈ NF_terms Q"
    and root: "Some (f,length ss) ∉ root ` Q"
  shows "(Fun f ss) ∈ NF_terms Q"
proof
  fix C l σ
  assume id: "Fun f ss = C ⟨ l ⋅ σ ⟩" and l: "l ∈ Q"
  show False
  proof (cases C)
    case Hole
    with id have id: "Fun f ss = l ⋅ σ" by simp
    show False
    proof (cases l)
      case (Fun g ls)
      with id have fg: "f = g" and ss: "ss = map (λ s. s ⋅ σ) ls" by auto
      from arg_cong[OF ss, of length] have len: "length ss = length ls" by simp
      from l[unfolded Fun] root[unfolded fg len] show False by force
    next
      case (Var x)
      from some_NF_imp_no_Var[OF someNF] Var l show False by auto
    qed
  next
    case (More g bef D aft)
    note id = id[unfolded More]
    from id have NF: "ss ! length bef = D ⟨l ⋅ σ⟩" by auto
    from id have mem: "ss ! length bef ∈ set ss" by auto
    from ss[OF mem, unfolded NF_ctxt_subst NF] l show False by auto
  qed
qed

lemma NF_Var_is_Fun:
  assumes Q: "Ball Q is_Fun"
  shows "Var x ∈ NF_terms Q"
proof
  fix C l σ
  assume x: "Var x = C ⟨ l ⋅ σ ⟩" and l: "l ∈ Q"
  from l Q obtain f ls where l: "l = Fun f ls" by (cases l, auto)
  then show False using x by (cases C, auto)
qed

lemma NF_terms_lhss [simp]: "NF_terms (lhss R) = NF (rstep R)"
proof
  show "NF (rstep R) ⊆ NF_terms (lhss R)" by force
next
  show "NF_terms (lhss R) ⊆ NF (rstep R)"
  proof
    fix s assume NF: "s ∈ NF_terms (lhss R)"
    show "s ∈ NF (rstep R)"
    proof (rule ccontr)
      assume "s ∉ NF (rstep R)"
      then obtain t where "(s, t) ∈ rstep R" by auto
      then obtain l r C σ where "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" by auto
      then have "(l, l) ∈ Id_on (lhss R)" by force
      then have "(s, s) ∈ rstep (Id_on (lhss R))" unfolding s by auto
      with NF show False by auto
    qed
  qed
qed

subsection‹Relative Rewrite Steps›

abbreviation "relstep R E ≡ relto (rstep R) (rstep E)"

lemma args_SN_on_relstep_nrrstep_imp_args_SN_on:
  assumes SN: "⋀ u. s ⊳ u ⟹ SN_on (relstep R E) {u}"
    and st: "(s,t) ∈ nrrstep (R ∪ E)"
    and supt: "t ⊳ u"
  shows "SN_on (relstep R E) {u}"
proof -
  from nrrstepE[OF st] obtain C l r σ where "C ≠ □" and lr: "(l,r) ∈ R ∪ E"
    and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by blast
  then obtain f bef C aft where s: "s = Fun f (bef @ C⟨l ⋅ σ⟩ # aft)" and t: "t = Fun f (bef @ C⟨r ⋅ σ⟩ # aft)"
    by (cases C, auto)
  let ?ts = "bef @ C⟨r ⋅ σ⟩ # aft"
  let ?ss = "bef @ C⟨l ⋅ σ⟩ # aft"
  from supt obtain D where "t = D⟨u⟩" and "D ≠ □" by auto
  then obtain bef' aft' D where t': "t = Fun f (bef' @ D⟨u⟩ # aft')" unfolding t by (cases D, auto)
  have "D⟨u⟩ ⊵ u" by auto
  then have supt: "⋀ s. s ⊳ D⟨u⟩ ⟹ s ⊳ u" by (metis supt_supteq_trans)
  show "SN_on (relstep R E) {u}"
  proof (cases "D⟨u⟩ ∈ set ?ss")
    case True
    then have "s ⊳ D⟨u⟩" unfolding s by auto
    then have "s ⊳ u" by (rule supt)
    with SN show ?thesis by auto
  next
    case False
    have "D⟨u⟩ ∈ set ?ts" using arg_cong[OF t'[unfolded t], of args] by auto
    with False have Du: "D⟨u⟩ = C⟨r ⋅ σ⟩" by auto
    have "s ⊳ C⟨l ⋅ σ⟩" unfolding s by auto
    with SN have "SN_on (relstep R E) {C⟨l ⋅ σ⟩}" by auto
    from step_preserves_SN_on_relto[OF _ this, of "C⟨r ⋅ σ⟩"] lr
    have SN: "SN_on (relstep R E) {D⟨u⟩}" using Du by auto
    show ?thesis
      by (rule ctxt_closed_SN_on_subt[OF ctxt.closed_relto SN], auto)
  qed
qed

lemma Tinf_nrrstep:
  assumes tinf: "s ∈ Tinf (relstep R E)" and st: "(s,t) ∈ nrrstep (R ∪ E)"
    and t: "¬ SN_on (relstep R E) {t}"
  shows "t ∈ Tinf (relstep R E)"
  unfolding Tinf_def
  by (intro CollectI conjI[OF t] allI impI)
    (rule args_SN_on_relstep_nrrstep_imp_args_SN_on[OF _ st],
      insert tinf[unfolded Tinf_def], auto)

lemma subterm_preserves_SN_on_relstep:
  "SN_on (relstep R E) {s} ⟹ s ⊵ t ⟹ SN_on (relstep R E) {t}"
  using SN_imp_SN_subt [of "rstep (rstep ((rstep E)⇧*) O rstep R O rstep ((rstep E)⇧*))"]
  by (simp only: rstep_relcomp_idemp2) (simp only: rstep_rtrancl_idemp)

inductive_set rstep_rule :: "('f, 'v) rule ⇒ ('f, 'v) term rel" for ρ
  where
    rule: "s = C⟨fst ρ ⋅ σ⟩ ⟹ t = C⟨snd ρ ⋅ σ⟩ ⟹ (s, t) ∈ rstep_rule ρ"

lemma rstep_ruleI [intro]:
  "s = C⟨l ⋅ σ⟩ ⟹ t = C⟨r ⋅ σ⟩ ⟹ (s, t) ∈ rstep_rule (l, r)"
  by (auto simp: rstep_rule.simps)

lemma rstep_rule_ctxt:
  "(s, t) ∈ rstep_rule ρ ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep_rule ρ"
  using rstep_rule.rule [of "C⟨s⟩" "C ∘⇩c D" ρ _ "C⟨t⟩" for D]
  by (auto elim: rstep_rule.cases simp: ctxt_of_pos_term_append)

lemma rstep_rule_subst:
  assumes "(s, t) ∈ rstep_rule ρ"
  shows "(s ⋅ σ, t ⋅ σ) ∈ rstep_rule ρ"
  using assms
proof (cases)
  case (rule C τ)
  then show ?thesis
    using rstep_rule.rule [of "s ⋅ σ" _ "ρ" "τ ∘⇩s σ"]
    by (auto elim!: rstep_rule.cases simp: ctxt_of_pos_term_subst)
qed

lemma rstep_rule_imp_rstep:
  "ρ ∈ R ⟹ (s, t) ∈ rstep_rule ρ ⟹ (s, t) ∈ rstep R"
  by (force elim: rstep_rule.cases)

lemma rstep_imp_rstep_rule:
  assumes "(s, t) ∈ rstep R"
  obtains l r where "(l, r) ∈ R" and "(s, t) ∈ rstep_rule (l, r)"
  using assms by blast

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

lemma term_subst_rsteps:
  assumes "⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ (rstep R)⇧*"
  shows "(t ⋅ σ, t ⋅ τ) ∈ (rstep R)⇧*"
  by (metis assms rstep_rtrancl_idemp rtrancl_idemp term_subst_rstep)

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

lemma funas_trs_converse [simp]: "funas_trs (R¯) = funas_trs R"
  by (auto simp: funas_defs)

lemma rstep_rev: assumes "(s, t) ∈ rstep_pos {(l,r)} p" shows "((t, s) ∈ rstep_pos {(r,l)} p)"
proof-
  from assms obtain σ where step:"t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩" "p ∈ poss s" "s |_ p = l ⋅ σ"
    unfolding rstep_pos.simps by auto
  with replace_at_below_poss[of p s p] have pt:"p ∈ poss t" by auto
  with step ctxt_supt_id[OF step(2)] have "s = (ctxt_of_pos_term p t)⟨l ⋅ σ⟩"
    by (simp add: ctxt_of_pos_term_replace_at_below)
  with step ctxt_supt_id[OF pt] show ?thesis unfolding rstep_pos.simps
    by (metis pt replace_at_subt_at singletonI)
qed

lemma conversion_ctxt_closed: "(s, t) ∈ (rstep R)⇧↔⇧* ⟹ (C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧↔⇧*"
  using rsteps_closed_ctxt unfolding conversion_def
  by (simp only: rstep_simps(5)[symmetric])

lemma conversion_subst_closed:
  "(s, t) ∈ (rstep R)⇧↔⇧* ⟹ (s ⋅ σ,  t ⋅ σ) ∈ (rstep R)⇧↔⇧*"
  using rsteps_closed_subst unfolding conversion_def
  by (simp only: rstep_simps(5)[symmetric])

lemma rstep_simulate_conv:
  assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
  shows "(rstep S) ⊆ (rstep R)⇧↔⇧*"
proof
  fix s t
  assume "(s, t) ∈ rstep S"
  then obtain l r C σ where s: "s = C⟨l ⋅ σ⟩" and t:"t = C⟨r ⋅ σ⟩" and lr: "(l, r) ∈ S"
    unfolding rstep_iff_rstep_r_c_s rstep_r_c_s_def by auto
  with assms have "(l, r) ∈ (rstep R)⇧↔⇧*" by auto
  then show "(s, t) ∈ (rstep R)⇧↔⇧*" using conversion_ctxt_closed conversion_subst_closed s t by metis
qed

lemma symcl_simulate_conv:
  assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
  shows "(rstep S)⇧↔ ⊆ (rstep R)⇧↔⇧*"
  using rstep_simulate_conv[OF assms]
  by auto (metis conversion_inv subset_iff)

lemma conv_union_simulate:
  assumes "⋀ l r. (l, r) ∈ S ⟹ (l, r) ∈ (rstep R)⇧↔⇧*"
  shows "(rstep (R ∪ S))⇧↔⇧* = (rstep R)⇧↔⇧*"
proof
  show "(rstep (R ∪ S))⇧↔⇧* ⊆ (rstep R)⇧↔⇧*"
    unfolding conversion_def
  proof
    fix s t
    assume "(s, t) ∈ ((rstep (R ∪ S))⇧↔)⇧*"
    then show "(s, t) ∈ ((rstep R)⇧↔)⇧*"
    proof (induct rule: rtrancl_induct)
      case (step u t)
      then have "(u, t) ∈ (rstep R)⇧↔ ∨ (u, t) ∈ (rstep S)⇧↔" by auto
      then show ?case
      proof
        assume "(u, t) ∈ (rstep R)⇧↔"
        with step show ?thesis using rtrancl_into_rtrancl by metis
      next
        assume "(u, t) ∈ (rstep S)⇧↔"
        with symcl_simulate_conv[OF assms] have "(u, t) ∈ (rstep R)⇧↔⇧*" by auto
        with step show ?thesis by auto
      qed
    qed simp
  qed
next
  show "(rstep R)⇧↔⇧* ⊆ (rstep (R ∪ S))⇧↔⇧*"
    unfolding conversion_def
    using rstep_union rtrancl_mono sup.cobounded1 symcl_Un
    by metis
qed

definition "suptrel R = (relto {⊳} (rstep R))⇧+"
end