[STATEMENT]
lemma zero_less_HMSet_iff[simp]: "0 < HMSet M \<longleftrightarrow> M \<noteq> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < HMSet M) = (M \<noteq> {#})
[PROOF STEP]
by (simp only: zero_less_iff_neq_zero_hmset HMSet_eq_0_iff)


[STATEMENT]
lemma gr_zeroI_hmset: "(M = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < M" for M :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < M
[PROOF STEP]
using not_gr_zero_hmset
[PROOF STATE]
proof (prove)
using this:
(\<not> 0 < ?M) = (?M = 0)

goal (1 subgoal):
 1. (M = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < M
[PROOF STEP]
by blast


[STATEMENT]
lemma gr_implies_not_zero_hmset: "M < N \<Longrightarrow> N \<noteq> 0" for M N :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M < N \<Longrightarrow> N \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma add_eq_0_iff_both_eq_0_hmset[simp]: "M + N = 0 \<longleftrightarrow> M = 0 \<and> N = 0" for M N :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M + N = 0) = (M = 0 \<and> N = 0)
[PROOF STEP]
by (intro add_nonneg_eq_0_iff zero_le_hmset)


[STATEMENT]
lemma trans_less_add1_hmset: "i < j \<Longrightarrow> i < j + m" for i j m :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j \<Longrightarrow> i < j + m
[PROOF STEP]
by (metis add_increasing2 leD le_less not_gr_zero_hmset)


[STATEMENT]
lemma trans_less_add2_hmset: "i < j \<Longrightarrow> i < m + j" for i j m :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j \<Longrightarrow> i < m + j
[PROOF STEP]
by (simp add: add.commute trans_less_add1_hmset)


[STATEMENT]
lemma trans_le_add1_hmset: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> i \<le> j + m
[PROOF STEP]
by (simp add: add_increasing2)


[STATEMENT]
lemma trans_le_add2_hmset: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> i \<le> m + j
[PROOF STEP]
by (simp add: add_increasing)


[STATEMENT]
lemma diff_le_self_hmset: "m - n \<le> m" for m n :: hmultiset
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m - n \<le> m
[PROOF STEP]
by (metis add.commute add.right_neutral diff_add_zero diff_diff_add_hmset
    le_minus_plus_same_hmset)


[STATEMENT]
lemma implies_completeness_for_repetition_sets_simps :
  assumes "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets"
  shows "(initial M,initial_preamble M) \<in> prs"
    and "\<And> q P . (q,P) \<in> prs \<Longrightarrow> (is_preamble P M q) \<and> (tps q) \<noteq> {}"
    and "\<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"
    and "\<And> q . q \<in> states M \<Longrightarrow> (\<exists>d \<in> set repetition_sets. q \<in> fst d)"
    and "\<And> d . d \<in> set repetition_sets \<Longrightarrow> (fst d \<subseteq> states M) \<and> (snd d = fst d \<inter> fst ` prs)"
    and "\<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> {}"
    and "\<And> q . q \<in> image 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"
    and "\<And> q p d p1 p2 p3 . q \<in> image 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))"
    and "\<And> q p d p1 p2 q' . q \<in> image fst prs \<Longrightarrow> (p,d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> p=p1@p2 \<Longrightarrow> q' \<in> image 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))"
    and "\<And> q p d q1 q2 . q \<in> image fst prs \<Longrightarrow> (p,d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> q1 \<in> snd d \<Longrightarrow> q2 \<in> snd d \<Longrightarrow> ([] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2,[]) \<and> q2 \<in> rd_targets (q1,[]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((FSM.initial M, initial_preamble M) \<in> prs &&& (\<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {})) &&& (\<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) &&& (\<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs)) &&& ((\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> separators (q1, q2) \<noteq> {}) &&& (\<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)) &&& (\<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)) &&& (\<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)) &&& (\<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, []))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. (FSM.initial M, initial_preamble M) \<in> prs
 2. \<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}
 3. \<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
 4. \<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
 5. \<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs
 6. \<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> {}
 7. \<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
 8. \<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)
 9. \<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)
 10. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
show "(initial M,initial_preamble M) \<in> prs"
  and  "\<And> q . q \<in> image 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. (FSM.initial M, initial_preamble M) \<in> prs &&& (\<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 assms
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> prs &&& (\<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]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs \<and> (\<forall>q P. (q, P) \<in> prs \<longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}) \<and> (\<forall>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) \<and> (\<forall>q. q \<in> FSM.states M \<longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)) \<and> (\<forall>d. d \<in> set repetition_sets \<longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})) \<and> (\<forall>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) \<and> (\<forall>q p d. q \<in> fst ` prs \<longrightarrow> (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<longrightarrow> ((\<forall>p1 p2 p3. 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)) \<and> (\<forall>p1 p2 q'. 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))) \<and> (\<forall>q1 q2. q1 \<noteq> q2 \<longrightarrow> q1 \<in> snd d \<longrightarrow> q2 \<in> snd d \<longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])))

goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> prs &&& (\<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 blast+
[PROOF STATE]
proof (state)
this:
(FSM.initial M, initial_preamble M) \<in> prs
?q \<in> fst ` prs \<Longrightarrow> tps ?q \<subseteq> {p1. \<exists>p2 d. (p1 @ p2, d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m} \<and> fst ` m_traversal_paths_with_witness M ?q repetition_sets m \<subseteq> tps ?q

goal (8 subgoals):
 1. \<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}
 2. \<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
 3. \<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
 4. \<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs
 5. \<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> {}
 6. \<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)
 7. \<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)
 8. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
show "\<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"
  and  "\<And> q P . (q,P) \<in> prs \<Longrightarrow> (is_preamble P M q) \<and> (tps q) \<noteq> {}"
  and  "\<And> q . q \<in> states M \<Longrightarrow> (\<exists>d \<in> set repetition_sets. q \<in> fst d)"
  and  "\<And> d . d \<in> set repetition_sets \<Longrightarrow> (fst d \<subseteq> states M) \<and> (snd d = fst d \<inter> fst ` prs)"
  and  "\<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>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) &&& (\<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {})) &&& (\<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets

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) &&& (\<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {})) &&& (\<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs \<and> (\<forall>q P. (q, P) \<in> prs \<longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}) \<and> (\<forall>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) \<and> (\<forall>q. q \<in> FSM.states M \<longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)) \<and> (\<forall>d. d \<in> set repetition_sets \<longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})) \<and> (\<forall>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) \<and> (\<forall>q p d. q \<in> fst ` prs \<longrightarrow> (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<longrightarrow> ((\<forall>p1 p2 p3. 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)) \<and> (\<forall>p1 p2 q'. 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))) \<and> (\<forall>q1 q2. q1 \<noteq> q2 \<longrightarrow> q1 \<in> snd d \<longrightarrow> q2 \<in> snd d \<longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])))

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) &&& (\<And>q P. (q, P) \<in> prs \<Longrightarrow> is_preamble P M q \<and> tps q \<noteq> {})) &&& (\<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d) &&& (\<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs) &&& (\<And>d q1 q2. \<lbrakk>d \<in> set repetition_sets; q1 \<in> fst d; q2 \<in> fst d; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
by force+
[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
(?q, ?P) \<in> prs \<Longrightarrow> is_preamble ?P M ?q \<and> tps ?q \<noteq> {}
?q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. ?q \<in> fst d
?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 (3 subgoals):
 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)
 2. \<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)
 3. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
show "\<And> q p d p1 p2 p3 . q \<in> image 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 assms
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets

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]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs \<and> (\<forall>q P. (q, P) \<in> prs \<longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}) \<and> (\<forall>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) \<and> (\<forall>q. q \<in> FSM.states M \<longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)) \<and> (\<forall>d. d \<in> set repetition_sets \<longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})) \<and> (\<forall>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) \<and> (\<forall>q p d. q \<in> fst ` prs \<longrightarrow> (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<longrightarrow> ((\<forall>p1 p2 p3. 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)) \<and> (\<forall>p1 p2 q'. 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))) \<and> (\<forall>q1 q2. q1 \<noteq> q2 \<longrightarrow> q1 \<in> snd d \<longrightarrow> q2 \<in> snd d \<longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])))

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 (metis (no_types, lifting))
[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 (2 subgoals):
 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)
 2. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
show "\<And> q p d p1 p2 q' . q \<in> image fst prs \<Longrightarrow> (p,d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> p=p1@p2 \<Longrightarrow> q' \<in> image 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 assms
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets

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]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs \<and> (\<forall>q P. (q, P) \<in> prs \<longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}) \<and> (\<forall>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) \<and> (\<forall>q. q \<in> FSM.states M \<longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)) \<and> (\<forall>d. d \<in> set repetition_sets \<longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})) \<and> (\<forall>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) \<and> (\<forall>q p d. q \<in> fst ` prs \<longrightarrow> (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<longrightarrow> ((\<forall>p1 p2 p3. 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)) \<and> (\<forall>p1 p2 q'. 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))) \<and> (\<forall>q1 q2. q1 \<noteq> q2 \<longrightarrow> q1 \<in> snd d \<longrightarrow> q2 \<in> snd d \<longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])))

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 (metis (no_types, lifting))
[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. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
show "\<And> q p d q1 q2 . q \<in> image fst prs \<Longrightarrow> (p,d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> q1 \<in> snd d \<Longrightarrow> q2 \<in> snd d \<Longrightarrow> ([] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2,[]) \<and> q2 \<in> rd_targets (q1,[]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> prs \<and> (\<forall>q P. (q, P) \<in> prs \<longrightarrow> is_preamble P M q \<and> tps q \<noteq> {}) \<and> (\<forall>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) \<and> (\<forall>q. q \<in> FSM.states M \<longrightarrow> (\<exists>d\<in>set repetition_sets. q \<in> fst d)) \<and> (\<forall>d. d \<in> set repetition_sets \<longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` prs \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})) \<and> (\<forall>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) \<and> (\<forall>q p d. q \<in> fst ` prs \<longrightarrow> (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<longrightarrow> ((\<forall>p1 p2 p3. 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)) \<and> (\<forall>p1 p2 q'. 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))) \<and> (\<forall>q1 q2. q1 \<noteq> q2 \<longrightarrow> q1 \<in> snd d \<longrightarrow> q2 \<in> snd d \<longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])))

goal (1 subgoal):
 1. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` prs; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; q1 \<noteq> q2; q1 \<in> snd d; q2 \<in> snd d\<rbrakk> \<Longrightarrow> [] \<in> tps q1 \<and> [] \<in> tps q2 \<and> q1 \<in> rd_targets (q2, []) \<and> q2 \<in> rd_targets (q1, [])
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> fst ` prs; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?q1.0 \<noteq> ?q2.0; ?q1.0 \<in> snd ?d; ?q2.0 \<in> snd ?d\<rbrakk> \<Longrightarrow> [] \<in> tps ?q1.0 \<and> [] \<in> tps ?q2.0 \<and> ?q1.0 \<in> rd_targets (?q2.0, []) \<and> ?q2.0 \<in> rd_targets (?q1.0, [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma passes_test_suite_soundness_helper_1 :
  assumes "is_preamble P M q"
  and     "observable M"
  and     "io@[(x,y)] \<in> L P"
  and     "io@[(x,y')] \<in> L M"
shows     "io@[(x,y')] \<in> L P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have   "is_submachine P M"
  and *: "\<And> q' x t t' . q'\<in>reachable_states P \<Longrightarrow> x\<in>FSM.inputs M \<Longrightarrow>
            t\<in>FSM.transitions P \<Longrightarrow> t_source t = q' \<Longrightarrow> t_input t = x \<Longrightarrow>
            t'\<in>FSM.transitions M \<Longrightarrow> t_source t' = q' \<Longrightarrow> t_input t' = x \<Longrightarrow> t' \<in> FSM.transitions P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_submachine P M &&& (\<And>q' x t t'. \<lbrakk>q' \<in> reachable_states P; x \<in> FSM.inputs M; t \<in> FSM.transitions P; t_source t = q'; t_input t = x; t' \<in> FSM.transitions M; t_source t' = q'; t_input t' = x\<rbrakk> \<Longrightarrow> t' \<in> FSM.transitions P)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q

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

goal (1 subgoal):
 1. is_submachine P M &&& (\<And>q' x t t'. \<lbrakk>q' \<in> reachable_states P; x \<in> FSM.inputs M; t \<in> FSM.transitions P; t_source t = q'; t_input t = x; t' \<in> FSM.transitions M; t_source t' = q'; t_input t' = x\<rbrakk> \<Longrightarrow> t' \<in> FSM.transitions P)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
is_submachine P M
\<lbrakk>?q' \<in> reachable_states P; ?x \<in> FSM.inputs M; ?t \<in> FSM.transitions P; t_source ?t = ?q'; t_input ?t = ?x; ?t' \<in> FSM.transitions M; t_source ?t' = ?q'; t_input ?t' = ?x\<rbrakk> \<Longrightarrow> ?t' \<in> FSM.transitions P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "initial P = initial M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial P = FSM.initial M
[PROOF STEP]
unfolding submachine_simps[OF \<open>is_submachine P M\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial M = FSM.initial M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.initial P = FSM.initial M

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

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path M (FSM.initial M) p; p_io p = io @ [(x, y')]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding submachine_simps[OF \<open>is_submachine P M\<close>]
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y')] \<in> L M

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

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
obtain p' t where "p = p'@[t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p' t. p = p' @ [t] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p_io p = io @ [(x,y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io p = io @ [(x, y')]

goal (1 subgoal):
 1. (\<And>p' t. p = p' @ [t] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (induction p rule: rev_induct; auto)
[PROOF STATE]
proof (state)
this:
p = p' @ [t]

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "path M (initial M) p'" and "t \<in> transitions M" and "t_source t = target (initial M) p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path M (FSM.initial M) p' &&& t \<in> FSM.transitions M &&& t_source t = target (FSM.initial M) p'
[PROOF STEP]
using \<open>path M (initial M) p\<close> path_append_transition_elim
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) p
path ?M ?q (?p @ [?t]) \<Longrightarrow> path ?M ?q ?p
path ?M ?q (?p @ [?t]) \<Longrightarrow> ?t \<in> FSM.transitions ?M
path ?M ?q (?p @ [?t]) \<Longrightarrow> t_source ?t = target ?q ?p

goal (1 subgoal):
 1. path M (FSM.initial M) p' &&& t \<in> FSM.transitions M &&& t_source t = target (FSM.initial M) p'
[PROOF STEP]
unfolding \<open>p = p'@[t]\<close>
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) (p' @ [t])
path ?M ?q (?p @ [?t]) \<Longrightarrow> path ?M ?q ?p
path ?M ?q (?p @ [?t]) \<Longrightarrow> ?t \<in> FSM.transitions ?M
path ?M ?q (?p @ [?t]) \<Longrightarrow> t_source ?t = target ?q ?p

goal (1 subgoal):
 1. path M (FSM.initial M) p' &&& t \<in> FSM.transitions M &&& t_source t = target (FSM.initial M) p'
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) p'
t \<in> FSM.transitions M
t_source t = target (FSM.initial M) p'

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "p_io p' = io" and "t_input t = x" and "t_output t = y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io p' = io &&& t_input t = x &&& t_output t = y'
[PROOF STEP]
using \<open>p_io p = io @ [(x,y')]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io p = io @ [(x, y')]

goal (1 subgoal):
 1. p_io p' = io &&& t_input t = x &&& t_output t = y'
[PROOF STEP]
unfolding \<open>p = p'@[t]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (p' @ [t]) = io @ [(x, y')]

goal (1 subgoal):
 1. p_io p' = io &&& t_input t = x &&& t_output t = y'
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
p_io p' = io
t_input t = x
t_output t = y'

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "p_io p' \<in> LS P (FSM.initial M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io p' \<in> LS P (FSM.initial M)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y)] \<in> L P

goal (1 subgoal):
 1. p_io p' \<in> LS P (FSM.initial M)
[PROOF STEP]
unfolding \<open>p_io p' = io\<close> \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y)] \<in> LS P (FSM.initial M)

goal (1 subgoal):
 1. io \<in> LS P (FSM.initial M)
[PROOF STEP]
by (meson language_prefix)
[PROOF STATE]
proof (state)
this:
p_io p' \<in> LS P (FSM.initial M)

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "FSM.initial M \<in> reachable_states P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial M \<in> reachable_states P
[PROOF STEP]
unfolding submachine_simps(1)[OF \<open>is_submachine P M\<close>, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial P \<in> reachable_states P
[PROOF STEP]
using reachable_states_initial
[PROOF STATE]
proof (prove)
using this:
FSM.initial ?M \<in> reachable_states ?M

goal (1 subgoal):
 1. FSM.initial P \<in> reachable_states P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
FSM.initial M \<in> reachable_states P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
obtain pp where "path P (initial P) pp" and "p_io pp = io @ [(x,y)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pp. \<lbrakk>path P (FSM.initial P) pp; p_io pp = io @ [(x, y)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
io @ [(x, y)] \<in> L P

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

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path P (FSM.initial P) pp
p_io pp = io @ [(x, y)]
[PROOF STEP]
obtain pp' t' where "pp = pp'@[t']"
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) pp
p_io pp = io @ [(x, y)]

goal (1 subgoal):
 1. (\<And>pp' t'. pp = pp' @ [t'] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>pp' t'. pp = pp' @ [t'] \<Longrightarrow> thesis; path P (FSM.initial P) pp; p_io pp = io @ [(x, y)]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume a1: "\<And>pp' t'. pp = pp' @ [t'] \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
pp = ?pp' @ [?t'] \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>pp' t'. pp = pp' @ [t'] \<Longrightarrow> thesis; path P (FSM.initial P) pp; p_io pp = io @ [(x, y)]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "pp \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp \<noteq> []
[PROOF STEP]
using \<open>p_io pp = io @ [(x, y)]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pp = io @ [(x, y)]

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

goal (1 subgoal):
 1. \<lbrakk>\<And>pp' t'. pp = pp' @ [t'] \<Longrightarrow> thesis; path P (FSM.initial P) pp; p_io pp = io @ [(x, y)]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pp \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pp \<noteq> []

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
pp \<noteq> []
pp = ?pp' @ [?t'] \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pp = pp' @ [t']

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "path P (initial P) pp'" and "t' \<in> transitions P" and "t_source t' = target (initial P) pp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path P (FSM.initial P) pp' &&& t' \<in> FSM.transitions P &&& t_source t' = target (FSM.initial P) pp'
[PROOF STEP]
using \<open>path P (initial P) pp\<close> path_append_transition_elim
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) pp
path ?M ?q (?p @ [?t]) \<Longrightarrow> path ?M ?q ?p
path ?M ?q (?p @ [?t]) \<Longrightarrow> ?t \<in> FSM.transitions ?M
path ?M ?q (?p @ [?t]) \<Longrightarrow> t_source ?t = target ?q ?p

goal (1 subgoal):
 1. path P (FSM.initial P) pp' &&& t' \<in> FSM.transitions P &&& t_source t' = target (FSM.initial P) pp'
[PROOF STEP]
unfolding \<open>pp = pp'@[t']\<close>
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) (pp' @ [t'])
path ?M ?q (?p @ [?t]) \<Longrightarrow> path ?M ?q ?p
path ?M ?q (?p @ [?t]) \<Longrightarrow> ?t \<in> FSM.transitions ?M
path ?M ?q (?p @ [?t]) \<Longrightarrow> t_source ?t = target ?q ?p

goal (1 subgoal):
 1. path P (FSM.initial P) pp' &&& t' \<in> FSM.transitions P &&& t_source t' = target (FSM.initial P) pp'
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
path P (FSM.initial P) pp'
t' \<in> FSM.transitions P
t_source t' = target (FSM.initial P) pp'

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "p_io pp' = io" and "t_input t' = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pp' = io &&& t_input t' = x
[PROOF STEP]
using \<open>p_io pp = io @ [(x,y)]\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pp = io @ [(x, y)]

goal (1 subgoal):
 1. p_io pp' = io &&& t_input t' = x
[PROOF STEP]
unfolding \<open>pp = pp'@[t']\<close>
[PROOF STATE]
proof (prove)
using this:
p_io (pp' @ [t']) = io @ [(x, y)]

goal (1 subgoal):
 1. p_io pp' = io &&& t_input t' = x
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
p_io pp' = io
t_input t' = x

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[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>path P (initial P) pp'\<close> submachine_path_initial[OF \<open>is_submachine P M\<close>]
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) pp'
path P (FSM.initial P) ?p \<Longrightarrow> path M (FSM.initial M) ?p

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. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "pp' = p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp' = p'
[PROOF STEP]
using observable_path_unique[OF assms(2) \<open>path M (initial M) pp'\<close> \<open>path M (initial M) p'\<close> ]
[PROOF STATE]
proof (prove)
using this:
p_io pp' = p_io p' \<Longrightarrow> pp' = p'

goal (1 subgoal):
 1. pp' = p'
[PROOF STEP]
unfolding \<open>p_io pp' = io\<close> \<open>p_io p' = io\<close>
[PROOF STATE]
proof (prove)
using this:
io = io \<Longrightarrow> pp' = p'

goal (1 subgoal):
 1. pp' = p'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pp' = p'

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pp' = p'
[PROOF STEP]
have "t_source t' = target (initial M) p'"
[PROOF STATE]
proof (prove)
using this:
pp' = p'

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

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

goal (1 subgoal):
 1. t_source t' = target (FSM.initial M) p'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t_source t' = target (FSM.initial M) p'

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "path P (FSM.initial M) p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path P (FSM.initial M) p'
[PROOF STEP]
using observable_preamble_paths[OF assms(1,2) \<open>path M (initial M) p'\<close>
                                                  \<open>p_io p' \<in> LS P (FSM.initial M)\<close>
                                                  \<open>FSM.initial M \<in> reachable_states P\<close>]
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial M) p'

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

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path P (FSM.initial M) p'
[PROOF STEP]
have "target (initial M) p' \<in> reachable_states P"
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial M) p'

goal (1 subgoal):
 1. target (FSM.initial M) p' \<in> reachable_states P
[PROOF STEP]
using reachable_states_intro
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial M) p'
path ?M (FSM.initial ?M) ?p \<Longrightarrow> target (FSM.initial ?M) ?p \<in> reachable_states ?M

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

goal (1 subgoal):
 1. target (FSM.initial P) p' \<in> reachable_states P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) p' \<in> reachable_states P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) p' \<in> reachable_states P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "x \<in> inputs M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> FSM.inputs M
[PROOF STEP]
using \<open>t \<in> transitions M\<close> \<open>t_input t = x\<close> fsm_transition_input
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions M
t_input t = x
?t \<in> FSM.transitions ?M \<Longrightarrow> t_input ?t \<in> FSM.inputs ?M

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

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
have "t \<in> transitions P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> FSM.transitions P
[PROOF STEP]
using *[OF \<open>target (initial M) p' \<in> reachable_states P\<close> \<open>x \<in> inputs M\<close> \<open>t' \<in> transitions P\<close>
               \<open>t_source t' = target (initial M) p'\<close> \<open>t_input t' = x\<close> \<open>t \<in> transitions M\<close>
               \<open>t_source t = target (FSM.initial M) p'\<close> \<open>t_input t = x\<close>]
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions P

goal (1 subgoal):
 1. t \<in> FSM.transitions P
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
t \<in> FSM.transitions P

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> FSM.transitions P
[PROOF STEP]
have "path P (initial P) (p'@[t])"
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions P

goal (1 subgoal):
 1. path P (FSM.initial P) (p' @ [t])
[PROOF STEP]
using \<open>path P (initial P) pp'\<close> \<open>t_source t = target (initial M) p'\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions P
path P (FSM.initial P) pp'
t_source t = target (FSM.initial M) p'

goal (1 subgoal):
 1. path P (FSM.initial P) (p' @ [t])
[PROOF STEP]
unfolding \<open>pp' = p'\<close> \<open>initial P = initial M\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions P
path P (FSM.initial M) p'
t_source t = target (FSM.initial M) p'

goal (1 subgoal):
 1. path P (FSM.initial M) (p' @ [t])
[PROOF STEP]
using path_append_transition
[PROOF STATE]
proof (prove)
using this:
t \<in> FSM.transitions P
path P (FSM.initial M) p'
t_source t = target (FSM.initial M) p'
\<lbrakk>path ?M ?q ?p; ?t \<in> FSM.transitions ?M; t_source ?t = target ?q ?p\<rbrakk> \<Longrightarrow> path ?M ?q (?p @ [?t])

goal (1 subgoal):
 1. path P (FSM.initial M) (p' @ [t])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
path P (FSM.initial P) (p' @ [t])

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path P (FSM.initial P) (p' @ [t])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) (p' @ [t])

goal (1 subgoal):
 1. io @ [(x, y')] \<in> L P
[PROOF STEP]
unfolding \<open>p = p'@[t]\<close>[symmetric] LS.simps
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) p

goal (1 subgoal):
 1. io @ [(x, y')] \<in> {p_io p |p. path P (FSM.initial P) p}
[PROOF STEP]
using \<open>p_io p = io@[(x,y')]\<close>
[PROOF STATE]
proof (prove)
using this:
path P (FSM.initial P) p
p_io p = io @ [(x, y')]

goal (1 subgoal):
 1. io @ [(x, y')] \<in> {p_io p |p. path P (FSM.initial P) p}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
io @ [(x, y')] \<in> L P

goal:
No subgoals!
[PROOF STEP]
qed