[STATEMENT]
lemma test_suite_to_io_code :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M"
shows "test_suite_to_io M T = test_suite_to_io' M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. test_suite_to_io M T = 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. test_suite_to_io M T = 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. test_suite_to_io M T = 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. test_suite_to_io M T = 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. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have test_suite_to_io'_alt_def: "test_suite_to_io' M T
    = (\<Union> (q,P) \<in> prs . L_acyclic P)
      \<union> (\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt)))))
      \<union> (\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io' M T = (\<Union>(q, P)\<in>prs. L_acyclic P) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
unfolding test_suite_to_io'.simps \<open>T = Test_Suite prs tps rd_targets atcs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)) \<union> (\<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A))) = (\<Union>(q, P)\<in>prs. L_acyclic P) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
test_suite_to_io' M T = (\<Union>(q, P)\<in>prs. L_acyclic P) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<union> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have test_suite_to_io_alt_def: "test_suite_to_io M T =
    (\<Union> (q,P) \<in> prs . L P)
    \<union> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (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 (initial P) p \<and> target (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)
goal (1 subgoal):
 1. test_suite_to_io M T = (\<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]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close> test_suite_to_io.simps
[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 force
[PROOF STATE]
proof (state)
this:
test_suite_to_io M T = (\<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')}

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have preamble_language_prop: "\<And> q P . (q,P) \<in> prs \<Longrightarrow> L_acyclic P = L P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> L_acyclic P = L P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> L_acyclic P = L P
[PROOF STEP]
fix q P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> L_acyclic P = 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> L_acyclic P = 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> L_acyclic P = L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.acyclic P
[PROOF STEP]
show "L_acyclic P = L P"
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P

goal (1 subgoal):
 1. L_acyclic P = L P
[PROOF STEP]
using LS_from_LS_acyclic
[PROOF STATE]
proof (prove)
using this:
FSM.acyclic P
FSM.acyclic ?M \<Longrightarrow> L ?M = L_acyclic ?M

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

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

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have preamble_path_prop: "\<And> q P ioP . (q,P) \<in> prs \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P) \<longleftrightarrow> (\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
fix q P ioP
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
assume "(q,P) \<in> prs"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs

goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
have "is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_preamble P M q
[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. is_preamble P M q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
is_preamble P M q

goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
have "ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> (\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
assume "ioP \<in> remove_proper_prefixes (L_acyclic P)"
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
have "ioP \<in> L P"  and "\<nexists>x'. x' \<noteq> [] \<and> ioP @ x' \<in> L P"
[PROOF STATE]
proof (prove)
using this:
ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. ioP \<in> L P &&& \<nexists>x'. x' \<noteq> [] \<and> ioP @ x' \<in> L P
[PROOF STEP]
unfolding preamble_language_prop[OF \<open>(q,P) \<in> prs\<close>] remove_proper_prefixes_def
[PROOF STATE]
proof (prove)
using this:
ioP \<in> {x \<in> L P. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> L P}

goal (1 subgoal):
 1. ioP \<in> L P &&& \<nexists>x'. x' \<noteq> [] \<and> ioP @ x' \<in> L P
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
ioP \<in> L P
\<nexists>x'. x' \<noteq> [] \<and> ioP @ x' \<in> L P

goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
show "(\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
using preamble_maximal_io_paths_rev[OF \<open>is_preamble P M q\<close> \<open>observable M\<close> \<open>ioP \<in> L P\<close> \<open>\<nexists>x'. x' \<noteq> [] \<and> ioP @ x' \<in> L P\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>p. \<lbrakk>path P (FSM.initial P) p; p_io p = ioP; target (FSM.initial P) p = q\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP

goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP

goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
have "(\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP) \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
assume "(\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP)"
[PROOF STATE]
proof (state)
this:
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP

goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
[PROOF STEP]
obtain p where "path P (initial P) p" and "target (initial P) p = q" and "p_io p = ioP"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path P (FSM.initial P) p; target (FSM.initial P) p = q; p_io p = ioP\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
p_io p = ioP

goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
p_io p = ioP
[PROOF STEP]
have "\<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P"
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
p_io p = ioP

goal (1 subgoal):
 1. \<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P
[PROOF STEP]
using preamble_maximal_io_paths[OF \<open>is_preamble P M q\<close> \<open>observable M\<close>]
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
p_io p = ioP
\<lbrakk>path P (FSM.initial P) ?p; target (FSM.initial P) ?p = q\<rbrakk> \<Longrightarrow> \<nexists>io'. io' \<noteq> [] \<and> p_io ?p @ io' \<in> L P

goal (1 subgoal):
 1. \<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P

goal (1 subgoal):
 1. \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P
[PROOF STEP]
show "ioP \<in> remove_proper_prefixes (L_acyclic P)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P

goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
using language_state_containment[OF \<open>path P (initial P) p\<close> \<open>p_io p = ioP\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>io'. io' \<noteq> [] \<and> p_io p @ io' \<in> L P
ioP \<in> L P

goal (1 subgoal):
 1. ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
unfolding preamble_language_prop[OF \<open>(q,P) \<in> prs\<close>] remove_proper_prefixes_def \<open>p_io p = ioP\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>io'. io' \<noteq> [] \<and> ioP @ io' \<in> L P
ioP \<in> L P

goal (1 subgoal):
 1. ioP \<in> {x \<in> L P. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> L P}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. \<And>q P ioP. (q, P) \<in> prs \<Longrightarrow> (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)
[PROOF STEP]
show "ioP \<in> remove_proper_prefixes (L_acyclic P) \<longleftrightarrow> (\<exists> p . path P (initial P) p \<and> target (initial P) p = q \<and> p_io p = ioP)"
[PROOF STATE]
proof (prove)
using this:
ioP \<in> remove_proper_prefixes (L_acyclic P) \<Longrightarrow> \<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP
\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP \<Longrightarrow> ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. (ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> prs \<Longrightarrow> (?ioP \<in> remove_proper_prefixes (L_acyclic ?P)) = (\<exists>p. path ?P (FSM.initial ?P) p \<and> target (FSM.initial ?P) p = ?q \<and> p_io p = ?ioP)

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have eq1: "(\<Union> (q,P) \<in> prs . L_acyclic P) = (\<Union> (q,P) \<in> prs . L P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. L_acyclic P) = (\<Union>(q, P)\<in>prs. L P)
[PROOF STEP]
using preamble_language_prop
[PROOF STATE]
proof (prove)
using this:
(?q, ?P) \<in> prs \<Longrightarrow> L_acyclic ?P = L ?P

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

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have eq2: "(\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt))))) = (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) = \<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 STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<subseteq> \<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}
 2. \<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} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
show "(\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<subseteq> \<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 (prove)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<subseteq> \<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 STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
assume "io \<in> (\<Union> (q,P) \<in> prs . (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt))))))"
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
obtain q P where "(q,P) \<in> prs"
                      and   "io \<in> (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt)))))"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> prs; io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, P) \<in> prs
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
obtain ioP where "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                      and   "io \<in> (\<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt)))))"
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. (\<And>ioP. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); io \<in> (\<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
io \<in> (\<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
obtain p where "path P (initial P) p" and "target (initial P) p = q" and "ioP = p_io p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path P (FSM.initial P) p; target (FSM.initial P) p = q; ioP = p_io p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using preamble_path_prop[OF \<open>(q,P) \<in> prs\<close>, of ioP] \<open>ioP \<in> remove_proper_prefixes (L_acyclic P)\<close>
[PROOF STATE]
proof (prove)
using this:
(ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path P (FSM.initial P) p; target (FSM.initial P) p = q; ioP = p_io p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
ioP = p_io p

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
obtain pt where "pt \<in> tps q" and "io \<in> ((\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pt. \<lbrakk>pt \<in> tps q; io \<in> (@) (p_io p) ` set (prefixes (p_io pt))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>io \<in> (\<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt)))))\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. (\<And>pt. \<lbrakk>pt \<in> tps q; io \<in> (@) (p_io p) ` set (prefixes (p_io pt))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>ioP = p_io p\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>pt\<in>tps q. (@) (p_io p) ` set (prefixes (p_io pt)))

goal (1 subgoal):
 1. (\<And>pt. \<lbrakk>pt \<in> tps q; io \<in> (@) (p_io p) ` set (prefixes (p_io pt))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pt \<in> tps q
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<Longrightarrow> x \<in> \<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 STEP]
show "io \<in> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> \<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 STEP]
using \<open>io \<in> ((\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))))\<close> \<open>(q,P) \<in> prs\<close> \<open>path P (initial P) p\<close> \<open>target (initial P) p = q\<close> \<open>pt \<in> tps q\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q

goal (1 subgoal):
 1. io \<in> \<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 STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> \<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) \<subseteq> \<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. \<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} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
show "\<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} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))"
[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} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<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} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<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} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
assume "io \<in> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})"
[PROOF STATE]
proof (state)
this:
io \<in> \<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. \<And>x. x \<in> \<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} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> \<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 STEP]
obtain p pt q P where "io \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
                           and   "(q,P) \<in> prs" and "path P (initial P) p" and "target (initial P) p = q" and "pt \<in> tps q"
[PROOF STATE]
proof (prove)
using this:
io \<in> \<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. (\<And>p pt q P. \<lbrakk>io \<in> (@) (p_io p) ` set (prefixes (p_io pt)); (q, P) \<in> prs; path P (FSM.initial P) p; target (FSM.initial P) p = q; pt \<in> tps q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q

goal (1 subgoal):
 1. \<And>x. x \<in> \<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} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q
[PROOF STEP]
obtain ioP where "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                      and   "p_io p = ioP"
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q

goal (1 subgoal):
 1. (\<And>ioP. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); p_io p = ioP\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using preamble_path_prop[OF \<open>(q,P) \<in> prs\<close>, of "p_io p"]
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))
(q, P) \<in> prs
path P (FSM.initial P) p
target (FSM.initial P) p = q
pt \<in> tps q
(p_io p \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>pa. path P (FSM.initial P) pa \<and> target (FSM.initial P) pa = q \<and> p_io pa = p_io p)

goal (1 subgoal):
 1. (\<And>ioP. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); p_io p = ioP\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
p_io p = ioP

goal (1 subgoal):
 1. \<And>x. x \<in> \<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} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
show "io \<in> (\<Union> (q,P) \<in> prs . (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>ioP \<in> remove_proper_prefixes (L_acyclic P)\<close> \<open>pt \<in> tps q\<close> \<open>io \<in> (\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt)))\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> (@) (p_io p) ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
unfolding \<open>p_io p = ioP\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> (@) ioP ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. (@) ioP ` set (prefixes (p_io pt))) = \<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. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
have eq3: "(\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)) = (\<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 (initial P) p \<and> target (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)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) = \<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]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<subseteq> \<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')}
 2. \<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')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
show "(\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<subseteq> (\<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 (initial P) p \<and> target (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)
goal (1 subgoal):
 1. (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<subseteq> \<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]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
assume "io \<in> (\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
obtain q P ioP pt q' A t1 t2 where "(q,P) \<in> prs"
                                        and   "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                                        and   "pt \<in> tps q"
                                        and   "q' \<in> rd_targets (q,pt)"
                                        and   "(A,t1,t2) \<in> atcs (target q pt,q')"
                                        and   "io \<in> (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. (\<And>q P ioP pt q' A t1 t2. \<lbrakk>(q, P) \<in> prs; ioP \<in> remove_proper_prefixes (L_acyclic P); pt \<in> tps q; q' \<in> rd_targets (q, pt); (A, t1, t2) \<in> atcs (target q pt, q'); io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
q' \<in> rd_targets (q, pt)
(A, t1, t2) \<in> atcs (target q pt, q')
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
obtain p where "path P (initial P) p" and "target (initial P) p = q" and "ioP = p_io p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path P (FSM.initial P) p; target (FSM.initial P) p = q; ioP = p_io p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using preamble_path_prop[OF \<open>(q,P) \<in> prs\<close>, of ioP] \<open>ioP \<in> remove_proper_prefixes (L_acyclic P)\<close>
[PROOF STATE]
proof (prove)
using this:
(ioP \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>p. path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> p_io p = ioP)
ioP \<in> remove_proper_prefixes (L_acyclic P)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path P (FSM.initial P) p; target (FSM.initial P) p = q; ioP = p_io p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path P (FSM.initial P) p
target (FSM.initial P) p = q
ioP = p_io p

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
have "acyclic A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic A
[PROOF STEP]
using t3[OF \<open>(A,t1,t2) \<in> atcs (target q pt,q')\<close>] is_separator_simps(2)
[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
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 metis
[PROOF STATE]
proof (state)
this:
FSM.acyclic A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
have "(acyclic_language_intersection (from_FSM M (target q pt)) A) = (atc_to_io_set (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic_language_intersection (from_FSM M (target q pt)) A = atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
unfolding acyclic_language_intersection_completeness[OF \<open>acyclic A\<close>] atc_to_io_set.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L (from_FSM M (target q pt)) \<inter> L A = L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
acyclic_language_intersection (from_FSM M (target q pt)) A = atc_to_io_set (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
have "io \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
using \<open>io \<in> (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io \<in> (\<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 \<open>(acyclic_language_intersection (from_FSM M (target q pt)) A) = (atc_to_io_set (from_FSM M (target q pt)) A)\<close> \<open>ioP = p_io p\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<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. io \<in> (\<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 simp
[PROOF STATE]
proof (state)
this:
io \<in> (\<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. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> x \<in> \<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]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
[PROOF STEP]
show "io \<in> (\<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 (initial P) p \<and> target (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:
io \<in> (\<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. io \<in> \<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]
using \<open>(q,P) \<in> prs\<close> \<open>path P (initial P) p\<close> \<open>target (initial P) p = q\<close> \<open>pt \<in> tps q\<close> \<open>q' \<in> rd_targets (q,pt)\<close> \<open>(A,t1,t2) \<in> atcs (target q pt,q')\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(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. io \<in> \<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 blast
[PROOF STATE]
proof (state)
this:
io \<in> \<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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) \<subseteq> \<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. \<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')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
show "(\<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 (initial P) p \<and> target (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> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
assume "io \<in> (\<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 (initial P) p \<and> target (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:
io \<in> \<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. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> \<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]
obtain p pt q A P q' t1 t2 where "io \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
                                      and   "(q,P) \<in> prs"
                                      and   "path P (initial P) p"
                                      and   "target (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:
io \<in> \<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. (\<And>p pt q A P q' t1 t2. \<lbrakk>io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A; (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:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(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>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(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')
[PROOF STEP]
obtain ioP where "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                      and   "p_io p = ioP"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(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>ioP. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); p_io p = ioP\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using preamble_path_prop[OF \<open>(q,P) \<in> prs\<close>, of "p_io p"]
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A
(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')
(p_io p \<in> remove_proper_prefixes (L_acyclic P)) = (\<exists>pa. path P (FSM.initial P) pa \<and> target (FSM.initial P) pa = q \<and> p_io pa = p_io p)

goal (1 subgoal):
 1. (\<And>ioP. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); p_io p = ioP\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
p_io p = ioP

goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
have "acyclic A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic A
[PROOF STEP]
using t3[OF \<open>(A,t1,t2) \<in> atcs (target q pt,q')\<close>] is_separator_simps(2)
[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
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 metis
[PROOF STATE]
proof (state)
this:
FSM.acyclic A

goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
have *: "(atc_to_io_set (from_FSM M (target q pt)) A) = (acyclic_language_intersection (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atc_to_io_set (from_FSM M (target q pt)) A = acyclic_language_intersection (from_FSM M (target q pt)) A
[PROOF STEP]
unfolding acyclic_language_intersection_completeness[OF \<open>acyclic A\<close>] atc_to_io_set.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L (from_FSM M (target q pt)) \<inter> L A = L (from_FSM M (target q pt)) \<inter> L A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atc_to_io_set (from_FSM M (target q pt)) A = acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
have "io \<in> (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A
[PROOF STEP]
using \<open>io \<in> (\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<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. io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A
[PROOF STEP]
unfolding * \<open>p_io p = ioP\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. \<And>x. x \<in> \<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')} \<Longrightarrow> x \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A
[PROOF STEP]
show "io \<in> (\<Union> (q,P) \<in> prs . \<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . \<Union> q' \<in> rd_targets (q,pt) . \<Union> (A,t1,t2) \<in> atcs (target q pt,q') . (\<lambda> io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>ioP \<in> remove_proper_prefixes (L_acyclic P)\<close> \<open>pt \<in> tps q\<close> \<open>q' \<in> rd_targets (q,pt)\<close> \<open>(A,t1,t2) \<in> atcs (target q pt,q')\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
q' \<in> rd_targets (q, pt)
(A, t1, t2) \<in> atcs (target q pt, q')

goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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')} \<subseteq> (\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>(q, P)\<in>prs. \<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. \<Union>q'\<in>rd_targets (q, pt). \<Union>(A, t1, t2)\<in>atcs (target q pt, q'). (\<lambda>io_atc. ioP @ p_io pt @ io_atc) ` acyclic_language_intersection (from_FSM M (target q pt)) A) = \<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. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
unfolding test_suite_to_io'_alt_def test_suite_to_io_alt_def eq1 eq2 eq3
[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 = test_suite_to_io' M T

goal:
No subgoals!
[PROOF STEP]
qed