Theory Lift_Root_Step

section ‹Lifting root steps to single/parallel root/non-root steps›
theory Lift_Root_Step
  imports UL.Basic_Utils
    FOR_Certificate
    GR.Context_Extensions
    TRS.Trs
    TRS.Multihole_Context
begin

― ‹Closure under all contexts›
"gctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"">abbreviation "gctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"
"gmctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"">abbreviation "gmctxtcl ℛ ≡ gctxtex_onp (λ C. True) ℛ"

― ‹Extension under all non empty contexts›
"gctxtex_nempty ℛ ≡ gctxtex_onp (λ C. C ≠ □_G) ℛ"">abbreviation "gctxtex_nempty ℛ ≡ gctxtex_onp (λ C. C ≠ □⇩G) ℛ"
"gmctxtex_nempty ℛ ≡ gmctxtex_onp (λ C. C ≠ GMHole) ℛ"">abbreviation "gmctxtex_nempty ℛ ≡ gmctxtex_onp (λ C. C ≠ GMHole) ℛ"

― ‹Closure under all contexts respecting the signature›
"gctxtcl_funas ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ) ℛ"">abbreviation "gctxtcl_funas ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ) ℛ"
"gmctxtcl_funas ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ) ℛ"">abbreviation "gmctxtcl_funas ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ) ℛ"

― ‹Closure under all multihole contexts with at least one hole respecting the signature›
"gmctxtcl_funas_strict ℱ ℛ ≡ gmctxtex_onp (λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ) ℛ"">abbreviation "gmctxtcl_funas_strict ℱ ℛ ≡ gmctxtex_onp (λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ) ℛ"

― ‹Extension under all non empty contexts respecting the signature›
"gctxtex_funas_nroot ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ C ≠ □_G) ℛ"">abbreviation "gctxtex_funas_nroot ℱ ℛ ≡ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ C ≠ □⇩G) ℛ"
"gmctxtex_funas_nroot ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole) ℛ"">abbreviation "gmctxtex_funas_nroot ℱ ℛ ≡ gmctxtex_onp (λ C. funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole) ℛ"

― ‹Extension under all non empty contexts respecting the signature›
"gmctxtex_funas_nroot_strict ℱ ℛ ≡">abbreviation "gmctxtex_funas_nroot_strict ℱ ℛ ≡
   gmctxtex_onp (λ C.  0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole) ℛ"


section ‹Definitions›

subsection ‹Rewrite steps connecting to IsaFoR›

definition grrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "grrstep ℛ = inv_image (rrstep ℛ) term_of_gterm"

definition gnrrstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "gnrrstep ℛ = inv_image (nrrstep ℛ) term_of_gterm"

definition grstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "grstep ℛ = inv_image (rstep ℛ) term_of_gterm"

definition gpar_rstep :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "gpar_rstep ℛ = inv_image (par_rstep ℛ) term_of_gterm"


subsection ‹Rewrite steps equivalent definitions›

definition gsubst_cl :: "('f, 'v) trs ⇒ 'f gterm rel" where
  "gsubst_cl ℛ = {(gterm_of_term (l ⋅ σ), gterm_of_term (r ⋅ σ)) |
    l r (σ :: 'v ⇒ ('f, 'v) Term.term). (l, r) ∈ ℛ ∧ ground (l ⋅ σ) ∧ ground (r ⋅ σ)}"

definition gnrrstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gnrrstepD ℱ ℛ = gctxtex_funas_nroot ℱ ℛ"

definition grstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "grstepD ℱ ℛ = gctxtcl_funas ℱ ℛ"

definition gpar_rstepD :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gpar_rstepD ℱ ℛ = gmctxtcl_funas ℱ ℛ"

inductive_set gpar_rstepD' :: "'f sig ⇒ 'f gterm rel ⇒ 'f gterm rel" for ℱ :: "'f sig" and ℛ :: "'f gterm rel"
  where groot_step [intro]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ gpar_rstepD' ℱ ℛ"
     |  gpar_step_fun [intro]: "⟦⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ gpar_rstepD' ℱ ℛ⟧ ⟹ length ss = length ts
             ⟹ (f, length ts) ∈ ℱ ⟹ (GFun f ss, GFun f ts) ∈ gpar_rstepD' ℱ ℛ"

subsection ‹Interface between rewrite step definitions and sets›

fun lift_root_step :: "('f × nat) set ⇒ pos_step ⇒ ext_step ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "lift_root_step ℱ PAny ESingle ℛ = gctxtcl_funas ℱ ℛ"
| "lift_root_step ℱ PAny EStrictParallel ℛ = gmctxtcl_funas_strict ℱ ℛ"
| "lift_root_step ℱ PAny EParallel ℛ = gmctxtcl_funas ℱ ℛ"
| "lift_root_step ℱ PNonRoot ESingle ℛ = gctxtex_funas_nroot ℱ ℛ"
| "lift_root_step ℱ PNonRoot EStrictParallel ℛ = gmctxtex_funas_nroot_strict ℱ ℛ"
| "lift_root_step ℱ PNonRoot EParallel ℛ = gmctxtex_funas_nroot ℱ ℛ"
| "lift_root_step ℱ PRoot ESingle ℛ = ℛ"
| "lift_root_step ℱ PRoot EStrictParallel ℛ = ℛ"
| "lift_root_step ℱ PRoot EParallel ℛ = ℛ ∪ Restr Id (𝒯⇩G ℱ)"


definition gcomp_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gcomp_rel ℱ R S = (R O lift_root_step ℱ PAny EParallel S) ∪ (lift_root_step ℱ PAny EParallel R O S)"

definition gtrancl_rel :: "('f × nat) set ⇒ 'f gterm rel ⇒ 'f gterm rel" where
  "gtrancl_rel ℱ ℛ = (lift_root_step ℱ PAny EParallel ℛ)⇧+ O ℛ O (lift_root_step ℱ PAny EParallel ℛ)⇧+"


subsection ‹Compatibility of used predicate extensions and signature closure›

lemma compatible_p [simp]:
  "compatible_p (λ C. C ≠ □⇩G) (λ C. C ≠ GMHole)"
  "compatible_p (λ C. funas_gctxt C ⊆ ℱ) (λ C. funas_gmctxt C ⊆ ℱ)"
  "compatible_p (λ C. funas_gctxt C ⊆ ℱ ∧ C ≠ □⇩G) (λ C. funas_gmctxt C ⊆ ℱ ∧ C ≠ GMHole)"
  unfolding compatible_p_def
  by rule (case_tac C, auto)+

lemma gmctxtcl_funas_sigcl:
  "signature_closed ℱ (gmctxtcl_funas ℱ ℛ)"
  by (intro gmctxtex_onp_sig_closed) auto

lemma gctxtex_funas_nroot_sigcl:
  "signature_closed ℱ (gmctxtex_funas_nroot ℱ ℛ)"
  by (intro gmctxtex_onp_sig_closed) auto

lemma gmctxtcl_funas_strict_funcl:
  "function_closed ℱ (gmctxtcl_funas_strict ℱ ℛ)"
  by (intro gmctxtex_onp_fun_closed) auto

lemma gmctxtex_funas_nroot_strict_funcl:
  "function_closed ℱ (gmctxtex_funas_nroot_strict ℱ ℛ)"
  by (intro gmctxtex_onp_fun_closed) auto

lemma gctxtcl_funas_dist:
  "gctxtcl_funas ℱ ℛ = gctxtex_onp (λ C. C = □⇩G) ℛ ∪ gctxtex_funas_nroot ℱ ℛ"
  by (intro gctxtex_onp_pred_dist) auto

lemma gmctxtex_funas_nroot_dist:
  "gmctxtex_funas_nroot ℱ ℛ = gmctxtex_funas_nroot_strict ℱ ℛ ∪
     gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ"
  by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtcl_funas_dist:
  "gmctxtcl_funas ℱ ℛ = gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ ∪
     gmctxtex_onp (λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ) ℛ"
  by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtcl_funas_strict_dist:
  "gmctxtcl_funas_strict ℱ ℛ = gmctxtex_funas_nroot_strict ℱ ℛ ∪ gmctxtex_onp (λ C. C = GMHole) ℛ"
  by (intro gmctxtex_onp_pred_dist) auto

lemma gmctxtex_onpzero_num_gholes_id [simp]:
  "gmctxtex_onp (λ C. num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ) ℛ = Restr Id (𝒯⇩G ℱ)" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Ls" from gmctxtex_onpE[OF this] obtain C us vs where
    *: "s = fill_gholes C us" "t = fill_gholes C vs" and
    len: "num_gholes C = length us" "length us = length vs" and
    inv: "num_gholes C = 0 ∧ funas_gmctxt C ⊆ ℱ" by auto
    then have "(s, t) ∈ ?Rs" using len inv unfolding *
      by (cases us; cases vs) (auto simp: 𝒯⇩G_funas_gterm_conv)}
  moreover have "?Rs ⊆ ?Ls"
    by (intro Restr_id_subset_gmctxtex_onp) auto
  ultimately show ?thesis by auto
qed

lemma gctxtex_onp_sign_trans_fst:
  assumes "(s, t) ∈ gctxtex_onp P R" and "s ∈ 𝒯⇩G ℱ"
  shows "(s, t) ∈ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ P C) R"
  using assms
  by (auto simp: 𝒯⇩G_equivalent_def elim!: gctxtex_onpE)

lemma gctxtex_onp_sign_trans_snd:
  assumes "(s, t) ∈ gctxtex_onp P R" and "t ∈ 𝒯⇩G ℱ"
  shows "(s, t) ∈ gctxtex_onp (λ C. funas_gctxt C ⊆ ℱ ∧ P C) R"
  using assms
  by (auto simp: 𝒯⇩G_equivalent_def elim!: gctxtex_onpE)

lemma gmctxtex_onp_sign_trans_fst:
  assumes "(s, t) ∈ gmctxtex_onp P R" and "s ∈ 𝒯⇩G ℱ"
  shows "(s, t) ∈ gmctxtex_onp (λ C. P C ∧ funas_gmctxt C ⊆ ℱ) R"
  using assms
  by (auto simp: 𝒯⇩G_equivalent_def simp add: gmctxtex_onpI)

lemma gmctxtex_onp_sign_trans_snd:
  assumes "(s, t) ∈ gmctxtex_onp P R" and "t ∈ 𝒯⇩G ℱ"
  shows "(s, t) ∈ gmctxtex_onp (λ C. P C ∧ funas_gmctxt C ⊆ ℱ) R"
  using assms
  by (auto simp: 𝒯⇩G_equivalent_def simp add: gmctxtex_onpI)

subsection ‹basic lemmas›

lemma gsubst_cl:
  fixes ℛ :: "('f, 'v) trs" and σ :: "'v ⇒ ('f, 'v) term"
  assumes "(l, r) ∈ ℛ" and "ground (l ⋅ σ)" "ground (r ⋅ σ)"
  shows "(gterm_of_term (l ⋅ σ), gterm_of_term (r ⋅ σ)) ∈ gsubst_cl ℛ"
  using assms unfolding gsubst_cl_def by auto

lemma grstepD [simp]:
  "(s, t) ∈ ℛ ⟹ (s, t) ∈ grstepD ℱ ℛ"
  by (auto simp: grstepD_def gctxtex_onp_def intro!: exI[of _ "□⇩G"])

lemma grstepD_ctxtI [intro]:
  "(l, r) ∈ ℛ ⟹ funas_gctxt C ⊆ ℱ ⟹ (C⟨l⟩⇩G, C⟨r⟩⇩G) ∈ grstepD ℱ ℛ"
  by (auto simp: grstepD_def gctxtex_onp_def intro!: exI[of _ "C"])

lemma gctxtex_funas_nroot_gctxtcl_funas_subseteq:
  "gctxtex_funas_nroot ℱ (grstepD ℱ ℛ) ⊆ grstepD ℱ ℛ"
  unfolding grstepD_def
  by (intro gctxtex_pred_cmp_subseteq) auto

lemma Restr_gnrrstepD_dist [simp]:
  "Restr (gnrrstepD ℱ ℛ) (𝒯⇩G 𝒢) = gnrrstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))"
  by (auto simp add: gnrrstepD_def)

lemma Restr_grstepD_dist [simp]:
  "Restr (grstepD ℱ ℛ) (𝒯⇩G 𝒢) = grstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))"
  by (auto simp add: grstepD_def)

lemma Restr_gpar_rstepD_dist [simp]:
  "Restr (gpar_rstepD ℱ ℛ) (𝒯⇩G 𝒢) = gpar_rstepD (ℱ ∩ 𝒢) (Restr ℛ (𝒯⇩G 𝒢))" (is "?Ls = ?Rs")
  by (auto simp: gpar_rstepD_def)

subsection ‹Equivalence lemmas›

lemma grrstep_subst_cl_conv:
  "grrstep ℛ = gsubst_cl ℛ"
  unfolding gsubst_cl_def grrstep_def rrstep_def rstep_r_p_s_def
  by (auto, metis ground_subst ground_term_of_gterm term_of_gterm_inv) blast

lemma gnrrstepD_gnrrstep_conv:
  "gnrrstep ℛ = gnrrstepD UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Ls" then obtain l r C σ where
      mem: "(l, r) ∈ ℛ" "C ≠ □" "term_of_gterm s = C⟨l ⋅ (σ :: 'b ⇒ ('a, 'b) term)⟩" "term_of_gterm t = C⟨r ⋅ σ⟩"
      unfolding gnrrstep_def inv_image_def nrrstep_def' by auto
    then have "(s, t) ∈ ?Rs" using gsubst_cl[OF mem(1)]
      using gctxtex_onpI[of "λ C. funas_gctxt C ⊆ UNIV ∧ C ≠ □⇩G" "gctxt_of_ctxt C" "gterm_of_term (l ⋅ σ)"
        "gterm_of_term (r ⋅ σ)" "gsubst_cl ℛ"]
      by (auto simp: gnrrstepD_def)}
  moreover
  {fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
      unfolding gnrrstepD_def gctxtex_onp_def gnrrstep_def inv_image_def nrrstep_def' gsubst_cl_def
      by auto (metis ctxt_of_gctxt.simps(1) ctxt_of_gctxt_inv ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply ground_subst)}
  ultimately show ?thesis by auto
qed

lemma grstepD_grstep_conv:
  "grstep ℛ = grstepD UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Ls" then obtain C l r σ where
    mem: "(l, r) ∈ ℛ" "term_of_gterm s = C⟨l ⋅ (σ :: 'b ⇒ ('a, 'b) term)⟩" "term_of_gterm t = C⟨r ⋅ σ⟩"
      unfolding grstep_def inv_image_def by auto
    then have "(s, t) ∈ ?Rs" using grstepD_ctxtI[OF gsubst_cl[OF mem(1)], of σ "gctxt_of_ctxt C" UNIV]
      by (auto simp: grstepD_def gctxtex_onp_def)}
  moreover
  {fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
      by (auto simp: gctxtex_onp_def grstepD_def grstep_def gsubst_cl_def)
       (metis ctxt_of_gctxt_apply_gterm ground_ctxt_apply
        ground_ctxt_of_gctxt ground_subst gterm_of_term_inv rstep.intros)}
  ultimately show ?thesis by auto
qed

lemma gpar_rstep_gpar_rstepD_conv:
  "gpar_rstep ℛ = gpar_rstepD' UNIV (gsubst_cl ℛ)" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Rs"
    then have "(s, t) ∈ gpar_rstep ℛ"
      by induct (auto simp: gpar_rstep_def gsubst_cl_def)}
  moreover
  {fix s t assume ass: "(s, t) ∈ ?Ls" then obtain u v where
      "(u, v) ∈ par_rstep ℛ" "u = term_of_gterm s" "v = term_of_gterm t"
        by (simp add: gpar_rstep_def inv_image_def)
    then have "(s, t) ∈ ?Rs"
    proof (induct arbitrary: s t)
      case (root_step u v σ)
      then have "(s, t) ∈ gsubst_cl ℛ" unfolding gsubst_cl_def
        by auto (metis ground_subst ground_term_of_gterm term_of_gterm_inv)
      then show ?case by auto
    next
      case (par_step_fun ts ss f)
      then show ?case by (cases s; cases t) auto
    next
      case (par_step_var x)
      then show ?case by (cases s) auto
  qed}
  ultimately show ?thesis by auto
qed

lemma gmctxtcl_funas_idem:
  "gmctxtcl_funas ℱ (gmctxtcl_funas ℱ ℛ) ⊆ gmctxtcl_funas ℱ ℛ"
  by (intro gmctxtex_pred_cmp_subseteq)
    (auto elim!: less_eq_to_sup_mctxt_args, blast+)

lemma gpar_rstepD_gpar_rstepD'_conv:
  "gpar_rstepD ℱ ℛ = gpar_rstepD' ℱ ℛ" (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t) ∈ ?Rs" then have "(s, t) ∈ ?Ls"
    proof induct
      case (groot_step s t) then show ?case unfolding gpar_rstepD_def
        using gmctxtex_onpI[of _ GMHole  "[s]" "[t]"]
        by auto
    next
      case (gpar_step_fun ts ss f)
      show ?case using gpar_step_fun(2-) unfolding gpar_rstepD_def
        using subsetD[OF gmctxtcl_funas_idem, of "(GFun f ss, GFun f ts)" ℱ ℛ]
        using gmctxtex_onpI[of _ "GMFun f (replicate (length ss) GMHole)" ss ts "gmctxtcl_funas ℱ ℛ"]
        by (auto simp del: fill_gholes.simps)
    qed}
  moreover
  {fix s t assume "(s, t) ∈ ?Ls" then obtain C ss ts where
    t: "s = fill_gholes C ss" "t = fill_gholes C ts" and
    inv: "num_gholes C = length ss" "num_gholes C = length ts" and
    pred: "funas_gmctxt C ⊆ ℱ" and rel: "∀ i < length ts. (ss ! i, ts ! i) ∈ ℛ"
      unfolding gpar_rstepD_def by auto
    have "(s, t) ∈ ?Rs" using inv pred rel unfolding t
    proof (induct rule: fill_gholes_induct2)
      case (GMHole x) then show ?case
        by (cases ts) auto
    next
      case (GMFun f Cs xs ys)
      from GMFun(1, 2, 5) have "i < length Cs ⟹ ∀ j < length (partition_gholes ys Cs ! i).
        (partition_gholes xs Cs ! i ! j, partition_gholes ys Cs ! i ! j) ∈ ℛ" for i
        by (auto simp: length_partition_by_nth partition_by_nth_nth(1, 2))
      from GMFun this show ?case unfolding partition_holes_fill_gholes_conv'
        by (intro gpar_step_fun) (auto, meson UN_I nth_mem subset_iff)
    qed}
  ultimately show ?thesis by auto
qed

subsection ‹Signature preserving lemmas›

lemma 𝒯⇩G_trans_closure_id [simp]:
  "(𝒯⇩G ℱ × 𝒯⇩G ℱ)⇧+ = 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  by (auto simp: trancl_full_on)

lemma signature_pres_funas_cl [simp]:
  "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gctxtcl_funas ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gmctxtcl_funas ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  apply (intro gctxtex_onp_in_signature) apply blast+
  apply (intro gmctxtex_onp_in_signature) apply blast+
  done

lemma relf_on_gmctxtcl_funas:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "refl_on (𝒯⇩G ℱ) (gmctxtcl_funas ℱ ℛ)"
proof -
  have "t ∈ 𝒯⇩G ℱ ⟹ (t, t) ∈ gmctxtcl_funas ℱ ℛ" for t
    using gmctxtex_onpI[of _ "gmctxt_of_gterm t"]
    by (auto simp: 𝒯⇩G_funas_gterm_conv)
  then show ?thesis using assms
    by (auto simp: refl_on_def)
qed

lemma gtrancl_rel_sound:
  "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gtrancl_rel ℱ ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  using relf_on_gmctxtcl_funas unfolding gtrancl_rel_def
  by (intro Restr_tracl_comp_simps(3)) auto


subsection ‹gcomp_rel and gtrancl_rel lemmas›

lemma gcomp_rel:
  "lift_root_step ℱ PAny EParallel (gcomp_rel ℱ ℛ 𝒮) = lift_root_step ℱ PAny EParallel ℛ O lift_root_step ℱ PAny EParallel 𝒮" (is "?Ls = ?Rs")
proof
  { fix s u assume "(s, u) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)"
     then have "∃t. (s, t) ∈ gpar_rstepD' ℱ ℛ ∧ (t, u) ∈ gpar_rstepD' ℱ 𝒮"
    proof (induct)
      case (gpar_step_fun ts ss f)
      from Ex_list_of_length_P[of _ "λ u i. (ss ! i, u) ∈ gpar_rstepD' ℱ ℛ ∧ (u, ts ! i) ∈ gpar_rstepD' ℱ 𝒮"]
      obtain us where l: "length us = length ts" and
        inv: "∀ i < length ts. (ss ! i, us ! i) ∈ gpar_rstepD' ℱ ℛ ∧ (us ! i, ts ! i) ∈ gpar_rstepD' ℱ 𝒮"
        using gpar_step_fun(2, 3) by blast
      then show ?case using gpar_step_fun(3, 4)
        by (auto intro!: exI[of _ "GFun f us"])
    qed auto}
  then show "?Ls ⊆ ?Rs" unfolding gcomp_rel_def
    by (auto simp flip: gpar_rstepD_gpar_rstepD'_conv[unfolded gpar_rstepD_def])
next
  {fix s t u assume "(s, t) ∈ gpar_rstepD' ℱ ℛ" "(t, u) ∈ gpar_rstepD' ℱ 𝒮"
    then have "(s, u) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)"
    proof (induct arbitrary: u rule: gpar_rstepD'.induct)
      case (gpar_step_fun ts ss f) note IS = this
      show ?case
      proof (cases "(GFun f ts, u) ∈ 𝒮")
        case True
        then have "(GFun f ss, u) ∈ gpar_rstepD' ℱ ℛ O 𝒮" using IS(1, 3, 4)
          by auto
        then show ?thesis by auto
      next
        case False
        then obtain us where u[simp]: "u = GFun f us" and l: "length ts = length us"
          using IS(5) by (cases u) (auto elim!: gpar_rstepD'.cases)
        have "i < length us ⟹
         (ss ! i, us ! i) ∈ gpar_rstepD' ℱ (ℛ O gpar_rstepD' ℱ 𝒮 ∪ gpar_rstepD' ℱ ℛ O 𝒮)" for i
          using IS(2, 5) False
          by (auto elim!: gpar_rstepD'.cases)
        then show ?thesis using l IS(3, 4) unfolding u
          by auto
      qed
    qed auto}
  then show "?Rs ⊆ ?Ls"
    by (auto simp: gcomp_rel_def gpar_rstepD_gpar_rstepD'_conv[unfolded gpar_rstepD_def])
qed

lemma gmctxtcl_funas_in_rtrancl_gctxtcl_funas:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gmctxtcl_funas ℱ ℛ ⊆ (gctxtcl_funas ℱ ℛ)⇧*" using assms
  by (intro gmctxtex_onp_gctxtex_onp_rtrancl) (auto simp: gmctxt_p_inv_def)

lemma R_in_gtrancl_rel:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "ℛ ⊆ gtrancl_rel ℱ ℛ"
proof
  fix s t assume ass: "(s, t) ∈ ℛ"
  then have "(s, s) ∈ gmctxtcl_funas ℱ ℛ" "(t, t) ∈ gmctxtcl_funas ℱ ℛ" using assms
    using signature_closed_imp_reflx_on_sig[OF gmctxtcl_funas_sigcl, of ℱ ℛ]
    by auto
  then show "(s, t) ∈ gtrancl_rel ℱ ℛ" using ass
    by (auto simp: relcomp_unfold gtrancl_rel_def)
qed

lemma trans_gtrancl_rel [simp]:
  "trans (gtrancl_rel ℱ ℛ)"
proof -
  have "(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxtcl_funas ℱ ℛ" for s t
    by (metis bot.extremum funas_gmctxt.simps(2) gmctxtex_closure subsetD)
  then show ?thesis unfolding trans_def gtrancl_rel_def
    by (auto, meson relcomp3_I trancl_into_trancl2 trancl_trans)
qed

lemma gtrancl_rel_cl:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
proof -
 have *:"(s, t) ∈ ℛ ⟹ (s, t) ∈ gmctxtcl_funas ℱ ℛ" for s t
    by (metis bot.extremum funas_gmctxt.simps(2) gmctxtex_closure subsetD)
  have "gmctxtcl_funas ℱ ((gmctxtcl_funas ℱ ℛ)⇧+) ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
    unfolding gtrancl_rel_def using relf_on_gmctxtcl_funas[OF assms]
    by (intro gmctxtex_onp_substep_trancl, intro gmctxtex_pred_cmp_subseteq2)
       (auto simp: less_sup_gmctxt_args_funas_gmctxt refl_on_def)
  moreover have "gtrancl_rel ℱ ℛ ⊆ (gmctxtcl_funas ℱ ℛ)⇧+"
    unfolding gtrancl_rel_def using *
    by (auto, meson trancl.trancl_into_trancl trancl_trans)
  ultimately show ?thesis using gmctxtex_onp_rel_mono by blast
qed

lemma gtrancl_rel_aux:
  "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) O gtrancl_rel ℱ ℛ ⊆ gtrancl_rel ℱ ℛ"
  "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ ⟹ gtrancl_rel ℱ ℛ O gmctxtcl_funas ℱ (gtrancl_rel ℱ ℛ) ⊆ gtrancl_rel ℱ ℛ"
  using subsetD[OF gtrancl_rel_cl[of ℛ ℱ]] unfolding gtrancl_rel_def
  by auto (meson relcomp3_I trancl_trans)+


declare subsetI [rule del]
lemma gtrancl_rel:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ" "compatible_p Q P"
    and "⋀ C. P C ⟹ funas_gmctxt C ⊆ ℱ"
    and "⋀ C D. P C ⟹ P D ⟹ (C, D) ∈ comp_gmctxt ⟹ P (C ⊓ D)"
  shows "(gctxtex_onp Q ℛ)⇧+ ⊆ gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
proof -
  have fst: "gctxtex_onp Q ℛ ⊆ gctxtex_onp Q (gtrancl_rel ℱ ℛ)"
    using R_in_gtrancl_rel[OF assms(1)]
    by (simp add: gctxtex_onp_rel_mono)
  have snd: "gctxtex_onp Q (gtrancl_rel ℱ ℛ) ⊆ gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
    using assms(2)
    by auto
  have "(gmctxtex_onp P (gtrancl_rel ℱ ℛ))⇧+ = gmctxtex_onp P (gtrancl_rel ℱ ℛ)"
    by (intro gmctxtex_onp_substep_tranclE[of _ "λ C. funas_gmctxt C ⊆ ℱ"])
      (auto simp: gtrancl_rel_aux[OF assms(1)] assms(3, 4) intro: funas_gmctxt_poss_gmctxt_subgm_at_funas)
  then show ?thesis using subset_trans[OF fst snd]
    using trancl_mono_set by fastforce
qed

lemma gtrancl_rel_subseteq_trancl_gctxtcl_funas:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gtrancl_rel ℱ ℛ ⊆ (gctxtcl_funas ℱ ℛ)⇧+"
proof -
  have [dest!]: "(s, t) ∈ ℛ ⟹ (s, t) ∈ (gctxtcl_funas ℱ ℛ)⇧+" for s t
    using grstepD grstepD_def by blast
  have [dest!]: "(s, t) ∈ (gmctxtcl_funas ℱ ℛ)⇧+ ⟹ (s, t) ∈ (gctxtcl_funas ℱ ℛ)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
    for s t
    using gmctxtcl_funas_in_rtrancl_gctxtcl_funas[OF assms]
    using signature_pres_funas_cl[OF assms]
    apply (auto simp: gtrancl_rel_def rtrancl_eq_or_trancl intro!: subsetI)
    apply (metis rtranclD rtrancl_trancl_absorb trancl_mono)
    apply (metis mem_Sigma_iff trancl_full_on trancl_mono)+
    done
  then show ?thesis using gtrancl_rel_sound[OF assms]
    by (auto simp: gtrancl_rel_def rtrancl_eq_or_trancl intro!: subsetI)
qed

lemma gmctxtex_onp_gtrancl_rel:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ" and "⋀ C D. Q C ⟹ funas_gctxt D ⊆ ℱ ⟹ Q (C ∘⇩G⇩c D)"
    and "⋀C. P C ⟹ 0 < num_gholes C ∧ funas_gmctxt C ⊆ ℱ"
    and "⋀C. P C ⟹ gmctxt_p_inv C ℱ Q"
  shows "gmctxtex_onp P (gtrancl_rel ℱ ℛ) ⊆ (gctxtex_onp Q ℛ)⇧+"
proof -
  {fix s t assume ass: "(s, t) ∈ gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+)"
    from gctxtex_onpE[OF ass] obtain C u v where
      *: "s = C⟨u⟩⇩G" "t = C⟨v⟩⇩G" and
      inv: "Q C" "(u, v) ∈ (gctxtcl_funas ℱ ℛ)⇧+" by blast
    from inv(2) have "(s, t) ∈ (gctxtex_onp Q ℛ)⇧+" unfolding *
    proof induct
      case (base y)
      then show ?case using assms(2)[OF inv(1)]
        by (auto elim!: gctxtex_onpE) (metis gctxt.cop_add gctxtex_onpI r_into_trancl')
    next
      case (step y z)
      from step(2) have "(C⟨y⟩⇩G, C⟨z⟩⇩G) ∈  gctxtex_onp Q ℛ" using assms(2)[OF inv(1)]
        by (auto elim!: gctxtex_onpE) (metis gctxt.cop_add gctxtex_onpI r_into_trancl')
      then show ?case using step(3)
        by auto
    qed}
  then have con: "gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+) ⊆ (gctxtex_onp Q ℛ)⇧+"
    using subrelI by blast
  have snd: "gmctxtex_onp P ((gctxtcl_funas ℱ ℛ)⇧+) ⊆ (gctxtex_onp Q ((gctxtcl_funas ℱ ℛ)⇧+))⇧+"
    using assms(1)
    by (intro gmctxtex_onp_gctxtex_onp_trancl[OF assms(3) _ assms(4)]) auto
  have fst: "gmctxtex_onp P (gtrancl_rel ℱ ℛ) ⊆ gmctxtex_onp P ((gctxtcl_funas ℱ ℛ)⇧+)"
    using gtrancl_rel_subseteq_trancl_gctxtcl_funas[OF assms(1)]
    by (simp add: gmctxtex_onp_rel_mono)
  show ?thesis using subset_trans[OF fst snd] con
    by (auto intro!: subsetI) (metis (mono_tags, lifting) in_mono trancl_absorb trancl_mono)
qed

lemma gmctxtcl_funas_strict_gtrancl_rel:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gmctxtcl_funas_strict ℱ (gtrancl_rel ℱ ℛ) = (gctxtcl_funas ℱ ℛ)⇧+" (is "?Ls = ?Rs")
proof
  show "?Ls ⊆ ?Rs"
    by (intro gmctxtex_onp_gtrancl_rel[OF assms]) (auto simp: gmctxt_p_inv_def)
next
  show "?Rs ⊆ ?Ls"
    by (intro gtrancl_rel[OF assms])
       (auto simp: compatible_p_def num_gholes_at_least1
          intro: subset_trans[OF inf_funas_gmctxt_subset2])
qed

lemma gmctxtex_funas_nroot_strict_gtrancl_rel:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gmctxtex_funas_nroot_strict ℱ (gtrancl_rel ℱ ℛ) = (gctxtex_funas_nroot ℱ ℛ)⇧+"
 (is "?Ls = ?Rs")
proof
  show "?Ls ⊆ ?Rs"
    by (intro gmctxtex_onp_gtrancl_rel[OF assms])
       (auto simp: gmctxt_p_inv_def gmctxt_closing_def
        dest!: less_eq_gmctxt_Hole gctxt_of_gmctxt_hole_dest gctxt_compose_HoleE(1))
next
  show "?Rs ⊆ ?Ls"
    by (intro gtrancl_rel[OF assms])
       (auto simp: compatible_p_def num_gholes_at_least1
          elim!: comp_gmctxt.cases
          dest: gmctxt_of_gctxt_GMHole_Hole
          intro: subset_trans[OF inf_funas_gmctxt_subset2])
qed

lemma lift_root_step_sig':
  assumes "ℛ ⊆ 𝒯⇩G 𝒢 × 𝒯⇩G ℋ" "ℱ ⊆ 𝒢" "ℱ ⊆ ℋ"
  shows "lift_root_step ℱ W X ℛ ⊆ 𝒯⇩G 𝒢 × 𝒯⇩G ℋ"
  using assms 𝒯⇩G_mono
  by (cases W; cases X) (auto simp add: Sigma_mono 𝒯⇩G_mono inf.coboundedI2)

lemmas lift_root_step_sig = lift_root_step_sig'[OF _ subset_refl subset_refl]

lemma lift_root_step_incr:
  "ℛ ⊆ 𝒮 ⟹ lift_root_step ℱ W X ℛ ⊆ lift_root_step ℱ W X 𝒮"
  by (cases W; cases X) (auto simp add: le_supI1 gctxtex_onp_rel_mono gmctxtex_onp_rel_mono)

lemma Restr_id_mono:
  "ℱ ⊆ 𝒢 ⟹ Restr Id (𝒯⇩G ℱ) ⊆ Restr Id (𝒯⇩G 𝒢)"
  by (meson Sigma_mono 𝒯⇩G_mono inf_mono subset_refl)

lemma lift_root_step_mono:
  "ℱ ⊆ 𝒢 ⟹ lift_root_step ℱ W X ℛ ⊆ lift_root_step 𝒢 W X ℛ"
  by (cases W; cases X) (auto simp: Restr_id_mono intro: gmctxtex_onp_mono gctxtex_onp_mono,
   metis Restr_id_mono sup.coboundedI1 sup_commute)


lemma grstep_lift_root_step:
  "lift_root_step ℱ PAny ESingle (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (grstep ℛ) (𝒯⇩G ℱ)"
  unfolding grstepD_grstep_conv grstepD_def grrstep_subst_cl_conv
  by auto

lemma prod_swap_id_on_refl [simp]:
  "Restr Id (𝒯⇩G ℱ) ⊆ prod.swap ` (ℛ ∪ Restr Id (𝒯⇩G ℱ))"
  by (auto intro: subsetI)

lemma swap_lift_root_step:
  "lift_root_step ℱ W X (prod.swap ` ℛ) = prod.swap ` lift_root_step ℱ W X ℛ"
  by (cases W; cases X) (auto simp add: image_mono swap_gmctxtex_onp swap_gctxtex_onp intro: subsetI)

lemma converse_lift_root_step:
  "(lift_root_step ℱ W X R)¯ = lift_root_step ℱ W X (R¯)"
  by (cases W; cases X) (auto simp add: converse_gctxtex_onp converse_gmctxtex_onp intro: subsetI)

lemma lift_root_step_sig_transfer:
  assumes "p ∈ lift_root_step ℱ W X R" "snd ` R ⊆ 𝒯⇩G ℱ" "funas_gterm (fst p) ⊆ 𝒢"
  shows "p ∈ lift_root_step 𝒢 W X R" using assms
proof -
  from assms have "p ∈ lift_root_step (ℱ ∩ 𝒢) W X R"
    by (cases p; cases W; cases X)
       (auto simp: gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢] gctxtex_onp_sign_trans_snd[of _ _ _ R 𝒢]
          gmctxtex_onp_sign_trans_fst gmctxtex_onp_sign_trans_snd simp flip: 𝒯⇩G_equivalent_def 𝒯⇩G_funas_gterm_conv
          intro: basic_trans_rules(30)[OF gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
              where ?B = "gctxtex_onp P R" for P]
            basic_trans_rules(30)[OF gmctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
              where ?B = "gmctxtex_onp P R" for P])
   then show ?thesis
    by (meson inf.cobounded2 lift_root_step_mono subsetD)
qed


lemma lift_root_step_sig_transfer2:
  assumes "p ∈ lift_root_step ℱ W X R" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm (fst p) ⊆ 𝒢"
  shows "p ∈ lift_root_step 𝒢 W X R"
proof -
  from assms have "p ∈ lift_root_step (ℱ ∩ 𝒢) W X R"
    by (cases p; cases W; cases X)
       (auto simp: gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢] gctxtex_onp_sign_trans_snd[of _ _ _ R 𝒢]
          gmctxtex_onp_sign_trans_fst gmctxtex_onp_sign_trans_snd simp flip: 𝒯⇩G_equivalent_def 𝒯⇩G_funas_gterm_conv
          intro: basic_trans_rules(30)[OF gctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
              where ?B = "gctxtex_onp P R" for P]
            basic_trans_rules(30)[OF gmctxtex_onp_sign_trans_fst[of _ _ _ R 𝒢],
              where ?B = "gmctxtex_onp P R" for P])
   then show ?thesis
    by (meson inf.cobounded2 lift_root_step_mono subsetD)
qed

lemma lift_root_steps_sig_transfer:
  assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧+" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm s ⊆ 𝒢"
  shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧+"
  using assms(1,3)
proof (induct rule: converse_trancl_induct)
  case (base s)
  show ?case using lift_root_step_sig_transfer2[OF base(1) assms(2)] base(2) by (simp add: r_into_trancl)
next
  case (step s s')
  show ?case using lift_root_step_sig_transfer2[OF step(1) assms(2)] step(3,4)
      lift_root_step_sig'[of R UNIV 𝒢 𝒢 W X, THEN subsetD, of "(s, s')"] assms(2)
    by (auto simp: 𝒯⇩G_funas_gterm_conv 𝒯⇩G_equivalent_def)
       (smt SigmaI UNIV_I image_subset_iff snd_conv subrelI trancl_into_trancl2)
qed

lemma lift_root_stepseq_sig_transfer:
  assumes "(s, t) ∈ (lift_root_step ℱ W X R)⇧*" "snd ` R ⊆ 𝒯⇩G 𝒢" "funas_gterm s ⊆ 𝒢"
  shows "(s, t) ∈ (lift_root_step 𝒢 W X R)⇧*"
  using assms by (auto simp flip: reflcl_trancl simp: lift_root_steps_sig_transfer)

lemmas lift_root_step_sig_transfer' = lift_root_step_sig_transfer[of "prod.swap p" ℱ W X "prod.swap ` R" 𝒢 for p ℱ W X 𝒢 R,
    unfolded swap_lift_root_step, OF imageI, THEN imageI [of _ _ prod.swap],
    unfolded image_comp comp_def fst_swap snd_swap swap_swap image_ident]

lemmas lift_root_steps_sig_transfer' = lift_root_steps_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
    THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_trancl pair_in_swap_image
    image_comp comp_def snd_swap swap_swap swap_simp image_ident]

lemmas lift_root_stepseq_sig_transfer' = lift_root_stepseq_sig_transfer[of t s ℱ W X "prod.swap ` R" 𝒢 for t s ℱ W X 𝒢 R,
    THEN imageI [of _ _ prod.swap], unfolded swap_lift_root_step swap_rtrancl pair_in_swap_image
    image_comp comp_def snd_swap swap_swap swap_simp image_ident]

lemma lift_root_step_PRoot_ESingle [simp]:
  "lift_root_step ℱ PRoot ESingle ℛ = ℛ"
  by auto

lemma lift_root_step_PRoot_EStrictParallel [simp]:
  "lift_root_step ℱ PRoot EStrictParallel ℛ = ℛ"
  by auto

lemma lift_root_step_Parallel_conv:
  shows "lift_root_step ℱ W EParallel ℛ = lift_root_step ℱ W EStrictParallel ℛ ∪ Restr Id (𝒯⇩G ℱ)"
  by (cases W) (auto simp: gmctxtcl_funas_dist gmctxtex_funas_nroot_dist)

lemma relax_pos_lift_root_step:
  "lift_root_step ℱ W X R ⊆ lift_root_step ℱ PAny X R"
  by (cases W; cases X) (auto simp: gctxtex_closure gmctxtex_closure)

lemma relax_pos_lift_root_steps:
  "(lift_root_step ℱ W X R)⇧+ ⊆ (lift_root_step ℱ PAny X R)⇧+"
  by (simp add: relax_pos_lift_root_step trancl_mono_set)

lemma relax_ext_lift_root_step:
  "lift_root_step ℱ W X R ⊆ lift_root_step ℱ W EParallel R"
  by (cases W; cases X) (auto simp: compatible_p_gctxtex_gmctxtex_subseteq)

lemma lift_root_step_StrictParallel_seq:
  assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "lift_root_step ℱ PAny EStrictParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+"
  using assms
  by (auto simp: gmctxt_p_inv_def intro!: gmctxtex_onp_gctxtex_onp_trancl)

lemma lift_root_step_Parallel_seq:
  assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "lift_root_step ℱ PAny EParallel R ⊆ (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
  unfolding lift_root_step_Parallel_conv using lift_root_step_StrictParallel_seq[OF assms]
  using Un_mono by blast

lemma lift_root_step_Single_to_Parallel:
  shows "lift_root_step ℱ PAny ESingle R ⊆ lift_root_step ℱ PAny EParallel R"
  by (simp add: compatible_p_gctxtex_gmctxtex_subseteq)

lemma trancl_partial_reflcl:
  "(X ∪ Restr Id Y)⇧+ = X⇧+ ∪ Restr Id Y"
proof (intro equalityI subrelI, goal_cases LR RL)
  case (LR a b) then show ?case by (induct) (auto dest: trancl_into_trancl)
qed (auto intro: trancl_mono)

lemma lift_root_step_Parallels_single:
  assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "(lift_root_step ℱ PAny EParallel R)⇧+ = (lift_root_step ℱ PAny ESingle R)⇧+ ∪ Restr Id (𝒯⇩G ℱ)"
  using trancl_mono_set[OF lift_root_step_Parallel_seq[OF assms]]
  using trancl_mono_set[OF lift_root_step_Single_to_Parallel, of ℱ R]
  by (auto simp: lift_root_step_Parallel_conv trancl_partial_reflcl)


lemma lift_root_Any_Single_eq:
  shows "lift_root_step ℱ PAny ESingle R = R ∪ lift_root_step ℱ PNonRoot ESingle R"
  by (auto simp: gctxtcl_funas_dist intro!: gctxtex_closure)

lemma lift_root_Any_EStrict_eq [simp]:
  shows "lift_root_step ℱ PAny EStrictParallel R = R ∪ lift_root_step ℱ PNonRoot EStrictParallel R"
  by (auto simp: gmctxtcl_funas_strict_dist)

lemma gar_rstep_lift_root_step:
  "lift_root_step ℱ PAny EParallel (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (gpar_rstep ℛ) (𝒯⇩G ℱ)"
  unfolding grrstep_subst_cl_conv gpar_rstep_gpar_rstepD_conv
  unfolding gpar_rstepD_gpar_rstepD'_conv[symmetric]
  by (auto simp: gpar_rstepD_def)

lemma grrstep_lift_root_gnrrstep:
  "lift_root_step ℱ PNonRoot ESingle (Restr (grrstep ℛ) (𝒯⇩G ℱ)) = Restr (gnrrstep ℛ) (𝒯⇩G ℱ)"
  unfolding gnrrstepD_gnrrstep_conv grrstep_subst_cl_conv
  by (simp add: gnrrstepD_def)

― ‹Restoring Isabelle standard attributes to lemmas›
declare subsetI [intro!] 
declare lift_root_step.simps[simp del]


(* This shows the power of Isabelles automation if it does not
  have to construct witnesses *)
lemma gpar_rstepD_grstepD_rtrancl_subseteq:
  assumes "ℛ ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
  shows "gpar_rstepD ℱ ℛ ⊆ (grstepD ℱ ℛ)⇧*"
  using assms unfolding gpar_rstepD_def grstepD_def
  by (intro gmctxtex_onp_gctxtex_onp_rtrancl) (auto simp: 𝒯⇩G_equivalent_def gmctxt_p_inv_def)
end