Theory Rewriting_Properties

section ‹Confluence related rewriting properties›
theory Rewriting_Properties
  imports Rewriting
    "Abstract-Rewriting.Abstract_Rewriting"
begin

subsection ‹Confluence related ARS properties›

definition "SCR_on r A ≡ (∀a ∈ A. ∀ b c. (a, b) ∈ r ∧ (a, c) ∈ r ⟶
  (∃ d. (b, d) ∈ r⇧= ∧  (c, d) ∈ r⇧*))"

abbreviation SCR :: "'a rel ⇒ bool" where "SCR r ≡ SCR_on r UNIV"

definition NFP_on :: "'a rel ⇒ 'a set ⇒ bool" where
  "NFP_on r A ⟷ (∀a∈A. ∀b c. (a, b) ∈ r⇧* ∧ (a, c) ∈ r⇧! ⟶ (b, c) ∈ r⇧*)"

abbreviation NFP :: "'a rel ⇒ bool" where "NFP r ≡ NFP_on r UNIV"

definition CE_on :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
  "CE_on r s A ⟷ (∀a∈A. ∀b. (a, b) ∈ r⇧↔⇧* ⟷ (a, b) ∈ s⇧↔⇧*)"

abbreviation CE :: "'a rel ⇒ 'a rel ⇒ bool" where "CE r s ≡ CE_on r s UNIV"

definition NE_on :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
  "NE_on r s A ⟷ (∀a∈A. ∀b. (a, b) ∈ r⇧! ⟷ (a, b) ∈ s⇧!)"

abbreviation NE :: "'a rel ⇒ 'a rel ⇒ bool" where "NE r s ≡ NE_on r s UNIV"

subsection ‹Signature closure of relation to model multihole context closure›

(* AUX lemmas *)

lemma sigstep_trancl_funas:
  "(s, t) ∈ (srstep ℱ 𝒮)⇧* ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ"
  "(s, t) ∈ (srstep ℱ 𝒮)⇧* ⟹ s ≠ t ⟹ funas_term t ⊆ ℱ"
  by (auto simp: rtrancl_eq_or_trancl dest: srstepsD)

lemma srrstep_to_srestep:
  "(s, t) ∈ srrstep ℱ ℛ ⟹ (s, t) ∈ srstep ℱ ℛ"
  by (meson in_mono rrstep_rstep_mono sig_step_mono2)

lemma srsteps_with_root_step_srstepsD:
  "(s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧+"
  by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)

lemma srsteps_with_root_step_sresteps_eqD:
  "(s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*"
  by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)

lemma symcl_srstep_conversion:
  "(s, t) ∈ srstep ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
  by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)

lemma symcl_srsteps_conversion:
  "(s, t) ∈ (srstep ℱ (ℛ⇧↔))⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
  by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)



lemma NF_srstep_args:
  assumes "Fun f ss ∈ NF (srstep ℱ ℛ)" "funas_term (Fun f ss) ⊆ ℱ" "i < length ss"
  shows "ss ! i ∈ NF (srstep ℱ ℛ)"
proof (rule ccontr)
  assume "ss ! i ∉ NF (srstep ℱ ℛ)"
  then obtain t where step: "(ss ! i, t) ∈ rstep ℛ" "funas_term t ⊆ ℱ"
    by (auto simp: NF_def sig_step_def)
  from assms(3) have [simp]: "Suc (length ss - Suc 0) = length ss" by auto
  from rstep_ctxt[OF step(1), where ?C = "ctxt_of_pos_term [i] (Fun f ss)"]  
  have "(Fun f ss, Fun f (ss[i := t])) ∈ srstep ℱ ℛ" using step(2) assms(2, 3)
    by (auto simp: sig_step_def upd_conv_take_nth_drop min_def UN_subset_iff
             dest: in_set_takeD in_set_dropD simp flip: id_take_nth_drop)
  then show False using assms(1)
    by (auto simp: NF_def)
qed

lemma all_ctxt_closed_srstep_conversions [simp]:
  "all_ctxt_closed ℱ ((srstep ℱ ℛ)⇧↔⇧*)"
  by (simp add: all_ctxt_closed_sig_rsteps sig_step_conversion_dist)

(* END AUX *)

lemma NFP_stepD:
  "NFP r ⟹ (a, b) ∈ r⇧* ⟹ (a, c) ∈ r⇧* ⟹ c ∈ NF r ⟹ (b, c) ∈ r⇧*"
  by (auto simp: NFP_on_def)
  
lemma NE_symmetric: "NE r s ⟹ NE s r"
  unfolding NE_on_def by auto

lemma CE_symmetric: "CE r s ⟹ CE s r"
  unfolding CE_on_def by auto

text ‹Reducing the quantification over rewrite sequences for properties @{const CR} ... to
rewrite sequences containing at least one root step›
lemma all_ctxt_closed_relcomp [intro]:
  "(⋀ s t. (s, t) ∈ ℛ ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ) ⟹
   (⋀ s t. (s, t) ∈ 𝒮 ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ) ⟹
   all_ctxt_closed ℱ ℛ ⟹ all_ctxt_closed ℱ 𝒮 ⟹ all_ctxt_closed ℱ (ℛ O 𝒮)"
proof -
  assume funas:"(⋀ s t. (s, t) ∈ ℛ ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ)"
    "(⋀ s t. (s, t) ∈ 𝒮 ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ)"
    and ctxt_cl: "all_ctxt_closed ℱ ℛ" "all_ctxt_closed ℱ 𝒮"
  {fix f ss ts assume ass: "(f, length ss) ∈ ℱ" "length ss = length ts" "⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ (ℛ O 𝒮)"
    "⋀ i . i < length ts ⟹ funas_term (ts ! i) ⊆ ℱ" "⋀i. i < length ts ⟹ funas_term (ss ! i) ⊆ ℱ"
    from ass(2, 3) obtain us where us: "length us = length ts" "⋀ i. i < length ts ⟹ (ss ! i, us ! i) ∈ ℛ"
      "⋀ i. i < length ts ⟹ (us ! i, ts ! i) ∈ 𝒮"
      using Ex_list_of_length_P[of "length ts" "λ x i. (ss ! i, x) ∈ ℛ ∧ (x, ts ! i) ∈ 𝒮"]
      by auto
    from funas have fu: "⋀ i . i < length us ⟹ funas_term (us ! i) ⊆ ℱ" using us ass(4, 5)
      by auto (metis in_mono)
    have "(Fun f ss, Fun f us) ∈ ℛ" using ass(1, 2, 5) us(1, 2) fu
      by (intro all_ctxt_closedD[OF ctxt_cl(1), of f]) auto
    moreover have "(Fun f us, Fun f ts) ∈ 𝒮"  using ass(1, 2, 4) us(1, 3) fu
      by (intro all_ctxt_closedD[OF ctxt_cl(2), of f]) auto
    ultimately have "(Fun f ss, Fun f ts) ∈ ℛ O 𝒮" by auto}
  moreover
  {fix x have "(Var x, Var x) ∈ ℛ" "(Var x, Var x) ∈ 𝒮" using ctxt_cl
      by (auto simp: all_ctxt_closed_def)
    then have "(Var x, Var x) ∈ ℛ O 𝒮" by auto}
  ultimately show ?thesis by (auto simp: all_ctxt_closed_def)
qed


abbreviation "prop_to_rel P ≡ {(s, t)| s t. P s t}"

abbreviation "prop_mctxt_cl ℱ P ≡ all_ctxt_closed ℱ (prop_to_rel P)"

lemma prop_mctxt_cl_Var:
  "prop_mctxt_cl ℱ P ⟹ P (Var x) (Var x)"
  by (simp add: all_ctxt_closed_def)

lemma prop_mctxt_cl_refl_on:
  "prop_mctxt_cl ℱ P ⟹ funas_term t ⊆ ℱ ⟹ P t t"
  using all_ctxt_closed_sig_reflE by blast

lemma prop_mctxt_cl_reflcl_on:
  "prop_mctxt_cl ℱ P ⟹ funas_term s ⊆ ℱ ⟹ P s s"
  using all_ctxt_closed_sig_reflE by blast

lemma reduction_relations_to_root_step:
  assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ P s t"
    and cl: "prop_mctxt_cl ℱ P"
    and well: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
    and steps: "(s, t) ∈ (srstep ℱ ℛ)⇧*"
  shows "P s t" using steps well
proof (induct s arbitrary: t)
  case (Var x)
  have "(Var x, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (Var x, t) ∈ srsteps_with_root_step ℱ ℛ"
    using nsrsteps_with_root_step_step_on_args by blast
  from assms(1)[OF this] show ?case using Var cl
    by (auto simp: rtrancl_eq_or_trancl dest: all_ctxt_closed_sig_reflE)
next
  case (Fun f ss) note IH = this show ?case
  proof (cases "Fun f ss = t")
    case True show ?thesis using IH(2, 4) unfolding True
      by (intro prop_mctxt_cl_reflcl_on[OF cl]) auto      
  next
    case False
    then have step: "(Fun f ss, t) ∈ (srstep ℱ ℛ)⇧+" using IH(2)
      by (auto simp: refl rtrancl_eq_or_trancl)
    show ?thesis
    proof (cases "(Fun f ss, t) ∈ srsteps_with_root_step ℱ ℛ")
      case False
      from nsrsteps_with_root_step_step_on_args[OF step this] obtain ts
        where *[simp]: "t = Fun f ts" and inv: "length ss = length ts"
          "∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*"
        by auto
      have funas: "(f, length ts) ∈ ℱ" "∀i<length ts. funas_term (ss ! i) ⊆ ℱ ∧ funas_term (ts ! i) ⊆ ℱ"
        using IH(3, 4) step inv(1) by (auto simp: UN_subset_iff)
      then have t: "∀ i < length ts. P (ss ! i) (ts ! i)"
        using prop_mctxt_cl_reflcl_on[OF cl]  IH(1) inv
        by (auto simp: rtrancl_eq_or_trancl)
      then show ?thesis unfolding * using funas inv(1) all_ctxt_closedD[OF cl]
        by auto
    qed (auto simp add: assms(1))
  qed
qed



abbreviation "comp_rrstep_rel ℱ ℛ 𝒮 ≡ srsteps_with_root_step ℱ ℛ O (srstep ℱ 𝒮)⇧* ∪
  (srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ 𝒮"

abbreviation "comp_rrstep_rel' ℱ ℛ 𝒮 ≡ srsteps_with_root_step ℱ ℛ O (srstep ℱ 𝒮)⇧+ ∪
  (srstep ℱ ℛ)⇧+ O srsteps_with_root_step ℱ 𝒮"

lemma reduction_join_relations_to_root_step:
  assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮 ⟹ P s t"
    and cl: "prop_mctxt_cl ℱ P"
    and well: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
    and steps: "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
  shows "P s t" using steps well
proof (induct s arbitrary: t)
  case (Var x)
  have f: "(Var x, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮"
    using nsrsteps_with_root_step_step_on_args[of "Var x" _ ℱ ℛ] unfolding srsteps_with_root_step_def
    by (metis (no_types, lifting) Term.term.simps(4) UnI1 relcomp.relcompI rtrancl_eq_or_trancl)
  have s: "(Var x, t) ∈ (srstep ℱ 𝒮)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮"
    using nsrsteps_with_root_step_step_on_args[of "Var x" _ ℱ 𝒮] unfolding srsteps_with_root_step_def
    by (metis (no_types, lifting) Term.term.simps(4) UnI2 relcomp.simps rtrancl.simps)
  have t: "(Var x, u) ∈ (srstep ℱ ℛ)⇧+ ⟹ (u, t) ∈ (srstep ℱ 𝒮)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" for u
    using nsrsteps_with_root_step_step_on_args[of "Var x" u ℱ ℛ] unfolding srsteps_with_root_step_def
    by auto (meson relcomp.simps trancl_into_rtrancl)
  show ?case using Var f[THEN assms(1)] s[THEN assms(1)] t[THEN assms(1)] cl
    by (auto simp: rtrancl_eq_or_trancl prop_mctxt_cl_Var)
next
  case (Fun f ss) note IH = this show ?case
  proof (cases "Fun f ss = t")
    case True show ?thesis using IH(2, 3, 4) cl
      by (auto simp: True prop_mctxt_cl_refl_on)
  next
    case False
    obtain u where u: "(Fun f ss, u) ∈ (srstep ℱ ℛ)⇧*" "(u, t) ∈ (srstep ℱ 𝒮)⇧*" using IH(2) by auto
    show ?thesis
    proof (cases "(Fun f ss, u) ∈ srsteps_with_root_step ℱ ℛ")
      case True
      then have "(Fun f ss, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" using u
        by (auto simp: srsteps_with_root_step_def)
      from assms(1)[OF this] show ?thesis by simp
    next
      case False note nt_fst = this show ?thesis
      proof (cases "(u, t) ∈ srsteps_with_root_step ℱ 𝒮")
        case True
        then have "(Fun f ss, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" using u unfolding srsteps_with_root_step_def
          by blast
        from assms(1)[OF this] show ?thesis by simp
      next
        case False note no_root = False nt_fst
        show ?thesis
        proof (cases "Fun f ss = u ∨ u = t")
          case True
          from assms(1) have f: "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ P s t"
            and s: "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ P s t" unfolding srsteps_with_root_step_def
            by blast+
          have "u = t ⟹ ?thesis" using u cl IH(3, 4)
            by (intro reduction_relations_to_root_step[OF f]) auto
          moreover have "Fun f ss = u ⟹ ?thesis" using u cl IH(3, 4)
            by (intro reduction_relations_to_root_step[OF s]) auto
          ultimately show ?thesis using True by auto
        next
          case False
          then have steps: "(Fun f ss, u) ∈ (srstep ℱ ℛ)⇧+" "(u, t) ∈ (srstep ℱ 𝒮)⇧+" using u
            by (auto simp: rtrancl_eq_or_trancl)
          obtain ts us
            where [simp]: "u = Fun f us" and inv_u: "length ss = length us" "∀ i < length ts. (ss ! i, us ! i) ∈ (srstep ℱ ℛ)⇧*"
              and [simp]: "t = Fun f ts" and inv_t: "length us = length ts" "∀ i < length ts. (us ! i, ts ! i) ∈ (srstep ℱ 𝒮)⇧*"
            using nsrsteps_with_root_step_step_on_args[OF steps(1) no_root(2)]
            using nsrsteps_with_root_step_step_on_args[OF steps(2) no_root(1)]
            by auto
          from inv_u inv_t cl IH(3, 4) have t: "∀ i < length ts. P (ss ! i) (ts ! i)"
            by (auto simp: UN_subset_iff intro!: IH(1)[OF nth_mem, of i "ts ! i" for i])
          moreover have "(f, length ts) ∈ ℱ" using IH(4) by auto 
          ultimately show ?thesis using IH(3, 4) inv_u inv_t all_ctxt_closedD[OF cl]
            by (auto simp: UN_subset_iff)
        qed
      qed
    qed
  qed
qed

― ‹Reducing search space for @{const commute} to conversions involving root steps›

definition "commute_redp ℱ ℛ 𝒮 s t ⟷ (s, t) ∈ ((srstep ℱ 𝒮)⇧* O ((srstep ℱ ℛ)¯)⇧*)"

declare subsetI[rule del]
lemma commute_redp_mctxt_cl:
  "prop_mctxt_cl ℱ (commute_redp ℱ ℛ 𝒮)"
  unfolding commute_redp_def rew_converse_inwards 
  by (auto dest: sigstep_trancl_funas)
declare subsetI[intro!]

lemma commute_rrstep_intro:
  assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t"
  shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
  have [simp]: "x ∈ srsteps_with_root_step ℱ 𝒰 ⟹ x ∈ (srstep ℱ 𝒰)⇧* O ℒ⇧*" for x 𝒰 ℒ
    by (cases x) (auto dest!: srsteps_with_root_step_sresteps_eqD)
  have [simp]: "x ∈ srsteps_with_root_step ℱ 𝒰 ⟹ x ∈ ℒ⇧* O (srstep ℱ 𝒰)⇧*" for x 𝒰 ℒ
    by (cases x) (auto dest!: srsteps_with_root_step_sresteps_eqD)
  have red: "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t" using assms
    unfolding commute_redp_def srstep_converse_dist 
    by (auto simp: rtrancl_eq_or_trancl)  blast+
  have comI: "(⋀ s t. (s, t) ∈ ((srstep ℱ (ℛ¯))⇧*) O (srstep ℱ 𝒮)⇧* ⟹ commute_redp ℱ ℛ 𝒮 s t) ⟹
    commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
    by (auto simp: commute_redp_def commute_def subsetD rew_converse_inwards)
  show ?thesis
    using reduction_join_relations_to_root_step[OF red commute_redp_mctxt_cl, of "ℛ¯" 𝒮]
    by (intro comI, auto) (metis (no_types, lifting) commute_redp_def relcompI rew_converse_inwards sigstep_trancl_funas srstep_converse_dist)
qed

lemma commute_to_rrstep:
  assumes "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t" using assms
  unfolding commute_def commute_redp_def srstep_converse_dist
  by (auto simp: srstep_converse_dist dest: srsteps_with_root_step_sresteps_eqD)

― ‹Reducing search space for @{const CR} to conversions involving root steps›

lemma CR_Aux:
  assumes "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
  shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
proof -
  have sym: "commute_redp ℱ ℛ ℛ s t ⟹ commute_redp ℱ ℛ ℛ t s" for s t
    by (auto simp: commute_redp_def) (metis converseI relcomp.relcompI rtrancl_converse rtrancl_converseD)
  {fix s t assume "(s, t) ∈ (srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ (ℛ¯)"
    then have "commute_redp ℱ ℛ ℛ s t"  unfolding commute_redp_def
      by (auto simp: srsteps_with_root_step_def rew_converse_inwards dest!: srrstep_to_srestep)}
  note * = this
  {fix s t assume ass: "(s, t) ∈ srsteps_with_root_step ℱ (ℛ¯) O (srstep ℱ ℛ)⇧*"
    have [dest!]: "(u, t) ∈ (srstep ℱ ℛ)⇧* ⟹ (t, u) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧*" for u
      by (metis rew_converse_outwards rtrancl_converseI srstep_converse_dist)
    from ass have "(t, s) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ"
      unfolding srsteps_with_root_step_def rstep_converse_dist
      by (metis (mono_tags, lifting) O_assoc converse.simps converse_converse converse_inward(1) converse_relcomp rew_converse_outwards(1, 2) sig_step_converse_rstep)
  from assms[OF this] have "commute_redp ℱ ℛ ℛ s t" using sym by blast}
  then show "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t" unfolding srsteps_with_root_step_def
    by (metis UnE assms srsteps_with_root_step_def)
qed

lemma CR_rrstep_intro:
  assumes "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ¯))⇧+ O srsteps_with_root_step ℱ ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
  shows "CR (srstep ℱ ℛ)"
proof -
  {fix s u assume "(s, u) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ"
    then obtain t where a: "(s, t) ∈ (srstep ℱ (ℛ¯))⇧*" "(t, u) ∈ srsteps_with_root_step ℱ ℛ" by blast
    have "commute_redp ℱ ℛ ℛ s u"
    proof (cases "s = t")
      case [simp]: True
      from srsteps_with_root_step_srstepsD[OF a(2)] show ?thesis
        by (auto simp: commute_redp_def)
    next
      case False
      then have "(s, t) ∈ (srstep ℱ (ℛ¯))⇧+" using a(1) unfolding rtrancl_eq_or_trancl
        by simp
      then show ?thesis using assms a(2) by blast
    qed}
  from commute_rrstep_intro[OF CR_Aux[OF this]]
  show ?thesis unfolding CR_iff_self_commute
    by (metis Un_iff reflcl_trancl relcomp_distrib relcomp_distrib2)
qed

lemma CR_to_rrstep:
  assumes "CR (srstep ℱ ℛ)"
  shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t" using assms
  using commute_to_rrstep[OF assms[unfolded CR_iff_self_commute]]
  by simp

― ‹Reducing search space for @{const NFP} to conversions involving root steps›

definition NFP_redp where
  "NFP_redp ℱ ℛ s t ⟷ t ∈ NF (srstep ℱ ℛ) ⟶ (s, t) ∈ (srstep ℱ ℛ)⇧*"

lemma prop_mctxt_cl_NFP_redp:
  "prop_mctxt_cl ℱ (NFP_redp ℱ ℛ)"
proof -
  {fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
      and steps: "∀ i < length ss. ss ! i ∈ NF (srstep ℱ ℛ) ⟶ (ts ! i, ss ! i) ∈ (srstep ℱ ℛ)⇧*"
      and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
      and NF: "Fun f ss ∈ NF (srstep ℱ ℛ)"
    from steps have steps:  "i < length ss ⟹ (ts ! i, ss ! i) ∈ (srstep ℱ ℛ)⇧*" for i
      using sig funas NF_srstep_args[OF NF]
      by (auto simp: UN_subset_iff) (metis in_set_idx)
    then have "(Fun f ts, Fun f ss) ∈ (srstep ℱ ℛ)⇧*" using sig
      by (metis all_ctxt_closed_def all_ctxt_closed_sig_rsteps funas le_sup_iff)}
  then show ?thesis
    by (auto simp: NFP_redp_def all_ctxt_closed_def)
qed

lemma NFP_rrstep_intro:
  assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ⟹ NFP_redp ℱ ℛ s t"
  shows "NFP (srstep ℱ ℛ)"
proof -
  from assms have red: "⋀ t u. (t, u) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ NFP_redp ℱ ℛ t u"
    apply (auto simp: NFP_redp_def rtrancl_eq_or_trancl)
    apply (metis NF_no_trancl_step converseD srstep_converse_dist srsteps_with_root_step_srstepsD trancl_converse)
    apply blast
    apply (meson NF_no_trancl_step srsteps_with_root_step_srstepsD)
    by blast
  have "⋀ s t. (s, t) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧* O (srstep ℱ ℛ)⇧* ⟹ NFP_redp ℱ ℛ s t"
    using reduction_join_relations_to_root_step[OF red prop_mctxt_cl_NFP_redp, of "ℛ¯" ℛ]
    by (auto simp: NFP_redp_def) (metis (no_types, lifting) relcomp.relcompI rstep_converse_dist rtranclD srstepsD)
  then show ?thesis unfolding NFP_on_def NFP_redp_def
    by (auto simp: normalizability_def) (metis meetI meet_def rstep_converse_dist srstep_converse_dist)
qed

lemma NFP_lift_to_conversion:
  assumes "NFP r" "(s, t) ∈ (r⇧↔)⇧*" and "t ∈ NF r"
  shows "(s, t) ∈ r⇧*" using assms(2, 3)
proof (induct rule: converse_rtrancl_induct)
  case (step s u)
  then have "(u, t) ∈ r⇧!" by auto
  then show ?case using assms(1) step(1) unfolding NFP_on_def
    by auto
qed simp

lemma NFP_to_rrstep:
  assumes "NFP (srstep ℱ ℛ)"
  shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ NFP_redp ℱ ℛ s t" using assms
  using NFP_lift_to_conversion[OF assms] unfolding NFP_redp_def srsteps_with_root_step_def
  by auto (metis (no_types, lifting) r_into_rtrancl rstep_converse_dist rtrancl_trans srrstep_to_srestep srstep_symcl_dist)


― ‹Reducing search space for @{const UNC} to conversions involving root steps›

definition "UN_redp ℱ ℛ s t ⟷ s ∈ NF (srstep ℱ ℛ) ∧ t ∈ NF (srstep ℱ ℛ) ⟶ s = t"

lemma prop_mctxt_cl_UN_redp:
  "prop_mctxt_cl ℱ (UN_redp ℱ ℛ)"
proof -
  {fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
      and steps: "∀ i < length ss. ts ! i ∈ NF (srstep ℱ ℛ) ∧ ss ! i ∈ NF (srstep ℱ ℛ) ⟶ ts ! i = ss ! i"
      and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
      and NF: "Fun f ts ∈ NF (srstep ℱ ℛ)" "Fun f ss ∈ NF (srstep ℱ ℛ)"
    from steps have steps: "i < length ss ⟹ ts ! i = ss ! i" for i
      using sig funas NF_srstep_args[OF NF(1)] NF_srstep_args[OF NF(2)]
      by (auto simp: UN_subset_iff) (metis in_set_idx)
    then have "Fun f ts = Fun f ss" using sig(2)
      by (simp add: nth_equalityI)}
  then show ?thesis
    by (auto simp: UN_redp_def all_ctxt_closed_def)
qed

lemma UNC_rrstep_intro:
  assumes"⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ UN_redp ℱ ℛ s t"
  shows "UNC (srstep ℱ ℛ)"
proof -
  have "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ⇧↔))⇧* ⟹ UN_redp ℱ ℛ s t"
    using reduction_relations_to_root_step[OF assms(1) prop_mctxt_cl_UN_redp, of "ℛ⇧↔"]
    by (auto simp: UN_redp_def) (meson rtranclD srstepsD)
  then show ?thesis unfolding UNC_def UN_redp_def
    by (auto simp: sig_step_conversion_dist)
qed

lemma UNC_to_rrstep:
  assumes "UNC (srstep ℱ ℛ)"
  shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ UN_redp ℱ ℛ s t"
  using assms unfolding UNC_def UN_redp_def srsteps_with_root_step_def
  by (auto dest!: srrstep_to_srestep symcl_srstep_conversion symcl_srsteps_conversion)
     (metis (no_types, opaque_lifting) conversion_def rtrancl_trans)


― ‹Reducing search space for @{const UNF} to conversions involving root steps›

lemma UNF_rrstep_intro:
  assumes "⋀ t u. (t, u) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ t u"
  shows "UNF (srstep ℱ ℛ)"
proof -
  from assms have red: "⋀ t u. (t, u) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ t u"
    apply (auto simp: UN_redp_def rtrancl_eq_or_trancl)
    apply (metis NF_no_trancl_step converseD srstep_converse_dist srsteps_with_root_step_srstepsD trancl_converse)
    apply blast
    apply (meson NF_no_trancl_step srsteps_with_root_step_srstepsD)
    by blast
  have "⋀ s t. (s, t) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧* O (srstep ℱ ℛ)⇧* ⟹ UN_redp ℱ ℛ s t"
    using reduction_join_relations_to_root_step[OF red prop_mctxt_cl_UN_redp, of "ℛ¯" ℛ]
    by (auto simp: UN_redp_def) (metis (no_types, lifting) relcomp.relcompI rstep_converse_dist rtranclD srstepsD)
  then show ?thesis unfolding UNF_on_def UN_redp_def
    by (auto simp: normalizability_def) (metis meetI meet_def rstep_converse_dist srstep_converse_dist)
qed

lemma UNF_to_rrstep:
  assumes "UNF (srstep ℱ ℛ)"
  shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ s t"
  using assms unfolding UNF_on_def UN_redp_def normalizability_def srsteps_with_root_step_def
  by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep)
   (metis (no_types, lifting) rstep_converse_dist rtrancl.rtrancl_into_rtrancl rtrancl_converseD rtrancl_idemp srstep_converse_dist)+

― ‹Reducing search space for @{const CE} to conversions involving root steps›

lemma CE_rrstep_intro:
  assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
    and "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (𝒮⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
  shows "CE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  using reduction_relations_to_root_step[OF assms(1), where ?s1 = "λ s t. s" and ?t1 = "λ s t. t", of ℱ "ℛ⇧↔"]
  using reduction_relations_to_root_step[OF assms(2), where ?s1 = "λ s t. s" and ?t1 = "λ s t. t", of ℱ "𝒮⇧↔"]
  by (auto simp: CE_on_def)
     (metis converseI conversion_converse rtrancl_eq_or_trancl sig_step_conversion_dist sigstep_trancl_funas(1, 2))+

lemma CE_to_rrstep:
  assumes "CE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
        "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (𝒮⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
  using assms unfolding CE_on_def srsteps_with_root_step_def
  by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep symcl_srsteps_conversion symcl_srstep_conversion)
     (metis converse_rtrancl_into_rtrancl conversion_rtrancl)+


― ‹Reducing search space for @{const NE} to conversions involving root steps›

definition NE_redp where
  "NE_redp ℱ ℛ 𝒮 s t ⟷ t ∈ NF (srstep ℱ ℛ) ⟶ t ∈ NF (srstep ℱ ℛ) ⟶ (s, t) ∈ (srstep ℱ 𝒮)⇧*"

lemma prop_mctxt_cl_NE_redp:
  "prop_mctxt_cl ℱ (NE_redp ℱ ℛ 𝒮)"
proof -
  {fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
      and steps: "∀ i < length ss. ss ! i ∈ NF (srstep ℱ ℛ) ⟶ (ts ! i, ss ! i) ∈ (srstep ℱ 𝒮)⇧*"
      and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
      and NF: "Fun f ss ∈ NF (srstep ℱ ℛ)"
    from steps have steps:  "i < length ss ⟹ (ts ! i, ss ! i) ∈ (srstep ℱ 𝒮)⇧*" for i
      using sig funas NF_srstep_args[OF NF]
      by (auto simp: UN_subset_iff) (metis in_set_idx)
    then have "(Fun f ts, Fun f ss) ∈ (srstep ℱ 𝒮)⇧*" using sig
      by (metis all_ctxt_closed_def all_ctxt_closed_sig_rsteps funas le_sup_iff)}
  then show ?thesis
    by (auto simp: all_ctxt_closed_def NE_redp_def)
qed
 
lemma NE_rrstep_intro:
  assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ NE_redp ℱ ℛ 𝒮 s t"
    and "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ NE_redp ℱ 𝒮 ℛ s t"
    and "NF (srstep ℱ ℛ) = NF (srstep ℱ 𝒮)"
  shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  using assms(3)
  using reduction_relations_to_root_step[OF assms(1) prop_mctxt_cl_NE_redp, of ℛ]
  using reduction_relations_to_root_step[OF assms(2) prop_mctxt_cl_NE_redp, of 𝒮]
  by (auto simp: NE_on_def NE_redp_def normalizability_def)
     (metis rtrancl.rtrancl_refl sigstep_trancl_funas)+


lemma NE_to_rrstep:
  assumes "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
  shows  "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ NE_redp ℱ ℛ 𝒮 s t"
         "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ NE_redp ℱ 𝒮 ℛ s t"
  using assms unfolding NE_on_def NE_redp_def srsteps_with_root_step_def
  by (auto simp: normalizability_def simp flip: srstep_converse_dist
     dest!: srrstep_to_srestep) (meson converse_rtrancl_into_rtrancl rtrancl_trans)+

lemma NE_NF_eq:
  "NE ℛ 𝒮 ⟹ NF ℛ = NF 𝒮"
  by (auto simp: NE_on_def NF_def normalizability_def)

― ‹Reducing search space for @{const SCR} and @{const WCR} involving root steps›
(*Brute forced proofs could be done nicer with more lemmas related to positions *)
 
abbreviation "SCRp ℱ ℛ t u ≡ ∃v. (t, v) ∈ (srstep ℱ ℛ)⇧= ∧ (u, v) ∈ (srstep ℱ ℛ)⇧*"
lemma SCR_rrstep_intro:
  assumes "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ SCRp ℱ ℛ t u"
    and "⋀ s t u. (s, t) ∈ srstep ℱ ℛ ⟹ (s, u) ∈ sig_step ℱ (rrstep ℛ) ⟹ SCRp ℱ ℛ t u"
  shows "SCR (srstep ℱ ℛ)"
proof -
  {fix s t u assume step: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
    from step(1) obtain p l r σ where st: "p ∈ poss s" "(l, r) ∈ ℛ" "s |_ p = l ⋅ σ" "t = s[p ← r ⋅ σ]"
      using rstep_to_pos_replace[of s t ℛ] unfolding sig_step_def by blast
    from step(2) obtain q l2 r2 σ2 where su: "q ∈ poss s" "(l2, r2) ∈ ℛ" "s |_ q = l2 ⋅ σ2" "u = s[q ← r2 ⋅ σ2]"
      using rstep_to_pos_replace[of s u ℛ] unfolding sig_step_def by blast
    from step st su have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
      by (auto dest: srstepD)
    have funas2 :"funas_term (r2 ⋅ σ2) ⊆ ℱ" using funas_term_replace_at_lower[OF su(1)]
      using funas(3) unfolding su(4) by blast
    consider (a) "p ≤⇩p q" | (b) "q ≤⇩p p" | (c) "p ⊥ q"
      unfolding Sublist.parallel_def by blast
    then have "SCRp ℱ ℛ t u"
    proof cases
      case a
      from a have up: "p ∈ poss u" using st(1) su(1) unfolding st(4) su(4)
        by (metis pos_replace_at_pres poss_append_poss prefix_pos_diff)
      let ?C = "ctxt_of_pos_term p s" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) st(1)
        by (metis ctxt_supt_id funas_term_ctxt_apply le_sup_iff)
      from funas have funas: "funas_term (s |_ p) ⊆ ℱ" "funas_term (t |_ p) ⊆ ℱ" "funas_term (u |_ p) ⊆ ℱ"
        using a st(1) pos_replace_at_pres[OF st(1)] up unfolding st(4) su(4)
        by (intro funas_term_subterm_atI, blast+)+
      have "(s |_ p, t |_ p) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis poss_of_termE poss_of_term_replace_term_at rrstepI sig_stepI st(4))
      moreover have "(s |_ p, u |_ p) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (smt (verit, del_insts) a less_eq_subt_at_replace pos_replace_to_rstep poss_append_poss prefix_pos_diff
            sig_stepI su(4) subt_at_append)
      ultimately obtain v where "(t |_ p, v) ∈ (srstep ℱ ℛ)⇧=" "(u |_ p, v) ∈ (srstep ℱ ℛ)⇧*"
        using assms(1) by blast
      from this(1) srsteps_eq_ctxt_closed[OF fc this(2)]
      show ?thesis using a st(1) su(1) srsteps_eq_ctxt_closed[OF fc] unfolding st(4) su(4)
        apply (intro exI[of _ "?C⟨v⟩"])
        apply (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
        apply (metis ctxt_of_pos_term_apply_replace_at_ident fc srstep_ctxt_closed)
        done
    next
      case b
      then have up: "q ∈ poss t" using st(1) su(1) unfolding st(4) su(4)
        by (metis pos_replace_at_pres poss_append_poss prefix_pos_diff)
      let ?C = "ctxt_of_pos_term q s" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) su(1)
        by (metis Un_subset_iff ctxt_supt_id funas_term_ctxt_apply)
      from funas have funas: "funas_term (s |_ q) ⊆ ℱ" "funas_term (t |_ q) ⊆ ℱ" "funas_term (u |_ q) ⊆ ℱ"
        using su(1) pos_replace_at_pres[OF su(1)] up unfolding st(4) su(4)
        by (intro funas_term_subterm_atI, blast+)+
      have "(s |_ q, t |_ q) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis b less_eq_subt_at_replace
            pos_replace_to_rstep[of "p -⇩p q" "s |_ q" l r ℛ σ "(s |_ q)[p -⇩p q ← r ⋅ σ]"]
            prefix_pos_diff sig_stepI st(4) subterm_poss_conv)
      moreover have "(s |_ q, u |_ q) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis poss_of_termE poss_of_term_replace_term_at rrstepI sig_stepI su(4))
      ultimately obtain v where "(t |_ q, v) ∈ (srstep ℱ ℛ)⇧=" "(u |_ q, v) ∈ (srstep ℱ ℛ)⇧*"
        using assms(2) by blast
      from this(1) srsteps_eq_ctxt_closed[OF fc this(2)]
      show ?thesis using b st(1) su(1) srsteps_eq_ctxt_closed[OF fc] unfolding st(4) su(4)
        apply (intro exI[of _ "?C⟨v⟩"])
        apply (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
        apply (smt (verit, best) ctxt_of_pos_term_apply_replace_at_ident fc less_eq_subt_at_replace replace_term_at_above replace_term_at_subt_at_id srstep_ctxt_closed)
        done
    next
      case c
      define v where "v = t[q ← r2 ⋅ σ2]"
      have funasv: "funas_term v ⊆ ℱ" using funas su(1) unfolding v_def su(4)
        using funas_term_replace_at_upper funas2 by blast
      from c have *: "v = u[p ← r ⋅ σ]" unfolding v_def st(4) su(4) using st(1) su(1)
        using parallel_replace_term_commute by blast
      from c have "(t, v) ∈ rstep ℛ" unfolding st(4) v_def
        using su(1 - 3) par_pos_replace_pres[OF su(1)]
        by (metis par_pos_replace_term_at pos_replace_to_rstep Sublist.parallel_def)
      moreover from c have "(u, v) ∈ rstep ℛ" unfolding su(4) *
        using st(1 - 3) par_pos_replace_pres[OF st(1)]
        by (intro pos_replace_to_rstep[of _ _ l]) (auto simp: par_pos_replace_term_at)
      ultimately show ?thesis using funas(2-) funasv
        by auto
    qed}
  then show ?thesis unfolding SCR_on_def
    by blast
qed

lemma SCE_to_rrstep:
  assumes "SCR (srstep ℱ ℛ)"
  shows "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ SCRp ℱ ℛ t u"
        "⋀ s t u. (s, t) ∈ srstep ℱ ℛ ⟹ (s, u) ∈ sig_step ℱ (rrstep ℛ) ⟹ SCRp ℱ ℛ t u"
  using assms unfolding SCR_on_def srsteps_with_root_step_def
  by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep symcl_srsteps_conversion symcl_srstep_conversion)

lemma WCR_rrstep_intro:
  assumes "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ (t, u) ∈ (srstep ℱ ℛ)⇧↓"
  shows "WCR (srstep ℱ ℛ)"
proof -
  {fix s t u assume step: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
    from step(1) obtain p l r σ where st: "p ∈ poss s" "(l, r) ∈ ℛ" "s |_ p = l ⋅ σ" "t = s[p ← r ⋅ σ]"
      using rstep_to_pos_replace[of s t ℛ] unfolding sig_step_def by blast
    from step(2) obtain q l2 r2 σ2 where su: "q ∈ poss s" "(l2, r2) ∈ ℛ" "s |_ q = l2 ⋅ σ2" "u = s[q ← r2 ⋅ σ2]"
      using rstep_to_pos_replace[of s u ℛ] unfolding sig_step_def by blast
    from step st su have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
      by (auto dest: srstepD)
    have funas2 :"funas_term (r2 ⋅ σ2) ⊆ ℱ" using funas_term_replace_at_lower[OF su(1)]
      using funas(3) unfolding su(4) by blast
    consider (a) "p ≤⇩p q" | (b) "q ≤⇩p p" | (c) "p ⊥ q"
      unfolding Sublist.parallel_def by blast
    then have "(t, u) ∈ (srstep ℱ ℛ)⇧↓"
    proof cases
      case a
      then have up: "p ∈ poss u" using st(1) su(1) unfolding st(4) su(4)
        by (metis pos_replace_at_pres poss_append_poss prefix_pos_diff)
      let ?C = "ctxt_of_pos_term p s" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) st(1)
        by (metis ctxt_of_pos_term_apply_replace_at_ident funas(2) funas_term_ctxt_apply le_sup_iff st(4))
      from funas have funas: "funas_term (s |_ p) ⊆ ℱ" "funas_term (t |_ p) ⊆ ℱ" "funas_term (u |_ p) ⊆ ℱ"
        using a st(1) pos_replace_at_pres[OF st(1)] up unfolding st(4) su(4)
        by (intro funas_term_subterm_atI, blast+)+
      have "(s |_ p, t |_ p) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis poss_of_termE poss_of_term_replace_term_at rrstepI sig_stepI st(4))
      moreover have "(s |_ p, u |_ p) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis a less_eq_subt_at_replace
            pos_replace_to_rstep[of "q -⇩p p" "s |_ p" l2 r2 ℛ σ2 "(s |_ p)[q -⇩p p ← r2 ⋅ σ2]"]
            prefix_pos_diff sig_stepI su(4) subterm_poss_conv)
      ultimately have "(t |_ p, u |_ p) ∈ (srstep ℱ ℛ)⇧↓"
        using assms(1) by blast
      from sig_steps_join_ctxt_closed[OF fc this(1)]
      show ?thesis using a st(1) su(1) srstep_ctxt_closed[OF fc] unfolding st(4) su(4)
        by (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
    next
      case b
      then have up: "q ∈ poss t" using st(1) su(1) unfolding st(4) su(4)
        by (metis replace_term_at_above replace_term_at_not_poss replace_term_at_subt_at_id)
      let ?C = "ctxt_of_pos_term q s" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) su(1)
        by (metis Un_subset_iff ctxt_supt_id funas_term_ctxt_apply)
      from funas have funas: "funas_term (s |_ q) ⊆ ℱ" "funas_term (t |_ q) ⊆ ℱ" "funas_term (u |_ q) ⊆ ℱ"
        using su(1) pos_replace_at_pres[OF su(1)] up unfolding st(4) su(4)
        by (intro funas_term_subterm_atI, blast+)+
      have "(s |_ q, t |_ q) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis b less_eq_subt_at_replace
            pos_replace_to_rstep[of "p -⇩p q" "s |_ q" l r ℛ σ "(s |_ q)[p -⇩p q ← r ⋅ σ]"]
            prefix_pos_diff sig_stepI st(4) subterm_poss_conv)
      moreover have "(s |_ q, u |_ q) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
        by (metis poss_of_termE poss_of_term_replace_term_at rrstepI sig_stepI su(4))
      ultimately have "(t |_ q, u |_ q) ∈ (srstep ℱ ℛ)⇧↓"
        using assms(1) by blast
      from sig_steps_join_ctxt_closed[OF fc this(1)]
      show ?thesis using b st(1) su(1) srstep_ctxt_closed[OF fc] unfolding st(4) su(4)
        by (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
    next
      case c
      define v where "v = t[q ← r2 ⋅ σ2]"
      have funasv: "funas_term v ⊆ ℱ" using funas su(1) unfolding v_def su(4)
        using funas_term_replace_at_upper funas2 by blast
      from c have *: "v = u[p ← r ⋅ σ]" unfolding v_def st(4) su(4) using st(1) su(1)
        using parallel_replace_term_commute by blast
      from c have "(t, v) ∈ rstep ℛ" unfolding st(4) v_def
        using su(1 - 3) par_pos_replace_pres[OF su(1)]
        by (metis par_pos_replace_term_at pos_replace_to_rstep Sublist.parallel_def)
      moreover from c have "(u, v) ∈ rstep ℛ" unfolding su(4) *
        using st(1 - 3) par_pos_replace_pres[OF st(1)]
        by (metis par_pos_replace_term_at pos_replace_to_rstep)
      ultimately show ?thesis using funas(2-) funasv
        by auto
    qed}
  then show ?thesis unfolding WCR_on_def
    by blast
qed

end