# 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)"

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]
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
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)"