Theory LS_Currying2

(*
Author:  Franziska Rapp <franziska.rapp@uibk.ac.at> (2015-2017)
Author:  Bertram Felgenhauer <bertram.felgenhauer@uibk.ac.at> (2015-2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Reflection of confluence by currying›

theory LS_Currying2
  imports LS_Currying
begin

context pp_cr
begin

lemma missing_persists_Cu [simp]:
  assumes "is_Fun l"
  shows "missing_args (mctxt_of_term ((Cu l) ⋅ σ)) n = missing_args (mctxt_of_term (l ⋅ σ)) n"
using assms
proof (induction l arbitrary: n)
  case (Fun f ts)
  { fix x
    assume asm: "x ∈ set ts"
    have "missing_args (mctxt_of_term (x ⋅ σ)) n' =
          missing_args (mctxt_of_term ((Cu x) ⋅ σ)) n'" for n'
      using Fun(1)[OF asm, of n'] by (cases x) simp+
  } note inner = this
  thus ?case
  proof (cases "f = Ap")
    case isAp: True
    thus ?thesis using inner isAp by simp
  next
    case notAp: False
    hence "Suc (arity f) - length (map mctxt_of_term ts) - n =
           missing_args (mctxt_of_term (Cu (Fun f ts) ⋅ σ)) n"
      using inner
    proof (induction "length ts" arbitrary: n ts)
      case (Suc n')
      then obtain ts' a where ts_def: "ts = ts' @ [a]"
        by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
      have "Suc (arity f) - Suc (length (map mctxt_of_term ts')) - n =
             missing_args (mctxt_of_term (Cu (Fun f ts') ⋅ σ)) (Suc n)"
        using Suc(1)[OF _ Suc(3), of ts' "Suc n"] Suc(2,4)
        unfolding ts_def by simp
      then show ?case using Suc(2-) unfolding ts_def by simp
    qed simp
    thus ?thesis using notAp by force
  qed
qed simp

lemma check_persists_Cu [simp]:
  assumes "is_Fun l"
  shows "check_first_non_Ap n ((Cu l) ⋅ σ) = check_first_non_Ap n (l ⋅ σ)"
using missing_args_unfold missing_persists_Cu[OF assms] by metis

lemma ℱ_in_𝔏⇩1:
  assumes "funas_term t ⊆ ℱ⇩U - { (Ap, 2) }"
  shows "𝔏⇩1 (mctxt_of_term t)"
using assms
proof (induction t)
  case (Fun f ts)
  moreover have "x ∈ set ts ⟶ 𝔏⇩1 (mctxt_of_term x)" for x using Fun by auto
  ultimately show ?case using Fun(2) 𝔏⇩1.simps[of "MFun f (map mctxt_of_term ts)"] by simp
qed auto

lemma Cu_ℱ_𝔏⇩1:
  assumes "funas_term t ⊆ ℱ⇩U - { (Ap, 2) }"
  shows "𝔏⇩1 (mctxt_of_term (Cu t))"
proof -
  have "𝔏⇩1 (mctxt_of_term t)" using ℱ_in_𝔏⇩1[OF assms] .
  thus ?thesis using assms
  proof (induction t)
    case (Fun f ts) thus ?case
    proof (induction "length ts" arbitrary: ts)
      case (Suc n)
      then obtain ts' a where ts_def: "ts = ts' @ [a]"
        by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
      have arity_f: "length ts ≤ arity f"
        using Suc(5) unfolding ℱ⇩U_def arity_def by fastforce
      have "f ≠ Ap" using Suc(5) fresh unfolding ℱ⇩U_def by fastforce
      have f_ts': "(f, length ts') ∈ ℱ⇩U - {(Ap, 2)}"
        using ℱ⇩U_def ℱ_def Suc(5) fresh unfolding ts_def by force
      have "x ∈ set ts ⟶ 𝔏⇩1 (mctxt_of_term x)" for x
        using Suc(4) 𝔏_def in_set_idx sub_layers by fastforce
      hence "x ∈ set ts' ⟶ 𝔏⇩1 (mctxt_of_term x)" for x unfolding ts_def by simp
      hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Fun f ts'))"
        using Suc(4) f_ts' unfolding ts_def mctxt_of_term.simps by fastforce
      have funas: "funas_term (Fun f ts') ⊆ ℱ⇩U - {(Ap, 2)}"
        using Suc(5) ‹f ≠ Ap› unfolding ts_def ℱ⇩U_def by auto
      have arg1: "𝔏⇩1 (mctxt_of_term (Cu (Fun f ts')))"
        using Suc(1)[OF _ _ in_𝔏⇩1 funas] Suc(2,3) unfolding ts_def by force
      have "check_first_non_Ap 1 (Fun f ts')"
        using arity_f ‹f ≠ Ap› unfolding ts_def by simp
      hence "check_first_non_Ap 1 (Cu (Fun f ts'))"
        using check_persists_Cu[of "Fun f ts'" 1 Var] by simp
      moreover have arg2: "𝔏⇩1 (mctxt_of_term (Cu a))"
        using Suc(3)[of a] Suc(5) ℱ_in_𝔏⇩1[of a] unfolding ts_def by auto
      ultimately show ?case using ‹f ≠ Ap› arg1
        unfolding ts_def missing_args_unfold[symmetric] by auto
    qed simp
  qed simp
qed

lemma Cu⇩R_NF_𝒰_ℛ_step:
  assumes "(Cu s, Cu t) ∈ rstep (Cu⇩R ℛ)" "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
  shows "(s, t) ∈ rstep ℛ"
proof -
  obtain C l r σ where s_def: "Cu s = C⟨l ⋅ σ⟩" and t_def: "Cu t = C⟨r ⋅ σ⟩" and
                      in_Cu⇩R: "(l, r) ∈ Cu⇩R ℛ"
    using assms(1) by fast
  then obtain l' r' where l_def: "l = Cu l'" and r_def: "r = Cu r'" and in_ℛ: "(l', r') ∈ ℛ"
    using Cu⇩R_def by auto
  obtain f ts' where l'_def: "l' = Fun f ts'" using in_ℛ wfR unfolding wf_trs_def
    by fastforce
  hence "f ≠ Ap" "arity f = length ts'" using in_ℛ sigR fresh
    unfolding arity_def funas_trs_def funas_rule_def by fastforce+
  moreover obtain ts where lσ_def: "l' ⋅ σ = Fun f ts" "length ts = length ts'"
    using l'_def by auto
  ultimately have "¬ check_first_non_Ap 1 (l' ⋅ σ)" by auto
  hence check_lσ: "¬ check_first_non_Ap 1 (l ⋅ σ)"
    using check_persists_Cu[of l' 1 σ] unfolding l_def by fastforce
  have Cu_s_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Cu s))"
    using Cu_ℱ_𝔏⇩1[of s] assms(2) fresh unfolding ℱ_def ℱ⇩U_def by auto
  { fix C' f' ss2
    assume "C = C' ∘⇩c More f' [] □ ss2"
    hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Fun f' ([] @ l ⋅ σ # ss2)))"
      using Cu_s_𝔏⇩1 subm_at_layers[of "mctxt_of_term (Cu s)" "hole_pos C'"] unfolding s_def 𝔏_def
      by simp (metis hole_pos_poss list.simps(9) mctxt_of_term.simps(2)
         subm_at.simps(1) subm_at_mctxt_of_term subt_at_hole_pos)
    have "f' ≠ Ap" using 𝔏⇩1.cases[OF in_𝔏⇩1] check_lσ fresh
      unfolding missing_args_unfold[symmetric] ℱ⇩U_def by simp ((cases "f' = Ap"), fastforce)
  }
  hence no_Ap_above: "∀C' f ss2. C = C' ∘⇩c More f [] □ ss2 ⟶ f ≠ Ap"
    by blast
  obtain D where "NF_𝒰 (Cu s) = D⟨NF_𝒰 (l ⋅ σ)⟩ ∧ NF_𝒰 (Cu t) = D⟨NF_𝒰 (r ⋅ σ)⟩"
    using NF_𝒰_persists[OF no_Ap_above]
    unfolding s_def t_def by blast
  moreover have "funas_term l' ⊆ ℱ" "funas_term r' ⊆ ℱ" using in_ℛ sigR ℱ_def
    unfolding funas_trs_def funas_rule_def by fastforce+
  ultimately have s_def: "s = D⟨l' ⋅ (NF_𝒰 ∘ σ)⟩" and NF_𝒰_t_def: "t = D⟨r' ⋅ (NF_𝒰 ∘ σ)⟩"
    using NF_𝒰_Cu_subst[of _ σ] NF_𝒰_Cu assms(2,3) unfolding l_def r_def by auto
  moreover have "(s, t) ∈ rstep ℛ" unfolding s_def NF_𝒰_t_def using in_ℛ by blast
  ultimately show ?thesis by blast
qed

inductive is_Cu' :: "('f, 'v) term ⇒ nat ⇒ bool" where
  var  [intro]: "is_Cu' (Var x) 0"
| funs [intro]: "sigF f = Some n ⟹ is_Cu' (Fun f []) n"
| ap   [intro]: "is_Cu' t⇩1 (Suc n) ⟹ is_Cu' t⇩2 0 ⟹ is_Cu' (Fun Ap [t⇩1, t⇩2]) n"

abbreviation is_Cu where "is_Cu t ≡ is_Cu' t 0"

lemma is_Cu_intro:
  assumes "funas_term t ⊆ ℱ"
  shows "is_Cu (Cu t)"
using assms
proof (induction t)
  case (Fun f ts)
  hence props: "Some (length ts) = sigF f" "∀t'∈set ts. funas_term t' ⊆ ℱ"
    using ℱ_def by auto
  hence "f ≠ Ap" using fresh by force
  { fix m
    assume "Some (length ts + m) = sigF f"
    moreover have "t' ∈ set ts ⟶ is_Cu (Cu t')" for t' using Fun by auto
    ultimately have "is_Cu' (Cu (Fun f ts)) m" using props(2)
    proof (induction "length ts" arbitrary: ts m)
      case (Suc n)
      then obtain ts' a where ts_def: "ts = ts' @ [a]"
        by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
      have "Cu (Fun f ts) = Fun Ap [Cu (Fun f ts'), Cu a]"
        using ‹f ≠ Ap› unfolding ts_def by simp
      have "is_Cu (Cu a)" using Suc(4) unfolding ts_def by auto
      moreover have "is_Cu' (Cu (Fun f ts')) (Suc m)"
        using Suc(1)[of ts' "Suc m"] Suc(2-) unfolding ts_def by auto
      ultimately show ?case using ‹f ≠ Ap› unfolding ts_def by auto
    qed auto
  }
  thus ?case using props(1) by fastforce
qed auto

lemma is_Cu_elim':
  assumes "is_Cu' t n"
  shows "(∃f ts. Some (length ts + n) = sigF f ∧
         (∀t' ∈ set ts. funas_term t' ⊆ ℱ) ∧ t = Cu (Fun f ts))
          ∨ n = 0 ∧ (∃x. t = Var x)"
using assms
proof (induction t n rule: is_Cu'.induct)
  case (funs f m)
  hence "Some (length [] + m) = sigF f ∧ (∀t'∈set []. funas_term t' ⊆ ℱ) ∧
         Fun f [] = Cu (Fun f [])" using arity_def by simp
  thus ?case by blast
next
  case (ap t⇩1 n t⇩2)
  then obtain f ts' where inner: "Some (length ts' + Suc n) = sigF f ∧
       (∀t' ∈ set ts'. funas_term t' ⊆ ℱ) ∧ t⇩1 = Cu (Fun f ts')" by blast
  hence "f ≠ Ap" using fresh by force
  obtain g ss where t⇩2'_props: "Some (length ss) = sigF g ∧
       (∀t'∈set ss. funas_term t' ⊆ ℱ) ∧ t⇩2 = Cu (Fun g ss) ∨ (∃x. t⇩2 = Var x)"
    using ap(4) by auto
  thus ?case
  proof (elim disjE)
    assume t⇩2_props: "Some (length ss) = sigF g ∧
                     (∀t'∈set ss. funas_term t' ⊆ ℱ) ∧ t⇩2 = Cu (Fun g ss)"
    let ?ts = "ts' @ [Fun g ss]"
    have "Some (length ?ts + n) = sigF f ∧
         (∀t' ∈ set ?ts. funas_term t' ⊆ ℱ) ∧ Fun Ap [t⇩1, t⇩2] = Cu (Fun f ?ts)"
      using inner t⇩2_props ‹f ≠ Ap› ℱ_def by auto
    thus ?thesis by blast
  next
    assume "∃x. t⇩2 = Var x"
    then obtain x where t⇩2_def: "t⇩2 = Var x" by blast
    let ?ts = "ts' @ [Var x]"
    have "Some (length ?ts + n) = sigF f ∧
         (∀t' ∈ set ?ts. funas_term t' ⊆ ℱ) ∧ Fun Ap [t⇩1, t⇩2] = Cu (Fun f ?ts)"
      using inner t⇩2_def ‹f ≠ Ap› by auto
    thus ?thesis by blast
  qed
qed blast

lemma is_Cu_elim:
  assumes "is_Cu' t 0"
  shows "∃t'. funas_term t' ⊆ ℱ ∧ t = Cu t'"
proof (cases t)
  case (Var x)
  thus ?thesis by (auto intro: exI[of _ "Var x"])
next
  case (Fun f ts)
  then obtain f' ts' where props: "Some (length ts' + 0) = sigF f' ∧
        (∀t'∈set ts'. funas_term t' ⊆ ℱ) ∧ t = Cu (Fun f' ts')"
    using is_Cu_elim'[OF assms] by blast
  hence "funas_term (Fun f' ts') ⊆ ℱ ∧ t = Cu (Fun f' ts')" unfolding ℱ_def by auto
  thus ?thesis by blast
qed

lemma Cu'_subst_Cu':
  assumes "is_Cu' t n" "∀x. x ∈ vars_term t ⟶ is_Cu (Var x ⋅ σ)"
  shows "is_Cu' (t ⋅ σ) n"
using assms by (induction rule: is_Cu'.induct) auto

lemma Cu_subst_Cu:
  assumes "is_Cu t" "∀x. x ∈ vars_term t ⟶ is_Cu (Var x ⋅ σ)"
  shows "is_Cu (t ⋅ σ)"
using assms Cu'_subst_Cu' by blast

lemma is_Cu'_unique:
  assumes "is_Cu' t n" "is_Cu' t m"
  shows "n = m"
using assms
by (induction t n arbitrary: m rule: is_Cu'.induct) (force elim: is_Cu'.cases)+

lemma replace_in_Cu:
  assumes "is_Cu' C⟨s'⟩ n" "is_Cu s'" "is_Cu t'"
  shows "is_Cu' C⟨t'⟩ n"
using assms
proof (induction C arbitrary: n)
  case Hole
  hence "n = 0" using is_Cu'_unique by force
  thus ?case using Hole by simp
next
  case (More f ss1 C' ss2)
  hence "f = Ap" by (auto elim: is_Cu'.cases)
  consider "∃a. ss1 = [] ∧ ss2 = [a]" | "∃a. ss2 = [] ∧ ss1 = [a]"
    using More(2) by (cases ss1; cases ss2) (auto elim: is_Cu'.cases)
  thus ?case
  proof cases
    case 1
    thus ?thesis using More by (auto elim: is_Cu'.cases)
  next
    case 2
    then obtain a where lists: "ss2 = [] ∧ ss1 = [a]" by blast
    hence "is_Cu' a (Suc n)" "is_Cu C'⟨t'⟩" using More by (auto elim: is_Cu'.cases)
    thus ?thesis using lists ‹f = Ap› by auto
  qed
qed

(*suggested by Aart*)
lemma vars_term_subst_Cu:
  assumes "is_Cu' t n" "is_Cu' (t ⋅ σ) n"
  shows "∀x ∈ vars_term t. is_Cu (Var x ⋅ σ)"
using assms by (induction rule: is_Cu'.induct) (auto elim: is_Cu'.cases)

lemma nothing_missing_lhs_Cu⇩R:
  assumes "r ∈ Cu⇩R ℛ"
  shows "missing_args (mctxt_of_term (fst r ⋅ σ)) 0 = 1"
proof -
  obtain l' r' where lhs_rhs_def: "fst r = Cu l'" "snd r = Cu r'" "(l', r') ∈ ℛ"
    using assms(1) Cu⇩R_def by auto
  moreover have "is_Fun l'"
    using ‹(l', r') ∈ ℛ› wfR unfolding wf_trs_def by blast
  ultimately have "missing_args (mctxt_of_term (l' ⋅ σ)) 0 = 1"
    using nothing_missing_lhs_ℛ by force
  hence "missing_args (mctxt_of_term ((Cu l') ⋅ σ)) 0 = 1"
    using missing_persists_Cu[of l' σ] unfolding missing_args_unfold[symmetric]
    by (cases "is_Fun l'") auto
  thus ?thesis using lhs_rhs_def by argo
qed

lemma is_Cu_Cu⇩R:
  assumes "(l, r) ∈ Cu⇩R ℛ"
  shows "is_Cu l" "is_Cu r"
proof -
  obtain l' r' where lr_def: "l = Cu l'" "r = Cu r'" "(l', r') ∈ ℛ"
    using assms unfolding Cu⇩R_def by blast
  moreover have "funas_term l' ⊆ ℱ" "funas_term r' ⊆ ℱ"
    using lr_def(3) sigR ℱ_def 
    unfolding funas_trs_def funas_rule_def by force+
  ultimately show "is_Cu l" "is_Cu r" using is_Cu_intro by simp+
qed

lemma is_Cu'_n0:
  assumes "missing_args (mctxt_of_term t) n = 1"
  shows "is_Cu' t m ⟶ m = n"
using assms
proof (induction "mctxt_of_term t" n arbitrary: t m rule: missing_args.induct)
  case (2 x n)
  then show ?case by (cases t) auto
next
  case (3 f Cs n)
  then obtain ts where t_def: "t = Fun f ts" "Cs = map mctxt_of_term ts" by (cases t) simp+
  thus ?case
  proof (cases "f = Ap ∧ length Cs = 2")
    case True
    then obtain "is_Cu' (ts ! 0) (Suc m) ⟶ Suc m = Suc n"
      using 3(1)[OF True, of "ts ! 0" "Suc m"] 3(3) unfolding t_def by auto
    thus ?thesis using True unfolding t_def by (auto elim: is_Cu'.cases)
  next
    case False
    thus ?thesis using 3(2-) unfolding t_def by (auto elim: is_Cu'.cases simp: arity_def)
  qed
qed simp

lemma Cu_subst_in_ctxt:
  assumes "is_Cu' C⟨l ⋅ σ⟩ n" "is_Cu l" "is_Fun l" "missing_args (mctxt_of_term (l ⋅ σ)) 0 = 1"
  shows "C ≠ □ ⟶ is_Cu (l ⋅ σ)"
using assms(1,4)
proof (induction C arbitrary: n)
  case (More f ss1 C' ss2)
  consider "∃a. ss1 = [] ∧ ss2 = [a]" | "∃a. ss2 = [] ∧ ss1 = [a]"
    using More(2) by (cases ss1; cases ss2) (auto elim: is_Cu'.cases)
  thus ?case
  proof cases
    case 1
    thus ?thesis using More is_Cu'_n0[OF More(3)] by (cases C') (auto elim: is_Cu'.cases)
  next
    case 2
    then obtain a where lists: "ss2 = [] ∧ ss1 = [a]" by blast
    hence "is_Cu' a (Suc n)" "is_Cu C'⟨l ⋅ σ⟩" using More by (auto elim: is_Cu'.cases)
    thus ?thesis using lists More by (cases C') auto
  qed
qed blast

lemma Cu_step_persists:
  assumes "(s, t) ∈ rstep (Cu⇩R ℛ)" "is_Cu s"
  shows "is_Cu t"
proof -
  obtain l r p σ where step: "(s, t) ∈ rstep_r_p_s (Cu⇩R ℛ) (l, r) p σ"
    using rstep_iff_rstep_r_p_s[of _ _ "Cu⇩R ℛ"] assms(1) by blast
  obtain C where props: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "p = hole_pos C" "(l, r) ∈ Cu⇩R ℛ"
    using hole_pos_ctxt_of_pos_term[of p s]
      Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
    unfolding fst_conv snd_conv by metis
  hence nothing_missing: "missing_args (mctxt_of_term (l ⋅ σ)) 0 = 1"
    using nothing_missing_lhs_Cu⇩R by force
  have "is_Cu l" "is_Cu r" using is_Cu_Cu⇩R[OF props(4)] by simp+
  hence "is_Cu (l ⋅ σ)"
    using Cu_subst_in_ctxt[OF _ _ _ nothing_missing] assms(2) wf_Cu props(4)
    unfolding props(1) wf_trs_def by (cases C) (simp, blast)
  hence is_Cu_σl: "∀x. x ∈ vars_term l ⟶ is_Cu (Var x ⋅ σ)"
    using vars_term_subst_Cu ‹is_Cu l› by blast
  hence is_Cu_σr: "∀x. x ∈ vars_term r ⟶ is_Cu (Var x ⋅ σ)"
    using wf_Cu props(4) unfolding wf_trs_def by blast
  have "is_Cu (r ⋅ σ)"
    using Cu_subst_Cu[OF ‹is_Cu r› is_Cu_σr] .
  thus ?thesis using replace_in_Cu[OF _ ‹is_Cu (l ⋅ σ)› ‹is_Cu (r ⋅ σ)›, of C]
    props(1,2) assms(2) by blast
qed

lemma Cu_eq_NF_𝒰_eq':
  assumes "Cu s = Cu t" "funas_term s ⊆ ℱ"
  shows "NF_𝒰 (Cu t) = s"
using assms(1) NF_𝒰_Cu[OF assms(2)] by simp

lemma Cu⇩R_NF_𝒰_ℛ_steps:
  assumes "(Cu s, Cu t) ∈ (rstep (Cu⇩R ℛ))⇧*" "funas_term s ⊆ ℱ"
  shows "(s, NF_𝒰 (Cu t)) ∈ (rstep ℛ)⇧*"
proof -
  show ?thesis using assms
  proof (induction "Cu s" arbitrary: s rule: converse_rtrancl_induct)
    case base
    thus ?case using Cu_eq_NF_𝒰_eq'[of s t] by simp
  next
    case (step z)
    have "is_Cu (Cu s)" using is_Cu_intro[OF step(4)] .
    then obtain z' where is_Cu_z: "funas_term z' ⊆ ℱ ∧ z = Cu z'"
        using is_Cu_elim[OF Cu_step_persists[OF step(1)]] by blast
    hence "(s, z') ∈ (rstep ℛ)⇧*"
      using Cu⇩R_NF_𝒰_ℛ_step[of s z'] step(1,4) by fastforce
    thus ?case using step(3)[of z'] is_Cu_z by fastforce
  qed
qed

theorem main_result_sound:
  assumes "CR (rstep (Cu⇩R ℛ))"
  shows "CR (rstep ℛ)"
proof -
  { fix a :: "('f, 'v) term"
    assume funas_a: "funas_term a ⊆ ℱ"
    { fix b c
      assume peak: "(a, b) ∈ (rstep ℛ)⇧*" "(a, c) ∈ (rstep ℛ)⇧*"
      hence funas: "funas_term b ⊆ ℱ" "funas_term c ⊆ ℱ"
        using rsteps_preserve_funas_terms[OF sigR funas_a[unfolded ℱ_def] _ wfR]
        unfolding ℱ_def by blast+
      hence NF_𝒰_Cu_bc: "NF_𝒰 (Cu b) = b" "NF_𝒰 (Cu c) = c" using NF_𝒰_Cu by auto
      have "(Cu a, Cu b) ∈ (rstep (Cu⇩R ℛ))⇧*" "(Cu a, Cu c) ∈ (rstep (Cu⇩R ℛ))⇧*"
        using peak rtrancl_map[OF g_prop1, of "rstep ℛ" id a] unfolding rtrancl_idemp by auto
      then obtain d' where join: "(Cu b, d') ∈ (rstep (Cu⇩R ℛ))⇧* ∧ (Cu c, d') ∈ (rstep (Cu⇩R ℛ))⇧*"
        using assms unfolding CR_defs by blast
      hence "d' ∈ 𝒯⇩C⇩u" using funas_Cu[OF funas(1)]
        by simp (meson funas_Cu⇩R rsteps_preserve_funas_terms wf_Cu)
      hence "Cu d' = d'" using 𝒯⇩C⇩u_Cu_eq by blast
      have "(b, NF_𝒰 d') ∈ (rstep ℛ)⇧* ∧ (c, NF_𝒰 d') ∈ (rstep ℛ)⇧*"
        using Cu⇩R_NF_𝒰_ℛ_steps[OF _ funas(1), of d'] Cu⇩R_NF_𝒰_ℛ_steps[OF _ funas(2), of d'] join 
        unfolding ‹Cu d' = d'› by blast
      hence "(b, c) ∈ (rstep ℛ)⇧↓" by blast
    }
    hence "CR_on (rstep ℛ) {a}" unfolding CR_defs by simp
  }
  hence "CR_on (rstep ℛ) { t. funas_term t ⊆ ℱ }" unfolding CR_on_def by auto
  thus ?thesis using CR_on_imp_CR[OF wfR sigR] unfolding ℱ_def by blast
qed

end

end