Theory GTT_Compose

theory GTT_Compose
  imports GTT
begin

definition Δ⇩ε :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" where
  "Δ⇩ε 𝒜 ℬ = { (α, β) . (∃t. ground t ∧ α ∈ ta_res 𝒜 t ∧ β ∈ ta_res ℬ t) }"

definition GTT_comp :: "('q, 'f) gtt ⇒ ('q, 'f) gtt ⇒ ('q, 'f) gtt" where
  "GTT_comp 𝒢⇩1 𝒢⇩2 = (ta.make {} (gtt_rules (fst 𝒢⇩1, fst 𝒢⇩2))
                       (ta_eps (fst 𝒢⇩1) ∪ ta_eps (fst 𝒢⇩2) ∪ Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)),
                     ta.make {} (gtt_rules (snd 𝒢⇩1, snd 𝒢⇩2))
                       (ta_eps (snd 𝒢⇩1) ∪ ta_eps (snd 𝒢⇩2) ∪ Δ⇩ε (fst 𝒢⇩2) (snd 𝒢⇩1)))"

lemma ta_eps_non_state_imp_eq:
  "(q', q) ∈ (ta_eps 𝒜)⇧* ⟹ q ∉ ta_states 𝒜 ⟹ q = q'"
  by (metis (no_types, lifting) converse_rtranclE mem_Sigma_iff rev_subsetD ta_eps_states ta_eps_ta_states)

lemma ta_res_not_state_imp_Var:
  "q ∉ ta_states 𝒜 ⟹ q ∈ ta_res 𝒜 t ⟹ t = Var q"
  by (cases t) (auto dest!: ta_eps_non_state_imp_eq simp: r_rhs_states)

lemma Δ⇩ε_states:
  assumes "(q, q') ∈ Δ⇩ε 𝒜 ℬ"
  shows "q ∈ ta_states 𝒜"
  using assms ta_res_states[of _ 𝒜] by (auto simp: Δ⇩ε_def)

lemma Δ⇩ε_swap:
  "prod.swap p ∈ Δ⇩ε 𝒜 ℬ ⟷ p ∈ Δ⇩ε ℬ 𝒜"
  by (auto simp: Δ⇩ε_def)

lemma Δ⇩ε_states':
  "∃x ∈ Δ⇩ε 𝒜 ℬ. q ∈ (case x of (q, q') ⇒ {q, q'}) ⟹ q ∈ ta_states 𝒜 ∪ ta_states ℬ"
  using Δ⇩ε_states[of _ _ 𝒜 ℬ] Δ⇩ε_states[OF iffD1[OF Δ⇩ε_swap], of _ _ 𝒜 ℬ] by auto

lemma gtt_states_comp_union:
  "gtt_states (GTT_comp 𝒢⇩1 𝒢⇩2) ⊆ gtt_states 𝒢⇩1 ∪ gtt_states 𝒢⇩2"
proof (intro subsetI, goal_cases lr)
  case (lr q) then show ?case
    using lr Δ⇩ε_states'[of "snd 𝒢⇩1" "fst 𝒢⇩2" q] Δ⇩ε_states'[of "fst 𝒢⇩2" "snd 𝒢⇩1" q]
    by (auto simp: GTT_comp_def make_def ta_states_def)
qed

lemma gtt_states_comp_union':
  assumes "ta_final (fst 𝒢⇩1) = {}" "ta_final (snd 𝒢⇩1) = {}"
    and "ta_final (fst 𝒢⇩2) = {}" "ta_final (snd 𝒢⇩2) = {}"
  shows "gtt_states (GTT_comp 𝒢⇩1 𝒢⇩2) = gtt_states 𝒢⇩1 ∪ gtt_states 𝒢⇩2"
proof -
  have "gtt_states (GTT_comp 𝒢⇩1 𝒢⇩2) ⊇ gtt_states 𝒢⇩1 ∪ gtt_states 𝒢⇩2"
    using assms by (fastforce simp: GTT_comp_def ta_states_def)
  then show ?thesis using gtt_states_comp_union[of 𝒢⇩1 𝒢⇩2] by blast
qed

lemma inf_mctxt_args_to_unfill_holes_mctxt:
  "(C, D) ∈ comp_mctxt ⟹ inf_mctxt_args C D = unfill_holes_mctxt (C ⊓ D) C"
  by (induct C D rule: comp_mctxt.induct) (auto intro!: arg_cong[of _ _ concat] simp: zip_nth_conv)

lemma unfill_holes_inf_comp_mctxt_MHole:
  assumes "(C, D) ∈ comp_mctxt" "i < num_holes (C ⊓ D)"
  shows "unfill_holes_mctxt (C ⊓ D) C ! i = MHole ∨ unfill_holes_mctxt (C ⊓ D) D ! i = MHole"
  using inf_mctxt_args_MHole[of C D i] assms
  by (simp add: inf_mctxt_args_to_unfill_holes_mctxt ac_simps comp_mctxt_sym)

lemma GTT_comp_swap [simp]:
  "GTT_comp (prod.swap 𝒢⇩2) (prod.swap 𝒢⇩1) = prod.swap (GTT_comp 𝒢⇩1 𝒢⇩2)"
  by (simp add: GTT_comp_def ac_simps)

lemma gtt_comp_only_if:
  fixes s t :: "('f, 'q) term"
  assumes "ground u"
  assumes su: "gtt_accept 𝒢⇩1 s u" and ut: "gtt_accept 𝒢⇩2 u t"
  shows "gtt_accept (GTT_comp 𝒢⇩1 𝒢⇩2) s t"
proof -
  obtain D :: "('f, 'q) mctxt" and ss us1 where su:
    "length ss = num_holes D" "length us1 = num_holes D"
    "s = fill_holes D ss" "u = fill_holes D us1"
    "∀i < num_holes D. ∃q. q ∈ ta_res (fst 𝒢⇩1) (ss ! i) ∧ q ∈ ta_res (snd 𝒢⇩1) (us1 ! i)"
    using gtt_accept'.cases[OF su[unfolded gtt_accept_equiv]] by metis
  obtain E :: "('f, 'q) mctxt" and us2 ts where ut:
    "length us2 = num_holes E" "length ts = num_holes E"
    "u = fill_holes E us2" "t = fill_holes E ts"
    "∀i < num_holes E. ∃q. q ∈ ta_res (fst 𝒢⇩2) (us2 ! i) ∧ q ∈ ta_res (snd 𝒢⇩2) (ts ! i)"
    using gtt_accept'.cases[OF ut[unfolded gtt_accept_equiv]] by metis
  { (* base case: 𝒢⇩1 touches the i-th hole of the common prefix D ⊓ E *)
    fix i D E 𝒢⇩1 𝒢⇩2 u and ss us1 us2 ts :: "('f, 'q) term list"
    assume i: "i < num_holes (D ⊓ E)" "unfill_holes_mctxt (D ⊓ E) D ! i = MHole" "ground u"
      and su: "length ss = num_holes D" "length us1 = num_holes D" "u = fill_holes D us1"
        "∀i < num_holes D. ∃q. q ∈ ta_res (fst 𝒢⇩1) (ss ! i) ∧ q ∈ ta_res (snd 𝒢⇩1) (us1 ! i)"
      and ut: "length us2 = num_holes E" "length ts = num_holes E" "u = fill_holes E us2"
        "∀i < num_holes E. ∃q. q ∈ ta_res (fst 𝒢⇩2) (us2 ! i) ∧ q ∈ ta_res (snd 𝒢⇩2) (ts ! i)"
    let ?𝒢 = "GTT_comp 𝒢⇩1 𝒢⇩2"
    have [simp]: "C ≤ D ⟹ sum_list (map num_holes (unfill_holes_mctxt C D)) = num_holes D" for C D
      by (metis fill_unfill_holes_mctxt length_unfill_holes_mctxt num_holes_fill_holes_mctxt)
    let ?D = "unfill_holes_mctxt (D ⊓ E) D ! i"
    let ?ss = "partition_holes ss (unfill_holes_mctxt (D ⊓ E) D) ! i"
    let ?us1 = "partition_holes us1 (unfill_holes_mctxt (D ⊓ E) D) ! i"
    let ?E = "unfill_holes_mctxt (D ⊓ E) E ! i"
    let ?us2 = "partition_holes us2 (unfill_holes_mctxt (D ⊓ E) E) ! i"
    let ?ts = "partition_holes ts (unfill_holes_mctxt (D ⊓ E) E) ! i"
    have "length ?us1 = Suc 0" using i su(2) by (simp add: length_partition_by_nth)
    then obtain u1 where u1: "?us1 = [u1]" by (cases ?us1) fastforce+
    have "length ?ss = Suc 0" using i su(1) by (simp add: length_partition_by_nth)
    then obtain s where s: "?ss = [s]" by (cases ?ss) fastforce+
    define u2 where "u2 = fill_holes ?E ?us2"
    define t where "t = fill_holes ?E ?ts"
    have "∀j < num_holes ?D. ∃q. q ∈ ta_res (fst 𝒢⇩1) (?ss ! j) ∧ q ∈ ta_res (snd 𝒢⇩1) (?us1 ! j)"
      using su(1-2) i(1)
      apply (intro allI impI)
      apply (subst partition_by_nth_nth, (simp_all)[3])
      apply (subst partition_by_nth_nth, (simp_all)[3])
      by (metis su(4) inf_mctxt_inf_mctxt_args length_map nth_map num_holes_fill_holes_mctxt
        num_holes_inf_mctxt partition_by_nth_nth(2) unfill_fill_holes_mctxt)
    then obtain q where q: "q ∈ ta_res (fst 𝒢⇩1) (?ss ! 0)" "q ∈ ta_res (snd 𝒢⇩1) u1"
      by (auto simp: i(2) u1)
    have "∀j < num_holes ?E. ∃q. q ∈ ta_res (fst 𝒢⇩2) (?us2 ! j) ∧ q ∈ ta_res (snd 𝒢⇩2) (?ts ! j)"
      using ut(1-2) i(1)
      apply (intro allI impI)
      apply (subst partition_by_nth_nth, (simp_all)[3])
      apply (subst partition_by_nth_nth, (simp_all)[3])
      by (metis ut(4) inf_mctxt_inf_mctxt_args length_map nth_map num_holes_fill_holes_mctxt
        num_holes_inf_mctxt partition_by_nth_nth(2) unfill_fill_holes_mctxt inf_mctxt_comm)
    then obtain qs' where
      "⋀i. i < num_holes ?E ⟹ qs' i ∈ ta_res (fst 𝒢⇩2) (?us2 ! i) ∧ qs' i ∈ ta_res (snd 𝒢⇩2) (?ts ! i)"
      by metis
    note qs' = conjunct1[OF this] conjunct2[OF this]
    have *: "fill_holes D us1 = fill_holes E us2" by (simp add: su(3)[symmetric] ut(3)[symmetric])
    have u1': "fill_holes ?E ?us2 = u1"
      using arg_cong[OF *, of "λt. unfill_holes (D ⊓ E) t ! i"] su(2) ut(1)
      apply (subst (asm) (3) fill_unfill_holes_mctxt[symmetric, OF inf_le2, of E D])
      apply (subst (asm) (2) fill_unfill_holes_mctxt[symmetric, OF inf_le1, of D E])
      apply (subst (asm) fill_holes_mctxt_fill_holes, simp, simp add: fill_unfill_holes_mctxt)+
      by (simp add: i unfill_fill_holes u1)
    obtain qs where qs: "length qs = num_holes ?E"
      "⋀j. j < num_holes ?E ⟹ qs ! j ∈ ta_res (snd 𝒢⇩1) (?us2 ! j)"
      "q ∈ ta_res (snd 𝒢⇩1) (fill_holes ?E (map Var qs))"
      using ta_res_fill_holes[of q "snd 𝒢⇩1" ?E ?us2] ut(1) i(1)
      by (auto simp: u1' q length_partition_by_nth)
    have "ta_rules (snd 𝒢⇩1) ⊆ ta_rules (snd ?𝒢)" "ta_eps (snd 𝒢⇩1) ⊆ ta_eps (snd ?𝒢)"
      by (auto simp: GTT_comp_def)
    then have "q ∈ ta_res (snd ?𝒢) (fill_holes ?E (map Var qs))"
      using qs(3) subsetD[OF ta_res_mono'[of "snd 𝒢⇩1" "snd ?𝒢" "fill_holes ?E (map Var qs)"], of q]
      by simp
    moreover {
      fix j assume j: "j < num_holes (unfill_holes_mctxt (D ⊓ E) E ! i)"
      have *: "ta_eps (snd 𝒢⇩2) ⊆ ta_eps (snd ?𝒢)" "ta_rules (snd 𝒢⇩2) ⊆ ta_rules (snd ?𝒢)"
        by (auto simp: GTT_comp_def)
      have "?us2 ! j ∈ set us2" using ut(1,3) i j
        by (intro partition_by_nth_nth_elem) auto
      then have "ground (?us2 ! j)" using ut(1,2,3) `ground u`
        supteq_imp_vars_term_subset[of u "?us2 ! j"] unfill_holes_subt[of E u "?us2 ! j"]
        by (simp add: ground_vars_term_empty unfill_fill_holes)
      then have "(qs' j, qs ! j) ∈ Δ⇩ε (fst 𝒢⇩2) (snd 𝒢⇩1)"
        using qs(2)[OF j] qs'(1)[OF j] by (auto simp: Δ⇩ε_def)
      then have "(qs' j, qs ! j) ∈ (Δ⇩ε (fst 𝒢⇩2) (snd 𝒢⇩1))⇧=" using qs(2)[OF j] qs'(1)[OF j]
        by (auto simp: Δ⇩ε_def dest!: ta_res_not_state_imp_Var ta_eps_non_state_imp_eq)
      then have "qs ! j ∈ ta_res (snd ?𝒢) (?ts ! j)"
        using qs'(2)[OF j] subsetD[OF ta_res_mono'[OF *]]
        by (subst ta_res_eps[of "qs' j"]) (auto simp: GTT_comp_def)
    }
    ultimately have "q ∈ ta_res (snd ?𝒢) t"
      using i(1) ut(2) fill_holes_ta_res[of ?ts ?E qs "snd ?𝒢" q]
      by (auto simp: t_def qs length_partition_by_nth)
    moreover have "ta_rules (fst 𝒢⇩1) ⊆ ta_rules (fst ?𝒢)" "ta_eps (fst 𝒢⇩1) ⊆ ta_eps (fst ?𝒢)"
      by (auto simp: GTT_comp_def ta_subset_def)
    then have "q ∈ ta_res (fst ?𝒢) s"
      using q(1) subsetD[OF ta_res_mono'[of "fst 𝒢⇩1" "fst ?𝒢" s], of q]
      by (simp add: s)
    ultimately have "gtt_accept ?𝒢 (fill_holes ?D ?ss) (fill_holes ?E ?ts)"
      unfolding gtt_accept_equiv
      using gtt_accept'.mctxt[of "[s]" "[t]" MHole "?𝒢"]
      by (simp add: s t_def[symmetric] i)
  } note base = this
  have "(D, E) ∈ comp_mctxt" using su(2,4) ut(1,3) fill_holes_suffix prefix_comp_mctxt by metis
  note [simp] = this su(1) ut(2) fill_unfill_holes_mctxt
  show ?thesis unfolding su(3) ut(4)
    (* extract common context: D ⊓ E *)
    apply (subst fill_unfill_holes_mctxt[symmetric, OF inf_le2, of E D])
    apply (subst fill_unfill_holes_mctxt[symmetric, OF inf_le1, of D E])
    apply (subst fill_holes_mctxt_fill_holes, simp, simp)
    apply (subst fill_holes_mctxt_fill_holes, simp, simp)
    (* drop context and finish proof *)
    apply (intro accept'_closed_ctxt[folded gtt_accept_equiv] allI; (simp; fail)?)
    subgoal for i using su(5) ut(5) unfill_holes_inf_comp_mctxt_MHole[of D E i]
      base[OF _ _ `ground u` su(1,2,4) _ ut(1,2,3), of i 𝒢⇩1 𝒢⇩2]
      base[OF _ _ `ground u` ut(2,1,3) _ su(2,1,4), of i "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1"]
      by (auto simp add: ac_simps conj_commute gtt_accept_equiv[symmetric])
    done
qed

lemma Δ⇩ε_states_subset_gtt_states:
  "Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2) ⊆ gtt_states 𝒢⇩1 × gtt_states 𝒢⇩2"
  by (auto simp: Δ⇩ε_def dest!: ta_res_not_state_imp_Var)

lemma Δ⇩ε_steps_from_𝒢⇩2:
  assumes "(q, q') ∈ (ta_eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "q ∈ gtt_states 𝒢⇩2"
    "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  shows "(q, q') ∈ (ta_eps (fst 𝒢⇩2))⇧* ∧ q' ∈ gtt_states 𝒢⇩2"
  using assms(1-2)
proof (induct rule: converse_rtrancl_induct)
  case (step q p)
  have "(q, p) ∈ (ta_eps (fst 𝒢⇩2))⇧*" "p ∈ gtt_states 𝒢⇩2"
    using step(1,4) assms(3) ta_eps_states subsetD[OF Δ⇩ε_states_subset_gtt_states[of 𝒢⇩1 𝒢⇩2], of "(q, p)"]
    by (auto simp: GTT_comp_def Δ⇩ε_def)
  then show ?case using step(3) by auto
qed auto

lemma Δ⇩ε_steps_from_𝒢⇩1:
  assumes "(q, q') ∈ (ta_eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "q ∈ gtt_states 𝒢⇩1"
    "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  obtains "q' ∈ gtt_states 𝒢⇩1" "(q, q') ∈ (ta_eps (fst 𝒢⇩1))⇧*"
  | p p' where "q' ∈ gtt_states 𝒢⇩2" "(q, p) ∈ (ta_eps (fst 𝒢⇩1))⇧*" "(p, p') ∈ Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)"
    "(p', q') ∈ (ta_eps (fst 𝒢⇩2))⇧*"
  using assms(1,2)
proof (induct arbitrary: thesis rule: converse_rtrancl_induct)
  case (step q p)
  consider "(q, p) ∈ (ta_eps (fst 𝒢⇩1))⇧*" "p ∈ gtt_states 𝒢⇩1"
    | "(q, p) ∈ Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "p ∈ gtt_states 𝒢⇩2"
    using subsetD[OF Δ⇩ε_states_subset_gtt_states[of 𝒢⇩1 𝒢⇩2], of "(q, p)"]
      assms(3) step(1) ta_eps_states step(6) by (auto simp: GTT_comp_def)
  then show ?case
  proof (cases)
    case 1 show ?thesis using 1(1,2) step.prems(2)
      by (cases rule: step(3), auto intro: step(4)) (metis rtrancl_trans)+
  next
    case 2 show ?thesis using Δ⇩ε_steps_from_𝒢⇩2[OF step(2) 2(2) assms(3)] step(5)[OF _ _ 2(1)] by auto
  qed
qed auto

lemma Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2:
  assumes "(q, q') ∈ (ta_eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "q ∈ gtt_states 𝒢⇩1 ∪ gtt_states 𝒢⇩2"
    "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  obtains "q ∈ gtt_states 𝒢⇩1" "q' ∈ gtt_states 𝒢⇩1" "(q, q') ∈ (ta_eps (fst 𝒢⇩1))⇧*"
  | p p' where "q ∈ gtt_states 𝒢⇩1" "q' ∈ gtt_states 𝒢⇩2" "(q, p) ∈ (ta_eps (fst 𝒢⇩1))⇧*"
    "(p, p') ∈ Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "(p', q') ∈ (ta_eps (fst 𝒢⇩2))⇧*"
  | "q ∈ gtt_states 𝒢⇩2" "(q, q') ∈ (ta_eps (fst 𝒢⇩2))⇧* ∧ q' ∈ gtt_states 𝒢⇩2"
  using assms Δ⇩ε_steps_from_𝒢⇩1 Δ⇩ε_steps_from_𝒢⇩2 by (metis (no_types, lifting) Un_iff)

lemma GTT_comp_first:
  assumes"q ∈ ta_res (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q ∈ gtt_states 𝒢⇩1"
    "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  shows "q ∈ ta_res (fst 𝒢⇩1) t"
  using assms(1,2)
proof (induct t arbitrary: q)
  case (Var q')
  then have *: "(q', q) ∈ (ta_eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "q' ∈ gtt_states 𝒢⇩1"
    by simp_all (smt Un_iff Var.prems(1) Δ⇩ε_steps_from_𝒢⇩2 assms(3) disjoint_iff_not_equal gtt_states_comp_union
      subsetCE sup_ge1 ta_eps_non_state_imp_eq ta_res_vars_states term.set_intros(3))
  then show ?case using Var assms(3)
    by (cases rule: Δ⇩ε_steps_from_𝒢⇩1[OF * assms(3)]) fastforce+
next
  case (Fun f ts)
  obtain q' qs where q': "f qs → q' ∈ ta_rules (fst (GTT_comp 𝒢⇩1 𝒢⇩2))"
    "(q', q) ∈ (ta_eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "length qs = length ts"
    "⋀i. i < length ts ⟹ qs ! i ∈ ta_res (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) (ts ! i)"
    using Fun(2) by auto
  have "q' ∈ gtt_states 𝒢⇩1"
    by (smt GTT_comp_def Un_iff Δ⇩ε_steps_from_𝒢⇩2 Fun(3) assms(3) disjoint_iff_not_equal fst_conv
      q'(1) q'(2) r_rhs_states snd_conv ta_make_simps(1))
  then have "f qs → q' ∈ ta_rules (fst 𝒢⇩1)"
    by (smt GTT_comp_def UnE UnI1 assms(3) disjoint_iff_not_equal fst_conv q'(1) r_rhs_states snd_conv ta_make_simps(1))
  moreover have "(q', q) ∈ (ta_eps (fst 𝒢⇩1))⇧*"
    using Fun.prems(2) Δ⇩ε_steps_from_𝒢⇩1[of _ _ 𝒢⇩1 𝒢⇩2] `q' ∈ gtt_states 𝒢⇩1` assms(3) q'(2) by blast
  moreover {
    fix i assume i: "i < length ts"
    then have "qs ! i ∈ ta_states (fst 𝒢⇩1)" using `f qs → q' ∈ ta_rules (fst 𝒢⇩1)` q'(3)
      by (force simp: ta_states_def r_states_def)
    then have "qs ! i ∈ ta_res (fst 𝒢⇩1) (ts ! i)"
      using q'(4)[of i] Fun(1)[of "ts ! i" "qs ! i"] i by simp
  }
  ultimately show ?case using q'(4)
    by (auto intro!: exI[of _ qs] exI[of _ q'] simp: q'(3))
qed

lemma GTT_comp_second:
  assumes "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}" "q ∈ gtt_states 𝒢⇩2"
    "q ∈ ta_res (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
  shows "q ∈ ta_res (snd 𝒢⇩2) t"
  using assms GTT_comp_first[of q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1"] by (auto simp: ac_simps)

lemma gtt_comp_if:
  fixes s t :: "('f, 'q) term"
  assumes "gtt_accept (GTT_comp 𝒢⇩1 𝒢⇩2) s t" "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  shows "∃u. gtt_accept 𝒢⇩1 s u ∧ gtt_accept 𝒢⇩2 u t"
proof -
  let ?𝒢 = "GTT_comp 𝒢⇩1 𝒢⇩2"
  obtain C :: "('f, 'q) mctxt" and ss ts where st:
    "length ss = num_holes C" "length ts = num_holes C"
    "s = fill_holes C ss" "t = fill_holes C ts"
    "∀i < num_holes C. ∃q. q ∈ ta_res (fst ?𝒢) (ss ! i) ∧ q ∈ ta_res (snd ?𝒢) (ts ! i)"
    using gtt_accept'.cases[OF assms(1)[unfolded gtt_accept_equiv]] by metis
  { fix i
    define s where "s = ss ! i" define t where "t = ts ! i"
    assume i: "i < num_holes C"
    then obtain q where q: "q ∈ ta_res (fst ?𝒢) (ss ! i)" "q ∈ ta_res (snd ?𝒢) (ts ! i)"
      using st(5) by blast
    { (* prepare symmetric cases: q ∈ gtt_states 𝒢⇩1 and q ∈ gtt_states 𝒢⇩2 *)
      fix 𝒢⇩1 𝒢⇩2 s t assume as2: "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
        and 1: "q ∈ ta_res (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s"
          "q ∈ ta_res (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q ∈ gtt_states 𝒢⇩1"
      have sq: "q ∈ ta_res (fst 𝒢⇩1) s" using GTT_comp_first[OF 1(1,3) as2] .
      moreover have "∃u. q ∈ ta_res (snd 𝒢⇩1) u ∧ gtt_accept 𝒢⇩2 u t" using 1(2,3)
      proof (induct t arbitrary: s q)
        case (Var q')
        have *: "(q', q) ∈ (ta_eps (snd (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" using Var by simp
        show ?case using Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of q' q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1"]
        proof (cases, goal_cases)
          case 2 then show ?case using Var
            by (metis (no_types, lifting) UnI2 * fst_swap gtt_states_comp_union snd_swap subsetCE sup_commute
              ta_eps_non_state_imp_eq ta_res_vars_states term.set_intros(3))
        next
          case (5 p p') then show ?case
            by (auto simp: Δ⇩ε_def)  (metis join mem_Collect_eq ta_res.simps(1) ta_res_eps)+
        next
          case 6
          then show ?case by (auto intro!: exI[of _ "Var q'"])
        qed (insert as2 Var(2), auto simp: * ac_simps)
      next
        case (Fun f ts)
        obtain q' qs where q': "f qs → q' ∈ ta_rules (snd (GTT_comp 𝒢⇩1 𝒢⇩2))"
          "(q', q) ∈ (ta_eps (snd (GTT_comp 𝒢⇩1 𝒢⇩2)))⇧*" "length qs = length ts"
          "⋀i. i < length ts ⟹ qs ! i ∈ ta_res (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (ts ! i)"
          using Fun(2) by auto
        show ?case using Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of q' q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1"]
        proof (cases, goal_cases)
          case 1 then show ?case using q'(2) by simp
        next
          case 2 then show ?case
            by (smt Un_subset_iff fst_swap gtt_states_comp_union q'(1) r_rhs_states snd_swap subsetCE sup_commute)
        next
          case (5 p p')
          have "q' ∈ ta_res (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (Fun f ts)"
            using q'(1,3,4) by auto
          then show ?case using 5(3-5) by (auto simp: Δ⇩ε_def)
            (metis 5(1) GTT_comp_second ‹q' ∈ ta_res (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (Fun f ts)› as2 fst_swap
            join snd_swap sup_commute ta_res_eps)+
        next
          case 6
          have *: "f qs → q' ∈ ta_rules (snd 𝒢⇩1)"
            using 6(1) q'(1) as2 by (auto simp: GTT_comp_def dest: r_rhs_states)
          moreover then have "i < length qs ⟹ qs ! i ∈ gtt_states 𝒢⇩1" for i
            by (force simp: ta_states_def r_states_def)
          moreover then have "i < length qs ⟹ ∃u. qs ! i ∈ ta_res (snd 𝒢⇩1) u ∧ gtt_accept 𝒢⇩2 u (ts ! i)" for i
            using Fun(1)[of "ts ! i" "qs ! i"] i by (simp add: q'(3,4))
          then obtain us where
            "⋀i. i < length qs ⟹ qs ! i ∈ ta_res (snd 𝒢⇩1) (us i) ∧ gtt_accept 𝒢⇩2 (us i) (ts ! i)"
            by metis
          moreover have "(q', q) ∈ (ta_eps (snd 𝒢⇩1))⇧*" using 6(2) by simp
          ultimately show ?case using q'(1)
            by (intro exI[of _ "Fun f (map us [0..<length ts])"])
              (auto simp: q'(3)[symmetric])
        qed (insert as2 Fun(3) q'(2), auto)
      qed
      ultimately have "∃u. gtt_accept 𝒢⇩1 s u ∧ gtt_accept 𝒢⇩2 u t" by auto
    } note base = this
    consider "q ∈ gtt_states 𝒢⇩1" | "q ∈ gtt_states 𝒢⇩2" | "q ∉ gtt_states 𝒢⇩1 ∪ gtt_states 𝒢⇩2"
      by blast
    then have "∃u. gtt_accept 𝒢⇩1 (ss ! i) u ∧ gtt_accept 𝒢⇩2 u (ts ! i)"
      using q unfolding s_def[symmetric] t_def[symmetric]
    proof (cases, goal_cases)
      case 1 then show ?case using base[of 𝒢⇩1 𝒢⇩2 s t] assms(2) by simp
    next
      case 2 then show ?case using base[of "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1" t s] assms(2) by auto
    next
      case 3 then show ?case using subsetD[OF gtt_states_comp_union[of 𝒢⇩1 𝒢⇩2], of q]
        ta_res_not_state_imp_Var[OF _ 3(1)] ta_res_not_state_imp_Var[OF _ 3(2)]
        by (intro exI[of _ "Var q"]) (simp, metis gtt_accept.refl)
    qed
  }
  then obtain us where
    "⋀i. i < num_holes C ⟹ gtt_accept 𝒢⇩1 (ss ! i) (us i) ∧ gtt_accept 𝒢⇩2 (us i) (ts ! i)" by metis
  then show ?thesis unfolding gtt_accept_equiv st(3,4) using st(1,2)
    by (auto intro!: exI[of _ "fill_holes C (map us [0..<num_holes C])"] accept'_closed_ctxt)
qed

lemma gtt_accept_vars_states:
  assumes "gtt_accept 𝒢 s t"
  shows "vars_term s ⊆ vars_term t ∪ gtt_states 𝒢"
proof -
  obtain C ss ts where st:
    "length ss = num_holes C" "length ts = num_holes C"
    "s = fill_holes C ss" "t = fill_holes C ts"
    "∀i < num_holes C. ∃q. q ∈ ta_res (fst 𝒢) (ss ! i) ∧ q ∈ ta_res (snd 𝒢) (ts ! i)"
    using gtt_accept'.cases[OF assms(1)[unfolded gtt_accept_equiv]] by metis
  { fix s assume "s ∈ set ss"
    then obtain i where i: "i < num_holes C" "s = ss ! i" using st(1) in_set_conv_nth by metis
    obtain q where q: "q ∈ ta_res (fst 𝒢) (ss ! i)" "q ∈ ta_res (snd 𝒢) (ts ! i)"
      using st(5) i(1) by blast
    then consider "q ∈ ta_states (fst 𝒢)" | "q ∈ ta_states (snd 𝒢)" | "vars_term (ss ! i) ⊆ vars_term (ts ! i)"
      by (metis ta_res_not_state_imp_Var eq_iff)
    then have "vars_term s ⊆ vars_term t ∪ gtt_states 𝒢"
    proof cases
      case 1 then show ?thesis using q ta_res_vars_states[of q "fst 𝒢" s] by (auto simp: i st(1))
    next
      case 2 then show ?thesis using q ta_res_vars_states[of q "snd 𝒢" "ts ! i"]
        by (auto simp: i st vars_term_fill_holes')
          (metis (no_types, lifting) singletonD subsetCE ta_res_not_state_imp_Var ta_res_vars_states term.set(3))
    next
      case 3 then show ?thesis using i st
        by (auto simp: i st vars_term_fill_holes' dest!: subsetD) (auto simp: i st(2))
    qed
  }
  then show ?thesis unfolding st(3,4) by (auto simp: vars_term_fill_holes' st(1,2))
qed

lemma gtt_comp_ground:
  assumes "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
    "gtt_accept 𝒢⇩1 s u" "gtt_accept 𝒢⇩2 u t" "ground s" "ground t"
  shows "ground u"
  using assms(1,4,5) gtt_accept_vars_states[of "prod.swap 𝒢⇩1" u s] gtt_accept_vars_states[of "𝒢⇩2" u t]
  by (auto simp: assms(2,3) ground_vars_term_empty)

lemma gtt_comp_lang_complete:
  shows "gtt_lang 𝒢⇩1 O gtt_lang 𝒢⇩2 ⊆ gtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2)"
  using gtt_comp_only_if [[show_types]] by blast

lemma gtt_comp_lang:
  assumes "gtt_states 𝒢⇩1 ∩ gtt_states 𝒢⇩2 = {}"
  shows "gtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) = gtt_lang 𝒢⇩1 O gtt_lang 𝒢⇩2"
  using gtt_comp_if[OF _ assms] gtt_comp_ground[OF assms]
  by (intro equalityI gtt_comp_lang_complete) blast

end