[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>2:
  assumes "(q, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|" "q |\<in>| gtt_states \<G>\<^sub>2"
    "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  shows "(q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using assms(1-2)
[PROOF STATE]
proof (prove)
using this:
(q, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
q |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
proof (induct rule: converse_ftrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
 2. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
case (Base y)
[PROOF STATE]
proof (state)
this:
(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
y |\<in>| gtt_states \<G>\<^sub>2

goal (2 subgoals):
 1. \<And>y. \<lbrakk>(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
 2. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
y |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
y |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
(y, q') |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
y |\<in>| gtt_states \<G>\<^sub>2
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (fastforce simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD \<Delta>\<^sub>\<epsilon>_statesD(1))
[PROOF STATE]
proof (state)
this:
(y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
case (Step q p)
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
(p, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (p, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
q |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
have "(q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|" "p |\<in>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| &&& p |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using Step(1, 4) assms(3)
[PROOF STATE]
proof (prove)
using this:
(q, p) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
q |\<in>| gtt_states \<G>\<^sub>2
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. (q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| &&& p |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD \<Delta>\<^sub>\<epsilon>_statesD(1))
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; z |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (z, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2; y |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (y, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using Step(3)
[PROOF STATE]
proof (prove)
using this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>2
p |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> (p, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (auto intro: ftrancl_trans)
[PROOF STATE]
proof (state)
this:
(q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1:
  assumes "(p, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|" "p |\<in>| gtt_states \<G>\<^sub>1"
    "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  obtains "r |\<in>| gtt_states \<G>\<^sub>1" "(p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|"
  | q p' where "r |\<in>| gtt_states \<G>\<^sub>2" "p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|" "(p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)"
    "q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
(p, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (induct arbitrary: thesis rule: converse_ftrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y thesis. \<lbrakk>(y, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Base p)
[PROOF STATE]
proof (state)
this:
(p, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = ?p' \<or> (p, ?p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (?p', ?q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); ?q = r \<or> (?q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
p |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. \<And>y thesis. \<lbrakk>(y, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from Base(1)
[PROOF STATE]
proof (chain)
picking this:
(p, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
[PROOF STEP]
consider (a) "(p, r) |\<in>| eps (fst \<G>\<^sub>1)" | (b) "(p, r) |\<in>| eps (fst \<G>\<^sub>2)" |
    (c) "(p, r) |\<in>| (\<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
(p, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (1 subgoal):
 1. \<lbrakk>(p, r) |\<in>| eps (fst \<G>\<^sub>1) \<Longrightarrow> thesis; (p, r) |\<in>| eps (fst \<G>\<^sub>2) \<Longrightarrow> thesis; (p, r) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: GTT_comp_def fmember.abs_eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(p, r) |\<in>| eps (fst \<G>\<^sub>1) \<Longrightarrow> ?thesis; (p, r) |\<in>| eps (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis; (p, r) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<And>y thesis. \<lbrakk>(y, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(p, r) |\<in>| eps (fst \<G>\<^sub>1) \<Longrightarrow> ?thesis; (p, r) |\<in>| eps (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis; (p, r) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(p, r) |\<in>| eps (fst \<G>\<^sub>1) \<Longrightarrow> ?thesis; (p, r) |\<in>| eps (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis; (p, r) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms(3) Base
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(p, r) |\<in>| eps (fst \<G>\<^sub>1) \<Longrightarrow> ?thesis; (p, r) |\<in>| eps (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis; (p, r) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
(p, r) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = ?p' \<or> (p, ?p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (?p', ?q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); ?q = r \<or> (?q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
p |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by cases (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD \<Delta>\<^sub>\<epsilon>_statesD)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Step q p)
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
(p, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
\<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (q, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; q = ?p' \<or> (q, ?p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (?p', ?q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); ?q = r \<or> (?q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
consider "(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|" "p |\<in>| gtt_states \<G>\<^sub>1"
    | "(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)" "p |\<in>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) Step(1, 6)
[PROOF STATE]
proof (prove)
using this:
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
(q, p) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD \<Delta>\<^sub>\<epsilon>_statesD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>y z thesis. \<lbrakk>(y, z) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); (z, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>thesis. \<lbrakk>\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (z, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; z = p' \<or> (z, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; z |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (y, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; y = p' \<or> (y, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; y |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. \<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note a = 1
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. \<lbrakk>(q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases rule: Step(3))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
 2. \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
 3. p |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
case (2 p' q)
[PROOF STATE]
proof (state)
this:
r |\<in>| gtt_states \<G>\<^sub>2
p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
(p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)
q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|

goal (3 subgoals):
 1. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
 2. \<And>p' q. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
 3. p |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r |\<in>| gtt_states \<G>\<^sub>2
p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
(p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)
q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r |\<in>| gtt_states \<G>\<^sub>2
p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
(p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)
q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms a
[PROOF STATE]
proof (prove)
using this:
r |\<in>| gtt_states \<G>\<^sub>2
p = p' \<or> (p, p') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
(p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)
q = r \<or> (q, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|
(p, r) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
(q__, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
p |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto intro: Step(5) ftrancl_trans)
[PROOF STATE]
proof (state)
this:
thesis

goal (2 subgoals):
 1. \<lbrakk>r |\<in>| gtt_states \<G>\<^sub>1; (p, r) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis
 2. p |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
qed (auto simp: a(2) intro: Step(4) ftrancl_trans[OF a(1)])
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)
p |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<lbrakk>(q, p) |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>2[OF Step(2) 2(2) assms(3)] Step(5)[OF _ _ 2(1)]
[PROOF STATE]
proof (prove)
using this:
(p, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> r |\<in>| gtt_states \<G>\<^sub>2
\<lbrakk>r |\<in>| gtt_states \<G>\<^sub>2; q = q \<or> (q, q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; p = r \<or> (p, r) |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1_\<G>\<^sub>2:
  assumes "(q, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|" "q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
    "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  obtains "q |\<in>| gtt_states \<G>\<^sub>1" "q' |\<in>| gtt_states \<G>\<^sub>1" "(q, q') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|"
  | p p' where "q |\<in>| gtt_states \<G>\<^sub>1" "q' |\<in>| gtt_states \<G>\<^sub>2" "q = p \<or> (q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|"
    "(p, p') |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2)" "p' = q' \<or> (p', q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|"
  | "q |\<in>| gtt_states \<G>\<^sub>2" "(q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1; q' |\<in>| gtt_states \<G>\<^sub>1; (q, q') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p p'. \<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1; q' |\<in>| gtt_states \<G>\<^sub>2; q = p \<or> (q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p, p') |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p' = q' \<or> (p', q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>q |\<in>| gtt_states \<G>\<^sub>2; (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1 \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>2
[PROOF STATE]
proof (prove)
using this:
(q, q') |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
\<lbrakk>(?p, ?r) |\<in>| (eps (fst (GTT_comp ?\<G>\<^sub>1 ?\<G>\<^sub>2)))|\<^sup>+|; ?p |\<in>| gtt_states ?\<G>\<^sub>1; gtt_states ?\<G>\<^sub>1 |\<inter>| gtt_states ?\<G>\<^sub>2 = {||}; \<lbrakk>?r |\<in>| gtt_states ?\<G>\<^sub>1; (?p, ?r) |\<in>| (eps (fst ?\<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis; \<And>q p'. \<lbrakk>?r |\<in>| gtt_states ?\<G>\<^sub>2; ?p = p' \<or> (?p, p') |\<in>| (eps (fst ?\<G>\<^sub>1))|\<^sup>+|; (p', q) |\<in>| \<Delta>\<^sub>\<epsilon> (snd ?\<G>\<^sub>1) (fst ?\<G>\<^sub>2); q = ?r \<or> (q, ?r) |\<in>| (eps (fst ?\<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>(?q, ?q') |\<in>| (eps (fst (GTT_comp ?\<G>\<^sub>1 ?\<G>\<^sub>2)))|\<^sup>+|; ?q |\<in>| gtt_states ?\<G>\<^sub>2; gtt_states ?\<G>\<^sub>1 |\<inter>| gtt_states ?\<G>\<^sub>2 = {||}\<rbrakk> \<Longrightarrow> (?q, ?q') |\<in>| (eps (fst ?\<G>\<^sub>2))|\<^sup>+| \<and> ?q' |\<in>| gtt_states ?\<G>\<^sub>2

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1; q' |\<in>| gtt_states \<G>\<^sub>1; (q, q') |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<And>p p'. \<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1; q' |\<in>| gtt_states \<G>\<^sub>2; q = p \<or> (q, p) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|; (p, p') |\<in>| \<Delta>\<^sub>\<epsilon> (snd \<G>\<^sub>1) (fst \<G>\<^sub>2); p' = q' \<or> (p', q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>q |\<in>| gtt_states \<G>\<^sub>2; (q, q') |\<in>| (eps (fst \<G>\<^sub>2))|\<^sup>+| \<and> q' |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis funion_iff)


[STATEMENT]
lemma GTT_comp_eps_fst_statesD:
  "(p, q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
  "(p, q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2) &&& ((p, q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def fmember.abs_eq dest: eps_statesD \<Delta>\<^sub>\<epsilon>_statesD)


[STATEMENT]
lemma GTT_comp_eps_ftrancl_fst_statesD:
  "(p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
  "(p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2) &&& ((p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2)
[PROOF STEP]
using GTT_comp_eps_fst_statesD[of _ _ \<G>\<^sub>1 \<G>\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
(?p, ?q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> ?p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
(?p, ?q) |\<in>| eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) \<Longrightarrow> ?q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. ((p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> p |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2) &&& ((p, q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+| \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2)
[PROOF STEP]
by (meson converse_ftranclE ftranclE)+


[STATEMENT]
lemma GTT_comp_first:
  assumes "q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t" "q |\<in>| gtt_states \<G>\<^sub>1"
    "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  shows "q |\<in>| ta_der (fst \<G>\<^sub>1) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) t
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) t
[PROOF STEP]
proof (induct t arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var x); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Var x)
 2. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
case (Var q')
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var q')
q |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var x); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Var x)
 2. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
have "q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using Var
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var q')
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (auto dest: GTT_comp_eps_ftrancl_fst_statesD)
[PROOF STATE]
proof (state)
this:
q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (2 subgoals):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var x); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Var x)
 2. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) (Var q')
[PROOF STEP]
using Var assms(3)
[PROOF STATE]
proof (prove)
using this:
q \<noteq> q' \<Longrightarrow> q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Var q')
q |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) (Var q')
[PROOF STEP]
by (auto elim: \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1_\<G>\<^sub>2)
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (fst \<G>\<^sub>1) (Var q')

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set ts; ?q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) ?x2a; ?q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> ?q |\<in>| ta_der (fst \<G>\<^sub>1) ?x2a
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f ts)
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
obtain q' qs where q': "TA_rule f qs q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))"
    "q' = q \<or> (q', q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|" "length qs = length ts"
    "\<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>qs q'. \<lbrakk>f qs \<rightarrow> q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); q' = q \<or> (q', q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; length qs = length ts; \<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Fun(2)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f ts)

goal (1 subgoal):
 1. (\<And>qs q'. \<lbrakk>f qs \<rightarrow> q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); q' = q \<or> (q', q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; length qs = length ts; \<And>i. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f qs \<rightarrow> q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
q' = q \<or> (q', q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
length qs = length ts
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! ?i)

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
have "q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
using q'(1)
[PROOF STATE]
proof (prove)
using this:
f qs \<rightarrow> q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (1 subgoal):
 1. q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
[PROOF STATE]
proof (state)
this:
q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
have st: "q' |\<in>| gtt_states \<G>\<^sub>1" and eps:"q' = q \<or> (q', q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|"
[PROOF STATE]
proof (prove)
using this:
q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. q' |\<in>| gtt_states \<G>\<^sub>1 &&& q' = q \<or> (q', q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
[PROOF STEP]
using q'(2) Fun(3) assms(3)
[PROOF STATE]
proof (prove)
using this:
q' |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
q' = q \<or> (q', q) |\<in>| (eps (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
q |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. q' |\<in>| gtt_states \<G>\<^sub>1 &&& q' = q \<or> (q', q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|
[PROOF STEP]
by (auto elim!: \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1_\<G>\<^sub>2)
[PROOF STATE]
proof (state)
this:
q' |\<in>| gtt_states \<G>\<^sub>1
q' = q \<or> (q', q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
from st
[PROOF STATE]
proof (chain)
picking this:
q' |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
have rule: "TA_rule f qs q' |\<in>| rules (fst \<G>\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
q' |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. f qs \<rightarrow> q' |\<in>| rules (fst \<G>\<^sub>1)
[PROOF STEP]
using assms(3) q'(1)
[PROOF STATE]
proof (prove)
using this:
q' |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
f qs \<rightarrow> q' |\<in>| rules (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))

goal (1 subgoal):
 1. f qs \<rightarrow> q' |\<in>| rules (fst \<G>\<^sub>1)
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
[PROOF STATE]
proof (state)
this:
f qs \<rightarrow> q' |\<in>| rules (fst \<G>\<^sub>1)

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
have "i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! i)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! i)
[PROOF STEP]
using rule q'(3, 4)
[PROOF STATE]
proof (prove)
using this:
f qs \<rightarrow> q' |\<in>| rules (fst \<G>\<^sub>1)
length qs = length ts
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (ts ! ?i)

goal (1 subgoal):
 1. i < length ts \<Longrightarrow> qs ! i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! i)
[PROOF STEP]
by (intro Fun(1)[OF nth_mem]) (auto simp: gtt_states_def dest!: rule_statesD(4))
[PROOF STATE]
proof (state)
this:
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! ?i)

goal (1 subgoal):
 1. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) x2a; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) x2a; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun x1a x2); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! ?i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! ?i)

goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun f ts)
[PROOF STEP]
using q'(3) rule eps
[PROOF STATE]
proof (prove)
using this:
?i < length ts \<Longrightarrow> qs ! ?i |\<in>| ta_der (fst \<G>\<^sub>1) (ts ! ?i)
length qs = length ts
f qs \<rightarrow> q' |\<in>| rules (fst \<G>\<^sub>1)
q' = q \<or> (q', q) |\<in>| (eps (fst \<G>\<^sub>1))|\<^sup>+|

goal (1 subgoal):
 1. q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun f ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (fst \<G>\<^sub>1) (Fun f ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GTT_comp_second:
  assumes "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}" "q |\<in>| gtt_states \<G>\<^sub>2"
    "q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t"
  shows "q |\<in>| ta_der (snd \<G>\<^sub>2) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| ta_der (snd \<G>\<^sub>2) t
[PROOF STEP]
using assms GTT_comp_first[of q "prod.swap \<G>\<^sub>2" "prod.swap \<G>\<^sub>1"]
[PROOF STATE]
proof (prove)
using this:
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>2
q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
\<lbrakk>q |\<in>| ta_der (fst (GTT_comp (prod.swap \<G>\<^sub>2) (prod.swap \<G>\<^sub>1))) ?t; q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}\<rbrakk> \<Longrightarrow> q |\<in>| ta_der (fst (prod.swap \<G>\<^sub>2)) ?t

goal (1 subgoal):
 1. q |\<in>| ta_der (snd \<G>\<^sub>2) t
[PROOF STEP]
by (auto simp: gtt_states_def)


[STATEMENT]
lemma gtt_comp_sound_semi:
  fixes \<G>\<^sub>1 \<G>\<^sub>2 :: "('f, 'q) gtt"
  assumes as2: "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  and 1: "q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s" "q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t" "q |\<in>| gtt_states \<G>\<^sub>1"
  shows "\<exists>u. q |\<in>| gta_der (snd \<G>\<^sub>1) u \<and> gtt_accept \<G>\<^sub>2 u t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. q |\<in>| gta_der (snd \<G>\<^sub>1) u \<and> gtt_accept \<G>\<^sub>2 u t
[PROOF STEP]
using 1(2,3)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<exists>u. q |\<in>| gta_der (snd \<G>\<^sub>1) u \<and> gtt_accept \<G>\<^sub>2 u t
[PROOF STEP]
unfolding gta_der_def
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm t)
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u t
[PROOF STEP]
proof (induct rule: ta_der_gterm_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f ts ps p q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); length ts = length ps; p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm (ts ! i)); \<And>i. \<lbrakk>i < length ts; ps ! i |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>u. ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! i); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case (GFun f ts ps p q)
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
length ts = length ps
p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm (ts ! ?i))
\<lbrakk>?i < length ts; ps ! ?i |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>u. ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! ?i)
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>f ts ps p q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)); length ts = length ps; p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|; \<And>i. i < length ts \<Longrightarrow> ps ! i |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm (ts ! i)); \<And>i. \<lbrakk>i < length ts; ps ! i |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>u. ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! i); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
proof (cases "p |\<in>| gtt_states \<G>\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
have *: "TA_rule f ps p |\<in>| rules (snd \<G>\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
[PROOF STEP]
using GFun(1, 6) as2
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states \<G>\<^sub>1
f ps \<rightarrow> p |\<in>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
q |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
[PROOF STEP]
by (auto simp: GTT_comp_def gtt_states_def dest: rule_statesD)
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
have st: "i < length ps \<Longrightarrow> ps ! i |\<in>| gtt_states \<G>\<^sub>1" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ps \<Longrightarrow> ps ! i |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)

goal (1 subgoal):
 1. i < length ps \<Longrightarrow> ps ! i |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
by (force simp: gtt_states_def dest: rule_statesD)
[PROOF STATE]
proof (state)
this:
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
have "i < length ps \<Longrightarrow> \<exists>u. ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! i)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ps \<Longrightarrow> \<exists>u. ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! i)
[PROOF STEP]
using st GFun(2)
[PROOF STATE]
proof (prove)
using this:
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1
length ts = length ps

goal (1 subgoal):
 1. i < length ps \<Longrightarrow> \<exists>u. ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! i)
[PROOF STEP]
by (intro GFun(5)) simp
[PROOF STATE]
proof (state)
this:
?i < length ps \<Longrightarrow> \<exists>u. ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! ?i)

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length ps \<Longrightarrow> \<exists>u. ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! ?i)
[PROOF STEP]
obtain us where
      "\<And>i. i < length ps \<Longrightarrow> ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us i)) \<and> gtt_accept \<G>\<^sub>2 (us i) (ts ! i)"
[PROOF STATE]
proof (prove)
using this:
?i < length ps \<Longrightarrow> \<exists>u. ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (ts ! ?i)

goal (1 subgoal):
 1. (\<And>us. (\<And>i. i < length ps \<Longrightarrow> ps ! i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us i)) \<and> gtt_accept \<G>\<^sub>2 (us i) (ts ! i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us ?i)) \<and> gtt_accept \<G>\<^sub>2 (us ?i) (ts ! ?i)

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us ?i)) \<and> gtt_accept \<G>\<^sub>2 (us ?i) (ts ! ?i)

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
have "p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
[PROOF STEP]
using GFun(3, 6) True as2
[PROOF STATE]
proof (prove)
using this:
p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
q |\<in>| gtt_states \<G>\<^sub>1
p |\<in>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
[PROOF STEP]
by (auto simp: gtt_states_def  elim!: \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1_\<G>\<^sub>2[of p q "prod.swap \<G>\<^sub>2" "prod.swap \<G>\<^sub>1", simplified])
[PROOF STATE]
proof (state)
this:
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|

goal (2 subgoals):
 1. p |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us ?i)) \<and> gtt_accept \<G>\<^sub>2 (us ?i) (ts ! ?i)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us ?i)) \<and> gtt_accept \<G>\<^sub>2 (us ?i) (ts ! ?i)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
using GFun(2)
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd \<G>\<^sub>1)
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| gtt_states \<G>\<^sub>1
?i < length ps \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm (us ?i)) \<and> gtt_accept \<G>\<^sub>2 (us ?i) (ts ! ?i)
p = q \<or> (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
length ts = length ps

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
by (intro exI[of _ "GFun f (map us [0..<length ts])"])
         (auto simp: gtt_accept_def intro!: exI[of _ ps] exI[of _ p])
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p |\<notin>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
note nt_st = this
[PROOF STATE]
proof (state)
this:
p |\<notin>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p |\<notin>| gtt_states \<G>\<^sub>1
[PROOF STEP]
have False: "p \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
p |\<notin>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
using GFun(6)
[PROOF STATE]
proof (prove)
using this:
p |\<notin>| gtt_states \<G>\<^sub>1
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<noteq> q

goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
[PROOF STEP]
have eps: "(p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q

goal (1 subgoal):
 1. (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
[PROOF STEP]
using GFun(3)
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|

goal (1 subgoal):
 1. (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|

goal (1 subgoal):
 1. p |\<notin>| gtt_states \<G>\<^sub>1 \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
using \<Delta>\<^sub>\<epsilon>_steps_from_\<G>\<^sub>1_\<G>\<^sub>2[of p q "prod.swap \<G>\<^sub>2" "prod.swap \<G>\<^sub>1", simplified, OF eps]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}; \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis; \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
proof (cases, goal_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
 2. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
 3. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 4. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 5. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
 2. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
 3. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 4. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 5. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
[PROOF STEP]
using False GFun(3)
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|

goal (1 subgoal):
 1. p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
[PROOF STEP]
by (metis GTT_comp_eps_ftrancl_fst_statesD(1) GTT_comp_swap fst_swap funion_iff)
[PROOF STATE]
proof (state)
this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2) \<or> p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)

goal (4 subgoals):
 1. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 4. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 4. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 4. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
[PROOF STEP]
using as2
[PROOF STATE]
proof (prove)
using this:
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}
[PROOF STEP]
by (auto simp: gtt_states_def)
[PROOF STATE]
proof (state)
this:
gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}

goal (3 subgoals):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
q |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
(p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|

goal (3 subgoals):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2); (p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 3. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
q |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
(p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
q |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
(p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
using as2 GFun(6)
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
q |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
(p, q) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
by (auto simp: gtt_states_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case (4 r p')
[PROOF STATE]
proof (state)
this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>2)
q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
p = r \<or> (p, r) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|
(r, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1)
p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|

goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
have meet: "r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))
[PROOF STEP]
using GFun(1 - 4) 4(3) False
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2))
length ts = length ps
p = q \<or> (p, q) |\<in>| (eps (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)))|\<^sup>+|
?i < length ts \<Longrightarrow> ps ! ?i |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm (ts ! ?i))
p = r \<or> (p, r) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|
p \<noteq> q

goal (1 subgoal):
 1. r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))
[PROOF STEP]
by (auto simp: GTT_comp_def in_ftrancl_UnI intro!: exI[ of _ ps] exI[ of _ p])
[PROOF STATE]
proof (state)
this:
r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))

goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))
[PROOF STEP]
obtain u where wit: "ground u" "p' |\<in>| ta_der (snd \<G>\<^sub>1) u" "r |\<in>| ta_der (fst \<G>\<^sub>2) u"
[PROOF STATE]
proof (prove)
using this:
r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>ground u; p' |\<in>| ta_der (snd \<G>\<^sub>1) u; r |\<in>| ta_der (fst \<G>\<^sub>2) u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 4(4-)
[PROOF STATE]
proof (prove)
using this:
r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))
(r, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1)
p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>ground u; p' |\<in>| ta_der (snd \<G>\<^sub>1) u; r |\<in>| ta_der (fst \<G>\<^sub>2) u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<Delta>\<^sub>\<epsilon>_def'
[PROOF STATE]
proof (prove)
using this:
r |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (Fun f (map term_of_gterm ts))
(r, p') |\<in>| {|(\<alpha>, \<beta>). \<exists>t. ground t \<and> \<alpha> |\<in>| ta_der (fst \<G>\<^sub>2) t \<and> \<beta> |\<in>| ta_der (snd \<G>\<^sub>1) t|}
p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>ground u; p' |\<in>| ta_der (snd \<G>\<^sub>1) u; r |\<in>| ta_der (fst \<G>\<^sub>2) u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ground u
p' |\<in>| ta_der (snd \<G>\<^sub>1) u
r |\<in>| ta_der (fst \<G>\<^sub>2) u

goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
from wit(1, 3)
[PROOF STATE]
proof (chain)
picking this:
ground u
r |\<in>| ta_der (fst \<G>\<^sub>2) u
[PROOF STEP]
have "gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)"
[PROOF STATE]
proof (prove)
using this:
ground u
r |\<in>| ta_der (fst \<G>\<^sub>2) u

goal (1 subgoal):
 1. gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)
[PROOF STEP]
using GTT_comp_second[OF as2 _ meet]
[PROOF STATE]
proof (prove)
using this:
ground u
r |\<in>| ta_der (fst \<G>\<^sub>2) u
r |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> r |\<in>| ta_der (snd \<G>\<^sub>2) (Fun f (map term_of_gterm ts))

goal (1 subgoal):
 1. gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)
[PROOF STEP]
unfolding gtt_accept_def
[PROOF STATE]
proof (prove)
using this:
ground u
r |\<in>| ta_der (fst \<G>\<^sub>2) u
r |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> r |\<in>| ta_der (snd \<G>\<^sub>2) (Fun f (map term_of_gterm ts))

goal (1 subgoal):
 1. (gterm_of_term u, GFun f ts) \<in> gtt_lang \<G>\<^sub>2
[PROOF STEP]
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)
[PROOF STATE]
proof (state)
this:
gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)

goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>2); q |\<in>| gtt_states (prod.swap \<G>\<^sub>1); p = pa \<or> (p, pa) |\<in>| (eps (snd \<G>\<^sub>2))|\<^sup>+|; (pa, p') |\<in>| \<Delta>\<^sub>\<epsilon> (fst \<G>\<^sub>2) (snd \<G>\<^sub>1); p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
 2. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
using 4(5) wit(1, 2)
[PROOF STATE]
proof (prove)
using this:
gtt_accept \<G>\<^sub>2 (gterm_of_term u) (GFun f ts)
p' = q \<or> (p', q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+|
ground u
p' |\<in>| ta_der (snd \<G>\<^sub>1) u

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
by (intro exI[of _ "gterm_of_term u"]) (auto simp add: ta_der_trancl_eps)
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal (1 subgoal):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
case 5
[PROOF STATE]
proof (state)
this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
(p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)

goal (1 subgoal):
 1. \<lbrakk>p |\<in>| gtt_states (prod.swap \<G>\<^sub>1); (p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)\<rbrakk> \<Longrightarrow> \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
(p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
(p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
using nt_st as2
[PROOF STATE]
proof (prove)
using this:
p |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
(p, q) |\<in>| (eps (snd \<G>\<^sub>1))|\<^sup>+| \<and> q |\<in>| gtt_states (prod.swap \<G>\<^sub>1)
p |\<notin>| gtt_states \<G>\<^sub>1
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. \<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)
[PROOF STEP]
by (simp add: gtt_states_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u. q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u) \<and> gtt_accept \<G>\<^sub>2 u (GFun f ts)

goal:
No subgoals!
[PROOF STEP]
qed