Theory Regular_Tree_Relations.GTT_Compose

theory GTT_Compose
  imports GTT
begin

subsection ‹GTT closure under composition›

inductive_set Δ⇩ε_set :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) set" for 𝒜 ℬ where
  Δ⇩ε_set_cong: "TA_rule f ps p |∈| rules 𝒜 ⟹ TA_rule f qs q |∈| rules ℬ ⟹ length ps = length qs ⟹
   (⋀i. i < length qs ⟹ (ps ! i, qs ! i) ∈ Δ⇩ε_set 𝒜 ℬ) ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ"
| Δ⇩ε_set_eps1: "(p, p') |∈| eps 𝒜 ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ ⟹ (p', q) ∈ Δ⇩ε_set 𝒜 ℬ"
| Δ⇩ε_set_eps2: "(q, q') |∈| eps ℬ ⟹ (p, q) ∈ Δ⇩ε_set 𝒜 ℬ ⟹ (p, q') ∈ Δ⇩ε_set 𝒜 ℬ"

lemma Δ⇩ε_states: "Δ⇩ε_set 𝒜 ℬ ⊆ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
proof -
  {fix p q assume "(p, q) ∈ Δ⇩ε_set 𝒜 ℬ" then have "(p, q) ∈ fset (𝒬 𝒜 |×| 𝒬 ℬ)"
      by (induct) (auto dest: rule_statesD eps_statesD)}
  then show ?thesis by auto
qed

lemma finite_Δ⇩ε [simp]: "finite (Δ⇩ε_set 𝒜 ℬ)"
  using finite_subset[OF Δ⇩ε_states]
  by simp

context
includes fset.lifting
begin
lift_definition Δ⇩ε :: "('q, 'f) ta ⇒ ('q, 'f) ta ⇒ ('q × 'q) fset" is Δ⇩ε_set by simp
lemmas Δ⇩ε_cong = Δ⇩ε_set_cong [Transfer.transferred]
lemmas Δ⇩ε_eps1 = Δ⇩ε_set_eps1 [Transfer.transferred]
lemmas Δ⇩ε_eps2 = Δ⇩ε_set_eps2 [Transfer.transferred]
lemmas Δ⇩ε_cases = Δ⇩ε_set.cases[Transfer.transferred]
lemmas Δ⇩ε_induct [consumes 1, case_names Δ⇩ε_cong Δ⇩ε_eps1  Δ⇩ε_eps2] = Δ⇩ε_set.induct[Transfer.transferred]
lemmas Δ⇩ε_intros = Δ⇩ε_set.intros[Transfer.transferred]
lemmas Δ⇩ε_simps = Δ⇩ε_set.simps[Transfer.transferred]
end

lemma finite_alt_def [simp]:
  "finite {(α, β). (∃t. ground t ∧ α |∈| ta_der 𝒜 t ∧ β |∈| ta_der ℬ t)}" (is "finite ?S")
  by (auto dest: ground_ta_der_states[THEN fsubsetD]
           intro!: finite_subset[of ?S "fset (𝒬 𝒜 |×| 𝒬 ℬ)"])

lemma Δ⇩ε_def':
  "Δ⇩ε 𝒜 ℬ = {|(α, β). (∃t. ground t ∧ α |∈| ta_der 𝒜 t ∧ β |∈| ta_der ℬ t)|}"
proof (intro fset_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
  have "∃t. ground t ∧ p |∈| ta_der 𝒜 t ∧ q |∈| ta_der ℬ t" using lr unfolding x
  proof (induct rule: Δ⇩ε_induct)
    case (Δ⇩ε_cong f ps p qs q)
    obtain ts where ts: "ground (ts i) ∧ ps ! i |∈| ta_der 𝒜 (ts i) ∧ qs ! i |∈| ta_der ℬ (ts i)"
      if "i < length qs" for i using Δ⇩ε_cong(5) by metis
    then show ?case using Δ⇩ε_cong(1-3)
      by (auto intro!: exI[of _ "Fun f (map ts [0..<length qs])"]) blast+
  qed (meson ta_der_eps)+
  then show ?case by auto
next
  case (rl x) obtain p q where x [simp]: "x = (p, q)" by (cases x)
  obtain t where "ground t" "p |∈| ta_der 𝒜 t" "q |∈| ta_der ℬ t" using rl by auto
  then show ?case unfolding x
  proof (induct t arbitrary: p q)
    case (Fun f ts)
    obtain p' ps where p': "TA_rule f ps p' |∈| rules 𝒜" "p' = p ∨ (p', p) |∈| (eps 𝒜)|⇧+|" "length ps = length ts"
      "⋀i. i < length ts ⟹ ps ! i |∈| ta_der 𝒜 (ts ! i)" using Fun(3) by auto
    obtain q' qs where q': "f qs → q' |∈| rules ℬ" "q' = q ∨ (q', q) |∈| (eps ℬ)|⇧+|" "length qs = length ts"
      "⋀i. i < length ts ⟹ qs ! i |∈| ta_der ℬ (ts ! i)" using Fun(4) by auto
    have st: "(p', q') |∈| Δ⇩ε 𝒜 ℬ"
      using Fun(1)[OF nth_mem _ p'(4) q'(4)] Fun(2) p'(3) q'(3)
      by (intro Δ⇩ε_cong[OF p'(1) q'(1)]) auto
    {assume "(p', p) |∈| (eps 𝒜)|⇧+|" then have "(p, q') |∈| Δ⇩ε 𝒜 ℬ" using st
        by (induct rule: ftrancl_induct) (auto intro: Δ⇩ε_eps1)}
    from st this p'(2) have st: "(p, q') |∈| Δ⇩ε 𝒜 ℬ" by auto
   {assume "(q', q) |∈| (eps ℬ)|⇧+|" then have "(p, q) |∈| Δ⇩ε 𝒜 ℬ" using st
        by (induct rule: ftrancl_induct) (auto intro: Δ⇩ε_eps2)}
    from st this q'(2) show "(p, q) |∈| Δ⇩ε 𝒜 ℬ" by auto
  qed auto
qed

lemma Δ⇩ε_fmember:
  "(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟷ (∃t. ground t ∧ p |∈| ta_der 𝒜 t ∧ q |∈| ta_der ℬ t)"
  by (auto simp: Δ⇩ε_def')

definition GTT_comp :: "('q, 'f) gtt ⇒ ('q, 'f) gtt ⇒ ('q, 'f) gtt" where
  "GTT_comp 𝒢⇩1 𝒢⇩2 =
    (let Δ = Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2) in
    (TA (gtt_rules (fst 𝒢⇩1, fst 𝒢⇩2)) (eps (fst 𝒢⇩1) |∪| eps (fst 𝒢⇩2) |∪| Δ),
     TA (gtt_rules (snd 𝒢⇩1, snd 𝒢⇩2)) (eps (snd 𝒢⇩1) |∪| eps (snd 𝒢⇩2) |∪| (Δ|¯|))))"

lemma gtt_syms_GTT_comp:
  "gtt_syms (GTT_comp A B) = gtt_syms A |∪| gtt_syms B"
  by (auto simp: GTT_comp_def ta_sig_def Let_def)

lemma Δ⇩ε_statesD:
  "(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟹ p |∈| 𝒬 𝒜"
  "(p, q) |∈| Δ⇩ε 𝒜 ℬ ⟹ q |∈| 𝒬 ℬ"
  using subsetD[OF Δ⇩ε_states, of "(p, q)" 𝒜 ℬ]
  by (auto simp flip: Δ⇩ε.rep_eq)

lemma Δ⇩ε_statesD':
  "q |∈| eps_states (Δ⇩ε 𝒜 ℬ) ⟹ q |∈| 𝒬 𝒜 |∪| 𝒬 ℬ"
  by (auto simp: eps_states_def dest: Δ⇩ε_statesD)

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

lemma Δ⇩ε_inverse [simp]:
  "(Δ⇩ε 𝒜 ℬ)|¯| = Δ⇩ε ℬ 𝒜"
  by (auto simp: Δ⇩ε_def')


lemma gtt_states_comp_union:
  "gtt_states (GTT_comp 𝒢⇩1 𝒢⇩2) |⊆| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
proof (intro fsubsetI, goal_cases lr)
  case (lr q) then show ?case
    by (auto simp: GTT_comp_def gtt_states_def 𝒬_def dest: Δ⇩ε_statesD')
qed

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_complete_semi:
  assumes s: "q |∈| gta_der (fst 𝒢⇩1) s" and u: "q |∈| gta_der (snd 𝒢⇩1) u" and ut: "gtt_accept 𝒢⇩2 u t"
  shows "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
proof (goal_cases L R)
  let ?𝒢 = "GTT_comp 𝒢⇩1 𝒢⇩2"
  have  sub1l: "rules (fst 𝒢⇩1) |⊆| rules (fst ?𝒢)" "eps (fst 𝒢⇩1) |⊆| eps (fst ?𝒢)"
    and sub1r: "rules (snd 𝒢⇩1) |⊆| rules (snd ?𝒢)" "eps (snd 𝒢⇩1) |⊆| eps (snd ?𝒢)" 
    and sub2r: "rules (snd 𝒢⇩2) |⊆| rules (snd ?𝒢)" "eps (snd 𝒢⇩2) |⊆| eps (snd ?𝒢)"
    by (auto simp: GTT_comp_def)
  { case L then show ?case using s ta_der_mono[OF sub1l]
      by (auto simp: gta_der_def)
  next
    case R then show ?case using ut u unfolding gtt_accept_def
    proof (induct arbitrary: q s)
      case (base s t)
      from base(1) obtain p where p: "p |∈| gta_der (fst 𝒢⇩2) s" "p |∈| gta_der (snd 𝒢⇩2) t"
        by (auto simp: agtt_lang_def)
      then have "(p, q) |∈| eps (snd (GTT_comp 𝒢⇩1 𝒢⇩2))"
        using Δ⇩ε_fmember[of p q "fst 𝒢⇩2" "snd 𝒢⇩1"] base(2)
        by (auto simp: GTT_comp_def gta_der_def)
      from ta_der_eps[OF this] show ?case using p ta_der_mono[OF sub2r]
        by (auto simp add: gta_der_def)
    next
      case (step ss ts f)
      from step(1, 4) obtain ps p where "TA_rule f ps p |∈| rules (snd 𝒢⇩1)" "p = q ∨ (p, q) |∈| (eps (snd 𝒢⇩1))|⇧+|"
        "length ps = length ts" "⋀i. i < length ts ⟹ ps ! i |∈| gta_der (snd 𝒢⇩1) (ss ! i)"
        unfolding gta_der_def by auto
      then show ?case using step(1, 2) sub1r(1) ftrancl_mono[OF _ sub1r(2)]
        by (auto simp: gta_der_def intro!: exI[of _ p] exI[of _ ps])
    qed}
qed

lemmas gtt_comp_complete_semi' = gtt_comp_complete_semi[of _ "prod.swap 𝒢⇩2" _ _ "prod.swap 𝒢⇩1" for 𝒢⇩1 𝒢⇩2,
  unfolded fst_swap snd_swap GTT_comp_swap gtt_accept_swap]

lemma gtt_comp_acomplete:
  "gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2) ⊆ agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2)"
proof (intro subrelI, goal_cases LR)
  case (LR s t)
  then consider
      q u where "q |∈| gta_der (fst 𝒢⇩1) s" "q |∈| gta_der (snd 𝒢⇩1) u" "gtt_accept 𝒢⇩2 u t"
    | q u where "q |∈| gta_der (snd 𝒢⇩2) t" "q |∈| gta_der (fst 𝒢⇩2) u" "gtt_accept 𝒢⇩1 s u"
    by (auto simp: gcomp_rel_def gtt_accept_def elim!: agtt_langE)
  then show ?case
  proof (cases)
    case 1 show ?thesis using gtt_comp_complete_semi[OF 1]
      by (auto simp: agtt_lang_def gta_der_def)
  next
    case 2 show ?thesis using gtt_comp_complete_semi'[OF 2]
      by (auto simp: agtt_lang_def gta_der_def)
  qed
qed

lemma Δ⇩ε_steps_from_𝒢⇩2:
  assumes "(q, q') |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "q |∈| gtt_states 𝒢⇩2"
    "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  shows "(q, q') |∈| (eps (fst 𝒢⇩2))|⇧+| ∧ q' |∈| gtt_states 𝒢⇩2"
  using assms(1-2)
proof (induct rule: converse_ftrancl_induct)
  case (Base y)
  then show ?case using assms(3)
    by (fastforce simp: GTT_comp_def gtt_states_def dest: eps_statesD Δ⇩ε_statesD(1))
next
  case (Step q p)
  have "(q, p) |∈| (eps (fst 𝒢⇩2))|⇧+|" "p |∈| gtt_states 𝒢⇩2"
    using Step(1, 4) assms(3)
    by (auto simp: GTT_comp_def gtt_states_def dest: eps_statesD Δ⇩ε_statesD(1))
  then show ?case using Step(3)
    by (auto intro: ftrancl_trans)
qed

lemma Δ⇩ε_steps_from_𝒢⇩1:
  assumes "(p, r) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "p |∈| gtt_states 𝒢⇩1"
    "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  obtains "r |∈| gtt_states 𝒢⇩1" "(p, r) |∈| (eps (fst 𝒢⇩1))|⇧+|"
  | q p' where "r |∈| gtt_states 𝒢⇩2" "p = p' ∨ (p, p') |∈| (eps (fst 𝒢⇩1))|⇧+|" "(p', q) |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)"
    "q = r ∨ (q, r) |∈| (eps (fst 𝒢⇩2))|⇧+|"
  using assms(1,2)
proof (induct arbitrary: thesis rule: converse_ftrancl_induct)
  case (Base p)
  from Base(1) consider (a) "(p, r) |∈| eps (fst 𝒢⇩1)" | (b) "(p, r) |∈| eps (fst 𝒢⇩2)" |
    (c) "(p, r) |∈| (Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2))"
    by (auto simp: GTT_comp_def)
  then show ?case using assms(3) Base
    by cases (auto simp: GTT_comp_def gtt_states_def dest: eps_statesD Δ⇩ε_statesD)
next
  case (Step q p)
  consider "(q, p) |∈| (eps (fst 𝒢⇩1))|⇧+|" "p |∈| gtt_states 𝒢⇩1"
    | "(q, p) |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "p |∈| gtt_states 𝒢⇩2" using assms(3) Step(1, 6)
    by (auto simp: GTT_comp_def gtt_states_def dest: eps_statesD Δ⇩ε_statesD)
  then show ?case
  proof (cases)
    case 1 note a = 1 show ?thesis
    proof (cases rule: Step(3))
      case (2 p' q)
      then show ?thesis using assms a
        by (auto intro: Step(5) ftrancl_trans)
    qed (auto simp: a(2) intro: Step(4) ftrancl_trans[OF a(1)])
  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

lemma Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2:
  assumes "(q, q') |∈| (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') |∈| (eps (fst 𝒢⇩1))|⇧+|"
  | p p' where "q |∈| gtt_states 𝒢⇩1" "q' |∈| gtt_states 𝒢⇩2" "q = p ∨ (q, p) |∈| (eps (fst 𝒢⇩1))|⇧+|"
    "(p, p') |∈| Δ⇩ε (snd 𝒢⇩1) (fst 𝒢⇩2)" "p' = q' ∨ (p', q') |∈| (eps (fst 𝒢⇩2))|⇧+|"
  | "q |∈| gtt_states 𝒢⇩2" "(q, q') |∈| (eps (fst 𝒢⇩2))|⇧+| ∧ q' |∈| gtt_states 𝒢⇩2"
  using assms Δ⇩ε_steps_from_𝒢⇩1 Δ⇩ε_steps_from_𝒢⇩2
  by (metis funion_iff)

lemma GTT_comp_eps_fst_statesD:
  "(p, q) |∈| eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) ⟹ p |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
  "(p, q) |∈| eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) ⟹ q |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
  by (auto simp: GTT_comp_def gtt_states_def dest: eps_statesD Δ⇩ε_statesD)

lemma GTT_comp_eps_ftrancl_fst_statesD:
  "(p, q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+| ⟹ p |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
  "(p, q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+| ⟹ q |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2"
  using GTT_comp_eps_fst_statesD[of _ _ 𝒢⇩1 𝒢⇩2]
  by (meson converse_ftranclE ftranclE)+

lemma GTT_comp_first:
  assumes "q |∈| ta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q |∈| gtt_states 𝒢⇩1"
    "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  shows "q |∈| ta_der (fst 𝒢⇩1) t"
  using assms(1,2)
proof (induct t arbitrary: q)
  case (Var q')
  have "q ≠ q' ⟹ q' |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" using Var
    by (auto dest: GTT_comp_eps_ftrancl_fst_statesD)
  then show ?case using Var assms(3)
    by (auto elim: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2)
next
  case (Fun f ts)
  obtain q' qs where q': "TA_rule f qs q' |∈| rules (fst (GTT_comp 𝒢⇩1 𝒢⇩2))"
    "q' = q ∨ (q', q) |∈| (eps (fst (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" "length qs = length ts"
    "⋀i. i < length ts ⟹ qs ! i |∈| ta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) (ts ! i)"
    using Fun(2) by auto
  have "q' |∈| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" using q'(1)
    by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
  then have st: "q' |∈| gtt_states 𝒢⇩1" and eps:"q' = q ∨ (q', q) |∈| (eps (fst 𝒢⇩1))|⇧+|"
    using q'(2) Fun(3) assms(3)
    by (auto elim!: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2)
  from st have rule: "TA_rule f qs q' |∈| rules (fst 𝒢⇩1)" using assms(3) q'(1)
    by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
  have "i < length ts ⟹ qs ! i |∈| ta_der (fst 𝒢⇩1) (ts ! i)" for i
    using rule q'(3, 4)
    by (intro Fun(1)[OF nth_mem]) (auto simp: gtt_states_def dest!: rule_statesD(4))
  then show ?case using q'(3) rule eps
    by auto
qed

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

lemma gtt_comp_sound_semi:
  fixes 𝒢⇩1 𝒢⇩2 :: "('f, 'q) gtt"
  assumes as2: "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  and 1: "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t" "q |∈| gtt_states 𝒢⇩1"
  shows "∃u. q |∈| gta_der (snd 𝒢⇩1) u ∧ gtt_accept 𝒢⇩2 u t" using 1(2,3) unfolding gta_der_def
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  show ?case
  proof (cases "p |∈| gtt_states 𝒢⇩1")
    case True
    then have *: "TA_rule f ps p |∈| rules (snd 𝒢⇩1)" using GFun(1, 6) as2
      by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
    moreover have st: "i < length ps ⟹ ps ! i |∈| gtt_states 𝒢⇩1" for i using *
      by (force simp: gtt_states_def dest: rule_statesD)
    moreover have "i < length ps ⟹ ∃u. ps ! i |∈| ta_der (snd 𝒢⇩1) (term_of_gterm u) ∧ gtt_accept 𝒢⇩2 u (ts ! i)" for i
      using st GFun(2) by (intro GFun(5)) simp
    then obtain us where
      "⋀i. i < length ps ⟹ ps ! i |∈| ta_der (snd 𝒢⇩1) (term_of_gterm (us i)) ∧ gtt_accept 𝒢⇩2 (us i) (ts ! i)"
      by metis
    moreover have "p = q ∨ (p, q) |∈| (eps (snd 𝒢⇩1))|⇧+|" using GFun(3, 6) True as2
      by (auto simp: gtt_states_def  elim!: Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of p q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1", simplified])
    ultimately show ?thesis using GFun(2)
      by (intro exI[of _ "GFun f (map us [0..<length ts])"])
         (auto simp: gtt_accept_def intro!: exI[of _ ps] exI[of _ p])
  next
    case False note nt_st = this
    then have False: "p ≠ q" using GFun(6) by auto
    then have eps: "(p, q) |∈| (eps (snd (GTT_comp 𝒢⇩1 𝒢⇩2)))|⇧+|" using GFun(3) by simp
    show ?thesis using Δ⇩ε_steps_from_𝒢⇩1_𝒢⇩2[of p q "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1", simplified, OF eps]
    proof (cases, goal_cases)
      case 1 then show ?case using False GFun(3)
        by (metis GTT_comp_eps_ftrancl_fst_statesD(1) GTT_comp_swap fst_swap funion_iff)
    next
      case 2 then show ?case using as2 by (auto simp: gtt_states_def)
    next
      case 3 then show ?case using as2 GFun(6) by (auto simp: gtt_states_def)
    next
      case (4 r p')
      have meet: "r |∈| ta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (Fun f (map term_of_gterm ts))"
        using GFun(1 - 4) 4(3) False
        by (auto simp: GTT_comp_def in_ftrancl_UnI intro!: exI[ of _ ps] exI[ of _ p])
      then obtain u where wit: "ground u" "p' |∈| ta_der (snd 𝒢⇩1) u" "r |∈| ta_der (fst 𝒢⇩2) u"
        using 4(4-) unfolding Δ⇩ε_def' by blast
      from wit(1, 3) have "gtt_accept 𝒢⇩2 (gterm_of_term u) (GFun f ts)"
        using GTT_comp_second[OF as2 _ meet] unfolding gtt_accept_def
        by (intro gmctxt_cl.base agtt_langI[of r])
           (auto simp add: gta_der_def gtt_states_def simp del: ta_der_Fun dest: ground_ta_der_states)
      then show ?case using 4(5) wit(1, 2)
        by (intro exI[of _ "gterm_of_term u"]) (auto simp add: ta_der_trancl_eps)
    next
      case 5
      then show ?case using nt_st as2
        by (simp add: gtt_states_def)  
    qed
  qed
qed

lemma gtt_comp_asound:
  assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  shows "agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) ⊆ gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
proof (intro subrelI, goal_cases LR)
  case (LR s t)
  obtain q where q: "q |∈| gta_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) s" "q |∈| gta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) t"
    using LR by (auto simp: agtt_lang_def)
  { (* 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_der (fst (GTT_comp 𝒢⇩1 𝒢⇩2)) (term_of_gterm s)"
        "q |∈| ta_der (snd (GTT_comp 𝒢⇩1 𝒢⇩2)) (term_of_gterm t)" "q |∈| gtt_states 𝒢⇩1"
    note st = GTT_comp_first[OF 1(1,3) as2]
    obtain u where u: "q |∈| ta_der (snd 𝒢⇩1) (term_of_gterm u)" "gtt_accept 𝒢⇩2 u t"
      using gtt_comp_sound_semi[OF as2 1[folded gta_der_def]] by (auto simp: gta_der_def)
    have "(s, u) ∈ agtt_lang 𝒢⇩1" using st u(1)
      by (auto simp: agtt_lang_def gta_der_def)
    moreover have "(u, t) ∈ gtt_lang 𝒢⇩2" using u(2)
      by (auto simp: gtt_accept_def)
    ultimately have "(s, t) ∈ agtt_lang 𝒢⇩1 O gmctxt_cl UNIV (agtt_lang 𝒢⇩2)"
      by auto}
  note base = this
  consider "q |∈| gtt_states 𝒢⇩1" | "q |∈| gtt_states 𝒢⇩2" | "q |∉| gtt_states 𝒢⇩1 |∪| gtt_states 𝒢⇩2" by blast
  then show ?case using q assms
  proof (cases, goal_cases)
    case 1 then show ?case using base[of 𝒢⇩1 𝒢⇩2 s t]
      by (auto simp: gcomp_rel_def gta_der_def)
  next
    case 2 then show ?case using base[of "prod.swap 𝒢⇩2" "prod.swap 𝒢⇩1" t s, THEN converseI]
      by (auto simp: gcomp_rel_def converse_relcomp converse_agtt_lang gta_der_def gtt_states_def)
         (simp add: finter_commute funion_commute gtt_lang_swap prod.swap_def)+
  next
    case 3 then show ?case using fsubsetD[OF gtt_states_comp_union[of 𝒢⇩1 𝒢⇩2], of q]
      by (auto simp: gta_der_def gtt_states_def)
  qed
qed

lemma gtt_comp_lang_complete:
  shows "gtt_lang 𝒢⇩1 O gtt_lang 𝒢⇩2 ⊆ gtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2)"
  using gmctxt_cl_mono_rel[OF gtt_comp_acomplete, of UNIV 𝒢⇩1 𝒢⇩2]
  by (simp only: gcomp_rel[symmetric])

lemma gtt_comp_alang:
  assumes "gtt_states 𝒢⇩1 |∩| gtt_states 𝒢⇩2 = {||}"
  shows "agtt_lang (GTT_comp 𝒢⇩1 𝒢⇩2) = gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
  by (intro equalityI gtt_comp_asound[OF assms] gtt_comp_acomplete)

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"
  by (simp only: arg_cong[OF gtt_comp_alang[OF assms], of "gmctxt_cl UNIV"] gcomp_rel)

abbreviation GTT_comp' where
  "GTT_comp' 𝒢⇩1 𝒢⇩2 ≡ GTT_comp (fmap_states_gtt Inl 𝒢⇩1) (fmap_states_gtt Inr 𝒢⇩2)"

lemma gtt_comp'_alang:
  shows "agtt_lang (GTT_comp' 𝒢⇩1 𝒢⇩2) = gcomp_rel UNIV (agtt_lang 𝒢⇩1) (agtt_lang 𝒢⇩2)"
proof -
  have [simp]: "finj_on Inl (gtt_states 𝒢⇩1)" "finj_on Inr (gtt_states 𝒢⇩2)"
    by (auto simp add: finj_on.rep_eq)
  then show ?thesis                                        
    by (subst gtt_comp_alang) (auto simp: agtt_lang_fmap_states_gtt)
qed

end