[STATEMENT]
lemma test_suite_to_io_finite :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
shows "finite (test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prs tps rd_targets atcs. T = Test_Suite prs tps rd_targets atcs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson test_suite.exhaust)
[PROOF STATE]
proof (state)
this:
T = Test_Suite prs tps rd_targets atcs

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = Test_Suite prs tps rd_targets atcs
[PROOF STEP]
obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs
implies_completeness T M m

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding implies_completeness_def
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs
Ex (implies_completeness_for_repetition_sets T M m)

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets
[PROOF STEP]
have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. implies_completeness (Test_Suite prs tps rd_targets atcs) M m
[PROOF STEP]
unfolding implies_completeness_def
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

goal (1 subgoal):
 1. Ex (implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m
[PROOF STEP]
have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M"
[PROOF STATE]
proof (prove)
using this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m

goal (1 subgoal):
 1. test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M
[PROOF STEP]
using test_suite_to_io_language
[PROOF STATE]
proof (prove)
using this:
implies_completeness (Test_Suite prs tps rd_targets atcs) M m
implies_completeness ?T ?M ?m \<Longrightarrow> test_suite_to_io ?M ?T \<subseteq> L ?M

goal (1 subgoal):
 1. test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
test_suite_to_io M (Test_Suite prs tps rd_targets atcs) \<subseteq> L M

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have f1: "(finite prs)"
  and  f2: "\<And> q p . q \<in> fst ` prs \<Longrightarrow> finite (rd_targets (q,p))"
  and  f3: "\<And> q q' . finite (atcs (q,q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite prs &&& (\<And>q p. q \<in> fst ` prs \<Longrightarrow> finite (rd_targets (q, p))) &&& (\<And>q q'. finite (atcs (q, q')))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
is_finite_test_suite T

goal (1 subgoal):
 1. finite prs &&& (\<And>q p. q \<in> fst ` prs \<Longrightarrow> finite (rd_targets (q, p))) &&& (\<And>q q'. finite (atcs (q, q')))
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close> is_finite_test_suite.simps
[PROOF STATE]
proof (prove)
using this:
finite prs \<and> (\<forall>q p. q \<in> fst ` prs \<longrightarrow> finite (rd_targets (q, p))) \<and> (\<forall>q q'. finite (atcs (q, q')))

goal (1 subgoal):
 1. finite prs &&& (\<And>q p. q \<in> fst ` prs \<Longrightarrow> finite (rd_targets (q, p))) &&& (\<And>q q'. finite (atcs (q, q')))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
finite prs
?q \<in> fst ` prs \<Longrightarrow> finite (rd_targets (?q, ?p))
finite (atcs (?q, ?q'))

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t1: "(initial M, initial_preamble M) \<in> prs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> prs
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs

goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> prs
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
(FSM.initial M, initial_preamble M) \<in> prs

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t2: "\<And> q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t3: "\<And> q1 q2 A d1 d2. (A, d1, d2) \<in> atcs (q1, q2) \<Longrightarrow> (A, d2, d1) \<in> atcs (q2, q1) \<and> is_separator M q1 q2 A d1 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q1 q2 A d1 d2. (A, d1, d2) \<in> atcs (q1, q2) \<Longrightarrow> (A, d2, d1) \<in> atcs (q2, q1) \<and> is_separator M q1 q2 A d1 d2
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
(?A, ?d1.0, ?d2.0) \<in> atcs (?q1.0, ?q2.0) \<Longrightarrow> (?A, ?d2.0, ?d1.0) \<in> atcs (?q2.0, ?q1.0) \<and> is_separator M ?q1.0 ?q2.0 ?A ?d1.0 ?d2.0

goal (1 subgoal):
 1. \<And>q1 q2 A d1 d2. (A, d1, d2) \<in> atcs (q1, q2) \<Longrightarrow> (A, d2, d1) \<in> atcs (q2, q1) \<and> is_separator M q1 q2 A d1 d2
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
(?A, ?d1.0, ?d2.0) \<in> atcs (?q1.0, ?q2.0) \<Longrightarrow> (?A, ?d2.0, ?d1.0) \<in> atcs (?q2.0, ?q1.0) \<and> is_separator M ?q1.0 ?q2.0 ?A ?d1.0 ?d2.0

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t5: "\<And>q. q \<in> FSM.states M \<Longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
?q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. ?q \<in> fst d

goal (1 subgoal):
 1. \<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
?q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. ?q \<in> fst d

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t6: "\<And> q. q \<in> fst ` prs \<Longrightarrow> tps q \<subseteq> {p1 . \<exists> p2 d . (p1@p2,d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<and> fst ` (m_traversal_paths_with_witness M q repetition_sets m) \<subseteq> tps q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M q repetition_sets m \<subseteq> tps q
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
?q \<in> fst ` prs \<Longrightarrow> tps ?q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M ?q repetition_sets m \<subseteq> tps ?q

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M q repetition_sets m \<subseteq> tps q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
?q \<in> fst ` prs \<Longrightarrow> tps ?q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M ?q repetition_sets m \<subseteq> tps ?q

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have t7: "\<And> d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M"
  and  t8: "\<And> d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d"
  and  t8':  "\<And> d. d \<in> set repetition_sets \<Longrightarrow> snd d = fst d \<inter> fst ` prs"
  and  t9: "\<And> d q1 q2. d \<in> set repetition_sets \<Longrightarrow> q1 \<in> fst d \<Longrightarrow> q2 \<in> fst d \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> atcs (q1, q2) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d)) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d = fst d \<inter> fst ` prs) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> atcs (q1, q2) \<noteq> {})
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M \<and> snd ?d = fst ?d \<inter> fst ` prs
\<lbrakk>?d \<in> set repetition_sets; ?q1.0 \<in> fst ?d; ?q2.0 \<in> fst ?d; ?q1.0 \<noteq> ?q2.0\<rbrakk> \<Longrightarrow> atcs (?q1.0, ?q2.0) \<noteq> {}

goal (1 subgoal):
 1. ((\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d)) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d = fst d \<inter> fst ` prs) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> atcs (q1, q2) \<noteq> {})
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M
?d \<in> set repetition_sets \<Longrightarrow> snd ?d \<subseteq> fst ?d
?d \<in> set repetition_sets \<Longrightarrow> snd ?d = fst ?d \<inter> fst ` prs
\<lbrakk>?d \<in> set repetition_sets; ?q1.0 \<in> fst ?d; ?q2.0 \<in> fst ?d; ?q1.0 \<noteq> ?q2.0\<rbrakk> \<Longrightarrow> atcs (?q1.0, ?q2.0) \<noteq> {}

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have f4: "\<And> q . q \<in> fst ` prs \<Longrightarrow> finite (tps q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
assume "q \<in> fst ` prs"
[PROOF STATE]
proof (state)
this:
q \<in> fst ` prs

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> fst ` prs
[PROOF STEP]
have "tps q \<subseteq> {p1 . \<exists> p2 d . (p1@p2,d) \<in> m_traversal_paths_with_witness M q repetition_sets m}"
[PROOF STATE]
proof (prove)
using this:
q \<in> fst ` prs

goal (1 subgoal):
 1. tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}
[PROOF STEP]
using t6
[PROOF STATE]
proof (prove)
using this:
q \<in> fst ` prs
?q \<in> fst ` prs \<Longrightarrow> tps ?q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M ?q repetition_sets m \<subseteq> tps ?q

goal (1 subgoal):
 1. tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
have "{p1 . \<exists> p2 d . (p1@p2,d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<subseteq> (\<Union> p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
fix p1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
assume "p1 \<in> {p1 . \<exists> p2 d . (p1@p2,d) \<in> m_traversal_paths_with_witness M q repetition_sets m}"
[PROOF STATE]
proof (state)
this:
p1 \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}

goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p1 \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}
[PROOF STEP]
obtain p2 d where "(p1@p2,d) \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}

goal (1 subgoal):
 1. (\<And>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
have "p1@p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
using this:
(p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. p1 @ p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
p1 @ p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p1 @ p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
have "p1 \<in> set (prefixes (p1@p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 \<in> set (prefixes (p1 @ p2))
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 \<in> {xs'. \<exists>xs''. xs' @ xs'' = p1 @ p2}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p1 \<in> set (prefixes (p1 @ p2))

goal (1 subgoal):
 1. \<And>x. x \<in> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<Longrightarrow> x \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p1 @ p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m
p1 \<in> set (prefixes (p1 @ p2))
[PROOF STEP]
show "p1 \<in> (\<Union> p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
[PROOF STATE]
proof (prove)
using this:
p1 @ p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m
p1 \<in> set (prefixes (p1 @ p2))

goal (1 subgoal):
 1. p1 \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p1 \<in> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}
{p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
have "tps q \<subseteq> (\<Union> p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
[PROOF STATE]
proof (prove)
using this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m}
{p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
have "finite (\<Union> p2 \<in> fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
have "finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)
[PROOF STEP]
using m_traversal_paths_with_witness_finite[of M q repetition_sets m]
[PROOF STATE]
proof (prove)
using this:
finite (m_traversal_paths_with_witness M q repetition_sets m)

goal (1 subgoal):
 1. finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)

goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)

goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
have "\<And> p2 . finite (set (prefixes p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p2. finite (set (prefixes p2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set (prefixes ?p2.0))

goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)
finite (set (prefixes ?p2.0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)
finite (set (prefixes ?p2.0))

goal (1 subgoal):
 1. finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
[PROOF STEP]
show "finite (tps q)"
[PROOF STATE]
proof (prove)
using this:
tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))

goal (1 subgoal):
 1. finite (tps q)
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
tps q \<subseteq> (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
finite (\<Union>p2\<in>fst ` m_traversal_paths_with_witness M q repetition_sets m. set (prefixes p2))
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (tps q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (tps q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q \<in> fst ` prs \<Longrightarrow> finite (tps ?q)

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?q \<in> fst ` prs \<Longrightarrow> finite (tps ?q)
[PROOF STEP]
have f4' : "\<And> q P . (q,P) \<in> prs \<Longrightarrow> finite (tps q)"
[PROOF STATE]
proof (prove)
using this:
?q \<in> fst ` prs \<Longrightarrow> finite (tps ?q)

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (tps q)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (tps ?q)

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
define T1 where T1_def : "T1 = (\<Union>(q, P)\<in>prs. L P)"
[PROOF STATE]
proof (state)
this:
T1 = (\<Union>(q, P)\<in>prs. L P)

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
define T2 where T2_def : "T2 = \<Union>{(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}"
[PROOF STATE]
proof (state)
this:
T2 = \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
define T3 where T3_def : "T3 = \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A.
        \<exists>P q' t1 t2.
           (q, P) \<in> prs \<and>
           path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}"
[PROOF STATE]
proof (state)
this:
T3 = \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have "test_suite_to_io M T = T1 \<union> T2 \<union> T3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io M T = T1 \<union> T2 \<union> T3
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close> test_suite_to_io.simps T1_def T2_def T3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} = (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
test_suite_to_io M T = T1 \<union> T2 \<union> T3

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
test_suite_to_io M T = T1 \<union> T2 \<union> T3

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have "finite T1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite T1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite T1
[PROOF STEP]
have "\<And> q P . (q, P)\<in>prs \<Longrightarrow> finite (L P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (L P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (L P)
[PROOF STEP]
fix q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (L P)
[PROOF STEP]
assume "(q, P)\<in>prs"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (L P)
[PROOF STEP]
have "acyclic P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
using t2[OF \<open>(q, P)\<in>prs\<close>]
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
unfolding is_preamble_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P \<and> single_input P \<and> is_submachine P M \<and> q \<in> reachable_states P \<and> deadlock_state P q \<and> (\<forall>q'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P)))

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.acyclic P

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (L P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.acyclic P
[PROOF STEP]
show "finite (L P)"
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P

goal (1 subgoal):
 1. finite (L P)
[PROOF STEP]
using acyclic_alt_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P
FSM.acyclic ?M = finite (L ?M)

goal (1 subgoal):
 1. finite (L P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (L P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (L ?P)

goal (1 subgoal):
 1. finite T1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (L ?P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (L ?P)

goal (1 subgoal):
 1. finite T1
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (L ?P)
finite prs

goal (1 subgoal):
 1. finite T1
[PROOF STEP]
unfolding T1_def
[PROOF STATE]
proof (prove)
using this:
(?q, ?P) \<in> prs \<Longrightarrow> finite (L ?P)
finite prs

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite T1

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

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite T1

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have "finite T2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite T2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite T2
[PROOF STEP]
have *: "T2 = (\<Union> (p,pt) \<in> {(p,pt) | p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} . ((@) (p_io p) ` set (prefixes (p_io pt))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T2 = (\<Union>(p, pt)\<in>{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}. (@) (p_io p) ` set (prefixes (p_io pt)))
[PROOF STEP]
unfolding T2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} = (\<Union>(p, pt)\<in>{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}. (@) (p_io p) ` set (prefixes (p_io pt)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T2 = (\<Union>(p, pt)\<in>{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}. (@) (p_io p) ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. finite T2
[PROOF STEP]
have "\<And> p pt . finite ((@) (p_io p) ` set (prefixes (p_io pt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p pt. finite ((@) (p_io p) ` set (prefixes (p_io pt)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ((@) (p_io ?p) ` set (prefixes (p_io ?pt)))

goal (1 subgoal):
 1. finite T2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite ((@) (p_io ?p) ` set (prefixes (p_io ?pt)))

goal (1 subgoal):
 1. finite T2
[PROOF STEP]
have "finite {(p,pt) | p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
have "{(p,pt) | p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union> (q,P) \<in> prs . {p . path P (initial P) p} \<times> (tps q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)

goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)

goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
have "finite (\<Union> (q,P) \<in> prs . {p . path P (initial P) p} \<times> (tps q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
note \<open>finite prs\<close>
[PROOF STATE]
proof (state)
this:
finite prs

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite prs

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
have "\<And> q P . (q,P) \<in> prs \<Longrightarrow> finite ({p . path P (initial P) p} \<times> (tps q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
fix q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
assume "(q,P) \<in> prs"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
have "acyclic P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
using t2[OF \<open>(q, P)\<in>prs\<close>]
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
unfolding is_preamble_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P \<and> single_input P \<and> is_submachine P M \<and> q \<in> reachable_states P \<and> deadlock_state P q \<and> (\<forall>q'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P)))

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.acyclic P

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.acyclic P
[PROOF STEP]
have "finite {p . path P (initial P) p}"
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
using acyclic_paths_finite[of P "initial P"]
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P
finite {p. path P (FSM.initial P) p \<and> distinct (visited_states (FSM.initial P) p)}

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
unfolding acyclic.simps
[PROOF STATE]
proof (prove)
using this:
\<forall>p. path P (FSM.initial P) p \<longrightarrow> distinct (visited_states (FSM.initial P) p)
finite {p. path P (FSM.initial P) p \<and> distinct (visited_states (FSM.initial P) p)}

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
by (metis (no_types, lifting) Collect_cong)
[PROOF STATE]
proof (state)
this:
finite {p. path P (FSM.initial P) p}

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {p. path P (FSM.initial P) p}
[PROOF STEP]
show "finite ({p . path P (initial P) p} \<times> (tps q))"
[PROOF STATE]
proof (prove)
using this:
finite {p. path P (FSM.initial P) p}

goal (1 subgoal):
 1. finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
using f4'[OF \<open>(q,P) \<in> prs\<close>]
[PROOF STATE]
proof (prove)
using this:
finite {p. path P (FSM.initial P) p}
finite (tps q)

goal (1 subgoal):
 1. finite ({p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite ({p. path P (FSM.initial P) p} \<times> tps q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?q1, ?P1) \<in> prs \<Longrightarrow> finite ({p. path ?P1 (FSM.initial ?P1) p} \<times> tps ?q1)

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite prs
(?q1, ?P1) \<in> prs \<Longrightarrow> finite ({p. path ?P1 (FSM.initial ?P1) p} \<times> tps ?q1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite prs
(?q1, ?P1) \<in> prs \<Longrightarrow> finite ({p. path ?P1 (FSM.initial ?P1) p} \<times> tps ?q1)

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)

goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<subseteq> (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)
finite (\<Union>(q, P)\<in>prs. {p. path P (FSM.initial P) p} \<times> tps q)

goal (1 subgoal):
 1. finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
by (meson rev_finite_subset)
[PROOF STATE]
proof (state)
this:
finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. finite T2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite ((@) (p_io ?p) ` set (prefixes (p_io ?pt)))
finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite ((@) (p_io ?p) ` set (prefixes (p_io ?pt)))
finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. finite T2
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite ((@) (p_io ?p) ` set (prefixes (p_io ?pt)))
finite {(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

goal (1 subgoal):
 1. finite (\<Union>(p, pt)\<in>{(p, pt) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}. (@) (p_io p) ` set (prefixes (p_io pt)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite T2

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

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite T2

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
have "finite T3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite T3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite T3
[PROOF STEP]
have scheme: "\<And> f P . (\<Union> {f a b c d | a b c d . P a b c d}) = (\<Union> (a,b,c,d) \<in> {(a,b,c,d) | a b c d . P a b c d} . f a b c d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f P. \<Union> {f a b c d |a b c d. P a b c d} = (\<Union>(a, b, c, d)\<in>{(a, b, c, d) |a b c d. P a b c d}. f a b c d)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> {?f a b c d |a b c d. ?P a b c d} = (\<Union>(a, b, c, d)\<in>{(a, b, c, d) |a b c d. ?P a b c d}. ?f a b c d)

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
have *: "T3 = (\<Union> (p,pt,q,A) \<in> {(p, pt, q, A) | p pt q A . \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
                       . (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T3 = (\<Union>(p, pt, q, A)\<in>{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}. (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
unfolding T3_def scheme
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(p, pt, q, A)\<in>{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}. (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A) = (\<Union>(p, pt, q, A)\<in>{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}. (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T3 = (\<Union>(p, pt, q, A)\<in>{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}. (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
have "{(p, pt, q, A) | p pt q A . \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
            \<subseteq> (\<Union> (q,P) \<in> prs . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
have "finite (\<Union> (q,P) \<in> prs . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
note \<open>finite prs\<close>
[PROOF STATE]
proof (state)
this:
finite prs

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite prs

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "\<And> q P . (q,P) \<in> prs \<Longrightarrow> finite (\<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
fix q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
assume "(q,P) \<in> prs"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, P) \<in> prs
[PROOF STEP]
have "q \<in> fst ` prs"
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs

goal (1 subgoal):
 1. q \<in> fst ` prs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
q \<in> fst ` prs

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "finite (tps q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (tps q)
[PROOF STEP]
using f4'[OF \<open>(q,P) \<in> prs\<close>]
[PROOF STATE]
proof (prove)
using this:
finite (tps q)

goal (1 subgoal):
 1. finite (tps q)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
finite (tps q)

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (tps q)

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "\<And> pt . pt \<in> tps q \<Longrightarrow> finite (\<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
fix pt
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
assume "pt \<in> tps q"
[PROOF STATE]
proof (state)
this:
pt \<in> tps q

goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "finite (rd_targets (q,pt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (rd_targets (q, pt))
[PROOF STEP]
using f2[OF \<open>q \<in> fst ` prs\<close>]
[PROOF STATE]
proof (prove)
using this:
finite (rd_targets (q, ?p))

goal (1 subgoal):
 1. finite (rd_targets (q, pt))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (rd_targets (q, pt))

goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (rd_targets (q, pt))

goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "\<And> q' . q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
fix q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
assume "q' \<in> rd_targets (q, pt)"
[PROOF STATE]
proof (state)
this:
q' \<in> rd_targets (q, pt)

goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "finite (atcs (target q pt, q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (atcs (target q pt, q'))
[PROOF STEP]
using f3
[PROOF STATE]
proof (prove)
using this:
finite (atcs (?q, ?q'))

goal (1 subgoal):
 1. finite (atcs (target q pt, q'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (atcs (target q pt, q'))

goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (atcs (target q pt, q'))

goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "finite {p . path P (initial P) p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
have "acyclic P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
using t2[OF \<open>(q, P)\<in>prs\<close>]
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
unfolding is_preamble_def
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P \<and> single_input P \<and> is_submachine P M \<and> q \<in> reachable_states P \<and> deadlock_state P q \<and> (\<forall>q'\<in>reachable_states P. (q = q' \<or> \<not> deadlock_state P q') \<and> (\<forall>x\<in>FSM.inputs M. (\<exists>t\<in>FSM.transitions P. t_source t = q' \<and> t_input t = x) \<longrightarrow> (\<forall>t'\<in>FSM.transitions M. t_source t' = q' \<and> t_input t' = x \<longrightarrow> t' \<in> FSM.transitions P)))

goal (1 subgoal):
 1. FSM.acyclic P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.acyclic P

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.acyclic P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
using acyclic_paths_finite[of P "initial P"]
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P
finite {p. path P (FSM.initial P) p \<and> distinct (visited_states (FSM.initial P) p)}

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
unfolding acyclic.simps
[PROOF STATE]
proof (prove)
using this:
\<forall>p. path P (FSM.initial P) p \<longrightarrow> distinct (visited_states (FSM.initial P) p)
finite {p. path P (FSM.initial P) p \<and> distinct (visited_states (FSM.initial P) p)}

goal (1 subgoal):
 1. finite {p. path P (FSM.initial P) p}
[PROOF STEP]
by (metis (no_types, lifting) Collect_cong)
[PROOF STATE]
proof (state)
this:
finite {p. path P (FSM.initial P) p}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {p. path P (FSM.initial P) p}

goal (1 subgoal):
 1. \<And>q'. q' \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (atcs (target q pt, q'))
finite {p. path P (FSM.initial P) p}
[PROOF STEP]
show "finite (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A})"
[PROOF STATE]
proof (prove)
using this:
finite (atcs (target q pt, q'))
finite {p. path P (FSM.initial P) p}

goal (1 subgoal):
 1. finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q'1 \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, ?q'1). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. \<And>pt. pt \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (rd_targets (q, pt))
?q'1 \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, ?q'1). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
show "finite (\<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
using this:
finite (rd_targets (q, pt))
?q'1 \<in> rd_targets (q, pt) \<Longrightarrow> finite (\<Union>(A, t1, t2)\<in>atcs (target q pt, ?q'1). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?pt1 \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, ?pt1). \<Union>(A, t1, t2)\<in>atcs (target q ?pt1, q'). {p. path P (FSM.initial P) p} \<times> {?pt1} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (tps q)
?pt1 \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, ?pt1). \<Union>(A, t1, t2)\<in>atcs (target q ?pt1, q'). {p. path P (FSM.initial P) p} \<times> {?pt1} \<times> {q} \<times> {A})
[PROOF STEP]
show "finite (\<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q, pt) . (\<Union> (A, t1, t2) \<in> atcs (target q pt, q') . {p . path P (initial P) p} \<times> {pt} \<times> {q} \<times> {A}))"
[PROOF STATE]
proof (prove)
using this:
finite (tps q)
?pt1 \<in> tps q \<Longrightarrow> finite (\<Union>q'\<in>rd_targets (q, ?pt1). \<Union>(A, t1, t2)\<in>atcs (target q ?pt1, q'). {p. path P (FSM.initial P) p} \<times> {?pt1} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (\<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?q1, ?P1) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps ?q1. \<Union>q'\<in>rd_targets (?q1, pt). \<Union>(A, t1, t2)\<in>atcs (target ?q1 pt, q'). {p. path ?P1 (FSM.initial ?P1) p} \<times> {pt} \<times> {?q1} \<times> {A})

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite prs
(?q1, ?P1) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps ?q1. \<Union>q'\<in>rd_targets (?q1, pt). \<Union>(A, t1, t2)\<in>atcs (target ?q1 pt, q'). {p. path ?P1 (FSM.initial ?P1) p} \<times> {pt} \<times> {?q1} \<times> {A})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite prs
(?q1, ?P1) \<in> prs \<Longrightarrow> finite (\<Union>pt\<in>tps ?q1. \<Union>q'\<in>rd_targets (?q1, pt). \<Union>(A, t1, t2)\<in>atcs (target ?q1 pt, q'). {p. path ?P1 (FSM.initial ?P1) p} \<times> {pt} \<times> {?q1} \<times> {A})

goal (1 subgoal):
 1. finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
[PROOF STEP]
have "finite {(p, pt, q, A) | p pt q A . \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}"
[PROOF STATE]
proof (prove)
using this:
{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})
finite (\<Union>(q, P)\<in>prs. \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). {p. path P (FSM.initial P) p} \<times> {pt} \<times> {q} \<times> {A})

goal (1 subgoal):
 1. finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
by (meson rev_finite_subset)
[PROOF STATE]
proof (state)
this:
finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
have "\<And> p pt q A . (p,pt,q,A) \<in> {(p, pt, q, A) | p pt q A . \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
                       \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
fix p pt q A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
assume "(p,pt,q,A) \<in> {(p, pt, q, A) | p pt q A . \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}"
[PROOF STATE]
proof (state)
this:
(p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
[PROOF STEP]
obtain P q' t1 t2 where "(q, P) \<in> prs" and "path P (FSM.initial P) p" and "target (FSM.initial P) p = q" and "pt \<in> tps q" and "q' \<in> rd_targets (q, pt)" and "(A, t1, t2) \<in> atcs (target q pt, q')"
[PROOF STATE]
proof (prove)
using this:
(p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. (\<And>P q' t1 t2. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q; q' \<in> rd_targets (q, pt); (A, t1, t2) \<in> atcs (target q pt, q')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q
q' \<in> rd_targets (q, pt)
(A, t1, t2) \<in> atcs (target q pt, q')

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
have "is_separator M (target q pt) q' A t1 t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_separator M (target q pt) q' A t1 t2
[PROOF STEP]
using t3[OF \<open>(A, t1, t2) \<in> atcs (target q pt, q')\<close>]
[PROOF STATE]
proof (prove)
using this:
(A, t2, t1) \<in> atcs (q', target q pt) \<and> is_separator M (target q pt) q' A t1 t2

goal (1 subgoal):
 1. is_separator M (target q pt) q' A t1 t2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_separator M (target q pt) q' A t1 t2

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_separator M (target q pt) q' A t1 t2
[PROOF STEP]
have "acyclic A"
[PROOF STATE]
proof (prove)
using this:
is_separator M (target q pt) q' A t1 t2

goal (1 subgoal):
 1. FSM.acyclic A
[PROOF STEP]
using is_separator_simps(2)
[PROOF STATE]
proof (prove)
using this:
is_separator M (target q pt) q' A t1 t2
is_separator ?M ?q1.0 ?q2.0 ?A ?t1.0 ?t2.0 \<Longrightarrow> FSM.acyclic ?A

goal (1 subgoal):
 1. FSM.acyclic A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.acyclic A

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.acyclic A
[PROOF STEP]
have "finite (L A)"
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic A

goal (1 subgoal):
 1. finite (L A)
[PROOF STEP]
unfolding acyclic_alt_def
[PROOF STATE]
proof (prove)
using this:
finite (L A)

goal (1 subgoal):
 1. finite (L A)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
finite (L A)

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (L A)
[PROOF STEP]
have "finite (atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
using this:
finite (L A)

goal (1 subgoal):
 1. finite (atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
unfolding atc_to_io_set.simps
[PROOF STATE]
proof (prove)
using this:
finite (L A)

goal (1 subgoal):
 1. finite (L (from_FSM M (target q pt)) \<inter> L A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (atc_to_io_set (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. \<And>p pt q A. (p, pt, q, A) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
show "finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
using this:
finite (atc_to_io_set (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?p1, ?pt1, ?q1, ?A1) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io ?p1 @ p_io ?pt1 @ io_atc) ` atc_to_io_set (from_FSM M (target ?q1 ?pt1)) ?A1)

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
(?p1, ?pt1, ?q1, ?A1) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io ?p1 @ p_io ?pt1 @ io_atc) ` atc_to_io_set (from_FSM M (target ?q1 ?pt1)) ?A1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
(?p1, ?pt1, ?q1, ?A1) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io ?p1 @ p_io ?pt1 @ io_atc) ` atc_to_io_set (from_FSM M (target ?q1 ?pt1)) ?A1)

goal (1 subgoal):
 1. finite T3
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}
(?p1, ?pt1, ?q1, ?A1) \<in> {(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> finite ((\<lambda>io_atc. p_io ?p1 @ p_io ?pt1 @ io_atc) ` atc_to_io_set (from_FSM M (target ?q1 ?pt1)) ?A1)

goal (1 subgoal):
 1. finite (\<Union>(p, pt, q, A)\<in>{(p, pt, q, A) |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}. (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite T3

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

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
test_suite_to_io M T = T1 \<union> T2 \<union> T3
finite T1
finite T2
finite T3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
test_suite_to_io M T = T1 \<union> T2 \<union> T3
finite T1
finite T2
finite T3

goal (1 subgoal):
 1. finite (test_suite_to_io M T)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (test_suite_to_io M T)

goal:
No subgoals!
[PROOF STEP]
qed