Theory Ground_Reduction_on_LLRG

section ‹Reducing Rewrite Properties to Properties on Ground Terms over Left-Linear Right-Ground Systems›
theory Ground_Reduction_on_LLRG
  imports
    Rewriting_Properties
    Rewriting_LLRG_LV_Mondaic
begin

lemma llrg_linear_sys:
  "llrg ℛ ⟹ linear_sys ℛ"
  by (auto simp: llrg_def)

section ‹LLRG results›

lemma llrg_commute:
  assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
   and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ" "llrg 𝒮"
   and com: "commute (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
  shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
  let ?σ = "λ _. Fun c []" let ?ℋ = "insert (c, 0) ℱ"
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel 𝒮" "(c, 0) ∉ funas_rel (ℛ¯)" using sig
    by (auto simp: funas_rel_def)
  have linear: "linear_sys 𝒮" "linear_sys (ℛ¯)" using llrg unfolding llrg_def by auto
  have sig': "funas_rel 𝒮 ⊆ ℱ" "funas_rel (ℛ¯) ⊆ ℱ" using sig by (auto simp: funas_rel_def)
  have mono: "ℱ ⊆ ?ℋ" by auto
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
      by (metis Un_iff relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
    from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ 𝒮)⇧*"
      using rtrancl_mono[OF sig_step_mono[OF mono]]
      by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
    have gr: "ground s ∨ ground t" using ass llrg 
      unfolding srstep_converse_dist trancl_converse
      by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
    have gstep: "(s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep ?ℋ 𝒮)⇧* O (gsrstep ?ℋ (ℛ¯))⇧*"
      using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ,
        THEN subsetD[OF com[unfolded commute_def], unfolded rew_converse_inwards]]
      by (auto simp: ground_substI)
    have [simp]: "ground s ⟹ (c, 0) ∉ funas_term s" "ground t ⟹ (c, 0) ∉ funas_term t"
      using funas fresh by auto
    have "(s, t) ∈ (rstep 𝒮)⇧* O (rstep (ℛ¯))⇧*"
      using remove_const_subst_relcomp_lhs[OF linear fresh_sys, of t s]
      using gsrsteps_eq_relcomp_to_rsteps_relcomp[OF gstep] gr
      using remove_const_subst_relcomp_lhs[OF linear fresh_sys, of t s]
      using remove_const_subst_relcomp_rhs[OF linear fresh_sys, of s t]
        by (cases "ground s") (simp_all add: ground_subst_apply)
    from rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig' funas this]
    have "commute_redp ℱ ℛ 𝒮 s t" unfolding commute_redp_def
      by (simp add: rew_converse_inwards)}
  then show ?thesis by (intro commute_rrstep_intro) simp
qed

lemma llrg_CR:
  assumes sig: "funas_rel ℛ ⊆ ℱ"
   and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ"
   and com: "CR (gsrstep (insert (c, 0) ℱ) ℛ)"
  shows "CR (srstep ℱ ℛ)"
  using assms llrg_commute unfolding CR_iff_self_commute
  by metis


lemma llrg_SCR:
  assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ"
   and scr: "SCR (gsrstep (insert (c, 0) ℱ) ℛ)"
  shows "SCR (srstep ℱ ℛ)"
proof -
  let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" using sig
    by (auto simp: funas_rel_def)
  have mono: "ℱ ⊆ ?ℋ" by auto note sig_trans = subsetD[OF srstep_monp[OF mono]]
  {fix s t u assume ass: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
    and root: "(s, t) ∈ sig_step ℱ (rrstep ℛ) ∨ (s, u) ∈ sig_step ℱ (rrstep ℛ)"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
      by (force dest: sig_stepE)+
    from root have gr: "ground t ∨ ground u" using ass llrg llrg_rrsteps_groundness
      unfolding srstep_converse_dist trancl_converse by blast
    have *: "ground (s ⋅ ?σ)" "ground (t ⋅ ?σ)" "ground (u ⋅ ?σ)" by auto
    from this scr obtain v where v: "(t ⋅ ?σ, v) ∈ (gsrstep ?ℋ ℛ)⇧= ∧ (u ⋅ ?σ, v) ∈ (gsrstep ?ℋ ℛ)⇧*"
      using srstep_subst_closed[OF sig_trans[OF ass(1)], of ?σ]
      using srstep_subst_closed[OF sig_trans[OF ass(2)], of ?σ]
      using ass unfolding SCR_on_def
      by auto (metis (no_types, lifting) * )
    then have fv: "funas_term v ⊆ ℱ" using gr llrg_funas_term_step_pres[OF llrg, of _ v]
      using llrg_funas_term_steps_pres[OF llrg, of _ v] funas sig
      by (auto simp: ground_subst_apply elim!: sig_stepE dest!: gsrsteps_eq_to_rsteps_eq) blast+
    then have c_free: "(c, 0) ∉ funas_term v" using fresh by blast
    then have "v = t ⋅ const_subst c ⟹ ground t" using arg_cong[of v "t ⋅ ?σ" funas_term]
      by (auto simp: funas_term_subst vars_term_empty_ground split: if_splits)
    from this v have "(t, v) ∈ (srstep ℱ ℛ)⇧=" "(u, v) ∈ (srstep ℱ ℛ)⇧*"
      using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg] fresh_sys c_free, of u,
        THEN rsteps_eq_srsteps_eqI[OF sig funas(3) fv]]
      using remove_const_subst_step_lhs[OF llrg_linear_sys[OF llrg] fresh_sys c_free, of t,
          THEN sig_stepI[OF _ funas(2) fv]]
      by (auto simp: ground_subst_apply dest: srstepD gsrsteps_eq_to_rsteps_eq)
    then have "SCRp ℱ ℛ t u" by blast}
  then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+ 
qed

lemma llrg_WCR:
  assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ"
   and wcr: "WCR (gsrstep (insert (c, 0) ℱ) ℛ)"
  shows "WCR (srstep ℱ ℛ)"
proof -
  let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel (ℛ¯)" using sig
    by (auto simp: funas_rel_def)
  have lin: "linear_sys ℛ" "linear_sys (ℛ¯)" using llrg unfolding llrg_def by auto
  have mono: "ℱ ⊆ ?ℋ" by auto note sig_trans = subsetD[OF srstep_monp[OF mono]]
  {fix s t u assume ass: "(s, t) ∈ sig_step ℱ (rrstep ℛ)" "(s, u) ∈ srstep ℱ ℛ"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
      by blast+
    then have c_free: "(c, 0) ∉ funas_term t" using fresh by blast
    from ass have gr: "ground t" using ass llrg llrg_rrsteps_groundness by blast
    have *: "ground (s ⋅ ?σ)" "ground (u ⋅ ?σ)" by auto
    from this wcr have w: "(t, u ⋅ ?σ) ∈ (gsrstep ?ℋ ℛ)⇧↓"
      using srstep_subst_closed[OF sig_trans[OF srrstep_to_srestep[OF ass(1)]], of ?σ]
      using srstep_subst_closed[OF sig_trans[OF ass(2)], of ?σ]
      using ass unfolding WCR_on_def
      by auto (metis * gr ground_subst_apply)
    have "(t, u) ∈ (srstep ℱ ℛ)⇧↓" unfolding join_def
      using remove_const_subst_relcomp_rhs[OF lin fresh_sys c_free
        gsrsteps_eq_relcomp_to_rsteps_relcomp[OF w[unfolded join_def rew_converse_inwards]],
        THEN rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig funas_trs_converse[OF sig] funas(2-)]]
      by (metis (no_types, lifting) srstep_converse_dist)}
  then show ?thesis by (intro WCR_rrstep_intro) simp
qed


lemma llrg_UNF:
  assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ"
   and unf: "UNF (gsrstep (insert (c, 0) ℱ) ℛ)"
  shows "UNF (srstep ℱ ℛ)"
proof -
  let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" using sig
    by (auto simp: funas_rel_def)
  have mono: "ℱ ⊆ ?ℋ" by auto
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
      by (metis Un_iff relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
    from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ ℛ)⇧*"
      using rtrancl_mono[OF sig_step_mono[OF mono]]
      by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
    have gr: "ground s ∨ ground t" using ass llrg 
      unfolding srstep_converse_dist trancl_converse
      by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
    have wit: "s ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ s ⋅ ?σ = t ⋅ ?σ" using unf
      using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ]
      by (auto simp: UNF_on_def rew_converse_outwards normalizability_def)
    from funas NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg] fresh_sys sig(1)]
    have "s ∈ NF (srstep ℱ ℛ) ⟹ s ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)" "t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)"
      by auto
    moreover have "s ⋅ ?σ = t ⋅ ?σ ⟹ s = t" using gr funas fresh
      by (cases "ground s") (auto simp: ground_subst_apply funas_term_subst vars_term_empty_ground split: if_splits)
    ultimately have "UN_redp ℱ ℛ s t" using wit unfolding UN_redp_def
      by auto}
  then show ?thesis by (intro UNF_rrstep_intro) simp
qed


lemma llrg_NFP:
  assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ"
   and nfp: "NFP (gsrstep (insert (c, 0) ℱ) ℛ)"
  shows "NFP (srstep ℱ ℛ)"
proof -
  let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ"
    using sig by (auto simp: funas_rel_def)
  have mono: "ℱ ⊆ ?ℋ" by auto
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
      by (metis Un_iff relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
    from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ ℛ)⇧*"
      using rtrancl_mono[OF sig_step_mono[OF mono]]
      by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
    have gr: "ground s ∨ ground t" using ass llrg 
      unfolding srstep_converse_dist trancl_converse
      by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
    have wit: "t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ (s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep (insert (c, 0) ℱ) ℛ)⇧*"
      using NFP_stepD[OF nfp]
      using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ]
      by (auto simp: rew_converse_outwards)
    from funas NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg] fresh_sys(1) sig(1)]
    have "t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)" by auto
    moreover have "(s ⋅ ?σ, t ⋅ ?σ) ∈ (rstep ℛ)⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*" using gr funas fresh
      using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg] fresh_sys, THEN rsteps_eq_srsteps_eqI[OF sig funas]]
      using remove_const_subst_steps_eq_rhs[OF llrg_linear_sys[OF llrg] fresh_sys, THEN rsteps_eq_srsteps_eqI[OF sig funas]]
      by (cases "ground s") (auto simp: ground_subst_apply)
    ultimately have "NFP_redp ℱ ℛ s t" using wit unfolding NFP_redp_def
      by (auto dest: gsrsteps_eq_to_rsteps_eq)}
  then show ?thesis by (intro NFP_rrstep_intro) simp
qed



lemma llrg_NE_aux:
  assumes "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
   and  sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ" "llrg 𝒮"
   and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
  shows "NE_redp ℱ ℛ 𝒮 s t"
proof -
  from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮"
    using sig by (auto simp: funas_rel_def)
  let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
  let ?ℋ = "insert (c, 0) ℱ"  have mono: "ℱ ⊆ ?ℋ" by auto
  from assms(1) have gr: "ground t" and funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
    using llrg_srsteps_with_root_step_ground[OF llrg(1)]
    by (meson srstepsD srsteps_with_root_step_srstepsD)+
  from funas have fresh_t: "(c, 0) ∉ funas_term t" using fresh by auto
  from srsteps_subst_closed[OF srsteps_monp[OF mono, THEN subsetD, OF srsteps_with_root_step_srstepsD[OF assms(1)]], of ?σ]
  have "(s ⋅ ?σ, t) ∈ (gsrstep?ℋ ℛ)⇧+" using gr
    by (auto simp: ground_subst_apply intro!: ground_srsteps_gsrsteps)
  then have "t ∈ NF (srstep ℱ ℛ) ⟹ (s ⋅ ?σ, t) ∈ (gsrstep (insert (c, 0) ℱ) 𝒮)⇧*"
    using NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg(1)] fresh_sys(1) sig(1) funas(2), of ?ℋ]
    using gr NE_NF_eq[OF ne, symmetric] ne unfolding NE_on_def
    by (auto simp: normalizability_def ground_subst_apply dest!: trancl_into_rtrancl)
  then show "NE_redp ℱ ℛ 𝒮 s t" unfolding NE_redp_def
    using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg(2)] fresh_sys(2) fresh_t,
      THEN rsteps_eq_srsteps_eqI[OF sig(2) funas]]
    by (auto dest: gsrsteps_eq_to_rsteps_eq)
qed

lemma llrg_NE:
  assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
   and llrg: "llrg ℛ" "llrg 𝒮"
   and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
  shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
  have f: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮" using fresh sig
    by (auto simp: funas_rel_def)
  {fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
    from llrg_NE_aux[OF this sig fresh llrg ne] have "NE_redp ℱ ℛ 𝒮 s t"
      by simp}
  moreover
  {fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ 𝒮"
    from llrg_NE_aux[OF this sig(2, 1) fresh llrg(2, 1) NE_symmetric[OF ne]]
    have "NE_redp ℱ 𝒮 ℛ s t" by simp}
  ultimately show ?thesis using linear_sys_gNF_eq_NF_eq[OF llrg_linear_sys[OF llrg(1)]
    llrg_linear_sys[OF llrg(2)] sig f _ _ NE_NF_eq[OF ne]]
    by (intro NE_rrstep_intro) auto
qed

subsection ‹Specialized for monadic signature›

lemma monadic_commute:
  assumes "llrg ℛ" "llrg 𝒮" "monadic ℱ"
   and com: "commute (gsrstep ℱ ℛ) (gsrstep ℱ 𝒮)"
  shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮"
    then obtain u where steps: "(s, u) ∈ (srstep ℱ (ℛ¯))⇧+" "(u, t) ∈ (srstep ℱ 𝒮)⇧+"
      by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
    have gr: "ground s" "ground t" using steps assms(1 - 3)
      unfolding rew_converse_outwards
      by (auto simp: llrg_srsteps_with_root_step_ground llrg_monadic_rsteps_groundness)
    from steps(1) have f: "funas_term s ⊆ ℱ" using srstepsD by blast 
    let ?σ = "λ _. s"
    from steps gr have "(s, u ⋅ ?σ) ∈ (gsrstep ℱ (ℛ¯))⇧+" "(u ⋅ ?σ, t) ∈ (gsrstep ℱ 𝒮)⇧+"
      unfolding rew_converse_outwards
      using srsteps_subst_closed[where ?σ = ?σ and ?s = u, of _ ℱ] f
      by (force simp: ground_subst_apply intro: ground_srsteps_gsrsteps)+
    then have "(s, t) ∈ (gsrstep ℱ 𝒮)⇧* O (gsrstep ℱ (ℛ¯))⇧*" using com
      unfolding commute_def rew_converse_inwards
      by (meson relcomp.relcompI subsetD trancl_into_rtrancl)
    from gsrsteps_eq_relcomp_srsteps_relcompD[OF this]
    have "commute_redp ℱ ℛ 𝒮 s t" unfolding commute_redp_def
      by (simp add: rew_converse_inwards)}
  then show ?thesis by (intro commute_rrstep_intro) simp
qed

lemma monadic_CR:
  assumes "llrg ℛ" "monadic ℱ"
   and "CR (gsrstep ℱ ℛ)"
  shows "CR (srstep ℱ ℛ)" using monadic_commute assms
  unfolding CR_iff_self_commute
  by blast


lemma monadic_SCR:
  assumes sig: "funas_rel ℛ ⊆ ℱ" "monadic ℱ"
   and llrg: "llrg ℛ"
   and scr: "SCR (gsrstep ℱ ℛ)"
  shows "SCR (srstep ℱ ℛ)"
proof -
  {fix s t u assume ass: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
    and root: "(s, t) ∈ sig_step ℱ (rrstep ℛ) ∨ (s, u) ∈ sig_step ℱ (rrstep ℛ)"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ" by blast+
    from root have gr: "ground t" "ground u" using ass sig(2) llrg
      by (metis llrg_monadic_rstep_pres_groundness)+
    let ?σ = "λ _. t" have grs: "ground (s ⋅ ?σ)" using gr by auto
    from this scr obtain v where v: "(t, v) ∈ (gsrstep ℱ ℛ)⇧= ∧ (u, v) ∈ (gsrstep ℱ ℛ)⇧*"
      using srstep_subst_closed[OF ass(1), of ?σ]
      using srstep_subst_closed[OF ass(2), of ?σ]
      using gr unfolding SCR_on_def
      by (metis Int_iff UNIV_I funas(2) ground_subst_apply mem_Collect_eq mem_Sigma_iff)
    then have "SCRp ℱ ℛ t u"
      by (metis Int_iff Un_iff gsrsteps_eq_to_srsteps_eq)}
  then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+ 
qed

lemma monadic_WCR:
  assumes sig: "funas_rel ℛ ⊆ ℱ" "monadic ℱ"
   and llrg: "llrg ℛ"
   and wcr: "WCR (gsrstep ℱ ℛ)"
  shows "WCR (srstep ℱ ℛ)"
proof -
  {fix s t u assume ass: "(s, t) ∈ sig_step ℱ (rrstep ℛ)" "(s, u) ∈ srstep ℱ ℛ"
    from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ" by blast+
    from srrstep_to_srestep ass have gr: "ground t" "ground u"using ass sig(2) llrg
      by (metis llrg_monadic_rstep_pres_groundness)+
    let ?σ = "λ _. t" have grs: "ground (s ⋅ ?σ)" using gr by auto
    from this wcr have w: "(t, u) ∈ (gsrstep ℱ ℛ)⇧↓" using gr ass(2) funas
      using srstep_subst_closed[OF srrstep_to_srestep[OF ass(1)], of ?σ]
      using srstep_subst_closed[OF ass(2), of ?σ]
      unfolding WCR_on_def
      by (metis IntI SigmaI UNIV_I ground_subst_apply mem_Collect_eq)
    then have "(t, u) ∈ (srstep ℱ ℛ)⇧↓" unfolding join_def
      by (metis gsrsteps_eq_to_srsteps_eq joinD joinI join_def)}
  then show ?thesis by (intro WCR_rrstep_intro) simp
qed

lemma monadic_UNF:
  assumes "llrg ℛ" "monadic ℱ"
   and unf: "UNF (gsrstep ℱ ℛ)"
  shows "UNF (srstep ℱ ℛ)"
proof -
  {fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
    then obtain u where steps: "(s, u) ∈ (srstep ℱ (ℛ¯))⇧+" "(u, t) ∈ (srstep ℱ ℛ)⇧+"
      by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
    have gr: "ground s" "ground t" using steps assms(1, 2)
      unfolding rew_converse_outwards
      by (auto simp: llrg_srsteps_with_root_step_ground llrg_monadic_rsteps_groundness)
    from steps(1) have f: "funas_term s ⊆ ℱ" using srstepsD by blast 
    let ?σ = "λ _. s"
    from steps gr have "(s, u ⋅ ?σ) ∈ (gsrstep ℱ (ℛ¯))⇧+" "(u ⋅ ?σ, t) ∈ (gsrstep ℱ ℛ)⇧+"
      unfolding rew_converse_outwards
      using srsteps_subst_closed[where ?σ = ?σ and ?s = u, of _ ℱ] f
      by (force simp: ground_subst_apply intro: ground_srsteps_gsrsteps)+
    then have "UN_redp ℱ ℛ s t" using unf ground_NF_srstep_gsrstep[OF gr(1), of ℱ ℛ]
      using ground_NF_srstep_gsrstep[OF gr(2), of ℱ ℛ]
        by (auto simp: UNF_on_def UN_redp_def normalizability_def rew_converse_outwards)
           (meson trancl_into_rtrancl)}
  then show ?thesis by (intro UNF_rrstep_intro) simp
qed


lemma monadic_UNC:
  assumes "llrg ℛ" "monadic ℱ"
   and well: "funas_rel ℛ ⊆ ℱ"
   and unc: "UNC (gsrstep ℱ ℛ)"
  shows "UNC (srstep ℱ ℛ)"
proof -
  {fix s t assume ass: "(s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*" "s ∈ NF (srstep ℱ ℛ)" "t ∈ NF (srstep ℱ ℛ)"
    then have "s = t"
    proof (cases "s = t")
      case False
      then have "∃ s' t'. (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧* ∧ (s', s) ∈ (srstep ℱ ℛ) ∧ (t', t) ∈ (srstep ℱ ℛ)"
        using ass by (auto simp: conversion_def rtrancl_eq_or_trancl dest: tranclD tranclD2)
      then obtain s' t' where split: "(s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*" "(s', s) ∈ (srstep ℱ ℛ)" "(t', t) ∈ (srstep ℱ ℛ)" by blast
      from split(2, 3) have gr: "ground s" "ground t" using llrg_monadic_rstep_pres_groundness[OF assms(1, 2)]
        by blast+
      from ground_srsteps_eq_gsrsteps_eq[OF this ass(1)[unfolded sig_step_conversion_dist]]
      have "(s, t) ∈ (gsrstep ℱ ℛ)⇧↔⇧*"
        unfolding conversion_def Restr_smycl_dist
        by (simp add: rstep_converse_dist srstep_symcl_dist)
      then show ?thesis using ass(2-) unc gr
        by (auto simp: UNC_def ground_NF_srstep_gsrstep)
    qed auto}
  then show ?thesis by (auto simp: UNC_def UN_redp_def)
qed


lemma monadic_NFP:
  assumes "llrg ℛ" "monadic ℱ"
   and nfp: "NFP (gsrstep ℱ ℛ)"
  shows "NFP (srstep ℱ ℛ)"
proof -
  {fix s t u assume ass: "(s, t) ∈ (srstep ℱ ℛ)⇧*" "(s, u) ∈ (srstep ℱ ℛ)⇧*" "u ∈ NF (srstep ℱ ℛ)"
    have "(t, u) ∈ (srstep ℱ ℛ)⇧*"
    proof (cases "s = u ∨ s = t")
      case [simp]: True show ?thesis using ass
        by (metis NF_not_suc True rtrancl.rtrancl_refl)
    next
      case False
      then have steps:"(s, t) ∈ (srstep ℱ ℛ)⇧+" "(s, u) ∈ (srstep ℱ ℛ)⇧+" using ass(1, 2)
        by (auto simp add: rtrancl_eq_or_trancl)
      then have gr: "ground t" "ground u" using assms(1, 2) llrg_monadic_rsteps_groundness
        by blast+
      let ?σ = "λ _. t" from steps gr have "(s ⋅ ?σ, t) ∈ (gsrstep ℱ ℛ)⇧+" "(s ⋅ ?σ, u) ∈ (gsrstep ℱ ℛ)⇧+"
        by (auto intro!: ground_srsteps_gsrsteps)
           (metis ground_subst_apply srstepsD srsteps_subst_closed)+
      then have "(t, u) ∈ (gsrstep ℱ ℛ)⇧*" using nfp ass(3) gr
        by (auto simp: NFP_on_def) (metis ground_NF_srstep_gsrstep normalizability_I trancl_into_rtrancl)
      then show ?thesis by (auto dest: gsrsteps_eq_to_srsteps_eq)
    qed}
  then show ?thesis unfolding NFP_on_def
    by auto
qed


end