[STATEMENT]
lemma test_suite_to_io_language :
  assumes "implies_completeness T M m"
shows "(test_suite_to_io M T) \<subseteq> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test_suite_to_io M T \<subseteq> L M
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[PROOF STEP]
fix io
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[PROOF STEP]
assume "io \<in> test_suite_to_io M T"
[PROOF STATE]
proof (state)
this:
io \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[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. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = Test_Suite prs tps rd_targets atcs
[PROOF STEP]
obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
[PROOF STATE]
proof (prove)
using this:
T = Test_Suite prs tps rd_targets atcs

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets
[PROOF STEP]
have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?d \<in> set repetition_sets \<Longrightarrow> snd ?d \<subseteq> fst ?d

goal (1 subgoal):
 1. \<And>x. x \<in> test_suite_to_io M T \<Longrightarrow> x \<in> L M
[PROOF STEP]
from \<open>io \<in> test_suite_to_io M T\<close>
[PROOF STATE]
proof (chain)
picking this:
io \<in> test_suite_to_io M T
[PROOF STEP]
consider
    (a) "io \<in> (\<Union> (q,P) \<in> prs . L P)" |
    (b) "io \<in> (\<Union>{(\<lambda> io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . \<exists> q P . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q})" |
    (c) "io \<in> (\<Union>{(\<lambda> io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . \<exists> P q' t1 t2 . (q,P) \<in> prs \<and> path P (initial P) p \<and> target (initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q,pt) \<and> (A,t1,t2) \<in> atcs (target q pt,q') })"
[PROOF STATE]
proof (prove)
using this:
io \<in> test_suite_to_io M T

goal (1 subgoal):
 1. \<lbrakk>io \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> thesis; io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> thesis; io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>T = Test_Suite prs tps rd_targets atcs\<close> test_suite_to_io.simps
[PROOF STATE]
proof (prove)
using this:
io \<in> (\<Union>(q, P)\<in>prs. L P) \<union> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<union> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')}

goal (1 subgoal):
 1. \<lbrakk>io \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> thesis; io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> thesis; io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>io \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> ?thesis; io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> ?thesis; io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. io \<in> L M
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. io \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> io \<in> L M
 2. io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io \<in> L M
 3. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
io \<in> (\<Union>(q, P)\<in>prs. L P)

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

goal (1 subgoal):
 1. (\<And>q P. \<lbrakk>(q, P) \<in> prs; io \<in> L P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io \<in> L P

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

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

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

goal (3 subgoals):
 1. io \<in> (\<Union>(q, P)\<in>prs. L P) \<Longrightarrow> io \<in> L M
 2. io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io \<in> L M
 3. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
show "io \<in> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io \<in> L M
[PROOF STEP]
using submachine_language[OF \<open>is_submachine P M\<close>] \<open>io \<in> L P\<close>
[PROOF STATE]
proof (prove)
using this:
L P \<subseteq> L M
io \<in> L P

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

goal (2 subgoals):
 1. io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io \<in> L M
 2. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io \<in> L M
 2. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q}

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
io = p_io p @ io'
io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}

goal (1 subgoal):
 1. (\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis; io = p_io p @ io'; io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume a1: "io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}"
[PROOF STATE]
proof (state)
this:
io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}

goal (1 subgoal):
 1. \<lbrakk>\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis; io = p_io p @ io'; io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>p_io pt = io' @ ?io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>io''. \<lbrakk>p_io pt = io' @ io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis; io = p_io p @ io'; io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p_io pt = io' @ ?io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pt = io' @ ?io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using a1 \<open>io = p_io p @ io'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pt = io' @ ?io''; io = p_io p @ io'\<rbrakk> \<Longrightarrow> thesis
io' \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pt}
io = p_io p @ io'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p_io pt = io' @ io''
io = p_io p @ io'

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

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

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

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

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

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

goal (1 subgoal):
 1. FSM.initial P = FSM.initial M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial P = FSM.initial M

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

goal (1 subgoal):
 1. path M (FSM.initial M) p
[PROOF STEP]
unfolding \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) p

goal (1 subgoal):
 1. path M (FSM.initial M) p
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) p

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

goal (1 subgoal):
 1. target (FSM.initial M) p = q
[PROOF STEP]
unfolding \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) p = q

goal (1 subgoal):
 1. target (FSM.initial M) p = q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) p = q

goal (2 subgoals):
 1. io \<in> \<Union> {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. \<exists>q P. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q} \<Longrightarrow> io \<in> L M
 2. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
obtain p2 d where "(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p2 d. (pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using t6[OF \<open>q \<in> fst ` prs\<close>] \<open>pt \<in> tps q\<close>
[PROOF STATE]
proof (prove)
using this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M q repetition_sets m \<subseteq> tps q
pt \<in> tps q

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

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

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF \<open>path M (initial M) p\<close>], of m]
[PROOF STATE]
proof (prove)
using this:
(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> q \<in> FSM.states M; \<And>d. d \<in> set repetition_sets \<Longrightarrow> d \<in> set repetition_sets\<rbrakk> \<Longrightarrow> m_traversal_paths_with_witness M (target (FSM.initial M) p) repetition_sets m = {(pa, d) |pa d. path M (target (FSM.initial M) p) pa \<and> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) pa)) repetition_sets = Some d \<and> (\<forall>p' p''. pa = p' @ p'' \<and> p'' \<noteq> [] \<longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)}

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
unfolding \<open>target (initial M) p = q\<close>
[PROOF STATE]
proof (prove)
using this:
(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> q \<in> FSM.states M; \<And>d. d \<in> set repetition_sets \<Longrightarrow> d \<in> set repetition_sets\<rbrakk> \<Longrightarrow> m_traversal_paths_with_witness M q repetition_sets m = {(p, d) |p d. path M q p \<and> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p)) repetition_sets = Some d \<and> (\<forall>p' p''. p = p' @ p'' \<and> p'' \<noteq> [] \<longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)}

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M q (pt @ p2)

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

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt)
[PROOF STEP]
using \<open>path M (initial M) p\<close> \<open>target (initial M) p = q\<close>
[PROOF STATE]
proof (prove)
using this:
path M q (pt @ p2)
path M (FSM.initial M) p
target (FSM.initial M) p = q

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ pt)

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

goal (1 subgoal):
 1. p_io p @ p_io pt \<in> L M
[PROOF STEP]
by (metis (mono_tags, lifting) language_intro map_append)
[PROOF STATE]
proof (state)
this:
p_io p @ p_io pt \<in> L M

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

goal (1 subgoal):
 1. io \<in> L M
[PROOF STEP]
unfolding \<open>io = p_io p @ io'\<close> \<open>p_io pt = io' @ io''\<close> append.assoc[symmetric]
[PROOF STATE]
proof (prove)
using this:
(p_io p @ io') @ io'' \<in> L M

goal (1 subgoal):
 1. p_io p @ io' \<in> L M
[PROOF STEP]
using language_prefix[of "p_io p @ io'" io'' M "initial M"]
[PROOF STATE]
proof (prove)
using this:
(p_io p @ io') @ io'' \<in> L M
(p_io p @ io') @ io'' \<in> L M \<Longrightarrow> p_io p @ io' \<in> L M

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

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

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

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

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

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

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

goal (1 subgoal):
 1. ioA \<in> L (from_FSM M (target q pt))
[PROOF STEP]
unfolding atc_to_io_set.simps
[PROOF STATE]
proof (prove)
using this:
io = p_io p @ p_io pt @ ioA
ioA \<in> L (from_FSM M (target q pt)) \<inter> L A

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

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

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

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

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

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

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

goal (1 subgoal):
 1. FSM.initial P = FSM.initial M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial P = FSM.initial M

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

goal (1 subgoal):
 1. path M (FSM.initial M) p
[PROOF STEP]
unfolding \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) p

goal (1 subgoal):
 1. path M (FSM.initial M) p
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) p

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

goal (1 subgoal):
 1. target (FSM.initial M) p = q
[PROOF STEP]
unfolding \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) p = q

goal (1 subgoal):
 1. target (FSM.initial M) p = q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) p = q

goal (1 subgoal):
 1. io \<in> \<Union> {(\<lambda>io_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (from_FSM M (target q pt)) A |p pt q A. \<exists>P q' t1 t2. (q, P) \<in> prs \<and> path P (FSM.initial P) p \<and> target (FSM.initial P) p = q \<and> pt \<in> tps q \<and> q' \<in> rd_targets (q, pt) \<and> (A, t1, t2) \<in> atcs (target q pt, q')} \<Longrightarrow> io \<in> L M
[PROOF STEP]
obtain p2 d where "(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p2 d. (pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using t6[OF \<open>q \<in> fst ` prs\<close>] \<open>pt \<in> tps q\<close>
[PROOF STATE]
proof (prove)
using this:
tps q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M q repetition_sets m \<subseteq> tps q
pt \<in> tps q

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

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

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF \<open>path M (initial M) p\<close>], of m]
[PROOF STATE]
proof (prove)
using this:
(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> q \<in> FSM.states M; \<And>d. d \<in> set repetition_sets \<Longrightarrow> d \<in> set repetition_sets\<rbrakk> \<Longrightarrow> m_traversal_paths_with_witness M (target (FSM.initial M) p) repetition_sets m = {(pa, d) |pa d. path M (target (FSM.initial M) p) pa \<and> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) pa)) repetition_sets = Some d \<and> (\<forall>p' p''. pa = p' @ p'' \<and> p'' \<noteq> [] \<longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)}

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
unfolding \<open>target (initial M) p = q\<close>
[PROOF STATE]
proof (prove)
using this:
(pt @ p2, d) \<in> m_traversal_paths_with_witness M q repetition_sets m
\<lbrakk>\<And>q. q \<in> FSM.states M \<Longrightarrow> q \<in> FSM.states M; \<And>d. d \<in> set repetition_sets \<Longrightarrow> d \<in> set repetition_sets\<rbrakk> \<Longrightarrow> m_traversal_paths_with_witness M q repetition_sets m = {(p, d) |p d. path M q p \<and> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p)) repetition_sets = Some d \<and> (\<forall>p' p''. p = p' @ p'' \<and> p'' \<noteq> [] \<longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)}

goal (1 subgoal):
 1. path M q (pt @ p2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path M q (pt @ p2)

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

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt)
[PROOF STEP]
using \<open>path M (initial M) p\<close> \<open>target (initial M) p = q\<close>
[PROOF STATE]
proof (prove)
using this:
path M q (pt @ p2)
path M (FSM.initial M) p
target (FSM.initial M) p = q

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ pt)

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

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

goal (1 subgoal):
 1. target q pt = target (FSM.initial M) (p @ pt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target q pt = target (FSM.initial M) (p @ pt)

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

goal (1 subgoal):
 1. target q pt \<in> FSM.states M
[PROOF STEP]
using path_target_is_state
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ pt)
target q pt = target (FSM.initial M) (p @ pt)
path ?M ?q ?p \<Longrightarrow> target ?q ?p \<in> FSM.states ?M

goal (1 subgoal):
 1. target q pt \<in> FSM.states M
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
target q pt \<in> FSM.states M

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

goal (1 subgoal):
 1. ioA \<in> LS M (target q pt)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioA \<in> LS M (target q pt)

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

goal (1 subgoal):
 1. (\<And>pA. \<lbrakk>path M (target q pt) pA; p_io pA = ioA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (target q pt) pA
p_io pA = ioA

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

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt @ pA)
[PROOF STEP]
using \<open>path M (initial M) (p@pt)\<close>
[PROOF STATE]
proof (prove)
using this:
path M (target q pt) pA
p_io pA = ioA
path M (FSM.initial M) (p @ pt)

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt @ pA)
[PROOF STEP]
unfolding \<open>(target q pt) = target (initial M) (p@pt)\<close>
[PROOF STATE]
proof (prove)
using this:
path M (target (FSM.initial M) (p @ pt)) pA
p_io pA = ioA
path M (FSM.initial M) (p @ pt)

goal (1 subgoal):
 1. path M (FSM.initial M) (p @ pt @ pA)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (p @ pt @ pA)

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

goal (1 subgoal):
 1. p_io p @ p_io pt @ ioA \<in> L M
[PROOF STEP]
unfolding \<open>p_io pA = ioA\<close>[symmetric]
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ pt @ pA)

goal (1 subgoal):
 1. p_io p @ p_io pt @ p_io pA \<in> L M
[PROOF STEP]
using language_intro
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p @ pt @ pA)
path ?M ?q ?p \<Longrightarrow> p_io ?p \<in> LS ?M ?q

goal (1 subgoal):
 1. p_io p @ p_io pt @ p_io pA \<in> L M
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p_io p @ p_io pt @ ioA \<in> L M

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

goal (1 subgoal):
 1. io \<in> L M
[PROOF STEP]
unfolding \<open>io = p_io p @ p_io pt @ ioA\<close>
[PROOF STATE]
proof (prove)
using this:
p_io p @ p_io pt @ ioA \<in> L M

goal (1 subgoal):
 1. p_io p @ p_io pt @ ioA \<in> L M
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
io \<in> L M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io \<in> L M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minimal_io_seq_to_failure :
  assumes "\<not> (L M' \<subseteq> L M)"
  and     "inputs M' = inputs M"
  and     "completely_specified M"
obtains io x y y' where "io@[(x,y)] \<in> L M" and "io@[(x,y')] \<notin>  L M" and "io@[(x,y')] \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain ioF where "ioF \<in> L M'" and "ioF \<notin> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ioF. \<lbrakk>ioF \<in> L M'; ioF \<notin> L M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> L M' \<subseteq> L M

goal (1 subgoal):
 1. (\<And>ioF. \<lbrakk>ioF \<in> L M'; ioF \<notin> L M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ioF \<in> L M'
ioF \<notin> L M

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?prefs = "{ioF' \<in> set (prefixes ioF) . ioF' \<in> L M' \<and> ioF' \<notin> L M}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "finite ?prefs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
[PROOF STEP]
using prefixes_finite
[PROOF STATE]
proof (prove)
using this:
finite {x \<in> set (prefixes ?xs). ?P x}

goal (1 subgoal):
 1. finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?prefs \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ioF' \<in> {xs'. \<exists>xs''. xs' @ xs'' = ioF}. ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}
[PROOF STEP]
using \<open>ioF \<in> L M'\<close> \<open>ioF \<notin> L M\<close>
[PROOF STATE]
proof (prove)
using this:
ioF \<in> L M'
ioF \<notin> L M

goal (1 subgoal):
 1. {ioF' \<in> {xs'. \<exists>xs''. xs' @ xs'' = ioF}. ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
{ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}
[PROOF STEP]
obtain ioF' where "ioF' \<in> ?prefs" and "\<And> ioF'' . ioF'' \<in> ?prefs \<Longrightarrow> length ioF' \<le> length ioF''"
[PROOF STATE]
proof (prove)
using this:
finite {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
{ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<noteq> {}

goal (1 subgoal):
 1. (\<And>ioF'. \<lbrakk>ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}; \<And>ioF''. ioF'' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<Longrightarrow> length ioF' \<le> length ioF''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson leI min_length_elem)
[PROOF STATE]
proof (state)
this:
ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
?ioF'' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<Longrightarrow> length ioF' \<le> length ?ioF''

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
?ioF'' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<Longrightarrow> length ioF' \<le> length ?ioF''
[PROOF STEP]
have "ioF' \<in> L M'" and "ioF' \<notin> L M"
[PROOF STATE]
proof (prove)
using this:
ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
?ioF'' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<Longrightarrow> length ioF' \<le> length ?ioF''

goal (1 subgoal):
 1. ioF' \<in> L M' &&& ioF' \<notin> L M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ioF' \<in> L M'
ioF' \<notin> L M

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioF' \<in> L M'
ioF' \<notin> L M
[PROOF STEP]
have "ioF' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
ioF' \<in> L M'
ioF' \<notin> L M

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

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioF' \<noteq> []
[PROOF STEP]
have "ioF' = (butlast ioF')@[last ioF']" and "length (butlast ioF') < length ioF'"
[PROOF STATE]
proof (prove)
using this:
ioF' \<noteq> []

goal (1 subgoal):
 1. ioF' = butlast ioF' @ [last ioF'] &&& length (butlast ioF') < length ioF'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ioF' = butlast ioF' @ [last ioF']
length (butlast ioF') < length ioF'

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ioF' = butlast ioF' @ [last ioF']
length (butlast ioF') < length ioF'
[PROOF STEP]
have "butlast ioF' \<notin> ?prefs"
[PROOF STATE]
proof (prove)
using this:
ioF' = butlast ioF' @ [last ioF']
length (butlast ioF') < length ioF'

goal (1 subgoal):
 1. butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
[PROOF STEP]
using \<open>\<And> ioF'' . ioF'' \<in> ?prefs \<Longrightarrow> length ioF' \<le> length ioF''\<close> leD
[PROOF STATE]
proof (prove)
using this:
ioF' = butlast ioF' @ [last ioF']
length (butlast ioF') < length ioF'
?ioF'' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M} \<Longrightarrow> length ioF' \<le> length ?ioF''
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "butlast ioF' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast ioF' \<in> L M'
[PROOF STEP]
using \<open>ioF' \<in> L M'\<close> language_prefix[of "butlast ioF'" "[last ioF']" M' "initial M'"]
[PROOF STATE]
proof (prove)
using this:
ioF' \<in> L M'
butlast ioF' @ [last ioF'] \<in> L M' \<Longrightarrow> butlast ioF' \<in> L M'

goal (1 subgoal):
 1. butlast ioF' \<in> L M'
[PROOF STEP]
unfolding \<open>ioF' = (butlast ioF')@[last ioF']\<close>[symmetric]
[PROOF STATE]
proof (prove)
using this:
ioF' \<in> L M'
ioF' \<in> L M' \<Longrightarrow> butlast ioF' \<in> L M'

goal (1 subgoal):
 1. butlast ioF' \<in> L M'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
butlast ioF' \<in> L M'

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
butlast ioF' \<in> L M'

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "butlast ioF' \<in> set (prefixes ioF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
using \<open>ioF' = (butlast ioF')@[last ioF']\<close> \<open>ioF' \<in> ?prefs\<close> prefixes_set
[PROOF STATE]
proof (prove)
using this:
ioF' = butlast ioF' @ [last ioF']
ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
set (prefixes ?xs) = {xs'. \<exists>xs''. xs' @ xs'' = ?xs}

goal (1 subgoal):
 1. butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ioF' = butlast ioF' @ [last ioF']; ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}; \<And>xs. set (prefixes xs) = {xs'. \<exists>xs''. xs' @ xs'' = xs}\<rbrakk> \<Longrightarrow> butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
have "\<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF
[PROOF STEP]
using \<open>ioF' = butlast ioF' @ [last ioF']\<close> \<open>ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}\<close>
[PROOF STATE]
proof (prove)
using this:
ioF' = butlast ioF' @ [last ioF']
ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. \<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
ioF' = butlast ioF' @ [last ioF']
ioF' \<in> {ioF' \<in> {xs'. \<exists>xs''. xs' @ xs'' = ioF}. ioF' \<in> L M' \<and> ioF' \<notin> L M}

goal (1 subgoal):
 1. \<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF

goal (1 subgoal):
 1. \<lbrakk>ioF' = butlast ioF' @ [last ioF']; ioF' \<in> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}; \<And>xs. set (prefixes xs) = {xs'. \<exists>xs''. xs' @ xs'' = xs}\<rbrakk> \<Longrightarrow> butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF

goal (1 subgoal):
 1. butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
using prefixes_set
[PROOF STATE]
proof (prove)
using this:
\<exists>ps. (butlast ioF' @ [last ioF']) @ ps = ioF
set (prefixes ?xs) = {xs'. \<exists>xs''. xs' @ xs'' = ?xs}

goal (1 subgoal):
 1. butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
butlast ioF' \<in> set (prefixes ioF)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
butlast ioF' \<in> set (prefixes ioF)

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
butlast ioF' \<in> L M'
butlast ioF' \<in> set (prefixes ioF)
[PROOF STEP]
have "butlast ioF' \<in> L M"
[PROOF STATE]
proof (prove)
using this:
butlast ioF' \<notin> {ioF' \<in> set (prefixes ioF). ioF' \<in> L M' \<and> ioF' \<notin> L M}
butlast ioF' \<in> L M'
butlast ioF' \<in> set (prefixes ioF)

goal (1 subgoal):
 1. butlast ioF' \<in> L M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
butlast ioF' \<in> L M

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have *: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<in> L M'
[PROOF STEP]
using \<open>ioF' \<in> L M'\<close> \<open>ioF' = (butlast ioF')@[last ioF']\<close>
[PROOF STATE]
proof (prove)
using this:
ioF' \<in> L M'
ioF' = butlast ioF' @ [last ioF']

goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<in> L M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<in> L M'

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have **: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] \<notin> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<notin> L M
[PROOF STEP]
using \<open>ioF' \<notin> L M\<close> \<open>ioF' = (butlast ioF')@[last ioF']\<close>
[PROOF STATE]
proof (prove)
using this:
ioF' \<notin> L M
ioF' = butlast ioF' @ [last ioF']

goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<notin> L M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast ioF' @ [(fst (last ioF'), snd (last ioF'))] \<notin> L M

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain p where "path M (initial M) p" and "p_io p = butlast ioF'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path M (FSM.initial M) p; p_io p = butlast ioF'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>butlast ioF' \<in> L M\<close>
[PROOF STATE]
proof (prove)
using this:
butlast ioF' \<in> L M

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

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) p
p_io p = butlast ioF'

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain t where "t \<in> transitions M"
                      and "t_source t = target (initial M) p"
                      and "t_input t = fst (last ioF')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "fst (last ioF') \<in> inputs M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (last ioF') \<in> FSM.inputs M'
[PROOF STEP]
using language_io(1)[OF *, of "fst (last ioF')" "snd (last ioF')"]
[PROOF STATE]
proof (prove)
using this:
(fst (last ioF'), snd (last ioF')) \<in> set (butlast ioF' @ [(fst (last ioF'), snd (last ioF'))]) \<Longrightarrow> fst (last ioF') \<in> FSM.inputs M'

goal (1 subgoal):
 1. fst (last ioF') \<in> FSM.inputs M'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (last ioF') \<in> FSM.inputs M'

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (last ioF') \<in> FSM.inputs M'
[PROOF STEP]
have "fst (last ioF') \<in> inputs M"
[PROOF STATE]
proof (prove)
using this:
fst (last ioF') \<in> FSM.inputs M'

goal (1 subgoal):
 1. fst (last ioF') \<in> FSM.inputs M
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
fst (last ioF') \<in> FSM.inputs M'
FSM.inputs M' = FSM.inputs M

goal (1 subgoal):
 1. fst (last ioF') \<in> FSM.inputs M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (last ioF') \<in> FSM.inputs M

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (last ioF') \<in> FSM.inputs M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (last ioF') \<in> FSM.inputs M

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that \<open>completely_specified M\<close> path_target_is_state[OF \<open>path M (initial M) p\<close>]
[PROOF STATE]
proof (prove)
using this:
fst (last ioF') \<in> FSM.inputs M
\<lbrakk>?t \<in> FSM.transitions M; t_source ?t = target (FSM.initial M) p; t_input ?t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis
completely_specified M
target (FSM.initial M) p \<in> FSM.states M

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding completely_specified.simps
[PROOF STATE]
proof (prove)
using this:
fst (last ioF') \<in> FSM.inputs M
\<lbrakk>?t \<in> FSM.transitions M; t_source ?t = target (FSM.initial M) p; t_input ?t = fst (last ioF')\<rbrakk> \<Longrightarrow> thesis
\<forall>q\<in>FSM.states M. \<forall>x\<in>FSM.inputs M. \<exists>t\<in>FSM.transitions M. t_source t = q \<and> t_input t = x
target (FSM.initial M) p \<in> FSM.states M

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> FSM.transitions M
t_source t = target (FSM.initial M) p
t_input t = fst (last ioF')

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M (FSM.initial M) p
p_io p = butlast ioF'
t \<in> FSM.transitions M
t_source t = target (FSM.initial M) p
t_input t = fst (last ioF')
[PROOF STEP]
have ***: "(butlast ioF')@[(fst (last ioF'), t_output t)] \<in> L M"
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) p
p_io p = butlast ioF'
t \<in> FSM.transitions M
t_source t = target (FSM.initial M) p
t_input t = fst (last ioF')

goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>path M (FSM.initial M) p; p_io p = butlast ioF'; t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M
[PROOF STEP]
have "p_io (p @ [t]) \<in> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (p @ [t]) \<in> L M
[PROOF STEP]
by (metis (no_types) \<open>path M (FSM.initial M) p\<close> \<open>t \<in> FSM.transitions M\<close> \<open>t_source t = target (FSM.initial M) p\<close>
            language_intro path_append single_transition_path)
[PROOF STATE]
proof (state)
this:
p_io (p @ [t]) \<in> L M

goal (1 subgoal):
 1. \<lbrakk>path M (FSM.initial M) p; p_io p = butlast ioF'; t \<in> FSM.transitions M; t_source t = target (FSM.initial M) p; t_input t = fst (last ioF')\<rbrakk> \<Longrightarrow> butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io (p @ [t]) \<in> L M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p_io (p @ [t]) \<in> L M

goal (1 subgoal):
 1. butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M
[PROOF STEP]
by (simp add: \<open>p_io p = butlast ioF'\<close> \<open>t_input t = fst (last ioF')\<close>)
[PROOF STATE]
proof (state)
this:
butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
butlast ioF' @ [(fst (last ioF'), t_output t)] \<in> L M

goal (1 subgoal):
 1. (\<And>io x y y'. \<lbrakk>io @ [(x, y)] \<in> L M; io @ [(x, y')] \<notin> L M; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[OF *** ** *]
[PROOF STATE]
proof (prove)
using this:
thesis

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

goal:
No subgoals!
[PROOF STEP]
qed