[STATEMENT]
lemma passes_test_suite_soundness :
  assumes "implies_completeness (Test_Suite prs tps rd_targets separators) M m"
  and     "observable M"
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "completely_specified M"
  and     "L M' \<subseteq> L M"
shows     "passes_test_suite M (Test_Suite prs tps rd_targets separators) M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
implies_completeness (Test_Suite prs tps rd_targets separators) M m

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

goal (1 subgoal):
 1. (\<And>repetition_sets. implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) 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 separators) M m repetition_sets

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t1: "(initial M, initial_preamble M) \<in> prs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> prs
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs

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

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t2: "\<And> q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}
[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 \<and> tps q \<noteq> {}
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t3: "\<And> q1 q2 A d1 d2. (A, d1, d2) \<in> separators (q1, q2) \<Longrightarrow> (A, d2, d1) \<in> separators (q2, q1) \<and> is_separator M q1 q2 A d1 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q1 q2 A d1 d2. (A, d1, d2) \<in> separators (q1, q2) \<Longrightarrow> (A, d2, d1) \<in> separators (q2, q1) \<and> is_separator M q1 q2 A d1 d2
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
(?A, ?d1.0, ?d2.0) \<in> separators (?q1.0, ?q2.0) \<Longrightarrow> (?A, ?d2.0, ?d1.0) \<in> separators (?q2.0, ?q1.0) \<and> is_separator M ?q1.0 ?q2.0 ?A ?d1.0 ?d2.0

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

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) 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. passes_test_suite M (Test_Suite prs tps rd_targets separators) 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. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t7: "\<And> d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M"
  and  t8: "\<And> d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d"
  and  t9: "\<And> d q1 q2. d \<in> set repetition_sets \<Longrightarrow> q1 \<in> fst d \<Longrightarrow> q2 \<in> fst d \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> separators (q1, q2) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> snd d \<subseteq> fst d) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M \<and> snd ?d = fst ?d \<inter> fst ` prs
\<lbrakk>?d \<in> set repetition_sets; ?q1.0 \<in> fst ?d; ?q2.0 \<in> fst ?d; ?q1.0 \<noteq> ?q2.0\<rbrakk> \<Longrightarrow> separators (?q1.0, ?q2.0) \<noteq> {}

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

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t10: "\<And> q p d p1 p2 p3.
              q \<in> fst ` prs \<Longrightarrow>
              (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow>
              p = p1 @ p2 @ p3 \<Longrightarrow>
              p2 \<noteq> [] \<Longrightarrow>
              target q p1 \<in> fst d \<Longrightarrow>
              target q (p1 @ p2) \<in> fst d \<Longrightarrow>
              target q p1 \<noteq> target q (p1 @ p2) \<Longrightarrow>
              p1 \<in> tps q \<and> p1 @ p2 \<in> tps q \<and> target q p1 \<in> rd_targets (q, p1 @ p2) \<and> target q (p1 @ p2) \<in> rd_targets (q, p1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q p d p1 p2 p3. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2 @ p3; p2 \<noteq> []; target q p1 \<in> fst d; target q (p1 @ p2) \<in> fst d; target q p1 \<noteq> target q (p1 @ p2)\<rbrakk> \<Longrightarrow> p1 \<in> tps q \<and> p1 @ p2 \<in> tps q \<and> target q p1 \<in> rd_targets (q, p1 @ p2) \<and> target q (p1 @ p2) \<in> rd_targets (q, p1)
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(8)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> fst ` prs; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?p = ?p1.0 @ ?p2.0 @ ?p3.0; ?p2.0 \<noteq> []; target ?q ?p1.0 \<in> fst ?d; target ?q (?p1.0 @ ?p2.0) \<in> fst ?d; target ?q ?p1.0 \<noteq> target ?q (?p1.0 @ ?p2.0)\<rbrakk> \<Longrightarrow> ?p1.0 \<in> tps ?q \<and> ?p1.0 @ ?p2.0 \<in> tps ?q \<and> target ?q ?p1.0 \<in> rd_targets (?q, ?p1.0 @ ?p2.0) \<and> target ?q (?p1.0 @ ?p2.0) \<in> rd_targets (?q, ?p1.0)

goal (1 subgoal):
 1. \<And>q p d p1 p2 p3. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2 @ p3; p2 \<noteq> []; target q p1 \<in> fst d; target q (p1 @ p2) \<in> fst d; target q p1 \<noteq> target q (p1 @ p2)\<rbrakk> \<Longrightarrow> p1 \<in> tps q \<and> p1 @ p2 \<in> tps q \<and> target q p1 \<in> rd_targets (q, p1 @ p2) \<and> target q (p1 @ p2) \<in> rd_targets (q, p1)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> fst ` prs; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?p = ?p1.0 @ ?p2.0 @ ?p3.0; ?p2.0 \<noteq> []; target ?q ?p1.0 \<in> fst ?d; target ?q (?p1.0 @ ?p2.0) \<in> fst ?d; target ?q ?p1.0 \<noteq> target ?q (?p1.0 @ ?p2.0)\<rbrakk> \<Longrightarrow> ?p1.0 \<in> tps ?q \<and> ?p1.0 @ ?p2.0 \<in> tps ?q \<and> target ?q ?p1.0 \<in> rd_targets (?q, ?p1.0 @ ?p2.0) \<and> target ?q (?p1.0 @ ?p2.0) \<in> rd_targets (?q, ?p1.0)

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have t11: "\<And> q p d p1 p2 q'.
              q \<in> fst ` prs \<Longrightarrow>
              (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow>
              p = p1 @ p2 \<Longrightarrow>
              q' \<in> fst ` prs \<Longrightarrow>
              target q p1 \<in> fst d \<Longrightarrow>
              q' \<in> fst d \<Longrightarrow>
              target q p1 \<noteq> q' \<Longrightarrow>
              p1 \<in> tps q \<and> [] \<in> tps q' \<and> target q p1 \<in> rd_targets (q', []) \<and> q' \<in> rd_targets (q, p1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q p d p1 p2 q'. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2; q' \<in> fst ` prs; target q p1 \<in> fst d; q' \<in> fst d; target q p1 \<noteq> q'\<rbrakk> \<Longrightarrow> p1 \<in> tps q \<and> [] \<in> tps q' \<and> target q p1 \<in> rd_targets (q', []) \<and> q' \<in> rd_targets (q, p1)
[PROOF STEP]
using implies_completeness_for_repetition_sets_simps(9)[OF repetition_sets_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> fst ` prs; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?p = ?p1.0 @ ?p2.0; ?q' \<in> fst ` prs; target ?q ?p1.0 \<in> fst ?d; ?q' \<in> fst ?d; target ?q ?p1.0 \<noteq> ?q'\<rbrakk> \<Longrightarrow> ?p1.0 \<in> tps ?q \<and> [] \<in> tps ?q' \<and> target ?q ?p1.0 \<in> rd_targets (?q', []) \<and> ?q' \<in> rd_targets (?q, ?p1.0)

goal (1 subgoal):
 1. \<And>q p d p1 p2 q'. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2; q' \<in> fst ` prs; target q p1 \<in> fst d; q' \<in> fst d; target q p1 \<noteq> q'\<rbrakk> \<Longrightarrow> p1 \<in> tps q \<and> [] \<in> tps q' \<and> target q p1 \<in> rd_targets (q', []) \<and> q' \<in> rd_targets (q, p1)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> fst ` prs; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?p = ?p1.0 @ ?p2.0; ?q' \<in> fst ` prs; target ?q ?p1.0 \<in> fst ?d; ?q' \<in> fst ?d; target ?q ?p1.0 \<noteq> ?q'\<rbrakk> \<Longrightarrow> ?p1.0 \<in> tps ?q \<and> [] \<in> tps ?q' \<and> target ?q ?p1.0 \<in> rd_targets (?q', []) \<and> ?q' \<in> rd_targets (?q, ?p1.0)

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have "\<And> q P io x y y' . (q,P) \<in> prs \<Longrightarrow> io@[(x,y)] \<in> L P \<Longrightarrow> io@[(x,y')] \<in> L M' \<Longrightarrow> io@[(x,y')] \<in> L P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
fix q P io x y y'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
assume "(q,P) \<in> prs" and "io@[(x,y)] \<in> L P" and "io@[(x,y')] \<in> L M'"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
io @ [(x, y)] \<in> L P
io @ [(x, y')] \<in> L M'

goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
have "is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_preamble P M q
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>\<And> q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}

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

goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
have "io@[(x,y')] \<in> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io @ [(x, y')] \<in> L M
[PROOF STEP]
using \<open>io@[(x,y')] \<in> L M'\<close> assms(6)
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y')] \<in> L M'
L M' \<subseteq> L M

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

goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> prs; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
show "io@[(x,y')] \<in> L P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
using passes_test_suite_soundness_helper_1[OF \<open>is_preamble P M q\<close> assms(2) \<open>io@[(x,y)] \<in> L P\<close> \<open>io@[(x,y')] \<in> L M\<close>]
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y')] \<in> L P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
io @ [(x, y')] \<in> L P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> prs; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?q, ?P) \<in> prs; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P
[PROOF STEP]
have p1: "(\<forall> q P io x y y' . (q,P) \<in> prs \<longrightarrow> io@[(x,y)] \<in> L P \<longrightarrow> io@[(x,y')] \<in> L M' \<longrightarrow> io@[(x,y')] \<in> L P)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?q, ?P) \<in> prs; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P

goal (1 subgoal):
 1. \<forall>q P io x y y'. (q, P) \<in> prs \<longrightarrow> io @ [(x, y)] \<in> L P \<longrightarrow> io @ [(x, y')] \<in> L M' \<longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>q P io x y y'. (q, P) \<in> prs \<longrightarrow> io @ [(x, y)] \<in> L P \<longrightarrow> io @ [(x, y')] \<in> L M' \<longrightarrow> io @ [(x, y')] \<in> L P

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have "\<And> q P pP ioT pT x x' y y' . (q,P) \<in> prs \<Longrightarrow>
                                     path P (initial P) pP \<Longrightarrow>
                                     target (initial P) pP = q \<Longrightarrow>
                                     pT \<in> tps q \<Longrightarrow>
                                     ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<Longrightarrow>
                                     (p_io pP)@ioT@[(x',y')] \<in> L M' \<Longrightarrow>
                                     (\<exists> pT' . pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
fix q P pP ioT pT x x' y y'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
assume "(q,P) \<in> prs"
       and "path P (initial P) pP"
       and "target (initial P) pP = q"
       and "pT \<in> tps q"
       and "ioT @ [(x, y)] \<in> set (prefixes (p_io pT))"
       and "(p_io pP)@ioT@[(x',y')] \<in> L M'"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
path P (FSM.initial P) pP
target (FSM.initial P) pP = q
pT \<in> tps q
ioT @ [(x, y)] \<in> set (prefixes (p_io pT))
p_io pP @ ioT @ [(x', y')] \<in> L M'

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_preamble P M q
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>\<And> q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}

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

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_preamble P M q
[PROOF STEP]
have "q \<in> states M"
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. q \<in> FSM.states 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. q \<in> FSM.states M
[PROOF STEP]
by (metis \<open>path P (FSM.initial P) pP\<close> \<open>target (FSM.initial P) pP = q\<close> path_target_is_state submachine_path)
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "initial P = initial M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial P = FSM.initial M
[PROOF STEP]
using \<open>is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. FSM.initial P = FSM.initial 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. 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. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "path M (initial M) pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) pP
[PROOF STEP]
using \<open>is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[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. path M (FSM.initial M) pP
[PROOF STEP]
using submachine_path_initial
[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)))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[PROOF STEP]
using \<open>path P (FSM.initial P) pP\<close>
[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)))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p
path P (FSM.initial P) pP

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

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "(p_io pP)@ioT@[(x',y')] \<in> L M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ ioT @ [(x', y')] \<in> L M
[PROOF STEP]
using \<open>(p_io pP)@ioT@[(x',y')] \<in> L M'\<close> assms(6)
[PROOF STATE]
proof (prove)
using this:
p_io pP @ ioT @ [(x', y')] \<in> L M'
L M' \<subseteq> L M

goal (1 subgoal):
 1. p_io pP @ ioT @ [(x', y')] \<in> L M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p_io pP @ ioT @ [(x', y')] \<in> L M

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io pP @ ioT @ [(x', y')] \<in> L M
[PROOF STEP]
obtain pM' where "path M (initial M) pM'" and "p_io pM' = (p_io pP)@ioT@[(x',y')]"
[PROOF STATE]
proof (prove)
using this:
p_io pP @ ioT @ [(x', y')] \<in> L M

goal (1 subgoal):
 1. (\<And>pM'. \<lbrakk>path M (FSM.initial M) pM'; p_io pM' = p_io pP @ ioT @ [(x', y')]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) pM'
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
let ?pP = "take (length pP) pM'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
let ?pT = "take (length ioT) (drop (length pP) pM')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
let ?t  = "last pM'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "pM' = ?pP @ ?pT @ [?t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']
[PROOF STEP]
have "length pM' = (length pP) + (length ioT) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length pM' = length pP + length ioT + 1
[PROOF STEP]
using \<open>p_io pM' = (p_io pP)@ioT@[(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. length pM' = length pP + length ioT + 1
[PROOF STEP]
unfolding length_map[of "(\<lambda> t . (t_input t, t_output t))", of pM', symmetric]
                  length_map[of "(\<lambda> t . (t_input t, t_output t))", of pP, symmetric]
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. length (p_io pM') = length (p_io pP) + length ioT + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length pM' = length pP + length ioT + 1

goal (1 subgoal):
 1. pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pM' = length pP + length ioT + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length pM' = length pP + length ioT + 1

goal (1 subgoal):
 1. pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']
[PROOF STEP]
by (metis (no_types, lifting) add_diff_cancel_right' antisym_conv antisym_conv2
              append_butlast_last_id append_eq_append_conv2 butlast_conv_take drop_Nil drop_eq_Nil
              le_add1 less_add_one take_add)
[PROOF STATE]
proof (state)
this:
pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "p_io ?pP = p_io pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length pP) pM') = p_io pP
[PROOF STEP]
using \<open>p_io pM' = (p_io pP)@ioT@[(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. p_io (take (length pP) pM') = p_io pP
[PROOF STEP]
by (metis (no_types, lifting) append_eq_conv_conj length_map take_map)
[PROOF STATE]
proof (state)
this:
p_io (take (length pP) pM') = p_io pP

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "p_io ?pT = ioT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length ioT) (drop (length pP) pM')) = ioT
[PROOF STEP]
using \<open>p_io pM' = (p_io pP)@ioT@[(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. p_io (take (length ioT) (drop (length pP) pM')) = ioT
[PROOF STEP]
using \<open>pM' = ?pP @ ?pT @ [?t]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]
pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']

goal (1 subgoal):
 1. p_io (take (length ioT) (drop (length pP) pM')) = ioT
[PROOF STEP]
by (metis (no_types, lifting) append_eq_conv_conj length_map map_append take_map)
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) (drop (length pP) pM')) = ioT

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "p_io [?t] = [(x',y')]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io [last pM'] = [(x', y')]
[PROOF STEP]
using \<open>p_io pM' = (p_io pP)@ioT@[(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]

goal (1 subgoal):
 1. p_io [last pM'] = [(x', y')]
[PROOF STEP]
using \<open>pM' = ?pP @ ?pT @ [?t]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pM' = p_io pP @ ioT @ [(x', y')]
pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']

goal (1 subgoal):
 1. p_io [last pM'] = [(x', y')]
[PROOF STEP]
by (metis (no_types, lifting) append_is_Nil_conv last_appendR last_map last_snoc list.simps(8) list.simps(9))
[PROOF STATE]
proof (state)
this:
p_io [last pM'] = [(x', y')]

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "path M (initial M) ?pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) (take (length pP) pM')
[PROOF STEP]
using \<open>path M (initial M) pM'\<close> \<open>pM' = ?pP @ ?pT @ [?t]\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) pM'
pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']

goal (1 subgoal):
 1. path M (FSM.initial M) (take (length pP) pM')
[PROOF STEP]
by (meson path_prefix_take)
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) (take (length pP) pM')

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "?pP = pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length pP) pM' = pP
[PROOF STEP]
using observable_path_unique[OF \<open>observable M\<close> \<open>path M (initial M) ?pP\<close> \<open>path M (initial M) pP\<close> \<open>p_io ?pP = p_io pP\<close>]
[PROOF STATE]
proof (prove)
using this:
take (length pP) pM' = pP

goal (1 subgoal):
 1. take (length pP) pM' = pP
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
take (length pP) pM' = pP

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length pP) pM' = pP
[PROOF STEP]
have "path M q (?pT@[?t])"
[PROOF STATE]
proof (prove)
using this:
take (length pP) pM' = pP

goal (1 subgoal):
 1. path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])
[PROOF STEP]
by (metis \<open>FSM.initial P = FSM.initial M\<close> \<open>pM' = take (length pP) pM' @ take (length ioT) (drop (length pP) pM') @ [last pM']\<close> \<open>path M (FSM.initial M) pM'\<close> \<open>target (FSM.initial P) pP = q\<close> path_suffix)
[PROOF STATE]
proof (state)
this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])
[PROOF STEP]
have "path M q ?pT"
         and  "?t \<in> transitions M"
         and  "t_source ?t = target q ?pT"
[PROOF STATE]
proof (prove)
using this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])

goal (1 subgoal):
 1. path M q (take (length ioT) (drop (length pP) pM')) &&& last pM' \<in> FSM.transitions M &&& t_source (last pM') = target q (take (length ioT) (drop (length pP) pM'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M q (take (length ioT) (drop (length pP) pM'))
last pM' \<in> FSM.transitions M
t_source (last pM') = target q (take (length ioT) (drop (length pP) pM'))

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "inputs M \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.inputs M \<noteq> {}
[PROOF STEP]
using language_io(1)[OF \<open>(p_io pP)@ioT@[(x',y')] \<in> L M\<close>, of x' y']
[PROOF STATE]
proof (prove)
using this:
(x', y') \<in> set (p_io pP @ ioT @ [(x', y')]) \<Longrightarrow> x' \<in> FSM.inputs M

goal (1 subgoal):
 1. FSM.inputs M \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.inputs M \<noteq> {}

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[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]
using image_iff
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

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

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
obtain ioT' where "p_io pT = (ioT @ [(x, y)]) @ ioT'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ioT'. p_io pT = (ioT @ [(x, y)]) @ ioT' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>ioT @ [(x, y)] \<in> set (prefixes (p_io pT))\<close>
[PROOF STATE]
proof (prove)
using this:
ioT @ [(x, y)] \<in> set (prefixes (p_io pT))

goal (1 subgoal):
 1. (\<And>ioT'. p_io pT = (ioT @ [(x, y)]) @ ioT' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
ioT @ [(x, y)] \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io pT}

goal (1 subgoal):
 1. (\<And>ioT'. p_io pT = (ioT @ [(x, y)]) @ ioT' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
p_io pT = (ioT @ [(x, y)]) @ ioT'

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io pT = (ioT @ [(x, y)]) @ ioT'
[PROOF STEP]
have "length pT > length ioT"
[PROOF STATE]
proof (prove)
using this:
p_io pT = (ioT @ [(x, y)]) @ ioT'

goal (1 subgoal):
 1. length ioT < length pT
[PROOF STEP]
using length_map[of "(\<lambda> t . (t_input t, t_output t))" pT]
[PROOF STATE]
proof (prove)
using this:
p_io pT = (ioT @ [(x, y)]) @ ioT'
length (p_io pT) = length pT

goal (1 subgoal):
 1. length ioT < length pT
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ioT < length pT

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
obtain pT' d' where "(pT @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pT' d'. (pT @ pT', 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>pT' d'. (pT @ pT', 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 @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
let ?p = "pT @ pT'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "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  "\<And> p' p''. ?p = p' @ p'' \<Longrightarrow> 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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M q (pT @ pT') &&& find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (pT @ pT'))) repetition_sets = Some d' &&& (\<And>p' p''. \<lbrakk>pT @ pT' = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)
[PROOF STEP]
using \<open>(pT @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
            m_traversal_paths_with_witness_set[OF t5 t8 \<open>q \<in> states M\<close>, of m]
[PROOF STATE]
proof (prove)
using this:
(pT @ pT', 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 @ pT') &&& find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (pT @ pT'))) repetition_sets = Some d' &&& (\<And>p' p''. \<lbrakk>pT @ pT' = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
path M q (pT @ pT')
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (pT @ pT'))) repetition_sets = Some d'
\<lbrakk>pT @ pT' = ?p' @ ?p''; ?p'' \<noteq> []\<rbrakk> \<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. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
let ?pIO = "take (length ioT) pT"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "?pIO = take (length ioT) ?p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length ioT) pT = take (length ioT) (pT @ pT')
[PROOF STEP]
using \<open>length pT > length ioT\<close>
[PROOF STATE]
proof (prove)
using this:
length ioT < length pT

goal (1 subgoal):
 1. take (length ioT) pT = take (length ioT) (pT @ pT')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (length ioT) pT = take (length ioT) (pT @ pT')

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length ioT) pT = take (length ioT) (pT @ pT')
[PROOF STEP]
have "?p = ?pIO@(drop (length ioT) ?p)"
[PROOF STATE]
proof (prove)
using this:
take (length ioT) pT = take (length ioT) (pT @ pT')

goal (1 subgoal):
 1. pT @ pT' = take (length ioT) pT @ drop (length ioT) (pT @ pT')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pT @ pT' = take (length ioT) pT @ drop (length ioT) (pT @ pT')

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "(drop (length ioT) ?p) \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length ioT) (pT @ pT') \<noteq> []
[PROOF STEP]
using \<open>length pT > length ioT\<close>
[PROOF STATE]
proof (prove)
using this:
length ioT < length pT

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

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "p_io ?pIO = ioT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
have "p_io ?pIO = take (length ioT) (p_io pT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io (take (length ioT) pT) = take (length ioT) (p_io pT)
[PROOF STEP]
by (simp add: take_map)
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) pT) = take (length ioT) (p_io pT)

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) pT) = take (length ioT) (p_io pT)

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
have "take (length ioT) (p_io pT) = ioT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length ioT) (p_io pT) = ioT
[PROOF STEP]
using \<open>p_io pT = (ioT @ [(x, y)]) @ ioT'\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pT = (ioT @ [(x, y)]) @ ioT'

goal (1 subgoal):
 1. take (length ioT) (p_io pT) = ioT
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (length ioT) (p_io pT) = ioT

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p_io (take (length ioT) pT) = take (length ioT) (p_io pT)
take (length ioT) (p_io pT) = ioT
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) pT) = take (length ioT) (p_io pT)
take (length ioT) (p_io pT) = ioT

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = ioT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) pT) = ioT

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) pT) = ioT

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io (take (length ioT) pT) = ioT
[PROOF STEP]
have "p_io ?pIO = p_io ?pT"
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) pT) = ioT

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = p_io (take (length ioT) (drop (length pP) pM'))
[PROOF STEP]
using \<open>p_io ?pT = ioT\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) pT) = ioT
p_io (take (length ioT) (drop (length pP) pM')) = ioT

goal (1 subgoal):
 1. p_io (take (length ioT) pT) = p_io (take (length ioT) (drop (length pP) pM'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p_io (take (length ioT) pT) = p_io (take (length ioT) (drop (length pP) pM'))

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "path M q ?pIO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M q (take (length ioT) pT)
[PROOF STEP]
using \<open>path M q ?p\<close>
[PROOF STATE]
proof (prove)
using this:
path M q (pT @ pT')

goal (1 subgoal):
 1. path M q (take (length ioT) pT)
[PROOF STEP]
unfolding \<open>?pIO = take (length ioT) ?p\<close>
[PROOF STATE]
proof (prove)
using this:
path M q (pT @ pT')

goal (1 subgoal):
 1. path M q (take (length ioT) (pT @ pT'))
[PROOF STEP]
using path_prefix_take
[PROOF STATE]
proof (prove)
using this:
path M q (pT @ pT')
path ?M ?q ?p \<Longrightarrow> path ?M ?q (take ?i ?p)

goal (1 subgoal):
 1. path M q (take (length ioT) (pT @ pT'))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
path M q (take (length ioT) pT)

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "?pT = ?pIO"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (length ioT) (drop (length pP) pM') = take (length ioT) pT
[PROOF STEP]
using observable_path_unique[OF \<open>observable M\<close> \<open>path M q ?pIO\<close> \<open>path M q ?pT\<close> \<open>p_io ?pIO = p_io ?pT\<close>]
[PROOF STATE]
proof (prove)
using this:
take (length ioT) pT = take (length ioT) (drop (length pP) pM')

goal (1 subgoal):
 1. take (length ioT) (drop (length pP) pM') = take (length ioT) pT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') = take (length ioT) pT

goal (1 subgoal):
 1. \<And>q P pP ioT pT x x' y y'. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; ioT @ [(x, y)] \<in> set (prefixes (p_io pT)); p_io pP @ ioT @ [(x', y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
show "(\<exists> pT' . pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
proof (cases "find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (?pT@[?t]))) repetition_sets = None")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None

goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
obtain pT' d' where "(?pT @ [?t] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pT' d'. (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using m_traversal_path_extension_exist[OF \<open>completely_specified M\<close> \<open>q \<in> states M\<close> \<open>inputs M \<noteq> {}\<close> t5 t8 \<open>path M q (?pT@[?t])\<close> True]
[PROOF STATE]
proof (prove)
using this:
\<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> \<exists>p2 d'. ((take (length ioT) (drop (length pP) pM') @ [last pM']) @ p2, d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. (\<And>pT' d'. (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
have "?pT @ [?t] @ pT' \<in> tps q"
[PROOF STATE]
proof (prove)
using this:
(take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q
[PROOF STEP]
using t6[OF \<open>q \<in> fst ` prs\<close>]
[PROOF STATE]
proof (prove)
using this:
(take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m
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. take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q

goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q

goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "ioT @ [(x', y')] \<in> set (prefixes (p_io (?pT @ [?t] @ pT')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT')))
[PROOF STEP]
using \<open>p_io ?pIO = ioT\<close> \<open>p_io [?t] = [(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) pT) = ioT
p_io [last pM'] = [(x', y')]

goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT')))
[PROOF STEP]
unfolding \<open>?pT = ?pIO\<close> prefixes_set
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) pT) = ioT
p_io [last pM'] = [(x', y')]

goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io (take (length ioT) pT @ [last pM'] @ pT')}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT')))

goal (2 subgoals):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
 2. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT')))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT' \<in> tps q
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'] @ pT')))

goal (1 subgoal):
 1. \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
note \<open>path M q (?pT @ [?t])\<close>
[PROOF STATE]
proof (state)
this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
obtain d' where "find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (?pT@[?t]))) repetition_sets = Some d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d'. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None

goal (1 subgoal):
 1. (\<And>d'. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d'

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d'

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "\<forall> p' p''. (?pT @ [?t]) = 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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
[PROOF STEP]
have "\<And> p' p''. (?pT @ [?t]) = p' @ p'' \<Longrightarrow> 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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
fix p' p''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
assume "(?pT @ [?t]) = p' @ p''" and "p'' \<noteq> []"
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''
p'' \<noteq> []

goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''
p'' \<noteq> []
[PROOF STEP]
obtain pIO' where "?pIO = p' @ pIO'"
[PROOF STATE]
proof (prove)
using this:
take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''
p'' \<noteq> []

goal (1 subgoal):
 1. (\<And>pIO'. take (length ioT) pT = p' @ pIO' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>?pT = ?pIO\<close>
[PROOF STATE]
proof (prove)
using this:
take (length ioT) pT @ [last pM'] = p' @ p''
p'' \<noteq> []

goal (1 subgoal):
 1. (\<And>pIO'. take (length ioT) pT = p' @ pIO' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis butlast_append butlast_snoc)
[PROOF STATE]
proof (state)
this:
take (length ioT) pT = p' @ pIO'

goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take (length ioT) pT = p' @ pIO'
[PROOF STEP]
have "?p = p'@pIO'@(drop (length ioT) ?p)"
[PROOF STATE]
proof (prove)
using this:
take (length ioT) pT = p' @ pIO'

goal (1 subgoal):
 1. pT @ pT' = p' @ pIO' @ drop (length ioT) (pT @ pT')
[PROOF STEP]
using \<open>?p = ?pIO@((drop (length ioT) ?p))\<close>
[PROOF STATE]
proof (prove)
using this:
take (length ioT) pT = p' @ pIO'
pT @ pT' = take (length ioT) pT @ drop (length ioT) (pT @ pT')

goal (1 subgoal):
 1. pT @ pT' = p' @ pIO' @ drop (length ioT) (pT @ pT')
[PROOF STEP]
by (metis append.assoc)
[PROOF STATE]
proof (state)
this:
pT @ pT' = p' @ pIO' @ drop (length ioT) (pT @ pT')

goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
have "pIO' @ drop (length ioT) (pT @ pT') \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pIO' @ drop (length ioT) (pT @ pT') \<noteq> []
[PROOF STEP]
using \<open>(drop (length ioT) ?p) \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
drop (length ioT) (pT @ pT') \<noteq> []

goal (1 subgoal):
 1. pIO' @ drop (length ioT) (pT @ pT') \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pIO' @ drop (length ioT) (pT @ pT') \<noteq> []

goal (1 subgoal):
 1. \<And>p' p''. \<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = p' @ p''; p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
show "find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
using \<open>\<And> p' p''. ?p = p' @ p'' \<Longrightarrow> 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\<close>
                  [of p' "pIO'@(drop (length ioT) ?p)", OF \<open>?p = p'@pIO'@(drop (length ioT) ?p)\<close> \<open>pIO' @ drop (length ioT) (pT @ pT') \<noteq> []\<close>]
[PROOF STATE]
proof (prove)
using this:
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. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) p')) repetition_sets = None

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = ?p' @ ?p''; ?p'' \<noteq> []\<rbrakk> \<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. \<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = ?p' @ ?p''; ?p'' \<noteq> []\<rbrakk> \<Longrightarrow> find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) ?p')) repetition_sets = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>take (length ioT) (drop (length pP) pM') @ [last pM'] = ?p' @ ?p''; ?p'' \<noteq> []\<rbrakk> \<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. \<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d'
\<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
[PROOF STEP]
have "((?pT @ [?t]),d') \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
using this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d'
\<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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. (take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
using m_traversal_paths_with_witness_set[OF t5 t8 \<open>q \<in> states M\<close>, of m]
[PROOF STATE]
proof (prove)
using this:
path M q (take (length ioT) (drop (length pP) pM') @ [last pM'])
find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets = Some d'
\<forall>p' p''. take (length ioT) (drop (length pP) pM') @ [last pM'] = 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
\<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. (take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
have "(?pT @ [?t]) \<in> tps q"
[PROOF STATE]
proof (prove)
using this:
(take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q
[PROOF STEP]
using t6[OF \<open>q \<in> fst ` prs\<close>]
[PROOF STATE]
proof (prove)
using this:
(take (length ioT) (drop (length pP) pM') @ [last pM'], d') \<in> m_traversal_paths_with_witness M q repetition_sets m
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. take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have "ioT @ [(x', y')] \<in> set (prefixes (p_io (?pT @ [?t])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])))
[PROOF STEP]
using \<open>p_io ?pT = ioT\<close> \<open>p_io [?t] = [(x',y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) (drop (length pP) pM')) = ioT
p_io [last pM'] = [(x', y')]

goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])))
[PROOF STEP]
unfolding prefixes_set
[PROOF STATE]
proof (prove)
using this:
p_io (take (length ioT) (drop (length pP) pM')) = ioT
p_io [last pM'] = [(x', y')]

goal (1 subgoal):
 1. ioT @ [(x', y')] \<in> {xs'. \<exists>xs''. xs' @ xs'' = p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])))

goal (1 subgoal):
 1. find (\<lambda>d. Suc (m - card (snd d)) \<le> length (filter (\<lambda>t. t_target t \<in> fst d) (take (length ioT) (drop (length pP) pM') @ [last pM']))) repetition_sets \<noteq> None \<Longrightarrow> \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take (length ioT) (drop (length pP) pM') @ [last pM'] \<in> tps q
ioT @ [(x', y')] \<in> set (prefixes (p_io (take (length ioT) (drop (length pP) pM') @ [last pM'])))

goal (1 subgoal):
 1. \<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x', y')] \<in> set (prefixes (p_io pT'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?ioT @ [(?x, ?y)] \<in> set (prefixes (p_io ?pT)); p_io ?pP @ ?ioT @ [(?x', ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps ?q \<and> ?ioT @ [(?x', ?y')] \<in> set (prefixes (p_io pT'))

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?ioT @ [(?x, ?y)] \<in> set (prefixes (p_io ?pT)); p_io ?pP @ ?ioT @ [(?x', ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps ?q \<and> ?ioT @ [(?x', ?y')] \<in> set (prefixes (p_io pT'))
[PROOF STEP]
have p2: "(\<forall> q P pP ioT pT x y y' . (q,P) \<in> prs \<longrightarrow>
                                            path P (initial P) pP \<longrightarrow>
                                            target (initial P) pP = q \<longrightarrow>
                                            pT \<in> tps q \<longrightarrow>
                                            ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow>
                                            (p_io pP)@ioT@[(x,y')] \<in> L M' \<longrightarrow>
                                            (\<exists> pT' . pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT'))))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?ioT @ [(?x, ?y)] \<in> set (prefixes (p_io ?pT)); p_io ?pP @ ?ioT @ [(?x', ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> \<exists>pT'. pT' \<in> tps ?q \<and> ?ioT @ [(?x', ?y')] \<in> set (prefixes (p_io pT'))

goal (1 subgoal):
 1. \<forall>q P pP ioT pT x y y'. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow> p_io pP @ ioT @ [(x, y')] \<in> L M' \<longrightarrow> (\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT')))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>q P pP ioT pT x y y'. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow> p_io pP @ ioT @ [(x, y')] \<in> L M' \<longrightarrow> (\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT')))

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
have "\<And> q P pP pT q' A d1 d2 qT . (q,P) \<in> prs \<Longrightarrow>
                                      path P (initial P) pP \<Longrightarrow>
                                      target (initial P) pP = q \<Longrightarrow>
                                      pT \<in> tps q \<Longrightarrow>
                                      q' \<in> rd_targets (q,pT) \<Longrightarrow>
                                      (A,d1,d2) \<in> separators (target q pT, q') \<Longrightarrow>
                                      qT \<in> io_targets M' ((p_io pP)@(p_io pT)) (initial M') \<Longrightarrow>
                                      pass_separator_ATC M' A qT d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
fix q P pP pT q' A d1 d2 qT
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
assume "(q,P) \<in> prs"
    and    "path P (initial P) pP"
    and    "target (initial P) pP = q"
    and    "pT \<in> tps q"
    and    "q' \<in> rd_targets (q,pT)"
    and    "(A,d1,d2) \<in> separators (target q pT, q')"
    and    "qT \<in> io_targets M' ((p_io pP)@(p_io pT)) (initial M')"
[PROOF STATE]
proof (state)
this:
(q, P) \<in> prs
path P (FSM.initial P) pP
target (FSM.initial P) pP = q
pT \<in> tps q
q' \<in> rd_targets (q, pT)
(A, d1, d2) \<in> separators (target q pT, q')
qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[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. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_preamble P M q
[PROOF STEP]
using \<open>(q,P) \<in> prs\<close> \<open>\<And> q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> prs
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}

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

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_preamble P M q
[PROOF STEP]
have "q \<in> states M"
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. q \<in> FSM.states 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. q \<in> FSM.states M
[PROOF STEP]
by (metis \<open>path P (FSM.initial P) pP\<close> \<open>target (FSM.initial P) pP = q\<close> path_target_is_state submachine_path)
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "initial P = initial M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial P = FSM.initial M
[PROOF STEP]
using \<open>is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. FSM.initial P = FSM.initial 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. 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. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "path M (initial M) pP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) pP
[PROOF STEP]
using \<open>is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[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. path M (FSM.initial M) pP
[PROOF STEP]
using submachine_path_initial
[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)))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p

goal (1 subgoal):
 1. path M (FSM.initial M) pP
[PROOF STEP]
using \<open>path P (FSM.initial P) pP\<close>
[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)))
\<lbrakk>is_submachine ?A ?B; path ?A (FSM.initial ?A) ?p\<rbrakk> \<Longrightarrow> path ?B (FSM.initial ?B) ?p
path P (FSM.initial P) pP

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

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "is_separator M (target q pT) q' A d1 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_separator M (target q pT) q' A d1 d2
[PROOF STEP]
using t3[OF \<open>(A,d1,d2) \<in> separators (target q pT, q')\<close>]
[PROOF STATE]
proof (prove)
using this:
(A, d2, d1) \<in> separators (q', target q pT) \<and> is_separator M (target q pT) q' A d1 d2

goal (1 subgoal):
 1. is_separator M (target q pT) q' A d1 d2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_separator M (target q pT) q' A d1 d2

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "qT \<in> states M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qT \<in> FSM.states M'
[PROOF STEP]
using \<open>qT \<in> io_targets M' ((p_io pP)@(p_io pT)) (initial M')\<close>
            io_targets_states
[PROOF STATE]
proof (prove)
using this:
qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')
io_targets ?M ?io ?q \<subseteq> FSM.states ?M

goal (1 subgoal):
 1. qT \<in> FSM.states M'
[PROOF STEP]
by (metis (no_types, lifting) subsetD)
[PROOF STATE]
proof (state)
this:
qT \<in> FSM.states M'

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
obtain pT' d' where "(pT @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pT' d'. (pT @ pT', 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>pT' d'. (pT @ pT', 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 @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pT @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m
[PROOF STEP]
have "path M q pT"
[PROOF STATE]
proof (prove)
using this:
(pT @ pT', d') \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. path M q pT
[PROOF STEP]
using m_traversal_paths_with_witness_set[OF t5 t8 \<open>q \<in> states M\<close>, of m]
[PROOF STATE]
proof (prove)
using this:
(pT @ pT', 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
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path M q pT

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path M q pT
[PROOF STEP]
have "target q pT \<in> FSM.states M"
[PROOF STATE]
proof (prove)
using this:
path M q 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 q 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. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "q' \<in> FSM.states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' \<in> FSM.states M
[PROOF STEP]
using is_separator_separated_state_is_state[OF \<open>is_separator M (target q pT) q' A d1 d2\<close>]
[PROOF STATE]
proof (prove)
using this:
target q pT \<in> FSM.states M
q' \<in> FSM.states M

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

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
using pass_separator_ATC_fail_no_reduction[OF \<open>observable M'\<close> \<open>observable M\<close> \<open>qT \<in> states M'\<close>
                                                    \<open>target q pT \<in> FSM.states M\<close> \<open>q' \<in> FSM.states M\<close>
                                                    \<open>is_separator M (target q pT) q' A d1 d2\<close> \<open>inputs M' = inputs M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. \<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
have "LS M' qT \<subseteq> LS M (target q pT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
have "(target q pT) = target (initial M) (pP@pT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q pT = target (FSM.initial M) (pP @ pT)
[PROOF STEP]
using \<open>target (initial P) pP = q\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial P) pP = q

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

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

goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
have "path M (initial M) (pP@pT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) (pP @ pT)
[PROOF STEP]
using \<open>path M (initial M) pP\<close> \<open>target (initial P) pP = q\<close> \<open>path M q pT\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) pP
target (FSM.initial P) pP = q
path M q pT

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

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

goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path M (FSM.initial M) (pP @ pT)
[PROOF STEP]
have "(target q pT) \<in> io_targets M (p_io pP @ p_io pT) (FSM.initial M)"
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (pP @ pT)

goal (1 subgoal):
 1. target q pT \<in> io_targets M (p_io pP @ p_io pT) (FSM.initial M)
[PROOF STEP]
unfolding io_targets.simps \<open>(target q pT) = target (initial M) (pP@pT)\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (pP @ pT)

goal (1 subgoal):
 1. target (FSM.initial M) (pP @ pT) \<in> {target (FSM.initial M) p |p. path M (FSM.initial M) p \<and> p_io p = p_io pP @ p_io pT}
[PROOF STEP]
using map_append
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (pP @ pT)
map ?f (?xs @ ?ys) = map ?f ?xs @ map ?f ?ys

goal (1 subgoal):
 1. target (FSM.initial M) (pP @ pT) \<in> {target (FSM.initial M) p |p. path M (FSM.initial M) p \<and> p_io p = p_io pP @ p_io pT}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
target q pT \<in> io_targets M (p_io pP @ p_io pT) (FSM.initial M)

goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
using observable_language_target[OF \<open>observable M\<close> \<open>(target q pT) \<in> io_targets M (p_io pP @ p_io pT) (FSM.initial M)\<close>
                                            \<open>qT \<in> io_targets M' ((p_io pP)@(p_io pT)) (initial M')\<close> \<open>L M' \<subseteq> L M\<close>]
[PROOF STATE]
proof (prove)
using this:
LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
LS M' qT \<subseteq> LS M (target q pT)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> prs; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; q' \<in> rd_targets (q, pT); (A, d1, d2) \<in> separators (target q pT, q'); qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT d2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)
LS M' qT \<subseteq> LS M (target q pT)
[PROOF STEP]
show "pass_separator_ATC M' A qT d2"
[PROOF STATE]
proof (prove)
using this:
\<not> pass_separator_ATC M' A qT d2 \<Longrightarrow> \<not> LS M' qT \<subseteq> LS M (target q pT)
LS M' qT \<subseteq> LS M (target q pT)

goal (1 subgoal):
 1. pass_separator_ATC M' A qT d2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pass_separator_ATC M' A qT d2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?q' \<in> rd_targets (?q, ?pT); (?A, ?d1.0, ?d2.0) \<in> separators (target ?q ?pT, ?q'); ?qT \<in> io_targets M' (p_io ?pP @ p_io ?pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' ?A ?qT ?d2.0

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?q' \<in> rd_targets (?q, ?pT); (?A, ?d1.0, ?d2.0) \<in> separators (target ?q ?pT, ?q'); ?qT \<in> io_targets M' (p_io ?pP @ p_io ?pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' ?A ?qT ?d2.0
[PROOF STEP]
have p3: "(\<forall> q P pP pT . (q,P) \<in> prs \<longrightarrow>
                                  path P (initial P) pP \<longrightarrow>
                                  target (initial P) pP = q \<longrightarrow>
                                  pT \<in> tps q \<longrightarrow>
                                  (p_io pP)@(p_io pT) \<in> L M' \<longrightarrow>
                                  (\<forall> q' A d1 d2 qT . q' \<in> rd_targets (q,pT) \<longrightarrow>
                                  (A,d1,d2) \<in> separators (target q pT, q') \<longrightarrow>
                                  qT \<in> io_targets M' ((p_io pP)@(p_io pT)) (initial M') \<longrightarrow>
                                  pass_separator_ATC M' A qT d2))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?q, ?P) \<in> prs; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; ?q' \<in> rd_targets (?q, ?pT); (?A, ?d1.0, ?d2.0) \<in> separators (target ?q ?pT, ?q'); ?qT \<in> io_targets M' (p_io ?pP @ p_io ?pT) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' ?A ?qT ?d2.0

goal (1 subgoal):
 1. \<forall>q P pP pT. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> p_io pP @ p_io pT \<in> L M' \<longrightarrow> (\<forall>q' A d1 d2 qT. q' \<in> rd_targets (q, pT) \<longrightarrow> (A, d1, d2) \<in> separators (target q pT, q') \<longrightarrow> qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M') \<longrightarrow> pass_separator_ATC M' A qT d2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>q P pP pT. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> p_io pP @ p_io pT \<in> L M' \<longrightarrow> (\<forall>q' A d1 d2 qT. q' \<in> rd_targets (q, pT) \<longrightarrow> (A, d1, d2) \<in> separators (target q pT, q') \<longrightarrow> qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M') \<longrightarrow> pass_separator_ATC M' A qT d2)

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
using p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
\<forall>q P io x y y'. (q, P) \<in> prs \<longrightarrow> io @ [(x, y)] \<in> L P \<longrightarrow> io @ [(x, y')] \<in> L M' \<longrightarrow> io @ [(x, y')] \<in> L P
\<forall>q P pP ioT pT x y y'. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow> p_io pP @ ioT @ [(x, y')] \<in> L M' \<longrightarrow> (\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT')))
\<forall>q P pP pT. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> p_io pP @ p_io pT \<in> L M' \<longrightarrow> (\<forall>q' A d1 d2 qT. q' \<in> rd_targets (q, pT) \<longrightarrow> (A, d1, d2) \<in> separators (target q pT, q') \<longrightarrow> qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M') \<longrightarrow> pass_separator_ATC M' A qT d2)

goal (1 subgoal):
 1. passes_test_suite M (Test_Suite prs tps rd_targets separators) M'
[PROOF STEP]
unfolding passes_test_suite.simps
[PROOF STATE]
proof (prove)
using this:
\<forall>q P io x y y'. (q, P) \<in> prs \<longrightarrow> io @ [(x, y)] \<in> L P \<longrightarrow> io @ [(x, y')] \<in> L M' \<longrightarrow> io @ [(x, y')] \<in> L P
\<forall>q P pP ioT pT x y y'. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow> p_io pP @ ioT @ [(x, y')] \<in> L M' \<longrightarrow> (\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT')))
\<forall>q P pP pT. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> p_io pP @ p_io pT \<in> L M' \<longrightarrow> (\<forall>q' A d1 d2 qT. q' \<in> rd_targets (q, pT) \<longrightarrow> (A, d1, d2) \<in> separators (target q pT, q') \<longrightarrow> qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M') \<longrightarrow> pass_separator_ATC M' A qT d2)

goal (1 subgoal):
 1. (\<forall>q P io x y y'. (q, P) \<in> prs \<longrightarrow> io @ [(x, y)] \<in> L P \<longrightarrow> io @ [(x, y')] \<in> L M' \<longrightarrow> io @ [(x, y')] \<in> L P) \<and> (\<forall>q P pP ioT pT x y y'. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> ioT @ [(x, y)] \<in> set (prefixes (p_io pT)) \<longrightarrow> p_io pP @ ioT @ [(x, y')] \<in> L M' \<longrightarrow> (\<exists>pT'. pT' \<in> tps q \<and> ioT @ [(x, y')] \<in> set (prefixes (p_io pT')))) \<and> (\<forall>q P pP pT. (q, P) \<in> prs \<longrightarrow> path P (FSM.initial P) pP \<longrightarrow> target (FSM.initial P) pP = q \<longrightarrow> pT \<in> tps q \<longrightarrow> p_io pP @ p_io pT \<in> L M' \<longrightarrow> (\<forall>q' A d1 d2 qT. q' \<in> rd_targets (q, pT) \<longrightarrow> (A, d1, d2) \<in> separators (target q pT, q') \<longrightarrow> qT \<in> io_targets M' (p_io pP @ p_io pT) (FSM.initial M') \<longrightarrow> pass_separator_ATC M' A qT d2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
passes_test_suite M (Test_Suite prs tps rd_targets separators) M'

goal:
No subgoals!
[PROOF STEP]
qed