[STATEMENT]
lemma test_suite_to_io_maximal_code :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M"
shows  "{io' \<in> (test_suite_to_io M T) . \<not> (\<exists> io'' . io'' \<noteq> [] \<and> io'@io'' \<in> (test_suite_to_io M T))} = test_suite_to_io_maximal M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal 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. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
have t_def: "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]
using test_suite_to_io_code[OF assms]
[PROOF STATE]
proof (prove)
using this:
test_suite_to_io M T = test_suite_to_io' M T

goal (1 subgoal):
 1. test_suite_to_io M T = test_suite_to_io' M T
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
test_suite_to_io M T = test_suite_to_io' M T

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
have t1_def : "test_suite_to_io' M T = (\<Union> (q,P) \<in> prs . L_acyclic P \<union> (\<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' \<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>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)))
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io' M (Test_Suite prs tps rd_targets atcs) = (\<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)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
test_suite_to_io' M T = (\<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)))

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
define tmax where tmax_def: "tmax = (\<Union> (q,P) \<in> prs . L_acyclic P \<union> (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . Set.insert (ioP @ p_io pt) (\<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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))))"
[PROOF STATE]
proof (state)
this:
tmax = (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
have t2_def : "test_suite_to_io_maximal M T = remove_proper_prefixes tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io_maximal M T = remove_proper_prefixes tmax
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close> tmax_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io_maximal M (Test_Suite prs tps rd_targets atcs) = remove_proper_prefixes (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
test_suite_to_io_maximal M T = remove_proper_prefixes tmax

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
have tmax_sub: "tmax \<subseteq> (test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tmax \<subseteq> test_suite_to_io M T
[PROOF STEP]
unfolding tmax_def t_def t1_def
[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. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))) \<subseteq> (\<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)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))) \<Longrightarrow> x \<in> (\<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)))
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))) \<Longrightarrow> x \<in> (\<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)))
[PROOF STEP]
assume "io \<in> (\<Union> (q,P) \<in> prs . L_acyclic P \<union> (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . Set.insert (ioP @ p_io pt) (\<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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))))"
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))

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

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> prs; io \<in> L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io \<in> L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))) \<Longrightarrow> x \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, P) \<in> prs
io \<in> L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))
[PROOF STEP]
consider (a) "io \<in> L_acyclic P" |
                  (b) "io \<in> (\<Union> ioP \<in> remove_proper_prefixes (L_acyclic P) . \<Union> pt \<in> tps q . Set.insert (ioP @ p_io pt) (\<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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
io \<in> L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))

goal (1 subgoal):
 1. \<lbrakk>io \<in> L_acyclic P \<Longrightarrow> thesis; io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))) \<Longrightarrow> x \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "io \<in> (\<Union> (q,P) \<in> prs . L_acyclic P \<union> (\<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' \<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:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io \<in> L_acyclic P \<Longrightarrow> io \<in> (\<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)))
 2. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
io \<in> L_acyclic P

goal (2 subgoals):
 1. io \<in> L_acyclic P \<Longrightarrow> io \<in> (\<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)))
 2. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> L_acyclic P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io \<in> L_acyclic P

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> L_acyclic P
(q, P) \<in> prs

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal (1 subgoal):
 1. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))

goal (1 subgoal):
 1. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))
[PROOF STEP]
obtain ioP pt where "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                         and   "pt \<in> tps q"
                         and   "io \<in> Set.insert (ioP @ p_io pt) (\<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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))

goal (1 subgoal):
 1. (\<And>ioP pt. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); pt \<in> tps q; io \<in> Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))

goal (1 subgoal):
 1. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))
[PROOF STEP]
consider (b1) "io = (ioP @ p_io pt)" |
                    (b2) "io \<in> (\<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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))"
[PROOF STATE]
proof (prove)
using this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))

goal (1 subgoal):
 1. \<lbrakk>io = ioP @ p_io pt \<Longrightarrow> thesis; io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io = ioP @ p_io pt \<Longrightarrow> ?thesis; io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io \<in> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io = ioP @ p_io pt \<Longrightarrow> ?thesis; io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>io = ioP @ p_io pt \<Longrightarrow> ?thesis; io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io = ioP @ p_io pt \<Longrightarrow> io \<in> (\<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)))
 2. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
case b1
[PROOF STATE]
proof (state)
this:
io = ioP @ p_io pt

goal (2 subgoals):
 1. io = ioP @ p_io pt \<Longrightarrow> io \<in> (\<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)))
 2. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io = ioP @ p_io pt
[PROOF STEP]
have "io \<in> ((\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt))))"
[PROOF STATE]
proof (prove)
using this:
io = ioP @ p_io pt

goal (1 subgoal):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt))
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
io = ioP @ p_io pt

goal (1 subgoal):
 1. io \<in> (@) ioP ` {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (@) ioP ` set (prefixes (p_io pt))

goal (2 subgoals):
 1. io = ioP @ p_io pt \<Longrightarrow> io \<in> (\<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)))
 2. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (@) ioP ` set (prefixes (p_io pt))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) ioP ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. io \<in> (\<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)))
[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>
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) ioP ` set (prefixes (p_io pt))
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal (1 subgoal):
 1. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
case b2
[PROOF STATE]
proof (state)
this:
io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))

goal (1 subgoal):
 1. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))
[PROOF STEP]
obtain q' A t1 t2 where "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) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))

goal (1 subgoal):
 1. (\<And>q' A t1 t2. \<lbrakk>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) ` remove_proper_prefixes (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' \<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
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) ` remove_proper_prefixes (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)
using this:
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) ` remove_proper_prefixes (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]
unfolding remove_proper_prefixes_def
[PROOF STATE]
proof (prove)
using this:
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) ` {x \<in> acyclic_language_intersection (from_FSM M (target q pt)) A. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> 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 blast
[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. io \<in> (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)) \<Longrightarrow> io \<in> (\<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)))
[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 ?thesis
[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. 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)))
[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. 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)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
tmax \<subseteq> test_suite_to_io M T

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
have tmax_max: "\<And> io . io \<in> test_suite_to_io M T \<Longrightarrow> io \<notin> tmax \<Longrightarrow> \<exists> io'' . io'' \<noteq> [] \<and> io@io'' \<in> (test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
assume "io \<in> test_suite_to_io M T" and "io \<notin> tmax"
[PROOF STATE]
proof (state)
this:
io \<in> test_suite_to_io M T
io \<notin> tmax

goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> test_suite_to_io M T
io \<notin> tmax
[PROOF STEP]
have "io \<in> (\<Union> (q,P) \<in> prs . L_acyclic P \<union> (\<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' \<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> test_suite_to_io M T
io \<notin> tmax

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
unfolding t_def t1_def
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<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)))
io \<notin> tmax

goal (1 subgoal):
 1. io \<in> (\<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)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> (\<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)))

goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<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)))
[PROOF STEP]
obtain q P where "(q,P) \<in> prs"
                    and   "io \<in> (L_acyclic P \<union> (\<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' \<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> (\<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)))

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> prs; io \<in> 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))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io \<in> 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))

goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, P) \<in> prs
io \<in> 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))
[PROOF STEP]
consider (a) "io \<in> L_acyclic P" |
                  (b) "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)))) \<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)))"
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
io \<in> 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))

goal (1 subgoal):
 1. \<lbrakk>io \<in> L_acyclic P \<Longrightarrow> thesis; io \<in> (\<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)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<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)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>io. \<lbrakk>io \<in> test_suite_to_io M T; io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<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)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "\<exists> io'' . io'' \<noteq> [] \<and> io@io'' \<in> (test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>io \<in> L_acyclic P \<Longrightarrow> ?thesis; io \<in> (\<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)) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io \<in> L_acyclic P \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
io \<in> L_acyclic P

goal (2 subgoals):
 1. io \<in> L_acyclic P \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> L_acyclic P
[PROOF STEP]
have "io \<in> tmax"
[PROOF STATE]
proof (prove)
using this:
io \<in> L_acyclic P

goal (1 subgoal):
 1. io \<in> tmax
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> L_acyclic P
(q, P) \<in> prs

goal (1 subgoal):
 1. io \<in> tmax
[PROOF STEP]
unfolding tmax_def
[PROOF STATE]
proof (prove)
using this:
io \<in> L_acyclic P
(q, P) \<in> prs

goal (1 subgoal):
 1. io \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> tmax

goal (2 subgoals):
 1. io \<in> L_acyclic P \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> tmax
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
using \<open>io \<notin> tmax\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax
io \<notin> tmax

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
io \<in> (\<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))

goal (1 subgoal):
 1. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<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))
[PROOF STEP]
obtain ioP pt where "ioP \<in> remove_proper_prefixes (L_acyclic P)"
                         and   "pt \<in> tps q"
                         and   "io \<in> ((\<lambda> io' . ioP @ io') ` (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))"
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<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))

goal (1 subgoal):
 1. (\<And>ioP pt. \<lbrakk>ioP \<in> remove_proper_prefixes (L_acyclic P); pt \<in> tps q; io \<in> (@) 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)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> (@) 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)

goal (1 subgoal):
 1. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> (@) 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)
[PROOF STEP]
consider (b1) "io \<in> (\<lambda> io' . ioP @ io') ` (set (prefixes (p_io pt)))" |
                    (b2) "io \<in> (\<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:
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q
io \<in> (@) 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)

goal (1 subgoal):
 1. \<lbrakk>io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> thesis; io \<in> (\<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> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> ?thesis; io \<in> (\<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> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io \<in> (\<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)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> ?thesis; io \<in> (\<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> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> ?thesis; io \<in> (\<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> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
case b1
[PROOF STATE]
proof (state)
this:
io \<in> (@) ioP ` set (prefixes (p_io pt))

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (@) ioP ` set (prefixes (p_io pt))
[PROOF STEP]
obtain pt1 pt2 where "io = ioP @ pt1" and "p_io pt = pt1@pt2"
[PROOF STATE]
proof (prove)
using this:
io \<in> (@) ioP ` set (prefixes (p_io pt))

goal (1 subgoal):
 1. (\<And>pt1 pt2. \<lbrakk>io = ioP @ pt1; p_io pt = pt1 @ pt2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, lifting) b1 image_iff prefixes_set_ob)
[PROOF STATE]
proof (state)
this:
io = ioP @ pt1
p_io pt = pt1 @ pt2

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
have "ioP @ (p_io pt) \<in> tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioP @ p_io pt \<in> tmax
[PROOF STEP]
using \<open>io \<notin> tmax\<close> \<open>(q,P) \<in> prs\<close> \<open>ioP \<in> remove_proper_prefixes (L_acyclic P)\<close> \<open>pt \<in> tps q\<close>
[PROOF STATE]
proof (prove)
using this:
io \<notin> tmax
(q, P) \<in> prs
ioP \<in> remove_proper_prefixes (L_acyclic P)
pt \<in> tps q

goal (1 subgoal):
 1. ioP @ p_io pt \<in> tmax
[PROOF STEP]
unfolding tmax_def
[PROOF STATE]
proof (prove)
using this:
io \<notin> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (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

goal (1 subgoal):
 1. ioP @ p_io pt \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ioP @ p_io pt \<in> tmax

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP @ p_io pt \<in> tmax
[PROOF STEP]
have "io \<noteq> ioP @ (p_io pt)"
[PROOF STATE]
proof (prove)
using this:
ioP @ p_io pt \<in> tmax

goal (1 subgoal):
 1. io \<noteq> ioP @ p_io pt
[PROOF STEP]
using \<open>io \<notin> tmax\<close>
[PROOF STATE]
proof (prove)
using this:
ioP @ p_io pt \<in> tmax
io \<notin> tmax

goal (1 subgoal):
 1. io \<noteq> ioP @ p_io pt
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<noteq> ioP @ p_io pt

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<noteq> ioP @ p_io pt
[PROOF STEP]
have "pt2 \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
io \<noteq> ioP @ p_io pt

goal (1 subgoal):
 1. pt2 \<noteq> []
[PROOF STEP]
using \<open>io = ioP @ pt1\<close>
[PROOF STATE]
proof (prove)
using this:
io \<noteq> ioP @ p_io pt
io = ioP @ pt1

goal (1 subgoal):
 1. pt2 \<noteq> []
[PROOF STEP]
unfolding \<open>p_io pt = pt1@pt2\<close>
[PROOF STATE]
proof (prove)
using this:
io \<noteq> ioP @ pt1 @ pt2
io = ioP @ pt1

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

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
have "ioP @ (p_io pt) \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioP @ p_io pt \<in> test_suite_to_io M T
[PROOF STEP]
using \<open>ioP @ (p_io pt) \<in> tmax\<close> tmax_sub
[PROOF STATE]
proof (prove)
using this:
ioP @ p_io pt \<in> tmax
tmax \<subseteq> test_suite_to_io M T

goal (1 subgoal):
 1. ioP @ p_io pt \<in> test_suite_to_io M T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioP @ p_io pt \<in> test_suite_to_io M T

goal (2 subgoals):
 1. io \<in> (@) ioP ` set (prefixes (p_io pt)) \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
 2. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioP @ p_io pt \<in> test_suite_to_io M T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ioP @ p_io pt \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
unfolding \<open>io = ioP @ pt1\<close> append.assoc \<open>p_io pt = pt1@pt2\<close>
[PROOF STATE]
proof (prove)
using this:
ioP @ pt1 @ pt2 \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> ioP @ pt1 @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
using \<open>pt2 \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
ioP @ pt1 @ pt2 \<in> test_suite_to_io M T
pt2 \<noteq> []

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> ioP @ pt1 @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
case b2
[PROOF STATE]
proof (state)
this:
io \<in> (\<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. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> (\<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' A t1 t2 where "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'\<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' A t1 t2. \<lbrakk>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' \<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. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
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
[PROOF STEP]
obtain ioA where "io = ioP @ p_io pt @ ioA"
                        and   "ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A"
[PROOF STATE]
proof (prove)
using this:
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>ioA. \<lbrakk>io = ioP @ p_io pt @ ioA; ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io = ioP @ p_io pt @ ioA
ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io = ioP @ p_io pt @ ioA
ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
have "ioA \<notin> (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioA \<notin> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> False
[PROOF STEP]
assume "ioA \<in> remove_proper_prefixes (acyclic_language_intersection (FSM.from_FSM M (target q pt)) A)"
[PROOF STATE]
proof (state)
this:
ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
have "io \<in> tmax"
[PROOF STATE]
proof (prove)
using this:
ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. io \<in> tmax
[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:
ioA \<in> remove_proper_prefixes (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> tmax
[PROOF STEP]
unfolding tmax_def \<open>io = ioP @ p_io pt @ ioA\<close>
[PROOF STATE]
proof (prove)
using this:
ioA \<in> remove_proper_prefixes (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. ioP @ p_io pt @ ioA \<in> (\<Union>(q, P)\<in>prs. L_acyclic P \<union> (\<Union>ioP\<in>remove_proper_prefixes (L_acyclic P). \<Union>pt\<in>tps q. Set.insert (ioP @ p_io pt) (\<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) ` remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io \<in> tmax

goal (1 subgoal):
 1. ioA \<in> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> tmax
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>io \<notin> tmax\<close>
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax
io \<notin> tmax

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ioA \<notin> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io = ioP @ p_io pt @ ioA
ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA \<notin> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)
[PROOF STEP]
obtain ioA2 where "ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A"
                               and   "ioA2 \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
io = ioP @ p_io pt @ ioA
ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA \<notin> remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)

goal (1 subgoal):
 1. (\<And>ioA2. \<lbrakk>ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A; ioA2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding remove_proper_prefixes_def
[PROOF STATE]
proof (prove)
using this:
io = ioP @ p_io pt @ ioA
ioA \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA \<notin> {x \<in> acyclic_language_intersection (from_FSM M (target q pt)) A. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> acyclic_language_intersection (from_FSM M (target q pt)) A}

goal (1 subgoal):
 1. (\<And>ioA2. \<lbrakk>ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A; ioA2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA2 \<noteq> []

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA2 \<noteq> []
[PROOF STEP]
have "io@ioA2 \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
using this:
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA2 \<noteq> []

goal (1 subgoal):
 1. io @ ioA2 \<in> test_suite_to_io M T
[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> \<open>ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A\<close>
[PROOF STATE]
proof (prove)
using this:
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA2 \<noteq> []
(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')
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. io @ ioA2 \<in> test_suite_to_io M T
[PROOF STEP]
unfolding t_def t1_def \<open>io = ioP @ p_io pt @ ioA\<close>
[PROOF STATE]
proof (prove)
using this:
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A
ioA2 \<noteq> []
(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')
ioA @ ioA2 \<in> acyclic_language_intersection (from_FSM M (target q pt)) A

goal (1 subgoal):
 1. (ioP @ p_io pt @ ioA) @ ioA2 \<in> (\<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)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io @ ioA2 \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> (\<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> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io @ ioA2 \<in> test_suite_to_io M T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
io @ ioA2 \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
using \<open>ioA2 \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
io @ ioA2 \<in> test_suite_to_io M T
ioA2 \<noteq> []

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?io \<in> test_suite_to_io M T; ?io \<notin> tmax\<rbrakk> \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> ?io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T
[PROOF STEP]
unfolding t2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = remove_proper_prefixes tmax
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<subseteq> remove_proper_prefixes tmax
 2. remove_proper_prefixes tmax \<subseteq> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
show "{io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<subseteq> remove_proper_prefixes tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<subseteq> remove_proper_prefixes tmax
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<Longrightarrow> x \<in> remove_proper_prefixes tmax
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<Longrightarrow> x \<in> remove_proper_prefixes tmax
[PROOF STEP]
assume "io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}"
[PROOF STATE]
proof (state)
this:
io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal (1 subgoal):
 1. \<And>x. x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<Longrightarrow> x \<in> remove_proper_prefixes tmax
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
have "io \<in> test_suite_to_io M T" and "\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
using this:
io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal (1 subgoal):
 1. io \<in> test_suite_to_io M T &&& \<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
io \<in> test_suite_to_io M T
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<And>x. x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<Longrightarrow> x \<in> remove_proper_prefixes tmax
[PROOF STEP]
show "io \<in> remove_proper_prefixes tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> remove_proper_prefixes tmax
[PROOF STEP]
using \<open>\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> remove_proper_prefixes tmax
[PROOF STEP]
using tmax_sub tmax_max[OF \<open>io \<in> test_suite_to_io M T\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
tmax \<subseteq> test_suite_to_io M T
io \<notin> tmax \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> remove_proper_prefixes tmax
[PROOF STEP]
unfolding remove_proper_prefixes_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
tmax \<subseteq> test_suite_to_io M T
io \<notin> tmax \<Longrightarrow> \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> {x \<in> tmax. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> tmax}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
io \<in> remove_proper_prefixes tmax

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} \<subseteq> remove_proper_prefixes tmax

goal (1 subgoal):
 1. remove_proper_prefixes tmax \<subseteq> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
show "remove_proper_prefixes tmax \<subseteq> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove_proper_prefixes tmax \<subseteq> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
assume "io \<in> remove_proper_prefixes tmax"
[PROOF STATE]
proof (state)
this:
io \<in> remove_proper_prefixes tmax

goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> remove_proper_prefixes tmax
[PROOF STEP]
have "io \<in> tmax" and "\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax"
[PROOF STATE]
proof (prove)
using this:
io \<in> remove_proper_prefixes tmax

goal (1 subgoal):
 1. io \<in> tmax &&& \<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax
[PROOF STEP]
unfolding remove_proper_prefixes_def
[PROOF STATE]
proof (prove)
using this:
io \<in> {x \<in> tmax. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> tmax}

goal (1 subgoal):
 1. io \<in> tmax &&& \<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> {x \<in> tmax. \<nexists>x'. x' \<noteq> [] \<and> x @ x' \<in> tmax}
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
io \<in> tmax
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax

goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io \<in> tmax
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax
[PROOF STEP]
have "io \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax

goal (1 subgoal):
 1. io \<in> test_suite_to_io M T
[PROOF STEP]
using tmax_sub
[PROOF STATE]
proof (prove)
using this:
io \<in> tmax
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax
tmax \<subseteq> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> test_suite_to_io M T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
have "\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T"
[PROOF STATE]
proof (state)
this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
obtain io'' where "io'' \<noteq> []" and "io @ io'' \<in> test_suite_to_io M T"
[PROOF STATE]
proof (prove)
using this:
\<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. (\<And>io''. \<lbrakk>io'' \<noteq> []; io @ io'' \<in> test_suite_to_io M T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io'' \<noteq> []
io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io'' \<noteq> []
io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
obtain io''' where "(io @ io'') @ io''' \<in> test_suite_to_io M T"
                          and   "(\<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T)"
[PROOF STATE]
proof (prove)
using this:
io'' \<noteq> []
io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. (\<And>io'''. \<lbrakk>(io @ io'') @ io''' \<in> test_suite_to_io M T; \<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_set_elem_maximal_extension_ex[OF \<open>io @ io'' \<in> test_suite_to_io M T\<close> test_suite_to_io_finite[OF assms(1,2)]]
[PROOF STATE]
proof (prove)
using this:
io'' \<noteq> []
io @ io'' \<in> test_suite_to_io M T
\<exists>ys. (io @ io'') @ ys \<in> test_suite_to_io M T \<and> (\<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ ys @ zs \<in> test_suite_to_io M T)

goal (1 subgoal):
 1. (\<And>io'''. \<lbrakk>(io @ io'') @ io''' \<in> test_suite_to_io M T; \<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(io @ io'') @ io''' \<in> test_suite_to_io M T
\<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
have "io @ (io'' @ io''') \<in> tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io @ io'' @ io''' \<in> tmax
[PROOF STEP]
using tmax_max[OF \<open>(io @ io'') @ io''' \<in> test_suite_to_io M T\<close>] \<open>(\<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T)\<close>
[PROOF STATE]
proof (prove)
using this:
(io @ io'') @ io''' \<notin> tmax \<Longrightarrow> \<exists>io''a. io''a \<noteq> [] \<and> ((io @ io'') @ io''') @ io''a \<in> test_suite_to_io M T
\<nexists>zs. zs \<noteq> [] \<and> (io @ io'') @ io''' @ zs \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io @ io'' @ io''' \<in> tmax
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io @ io'' @ io''' \<in> tmax

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
io @ io'' @ io''' \<in> tmax

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
have "io''@io''' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io'' @ io''' \<noteq> []
[PROOF STEP]
using \<open>io'' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
io'' \<noteq> []

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

goal (1 subgoal):
 1. \<exists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io @ io'' @ io''' \<in> tmax
io'' @ io''' \<noteq> []
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
io @ io'' @ io''' \<in> tmax
io'' @ io''' \<noteq> []

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax\<close>
[PROOF STATE]
proof (prove)
using this:
io @ io'' @ io''' \<in> tmax
io'' @ io''' \<noteq> []
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> remove_proper_prefixes tmax

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (mono_tags, lifting) \<open>io \<in> remove_proper_prefixes tmax\<close> mem_Collect_eq remove_proper_prefixes_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<And>x. x \<in> remove_proper_prefixes tmax \<Longrightarrow> x \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
io \<in> test_suite_to_io M T
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T
[PROOF STEP]
show "io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}"
[PROOF STATE]
proof (prove)
using this:
io \<in> test_suite_to_io M T
\<nexists>io''. io'' \<noteq> [] \<and> io @ io'' \<in> test_suite_to_io M T

goal (1 subgoal):
 1. io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
io \<in> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
remove_proper_prefixes tmax \<subseteq> {io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{io' \<in> test_suite_to_io M T. \<nexists>io''. io'' \<noteq> [] \<and> io' @ io'' \<in> test_suite_to_io M T} = test_suite_to_io_maximal M T

goal:
No subgoals!
[PROOF STEP]
qed