[STATEMENT]
lemma passes_test_suite_exhaustiveness_helper_1 :
  assumes "completely_specified M'"
  and     "inputs M' = inputs M"
  and     "observable M"
  and     "observable M'"
  and     "(q,P) \<in> PS"
  and     "path P (initial P) pP"
  and     "target (initial P) pP = q"
  and     "p_io pP @ p_io p \<in> L M'"
  and     "(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m"
  and     "implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets"
  and     "passes_test_suite M (Test_Suite PS tps rd_targets separators) M'"
  and     "q' \<noteq> q''"
  and     "q' \<in> fst d"
  and     "q'' \<in> fst d"
  and     "pR1 \<in> (RP M q q' pP p PS M')"
  and     "pR2 \<in> (RP M q q'' pP p PS M')"
shows "io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pR2) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
let ?RP1 = "(RP M q q' pP p PS M')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
let ?RP2 = "(RP M q q'' pP p PS M')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
let ?R1  = "(R M q q' pP p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
let ?R2  = "(R M q q'' pP p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* sufficiency properties *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t1: "(initial M, initial_preamble M) \<in> PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> PS
[PROOF STEP]
using \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. (FSM.initial M, initial_preamble M) \<in> PS
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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> PS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(FSM.initial M, initial_preamble M) \<in> PS

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t2: "\<And> q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q
[PROOF STEP]
using \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(?q, ?P) \<in> PS \<Longrightarrow> is_preamble ?P M ?q

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial 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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS 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
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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
[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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial 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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
[PROOF STEP]
unfolding implies_completeness_for_repetition_sets.simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial M, initial_preamble M) \<in> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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. q \<in> FSM.states M \<Longrightarrow> \<exists>d\<in>set repetition_sets. q \<in> fst d
[PROOF STEP]
by force
[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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t6: "\<And> q. q \<in> fst ` PS \<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 ` PS \<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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q. q \<in> fst ` PS \<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> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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. q \<in> fst ` PS \<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 auto
[PROOF STATE]
proof (state)
this:
?q \<in> fst ` PS \<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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "\<And> d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` PS \<and> (\<forall>q1 q2. 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> snd d = fst d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
using \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<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> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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>d. d \<in> set repetition_sets \<Longrightarrow> fst d \<subseteq> FSM.states M \<and> snd d = fst d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst d \<longrightarrow> q2 \<in> fst d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M \<and> snd ?d = fst ?d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst ?d \<longrightarrow> q2 \<in> fst ?d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M \<and> snd ?d = fst ?d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst ?d \<longrightarrow> q2 \<in> fst ?d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<noteq> {})
[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  t8': "\<And> d. d \<in> set repetition_sets \<Longrightarrow> snd d = fst d \<inter> fst ` PS"
  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)
using this:
?d \<in> set repetition_sets \<Longrightarrow> fst ?d \<subseteq> FSM.states M \<and> snd ?d = fst ?d \<inter> fst ` PS \<and> (\<forall>q1 q2. q1 \<in> fst ?d \<longrightarrow> q2 \<in> fst ?d \<longrightarrow> q1 \<noteq> q2 \<longrightarrow> separators (q1, q2) \<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. d \<in> set repetition_sets \<Longrightarrow> snd d = fst d \<inter> fst ` PS) &&& (\<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
?d \<in> set repetition_sets \<Longrightarrow> snd ?d = fst ?d \<inter> fst ` PS
\<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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t10: "\<And> q p d p1 p2 p3.
              q \<in> fst ` PS \<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 ` PS; (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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q p d p1 p2 p3. \<lbrakk>q \<in> fst ` PS; (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> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS; (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 ` PS; (?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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t11: "\<And> q p d p1 p2 q'.
              q \<in> fst ` PS \<Longrightarrow>
              (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m \<Longrightarrow>
              p = p1 @ p2 \<Longrightarrow>
              q' \<in> fst ` PS \<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 ` PS; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2; q' \<in> fst ` PS; 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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q p d p1 p2 q'. \<lbrakk>q \<in> fst ` PS; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2; q' \<in> fst ` PS; 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> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS; (p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m; p = p1 @ p2; q' \<in> fst ` PS; 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 ` PS; (?p, ?d) \<in> m_traversal_paths_with_witness M ?q repetition_sets m; ?p = ?p1.0 @ ?p2.0; ?q' \<in> fst ` PS; 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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have t12: "\<And> q p d q1 q2.
              q \<in> fst ` PS \<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 ` PS; (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 \<open>implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets\<close>
[PROOF STATE]
proof (prove)
using this:
implies_completeness_for_repetition_sets (Test_Suite PS tps rd_targets separators) M m repetition_sets

goal (1 subgoal):
 1. \<And>q p d q1 q2. \<lbrakk>q \<in> fst ` PS; (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> PS \<and> (\<forall>q P. (q, P) \<in> PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS \<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 ` PS; (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 ` PS; (?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 (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* pass properties *)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> fst ` PS; (?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 (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have pass1: "\<And> q P io x y y' . (q,P) \<in> PS \<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> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
using \<open>passes_test_suite M (Test_Suite PS tps rd_targets separators) M'\<close>
[PROOF STATE]
proof (prove)
using this:
passes_test_suite M (Test_Suite PS tps rd_targets separators) M'

goal (1 subgoal):
 1. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
unfolding passes_test_suite.simps
[PROOF STATE]
proof (prove)
using this:
(\<forall>q P io x y y'. (q, P) \<in> PS \<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> PS \<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> PS \<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. \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L P
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> PS; ?io @ [(?x, ?y)] \<in> L ?P; ?io @ [(?x, ?y')] \<in> L M'\<rbrakk> \<Longrightarrow> ?io @ [(?x, ?y')] \<in> L ?P

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have pass2: "\<And> q P pP ioT pT x y y' . (q,P) \<in> PS \<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 y y'. \<lbrakk>(q, P) \<in> PS; 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]
using \<open>passes_test_suite M (Test_Suite PS tps rd_targets separators) M'\<close>
[PROOF STATE]
proof (prove)
using this:
passes_test_suite M (Test_Suite PS tps rd_targets separators) M'

goal (1 subgoal):
 1. \<And>q P pP ioT pT x y y'. \<lbrakk>(q, P) \<in> PS; 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]
unfolding passes_test_suite.simps
[PROOF STATE]
proof (prove)
using this:
(\<forall>q P io x y y'. (q, P) \<in> PS \<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> PS \<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> PS \<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. \<And>q P pP ioT pT x y y'. \<lbrakk>(q, P) \<in> PS; 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]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> PS; 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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have pass3: "\<And> q P pP pT q' A d1 d2 qT . (q,P) \<in> PS \<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> 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> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; p_io pP @ p_io pT \<in> L M'; 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]
using \<open>passes_test_suite M (Test_Suite PS tps rd_targets separators) M'\<close>
[PROOF STATE]
proof (prove)
using this:
passes_test_suite M (Test_Suite PS tps rd_targets separators) M'

goal (1 subgoal):
 1. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; p_io pP @ p_io pT \<in> L M'; 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]
unfolding passes_test_suite.simps
[PROOF STATE]
proof (prove)
using this:
(\<forall>q P io x y y'. (q, P) \<in> PS \<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> PS \<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> PS \<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. \<And>q P pP pT q' A d1 d2 qT. \<lbrakk>(q, P) \<in> PS; path P (FSM.initial P) pP; target (FSM.initial P) pP = q; pT \<in> tps q; p_io pP @ p_io pT \<in> L M'; 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]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> PS; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; p_io ?pP @ p_io ?pT \<in> L M'; ?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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
(* additional props *)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?q, ?P) \<in> PS; path ?P (FSM.initial ?P) ?pP; target (FSM.initial ?P) ?pP = ?q; ?pT \<in> tps ?q; p_io ?pP @ p_io ?pT \<in> L M'; ?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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[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> PS\<close> \<open>\<And> q P. (q, P) \<in> PS \<Longrightarrow> is_preamble P M q\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> PS
(?q, ?P) \<in> PS \<Longrightarrow> is_preamble ?P M ?q

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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[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> submachine_path_initial \<open>path P (FSM.initial P) pP\<close>
[PROOF STATE]
proof (prove)
using this:
is_preamble P M q
\<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]
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)))
\<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. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path M (FSM.initial M) pP

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "target (initial M) pP = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pP = q
[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 (FSM.initial M) pP = q
[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 (FSM.initial M) pP = q
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
target (FSM.initial M) pP = q

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path M (FSM.initial M) pP
target (FSM.initial M) pP = q
[PROOF STEP]
have "q \<in> states M"
[PROOF STATE]
proof (prove)
using this:
path M (FSM.initial M) pP
target (FSM.initial M) pP = q

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

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "q \<in> fst ` PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> fst ` PS
[PROOF STEP]
using \<open>(q,P) \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
(q, P) \<in> PS

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "d \<in> set repetition_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> set repetition_sets
[PROOF STEP]
using \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
[PROOF STATE]
proof (prove)
using this:
(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m

goal (1 subgoal):
 1. d \<in> set repetition_sets
[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:
(p, 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. d \<in> set repetition_sets
[PROOF STEP]
using find_set
[PROOF STATE]
proof (prove)
using this:
(p, 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)}
find ?P ?xs = Some ?x \<Longrightarrow> ?x \<in> set ?xs

goal (1 subgoal):
 1. d \<in> set repetition_sets
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
d \<in> set repetition_sets

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "q' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' \<in> FSM.states M
[PROOF STEP]
by (meson \<open>d \<in> set repetition_sets\<close> assms(13) subset_iff t7)
[PROOF STATE]
proof (state)
this:
q' \<in> FSM.states M

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "q'' \<in> states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q'' \<in> FSM.states M
[PROOF STEP]
by (meson \<open>d \<in> set repetition_sets\<close> assms(14) subset_iff t7)
[PROOF STATE]
proof (state)
this:
q'' \<in> FSM.states M

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "target (initial M) pR1 = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pR1 = q'
[PROOF STEP]
using RP_target[OF \<open>pR1 \<in> ?RP1\<close> t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> target (FSM.initial M) pR1 = q'

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (FSM.initial M) pR1 = q'
[PROOF STEP]
have "target (initial M) pR1 \<in> fst d"
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR1 = q'

goal (1 subgoal):
 1. target (FSM.initial M) pR1 \<in> fst d
[PROOF STEP]
using \<open>q' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR1 = q'
q' \<in> fst d

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "target (initial M) pR2 = q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target (FSM.initial M) pR2 = q''
[PROOF STEP]
using RP_target[OF \<open>pR2 \<in> ?RP2\<close> t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (?q1 q P io x y y', P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, ?y1 q P io x y y')] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> target (FSM.initial M) pR2 = q''

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target (FSM.initial M) pR2 = q''
[PROOF STEP]
have "target (initial M) pR2 \<in> fst d"
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR2 = q''

goal (1 subgoal):
 1. target (FSM.initial M) pR2 \<in> fst d
[PROOF STEP]
using \<open>q'' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR2 = q''
q'' \<in> fst d

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "pR1 \<noteq> pR2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR1 \<noteq> pR2
[PROOF STEP]
using \<open>target (initial M) pR1 = q'\<close> \<open>target (initial M) pR2 = q''\<close> \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR1 = q'
target (FSM.initial M) pR2 = q''
q' \<noteq> q''

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
obtain A t1 t2 where "(A,t1,t2) \<in> separators (q',q'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A t1 t2. (A, t1, t2) \<in> separators (q', q'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using t9[OF \<open>d \<in> set repetition_sets\<close> \<open>q' \<in> fst d\<close> \<open>q'' \<in> fst d\<close> \<open>q' \<noteq> q''\<close>]
[PROOF STATE]
proof (prove)
using this:
separators (q', q'') \<noteq> {}

goal (1 subgoal):
 1. (\<And>A t1 t2. (A, t1, t2) \<in> separators (q', q'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A, t1, t2) \<in> separators (q', q'')

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
have "(A,t2,t1) \<in> separators (q'',q')" and "is_separator M q' q'' A t1 t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, t2, t1) \<in> separators (q'', q') &&& is_separator M q' q'' A t1 t2
[PROOF STEP]
using t3[OF \<open>(A,t1,t2) \<in> separators (q',q'')\<close>]
[PROOF STATE]
proof (prove)
using this:
(A, t2, t1) \<in> separators (q'', q') \<and> is_separator M q' q'' A t1 t2

goal (1 subgoal):
 1. (A, t2, t1) \<in> separators (q'', q') &&& is_separator M q' q'' A t1 t2
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
(A, t2, t1) \<in> separators (q'', q')
is_separator M q' q'' A t1 t2

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(A, t2, t1) \<in> separators (q'', q')
is_separator M q' q'' A t1 t2
[PROOF STEP]
have "is_separator M q'' q' A t2 t1"
[PROOF STATE]
proof (prove)
using this:
(A, t2, t1) \<in> separators (q'', q')
is_separator M q' q'' A t1 t2

goal (1 subgoal):
 1. is_separator M q'' q' A t2 t1
[PROOF STEP]
using is_separator_sym
[PROOF STATE]
proof (prove)
using this:
(A, t2, t1) \<in> separators (q'', q')
is_separator M q' q'' A t1 t2
is_separator ?M ?q1.0 ?q2.0 ?A ?t1.0 ?t2.0 \<Longrightarrow> is_separator ?M ?q2.0 ?q1.0 ?A ?t2.0 ?t1.0

goal (1 subgoal):
 1. is_separator M q'' q' A t2 t1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_separator M q'' q' A t2 t1

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
show "io_targets M' (p_io pR1) (initial M') \<inter> io_targets M' (p_io pR2) (initial M') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {}"
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {}

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {}
[PROOF STEP]
obtain qT where "qT \<in> io_targets M' (p_io pR1) (FSM.initial M')"
                   and   "qT \<in> io_targets M' (p_io pR2) (FSM.initial M')"
[PROOF STATE]
proof (prove)
using this:
io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {}

goal (1 subgoal):
 1. (\<And>qT. \<lbrakk>qT \<in> io_targets M' (p_io pR1) (FSM.initial M'); qT \<in> io_targets M' (p_io pR2) (FSM.initial M')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')
[PROOF STEP]
have "qT \<in> states M'"
[PROOF STATE]
proof (prove)
using this:
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')

goal (1 subgoal):
 1. qT \<in> FSM.states M'
[PROOF STEP]
using path_target_is_state
[PROOF STATE]
proof (prove)
using this:
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')
path ?M ?q ?p \<Longrightarrow> target ?q ?p \<in> FSM.states ?M

goal (1 subgoal):
 1. qT \<in> FSM.states M'
[PROOF STEP]
unfolding io_targets.simps
[PROOF STATE]
proof (prove)
using this:
qT \<in> {target (FSM.initial M') p |p. path M' (FSM.initial M') p \<and> p_io p = p_io pR1}
qT \<in> {target (FSM.initial M') p |p. path M' (FSM.initial M') p \<and> p_io p = p_io pR2}
path ?M ?q ?p \<Longrightarrow> target ?q ?p \<in> FSM.states ?M

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

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
consider (a) "pR1 \<in> ?R1 \<and> pR2 \<in> ?R2" |
             (b) "pR1 \<in> ?R1 \<and> pR2 \<notin> ?R2" |
             (c) "pR1 \<notin> ?R1 \<and> pR2 \<in> ?R2" |
             (d) "pR1 \<notin> ?R1 \<and> pR2 \<notin> ?R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> thesis; pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> ?thesis; pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
case a
[PROOF STATE]
proof (state)
this:
pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p
[PROOF STEP]
have "pR1 \<in> ?R1" and "pR2 \<in> ?R2"
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p

goal (1 subgoal):
 1. pR1 \<in> R M q q' pP p &&& pR2 \<in> R M q q'' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pR1 \<in> R M q q' pP p
pR2 \<in> R M q q'' pP p

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain pR1' where "pR1 = pP@pR1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pR1'. pR1 = pP @ pR1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>pR1 \<in> ?R1\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. pR1 = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pR1'. pR1 = pP @ pR1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR1 = pP @ pR1'

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain pR2' where "pR2 = pP@pR2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pR2'. pR2 = pP @ pR2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>pR2 \<in> ?R2\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. pR2 = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pR2'. pR2 = pP @ pR2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR2 = pP @ pR2'

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR1' = take (length pR1') p" and "length pR1' \<le> length p" and "t_target (p ! (length pR1' - 1)) = q'" and "pR1' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
using R_component[of pP pR1' M q q' p] \<open>pR1 \<in> ?R1\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' = take (length pR1') p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> length pR1' \<le> length p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> t_target (p ! (length pR1' - 1)) = q'
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' \<noteq> []
pR1 \<in> R M q q' pP p

goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
unfolding \<open>pR1 = pP@pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' = take (length pR1') p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> length pR1' \<le> length p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> t_target (p ! (length pR1' - 1)) = q'
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' \<noteq> []
pP @ pR1' \<in> R M q q' pP p

goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR1' = take (length pR1') p
length pR1' \<le> length p
t_target (p ! (length pR1' - 1)) = q'
pR1' \<noteq> []

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR2' = take (length pR2') p" and "length pR2' \<le> length p" and "t_target (p ! (length pR2' - 1)) = q''" and "pR2' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
using R_component[of pP pR2' M q q'' p] \<open>pR2 \<in> ?R2\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' = take (length pR2') p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> length pR2' \<le> length p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> t_target (p ! (length pR2' - 1)) = q''
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' \<noteq> []
pR2 \<in> R M q q'' pP p

goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
unfolding \<open>pR2 = pP@pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' = take (length pR2') p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> length pR2' \<le> length p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> t_target (p ! (length pR2' - 1)) = q''
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' \<noteq> []
pP @ pR2' \<in> R M q q'' pP p

goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR2' = take (length pR2') p
length pR2' \<le> length p
t_target (p ! (length pR2' - 1)) = q''
pR2' \<noteq> []

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "target q pR1' = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q pR1' = q'
[PROOF STEP]
using \<open>target (initial M) pR1 = q'\<close> \<open>pR1' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR1 = q'
pR1' \<noteq> []

goal (1 subgoal):
 1. target q pR1' = q'
[PROOF STEP]
unfolding target.simps visited_states.simps \<open>pR1 = pP@pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
last (FSM.initial M # map t_target (pP @ pR1')) = q'
pR1' \<noteq> []

goal (1 subgoal):
 1. last (q # map t_target pR1') = q'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
target q pR1' = q'

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q pR1' = q'
[PROOF STEP]
have "target q pR1' \<in> fst d"
[PROOF STATE]
proof (prove)
using this:
target q pR1' = q'

goal (1 subgoal):
 1. target q pR1' \<in> fst d
[PROOF STEP]
using \<open>q' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
target q pR1' = q'
q' \<in> fst d

goal (1 subgoal):
 1. target q pR1' \<in> fst d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
target q pR1' \<in> fst d

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "target q pR2' = q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q pR2' = q''
[PROOF STEP]
using \<open>target (initial M) pR2 = q''\<close> \<open>pR2' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR2 = q''
pR2' \<noteq> []

goal (1 subgoal):
 1. target q pR2' = q''
[PROOF STEP]
unfolding target.simps visited_states.simps \<open>pR2 = pP@pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
last (FSM.initial M # map t_target (pP @ pR2')) = q''
pR2' \<noteq> []

goal (1 subgoal):
 1. last (q # map t_target pR2') = q''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
target q pR2' = q''

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q pR2' = q''
[PROOF STEP]
have "target q pR2' \<in> fst d"
[PROOF STATE]
proof (prove)
using this:
target q pR2' = q''

goal (1 subgoal):
 1. target q pR2' \<in> fst d
[PROOF STEP]
using \<open>q'' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
target q pR2' = q''
q'' \<in> fst d

goal (1 subgoal):
 1. target q pR2' \<in> fst d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
target q pR2' \<in> fst d

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR1' \<noteq> pR2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR1' \<noteq> pR2'
[PROOF STEP]
using \<open>pR1 \<noteq> pR2\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 \<noteq> pR2

goal (1 subgoal):
 1. pR1' \<noteq> pR2'
[PROOF STEP]
unfolding \<open>pR1 = pP@pR1'\<close> \<open>pR2 = pP@pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1' \<noteq> pP @ pR2'

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1' \<noteq> pR2'
[PROOF STEP]
have "length pR1' \<noteq> length pR2'"
[PROOF STATE]
proof (prove)
using this:
pR1' \<noteq> pR2'

goal (1 subgoal):
 1. length pR1' \<noteq> length pR2'
[PROOF STEP]
using \<open>pR1' = take (length pR1') p\<close> \<open>pR2' = take (length pR2') p\<close>
[PROOF STATE]
proof (prove)
using this:
pR1' \<noteq> pR2'
pR1' = take (length pR1') p
pR2' = take (length pR2') p

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pR1' \<noteq> length pR2'
[PROOF STEP]
consider (a1) "length pR1' < length pR2'" | (a2) "length pR2' < length pR1'"
[PROOF STATE]
proof (prove)
using this:
length pR1' \<noteq> length pR2'

goal (1 subgoal):
 1. \<lbrakk>length pR1' < length pR2' \<Longrightarrow> thesis; length pR2' < length pR1' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
length pR1' \<noteq> length pR2'
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

goal (1 subgoal):
 1. \<lbrakk>length pR1' < length pR2' \<Longrightarrow> thesis; length pR2' < length pR1' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>length pR1' < length pR2' \<Longrightarrow> ?thesis; length pR2' < length pR1' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length pR1' < length pR2' \<Longrightarrow> ?thesis; length pR2' < length pR1' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length pR1' < length pR2' \<Longrightarrow> ?thesis; length pR2' < length pR1' \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
case a1
[PROOF STATE]
proof (state)
this:
length pR1' < length pR2'

goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pR1' < length pR2'
[PROOF STEP]
have "pR2' = pR1' @ (drop (length pR1') pR2')"
[PROOF STATE]
proof (prove)
using this:
length pR1' < length pR2'

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

goal (1 subgoal):
 1. pR2' = pR1' @ drop (length pR1') pR2'
[PROOF STEP]
by (metis append_take_drop_id less_imp_le_nat take_le)
[PROOF STATE]
proof (state)
this:
pR2' = pR1' @ drop (length pR1') pR2'

goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR2' = pR1' @ drop (length pR1') pR2'
[PROOF STEP]
have "p = pR1' @ (drop (length pR1') pR2') @ (drop (length pR2') p)"
[PROOF STATE]
proof (prove)
using this:
pR2' = pR1' @ drop (length pR1') pR2'

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

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

goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
have "(drop (length pR1') pR2') \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length pR1') pR2' \<noteq> []
[PROOF STEP]
using a1 \<open>pR2' = take (length pR2') p\<close>
[PROOF STATE]
proof (prove)
using this:
length pR1' < length pR2'
pR2' = take (length pR2') p

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

goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
have "target q (pR1' @ drop (length pR1') pR2') \<in> fst d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q (pR1' @ drop (length pR1') pR2') \<in> fst d
[PROOF STEP]
using \<open>pR2' = pR1' @ (drop (length pR1') pR2')\<close>[symmetric] \<open>target q pR2' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
pR1' @ drop (length pR1') pR2' = pR2'
target q pR2' \<in> fst d

goal (1 subgoal):
 1. target q (pR1' @ drop (length pR1') pR2') \<in> fst d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target q (pR1' @ drop (length pR1') pR2') \<in> fst d

goal (2 subgoals):
 1. length pR1' < length pR2' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
 2. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
using t10[OF \<open>q \<in> fst ` PS\<close> \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
                       \<open>p = pR1' @ (drop (length pR1') pR2') @ (drop (length pR2') p)\<close>
                       \<open>(drop (length pR1') pR2') \<noteq> []\<close> \<open>target q pR1' \<in> fst d\<close>
                       \<open>target q (pR1' @ drop (length pR1') pR2') \<in> fst d\<close>]
[PROOF STATE]
proof (prove)
using this:
target q pR1' \<noteq> target q (pR1' @ drop (length pR1') pR2') \<Longrightarrow> pR1' \<in> tps q \<and> pR1' @ drop (length pR1') pR2' \<in> tps q \<and> target q pR1' \<in> rd_targets (q, pR1' @ drop (length pR1') pR2') \<and> target q (pR1' @ drop (length pR1') pR2') \<in> rd_targets (q, pR1')

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
unfolding \<open>pR2' = pR1' @ (drop (length pR1') pR2')\<close>[symmetric] \<open>target q pR1' = q'\<close>  \<open>target q pR2' = q''\<close>
[PROOF STATE]
proof (prove)
using this:
q' \<noteq> q'' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
using \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
q' \<noteq> q'' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
q' \<noteq> q''

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
case a2
[PROOF STATE]
proof (state)
this:
length pR2' < length pR1'

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length pR2' < length pR1'
[PROOF STEP]
have "pR1' = pR2' @ (drop (length pR2') pR1')"
[PROOF STATE]
proof (prove)
using this:
length pR2' < length pR1'

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

goal (1 subgoal):
 1. pR1' = pR2' @ drop (length pR2') pR1'
[PROOF STEP]
by (metis append_take_drop_id less_imp_le_nat take_le)
[PROOF STATE]
proof (state)
this:
pR1' = pR2' @ drop (length pR2') pR1'

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1' = pR2' @ drop (length pR2') pR1'
[PROOF STEP]
have "p = pR2' @ (drop (length pR2') pR1') @ (drop (length pR1') p)"
[PROOF STATE]
proof (prove)
using this:
pR1' = pR2' @ drop (length pR2') pR1'

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

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

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
have "(drop (length pR2') pR1') \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length pR2') pR1' \<noteq> []
[PROOF STEP]
using a2 \<open>pR1' = take (length pR1') p\<close>
[PROOF STATE]
proof (prove)
using this:
length pR2' < length pR1'
pR1' = take (length pR1') p

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

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
have "target q (pR2' @ drop (length pR2') pR1') \<in> fst d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q (pR2' @ drop (length pR2') pR1') \<in> fst d
[PROOF STEP]
using \<open>pR1' = pR2' @ (drop (length pR2') pR1')\<close>[symmetric] \<open>target q pR1' \<in> fst d\<close>
[PROOF STATE]
proof (prove)
using this:
pR2' @ drop (length pR2') pR1' = pR1'
target q pR1' \<in> fst d

goal (1 subgoal):
 1. target q (pR2' @ drop (length pR2') pR1') \<in> fst d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
target q (pR2' @ drop (length pR2') pR1') \<in> fst d

goal (1 subgoal):
 1. length pR2' < length pR1' \<Longrightarrow> pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
using t10[OF \<open>q \<in> fst ` PS\<close> \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
                       \<open>p = pR2' @ (drop (length pR2') pR1') @ (drop (length pR1') p)\<close>
                       \<open>(drop (length pR2') pR1') \<noteq> []\<close> \<open>target q pR2' \<in> fst d\<close>
                       \<open>target q (pR2' @ drop (length pR2') pR1') \<in> fst d\<close>]
[PROOF STATE]
proof (prove)
using this:
target q pR2' \<noteq> target q (pR2' @ drop (length pR2') pR1') \<Longrightarrow> pR2' \<in> tps q \<and> pR2' @ drop (length pR2') pR1' \<in> tps q \<and> target q pR2' \<in> rd_targets (q, pR2' @ drop (length pR2') pR1') \<and> target q (pR2' @ drop (length pR2') pR1') \<in> rd_targets (q, pR2')

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
unfolding \<open>pR1' = pR2' @ (drop (length pR2') pR1')\<close>[symmetric] \<open>target q pR1' = q'\<close> \<open>target q pR2' = q''\<close>
[PROOF STATE]
proof (prove)
using this:
q'' \<noteq> q' \<Longrightarrow> pR2' \<in> tps q \<and> pR1' \<in> tps q \<and> q'' \<in> rd_targets (q, pR1') \<and> q' \<in> rd_targets (q, pR2')

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
using \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
q'' \<noteq> q' \<Longrightarrow> pR2' \<in> tps q \<and> pR1' \<in> tps q \<and> q'' \<in> rd_targets (q, pR1') \<and> q' \<in> rd_targets (q, pR2')
q' \<noteq> q''

goal (1 subgoal):
 1. pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
have "pR1' \<in> tps q" and "pR2' \<in> tps q" and "q' \<in> rd_targets (q, pR2')" and "q'' \<in> rd_targets (q, pR1')"
[PROOF STATE]
proof (prove)
using this:
pR1' \<in> tps q \<and> pR2' \<in> tps q \<and> q' \<in> rd_targets (q, pR2') \<and> q'' \<in> rd_targets (q, pR1')

goal (1 subgoal):
 1. (pR1' \<in> tps q &&& pR2' \<in> tps q) &&& q' \<in> rd_targets (q, pR2') &&& q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
pR1' \<in> tps q
pR2' \<in> tps q
q' \<in> rd_targets (q, pR2')
q'' \<in> rd_targets (q, pR1')

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p_io pP @ p_io pR1' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ p_io pR1' \<in> L M'
[PROOF STEP]
using language_prefix_append[OF \<open>p_io pP @ p_io p \<in> L M'\<close>, of "length pR1'"]
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR1') p) \<in> L M'

goal (1 subgoal):
 1. p_io pP @ p_io pR1' \<in> L M'
[PROOF STEP]
using \<open>pR1' = take (length pR1') p\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR1') p) \<in> L M'
pR1' = take (length pR1') p

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
using pass3[OF \<open>(q, P) \<in> PS\<close> \<open>path P (initial P) pP\<close> \<open>target (initial P) pP = q\<close> \<open>pR1' \<in> tps q\<close>
                       \<open>p_io pP @ p_io pR1' \<in> L M'\<close> \<open>q'' \<in> rd_targets (q, pR1')\<close>, of A t1 t2]
              \<open>(A, t1, t2) \<in> separators (q', q'')\<close> \<open>qT \<in> io_targets M' (p_io pR1) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t1, t2) \<in> separators (target q pR1', q''); ?qT \<in> io_targets M' (p_io pP @ p_io pR1') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
unfolding \<open>target q pR1' = q'\<close> \<open>pR1 = pP @ pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t1, t2) \<in> separators (q', q''); ?qT \<in> io_targets M' (p_io pP @ p_io pR1') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io (pP @ pR1')) (FSM.initial M')

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p_io pP @ p_io pR2' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ p_io pR2' \<in> L M'
[PROOF STEP]
using language_prefix_append[OF \<open>p_io pP @ p_io p \<in> L M'\<close>, of "length pR2'"]
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR2') p) \<in> L M'

goal (1 subgoal):
 1. p_io pP @ p_io pR2' \<in> L M'
[PROOF STEP]
using \<open>pR2' = take (length pR2') p\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR2') p) \<in> L M'
pR2' = take (length pR2') p

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
using pass3[OF \<open>(q, P) \<in> PS\<close> \<open>path P (initial P) pP\<close> \<open>target (initial P) pP = q\<close> \<open>pR2' \<in> tps q\<close>
                       \<open>p_io pP @ p_io pR2' \<in> L M'\<close> \<open>q' \<in> rd_targets (q, pR2')\<close>, of A t2 t1]
              \<open>(A, t2, t1) \<in> separators (q'', q')\<close> \<open>qT \<in> io_targets M' (p_io pR2) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t2, t1) \<in> separators (target q pR2', q'); ?qT \<in> io_targets M' (p_io pP @ p_io pR2') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
unfolding \<open>target q pR2' = q''\<close> \<open>pR2 = pP @ pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t2, t1) \<in> separators (q'', q'); ?qT \<in> io_targets M' (p_io pP @ p_io pR2') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io (pP @ pR2')) (FSM.initial M')

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
(* the state qT reached by both paths cannot satisfy the ATC that r-distinguishes their respective targets for both targets at the same time *)
[PROOF STATE]
proof (state)
this:
pass_separator_ATC M' A qT t1

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "qT \<noteq> qT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qT \<noteq> qT
[PROOF STEP]
using pass_separator_ATC_reduction_distinction[OF \<open>observable M\<close> \<open>observable M'\<close> \<open>inputs M' = inputs M\<close> \<open>pass_separator_ATC M' A qT t2\<close> \<open>pass_separator_ATC M' A qT t1\<close> \<open>q' \<in> states M\<close> \<open>q'' \<in> states M\<close> \<open>q' \<noteq> q''\<close> \<open>qT \<in> states M'\<close> \<open>qT \<in> states M'\<close> \<open>is_separator M q' q'' A t1 t2\<close> \<open>completely_specified M'\<close>]
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal (4 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 4. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qT \<noteq> qT
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p
[PROOF STEP]
have "pR1 \<in> ?R1" and "pR2 \<notin> ?R2"
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p

goal (1 subgoal):
 1. pR1 \<in> R M q q' pP p &&& pR2 \<notin> R M q q'' pP p
[PROOF STEP]
using \<open>pR1 \<in> ?RP1\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p
pR1 \<in> RP M q q' pP p PS M'

goal (1 subgoal):
 1. pR1 \<in> R M q q' pP p &&& pR2 \<notin> R M q q'' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pR1 \<in> R M q q' pP p
pR2 \<notin> R M q q'' pP p

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain pR1' where "pR1 = pP@pR1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pR1'. pR1 = pP @ pR1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>pR1 \<in> ?R1\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. pR1 = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pR1'. pR1 = pP @ pR1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR1 = pP @ pR1'

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR1' = take (length pR1') p" and "length pR1' \<le> length p" and "t_target (p ! (length pR1' - 1)) = q'" and "pR1' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
using R_component[of pP pR1' M q q' p] \<open>pR1 \<in> ?R1\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' = take (length pR1') p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> length pR1' \<le> length p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> t_target (p ! (length pR1' - 1)) = q'
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' \<noteq> []
pR1 \<in> R M q q' pP p

goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
unfolding \<open>pR1 = pP@pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' = take (length pR1') p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> length pR1' \<le> length p
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> t_target (p ! (length pR1' - 1)) = q'
pP @ pR1' \<in> R M q q' pP p \<Longrightarrow> pR1' \<noteq> []
pP @ pR1' \<in> R M q q' pP p

goal (1 subgoal):
 1. (pR1' = take (length pR1') p &&& length pR1' \<le> length p) &&& t_target (p ! (length pR1' - 1)) = q' &&& pR1' \<noteq> []
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR1' = take (length pR1') p
length pR1' \<le> length p
t_target (p ! (length pR1' - 1)) = q'
pR1' \<noteq> []

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "target q pR1' = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q pR1' = q'
[PROOF STEP]
using \<open>target (initial M) pR1 = q'\<close> \<open>pR1' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR1 = q'
pR1' \<noteq> []

goal (1 subgoal):
 1. target q pR1' = q'
[PROOF STEP]
unfolding target.simps visited_states.simps \<open>pR1 = pP@pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
last (FSM.initial M # map t_target (pP @ pR1')) = q'
pR1' \<noteq> []

goal (1 subgoal):
 1. last (q # map t_target pR1') = q'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
target q pR1' = q'

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q pR1' = q'
[PROOF STEP]
have "target q pR1' \<in> fst d" and "target q pR1' \<noteq> q''"
[PROOF STATE]
proof (prove)
using this:
target q pR1' = q'

goal (1 subgoal):
 1. target q pR1' \<in> fst d &&& target q pR1' \<noteq> q''
[PROOF STEP]
using \<open>q' \<in> fst d\<close> \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
target q pR1' = q'
q' \<in> fst d
q' \<noteq> q''

goal (1 subgoal):
 1. target q pR1' \<in> fst d &&& target q pR1' \<noteq> q''
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
target q pR1' \<in> fst d
target q pR1' \<noteq> q''

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain P' where "(q'', P') \<in> PS"
                      "path P' (FSM.initial P') pR2"
                      "target (FSM.initial P') pR2 = q''"
                      "path M (FSM.initial M) pR2"
                      "target (FSM.initial M) pR2 = q''"
                      "p_io pR2 \<in> L M'"
                      "RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q'', P') \<in> PS; path P' (FSM.initial P') pR2; target (FSM.initial P') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RP_from_R_inserted[OF t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close> \<open>pR2 \<in> ?RP2\<close> \<open>pR2 \<notin> ?R2\<close>,
                                 of "\<lambda> q P io x y y' . q" "\<lambda> q P io x y y' . y"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y)] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'; \<And>P'. \<lbrakk>(q'', P') \<in> PS; path P' (FSM.initial P') pR2; target (FSM.initial P') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q'', P') \<in> PS; path P' (FSM.initial P') pR2; target (FSM.initial P') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q'', P') \<in> PS
path P' (FSM.initial P') pR2
target (FSM.initial P') pR2 = q''
path M (FSM.initial M) pR2
target (FSM.initial M) pR2 = q''
p_io pR2 \<in> L M'
RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "q'' \<in> fst ` PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q'' \<in> fst ` PS
[PROOF STEP]
using \<open>(q'',P') \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
(q'', P') \<in> PS

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p = pR1' @ (drop (length pR1') p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = pR1' @ drop (length pR1') p
[PROOF STEP]
using \<open>pR1' = take (length pR1') p\<close>
[PROOF STATE]
proof (prove)
using this:
pR1' = take (length pR1') p

goal (1 subgoal):
 1. p = pR1' @ drop (length pR1') p
[PROOF STEP]
by (metis append_take_drop_id)
[PROOF STATE]
proof (state)
this:
p = pR1' @ drop (length pR1') p

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR1' \<in> tps q" and "[] \<in> tps q''" and "target q pR1' \<in> rd_targets (q'', [])" and "q'' \<in> rd_targets (q, pR1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR1' \<in> tps q &&& [] \<in> tps q'') &&& target q pR1' \<in> rd_targets (q'', []) &&& q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
using t11[OF \<open>q \<in> fst ` PS\<close> \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
                     \<open>p = pR1' @ (drop (length pR1') p)\<close> \<open>q'' \<in> fst ` PS\<close>
                     \<open>target q pR1' \<in> fst d\<close> \<open>q'' \<in> fst d\<close> \<open>target q pR1' \<noteq> q''\<close>]
[PROOF STATE]
proof (prove)
using this:
pR1' \<in> tps q \<and> [] \<in> tps q'' \<and> target q pR1' \<in> rd_targets (q'', []) \<and> q'' \<in> rd_targets (q, pR1')

goal (1 subgoal):
 1. (pR1' \<in> tps q &&& [] \<in> tps q'') &&& target q pR1' \<in> rd_targets (q'', []) &&& q'' \<in> rd_targets (q, pR1')
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
pR1' \<in> tps q
[] \<in> tps q''
target q pR1' \<in> rd_targets (q'', [])
q'' \<in> rd_targets (q, pR1')

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p_io pP @ p_io pR1' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ p_io pR1' \<in> L M'
[PROOF STEP]
using language_prefix_append[OF \<open>p_io pP @ p_io p \<in> L M'\<close>, of "length pR1'"]
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR1') p) \<in> L M'

goal (1 subgoal):
 1. p_io pP @ p_io pR1' \<in> L M'
[PROOF STEP]
using \<open>pR1' = take (length pR1') p\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR1') p) \<in> L M'
pR1' = take (length pR1') p

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
using pass3[OF \<open>(q, P) \<in> PS\<close> \<open>path P (initial P) pP\<close> \<open>target (initial P) pP = q\<close> \<open>pR1' \<in> tps q\<close>
                       \<open>p_io pP @ p_io pR1' \<in> L M'\<close> \<open>q'' \<in> rd_targets (q, pR1')\<close>, of A t1 t2]
              \<open>(A, t1, t2) \<in> separators (q', q'')\<close> \<open>qT \<in> io_targets M' (p_io pR1) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t1, t2) \<in> separators (target q pR1', q''); ?qT \<in> io_targets M' (p_io pP @ p_io pR1') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
unfolding \<open>target q pR1' = q'\<close> \<open>pR1 = pP @ pR1'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t1, t2) \<in> separators (q', q''); ?qT \<in> io_targets M' (p_io pP @ p_io pR1') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io (pP @ pR1')) (FSM.initial M')

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
using pass3[OF \<open>(q'', P') \<in> PS\<close> \<open>path P' (FSM.initial P') pR2\<close> \<open>target (FSM.initial P') pR2 = q''\<close>
                       \<open>[] \<in> tps q''\<close> _ \<open>target q pR1' \<in> rd_targets (q'', [])\<close>, of A t2 t1 qT]
              \<open>(A, t2, t1) \<in> separators (q'', q')\<close> \<open>qT \<in> io_targets M' (p_io pR2) (FSM.initial M')\<close> \<open>p_io pR2 \<in> L M'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR2 @ p_io [] \<in> L M'; (A, t2, t1) \<in> separators (target q'' [], target q pR1'); qT \<in> io_targets M' (p_io pR2 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')
p_io pR2 \<in> L M'

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
unfolding \<open>target q pR1' = q'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR2 @ p_io [] \<in> L M'; (A, t2, t1) \<in> separators (target q'' [], q'); qT \<in> io_targets M' (p_io pR2 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')
p_io pR2 \<in> L M'

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "qT \<noteq> qT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qT \<noteq> qT
[PROOF STEP]
using pass_separator_ATC_reduction_distinction[OF \<open>observable M\<close> \<open>observable M'\<close> \<open>inputs M' = inputs M\<close>
                                                          \<open>pass_separator_ATC M' A qT t2\<close>
                                                          \<open>pass_separator_ATC M' A qT t1\<close> \<open>q' \<in> states M\<close>
                                                          \<open>q'' \<in> states M\<close> \<open>q' \<noteq> q''\<close> \<open>qT \<in> states M'\<close>
                                                          \<open>qT \<in> states M'\<close> \<open>is_separator M q' q'' A t1 t2\<close>
                                                          \<open>completely_specified M'\<close>]
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal (3 subgoals):
 1. pR1 \<in> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 3. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qT \<noteq> qT
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
case c
[PROOF STATE]
proof (state)
this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p
[PROOF STEP]
have "pR2 \<in> ?R2" and "pR1 \<notin> ?R1"
[PROOF STATE]
proof (prove)
using this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p

goal (1 subgoal):
 1. pR2 \<in> R M q q'' pP p &&& pR1 \<notin> R M q q' pP p
[PROOF STEP]
using \<open>pR2 \<in> ?RP2\<close>
[PROOF STATE]
proof (prove)
using this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p
pR2 \<in> RP M q q'' pP p PS M'

goal (1 subgoal):
 1. pR2 \<in> R M q q'' pP p &&& pR1 \<notin> R M q q' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pR2 \<in> R M q q'' pP p
pR1 \<notin> R M q q' pP p

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain pR2' where "pR2 = pP@pR2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pR2'. pR2 = pP @ pR2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R_component_ob[OF \<open>pR2 \<in> ?R2\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<And>pR. pR2 = pP @ pR \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pR2'. pR2 = pP @ pR2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pR2 = pP @ pR2'

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR2' = take (length pR2') p"
       and "length pR2' \<le> length p"
       and "t_target (p ! (length pR2' - 1)) = q''"
       and "pR2' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
using R_component[of pP pR2' M q q'' p] \<open>pR2 \<in> ?R2\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' = take (length pR2') p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> length pR2' \<le> length p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> t_target (p ! (length pR2' - 1)) = q''
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' \<noteq> []
pR2 \<in> R M q q'' pP p

goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
unfolding \<open>pR2 = pP@pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' = take (length pR2') p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> length pR2' \<le> length p
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> t_target (p ! (length pR2' - 1)) = q''
pP @ pR2' \<in> R M q q'' pP p \<Longrightarrow> pR2' \<noteq> []
pP @ pR2' \<in> R M q q'' pP p

goal (1 subgoal):
 1. (pR2' = take (length pR2') p &&& length pR2' \<le> length p) &&& t_target (p ! (length pR2' - 1)) = q'' &&& pR2' \<noteq> []
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pR2' = take (length pR2') p
length pR2' \<le> length p
t_target (p ! (length pR2' - 1)) = q''
pR2' \<noteq> []

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "target q pR2' = q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. target q pR2' = q''
[PROOF STEP]
using \<open>target (initial M) pR2 = q''\<close> \<open>pR2' \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
target (FSM.initial M) pR2 = q''
pR2' \<noteq> []

goal (1 subgoal):
 1. target q pR2' = q''
[PROOF STEP]
unfolding target.simps visited_states.simps \<open>pR2 = pP@pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
last (FSM.initial M # map t_target (pP @ pR2')) = q''
pR2' \<noteq> []

goal (1 subgoal):
 1. last (q # map t_target pR2') = q''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
target q pR2' = q''

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
target q pR2' = q''
[PROOF STEP]
have "target q pR2' \<in> fst d" and "target q pR2' \<noteq> q'"
[PROOF STATE]
proof (prove)
using this:
target q pR2' = q''

goal (1 subgoal):
 1. target q pR2' \<in> fst d &&& target q pR2' \<noteq> q'
[PROOF STEP]
using \<open>q'' \<in> fst d\<close> \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
target q pR2' = q''
q'' \<in> fst d
q' \<noteq> q''

goal (1 subgoal):
 1. target q pR2' \<in> fst d &&& target q pR2' \<noteq> q'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
target q pR2' \<in> fst d
target q pR2' \<noteq> q'

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain P' where "(q', P') \<in> PS"
                      "path P' (FSM.initial P') pR1"
                      "target (FSM.initial P') pR1 = q'"
                      "path M (FSM.initial M) pR1"
                      "target (FSM.initial M) pR1 = q'"
                      "p_io pR1 \<in> L M'"
                      "RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RP_from_R_inserted[OF t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close> \<open>pR1 \<in> ?RP1\<close> \<open>pR1 \<notin> ?R1\<close>,
                                 of "\<lambda> q P io x y y' . q" "\<lambda> q P io x y y' . y"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y)] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'; \<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q', P') \<in> PS
path P' (FSM.initial P') pR1
target (FSM.initial P') pR1 = q'
path M (FSM.initial M) pR1
target (FSM.initial M) pR1 = q'
p_io pR1 \<in> L M'
RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "q' \<in> fst ` PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' \<in> fst ` PS
[PROOF STEP]
using \<open>(q',P') \<in> PS\<close>
[PROOF STATE]
proof (prove)
using this:
(q', P') \<in> PS

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p = pR2' @ (drop (length pR2') p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = pR2' @ drop (length pR2') p
[PROOF STEP]
using \<open>pR2' = take (length pR2') p\<close>
[PROOF STATE]
proof (prove)
using this:
pR2' = take (length pR2') p

goal (1 subgoal):
 1. p = pR2' @ drop (length pR2') p
[PROOF STEP]
by (metis append_take_drop_id)
[PROOF STATE]
proof (state)
this:
p = pR2' @ drop (length pR2') p

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pR2' \<in> tps q" and "[] \<in> tps q'" and "target q pR2' \<in> rd_targets (q', [])" and "q' \<in> rd_targets (q, pR2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pR2' \<in> tps q &&& [] \<in> tps q') &&& target q pR2' \<in> rd_targets (q', []) &&& q' \<in> rd_targets (q, pR2')
[PROOF STEP]
using t11[OF \<open>q \<in> fst ` PS\<close> \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close>
                     \<open>p = pR2' @ (drop (length pR2') p)\<close> \<open>q' \<in> fst ` PS\<close> \<open>target q pR2' \<in> fst d\<close>
                     \<open>q' \<in> fst d\<close> \<open>target q pR2' \<noteq> q'\<close>]
[PROOF STATE]
proof (prove)
using this:
pR2' \<in> tps q \<and> [] \<in> tps q' \<and> target q pR2' \<in> rd_targets (q', []) \<and> q' \<in> rd_targets (q, pR2')

goal (1 subgoal):
 1. (pR2' \<in> tps q &&& [] \<in> tps q') &&& target q pR2' \<in> rd_targets (q', []) &&& q' \<in> rd_targets (q, pR2')
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
pR2' \<in> tps q
[] \<in> tps q'
target q pR2' \<in> rd_targets (q', [])
q' \<in> rd_targets (q, pR2')

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "p_io pP @ p_io pR2' \<in> L M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io pP @ p_io pR2' \<in> L M'
[PROOF STEP]
using language_prefix_append[OF \<open>p_io pP @ p_io p \<in> L M'\<close>, of "length pR2'"]
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR2') p) \<in> L M'

goal (1 subgoal):
 1. p_io pP @ p_io pR2' \<in> L M'
[PROOF STEP]
using \<open>pR2' = take (length pR2') p\<close>
[PROOF STATE]
proof (prove)
using this:
p_io pP @ p_io (take (length pR2') p) \<in> L M'
pR2' = take (length pR2') p

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
using pass3[OF \<open>(q, P) \<in> PS\<close> \<open>path P (initial P) pP\<close> \<open>target (initial P) pP = q\<close> \<open>pR2' \<in> tps q\<close>
                       \<open>p_io pP @ p_io pR2' \<in> L M'\<close> \<open>q' \<in> rd_targets (q, pR2')\<close>, of A t2 t1]
              \<open>(A, t2, t1) \<in> separators (q'', q')\<close> \<open>qT \<in> io_targets M' (p_io pR2) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t2, t1) \<in> separators (target q pR2', q'); ?qT \<in> io_targets M' (p_io pP @ p_io pR2') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
unfolding \<open>target q pR2' = q''\<close> \<open>pR2 = pP @ pR2'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(A, t2, t1) \<in> separators (q'', q'); ?qT \<in> io_targets M' (p_io pP @ p_io pR2') (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A ?qT t1
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io (pP @ pR2')) (FSM.initial M')

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
using pass3[OF \<open>(q', P') \<in> PS\<close> \<open>path P' (FSM.initial P') pR1\<close> \<open>target (FSM.initial P') pR1 = q'\<close>
                       \<open>[] \<in> tps q'\<close> _ \<open>target q pR2' \<in> rd_targets (q', [])\<close>, of A t1 t2 qT]
              \<open>(A, t1, t2) \<in> separators (q', q'')\<close> \<open>qT \<in> io_targets M' (p_io pR1) (FSM.initial M')\<close> \<open>p_io pR1 \<in> L M'\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR1 @ p_io [] \<in> L M'; (A, t1, t2) \<in> separators (target q' [], target q pR2'); qT \<in> io_targets M' (p_io pR1 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
p_io pR1 \<in> L M'

goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
unfolding \<open>target q pR2' = q''\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR1 @ p_io [] \<in> L M'; (A, t1, t2) \<in> separators (target q' [], q''); qT \<in> io_targets M' (p_io pR1 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t2
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')
p_io pR1 \<in> L M'

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "qT \<noteq> qT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qT \<noteq> qT
[PROOF STEP]
using pass_separator_ATC_reduction_distinction[OF \<open>observable M\<close> \<open>observable M'\<close> \<open>inputs M' = inputs M\<close>
                                                          \<open>pass_separator_ATC M' A qT t1\<close> \<open>pass_separator_ATC M' A qT t2\<close>
                                                          \<open>q'' \<in> states M\<close> \<open>q' \<in> states M\<close> _ \<open>qT \<in> states M'\<close> \<open>qT \<in> states M'\<close>
                                                          \<open>is_separator M q'' q' A t2 t1\<close> \<open>completely_specified M'\<close>]
              \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
q'' \<noteq> q' \<Longrightarrow> qT \<noteq> qT
q' \<noteq> q''

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

goal (2 subgoals):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<in> R M q q'' pP p \<Longrightarrow> False
 2. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qT \<noteq> qT
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
case d
[PROOF STATE]
proof (state)
this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p
[PROOF STEP]
have "pR1 \<notin> ?R1" and "pR2 \<notin> ?R2"
[PROOF STATE]
proof (prove)
using this:
pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p &&& pR2 \<notin> R M q q'' pP p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pR1 \<notin> R M q q' pP p
pR2 \<notin> R M q q'' pP p

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain P' where "(q', P') \<in> PS"
                      "path P' (FSM.initial P') pR1"
                      "target (FSM.initial P') pR1 = q'"
                      "path M (FSM.initial M) pR1"
                      "target (FSM.initial M) pR1 = q'"
                      "p_io pR1 \<in> L M'"
                      "RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RP_from_R_inserted[OF t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close>
                                    \<open>pR1 \<in> ?RP1\<close> \<open>pR1 \<notin> ?R1\<close>, of "\<lambda> q P io x y y' . q" "\<lambda> q P io x y y' . y"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y)] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'; \<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(q', P') \<in> PS; path P' (FSM.initial P') pR1; target (FSM.initial P') pR1 = q'; path M (FSM.initial M) pR1; target (FSM.initial M) pR1 = q'; p_io pR1 \<in> L M'; RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q', P') \<in> PS
path P' (FSM.initial P') pR1
target (FSM.initial P') pR1 = q'
path M (FSM.initial M) pR1
target (FSM.initial M) pR1 = q'
p_io pR1 \<in> L M'
RP M q q' pP p PS M' = insert pR1 (R M q q' pP p)

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "q' \<in> snd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q' \<in> snd d
[PROOF STEP]
by (metis IntI \<open>(q', P') \<in> PS\<close> \<open>d \<in> set repetition_sets\<close> assms(13) fst_eqD image_eqI t8')
[PROOF STATE]
proof (state)
this:
q' \<in> snd d

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
obtain P'' where "(q'', P'') \<in> PS"
                      "path P'' (FSM.initial P'') pR2"
                      "target (FSM.initial P'') pR2 = q''"
                      "path M (FSM.initial M) pR2"
                      "target (FSM.initial M) pR2 = q''"
                      "p_io pR2 \<in> L M'"
                      "RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>(q'', P'') \<in> PS; path P'' (FSM.initial P'') pR2; target (FSM.initial P'') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RP_from_R_inserted[OF t2 pass1 \<open>completely_specified M'\<close> \<open>inputs M' = inputs M\<close> \<open>pR2 \<in> ?RP2\<close> \<open>pR2 \<notin> ?R2\<close>,
                                 of "\<lambda> q P io x y y' . q" "\<lambda> q P io x y y' . y"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q P. (q, P) \<in> PS \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> (q, P) \<in> PS; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y)] \<in> L P; \<And>q P io x y y'. \<lbrakk>(q, P) \<in> PS; io @ [(x, y)] \<in> L P; io @ [(x, y')] \<in> L M'\<rbrakk> \<Longrightarrow> io @ [(x, y')] \<in> L M'; \<And>P'. \<lbrakk>(q'', P') \<in> PS; path P' (FSM.initial P') pR2; target (FSM.initial P') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>(q'', P'') \<in> PS; path P'' (FSM.initial P'') pR2; target (FSM.initial P'') pR2 = q''; path M (FSM.initial M) pR2; target (FSM.initial M) pR2 = q''; p_io pR2 \<in> L M'; RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(q'', P'') \<in> PS
path P'' (FSM.initial P'') pR2
target (FSM.initial P'') pR2 = q''
path M (FSM.initial M) pR2
target (FSM.initial M) pR2 = q''
p_io pR2 \<in> L M'
RP M q q'' pP p PS M' = insert pR2 (R M q q'' pP p)

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "q'' \<in> snd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q'' \<in> snd d
[PROOF STEP]
by (metis IntI \<open>(q'', P'') \<in> PS\<close> \<open>d \<in> set repetition_sets\<close> assms(14) fst_eqD image_eqI t8')
[PROOF STATE]
proof (state)
this:
q'' \<in> snd d

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "[] \<in> tps q'" and "[] \<in> tps q''" and "q' \<in> rd_targets (q'', [])" and "q'' \<in> rd_targets (q', [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([] \<in> tps q' &&& [] \<in> tps q'') &&& q' \<in> rd_targets (q'', []) &&& q'' \<in> rd_targets (q', [])
[PROOF STEP]
using t12[OF \<open>q \<in> fst ` PS\<close> \<open>(p, d) \<in> m_traversal_paths_with_witness M q repetition_sets m\<close> \<open>q' \<noteq> q''\<close> \<open>q' \<in> snd d\<close> \<open>q'' \<in> snd d\<close>]
[PROOF STATE]
proof (prove)
using this:
[] \<in> tps q' \<and> [] \<in> tps q'' \<and> q' \<in> rd_targets (q'', []) \<and> q'' \<in> rd_targets (q', [])

goal (1 subgoal):
 1. ([] \<in> tps q' &&& [] \<in> tps q'') &&& q' \<in> rd_targets (q'', []) &&& q'' \<in> rd_targets (q', [])
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
[] \<in> tps q'
[] \<in> tps q''
q' \<in> rd_targets (q'', [])
q'' \<in> rd_targets (q', [])

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t1
[PROOF STEP]
using pass3[OF \<open>(q'', P'') \<in> PS\<close> \<open>path P'' (initial P'') pR2\<close> \<open>target (initial P'') pR2 = q''\<close>
                       \<open>[] \<in> tps q''\<close> _ \<open>q' \<in> rd_targets (q'', [])\<close>, of A t2 t1 qT]
              \<open>p_io pR2 \<in> L M'\<close> \<open>(A, t2, t1) \<in> separators (q'', q')\<close> \<open>qT \<in> io_targets M' (p_io pR2) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR2 @ p_io [] \<in> L M'; (A, t2, t1) \<in> separators (target q'' [], q'); qT \<in> io_targets M' (p_io pR2 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t1
p_io pR2 \<in> L M'
(A, t2, t1) \<in> separators (q'', q')
qT \<in> io_targets M' (p_io pR2) (FSM.initial M')

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

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "pass_separator_ATC M' A qT t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pass_separator_ATC M' A qT t2
[PROOF STEP]
using pass3[OF \<open>(q', P') \<in> PS\<close> \<open>path P' (initial P') pR1\<close> \<open>target (initial P') pR1 = q'\<close>
                       \<open>[] \<in> tps q'\<close> _ \<open>q'' \<in> rd_targets (q', [])\<close>, of A t1 t2 qT]
              \<open>p_io pR1 \<in> L M'\<close> \<open>(A, t1, t2) \<in> separators (q', q'')\<close> \<open>qT \<in> io_targets M' (p_io pR1) (FSM.initial M')\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p_io pR1 @ p_io [] \<in> L M'; (A, t1, t2) \<in> separators (target q' [], q''); qT \<in> io_targets M' (p_io pR1 @ p_io []) (FSM.initial M')\<rbrakk> \<Longrightarrow> pass_separator_ATC M' A qT t2
p_io pR1 \<in> L M'
(A, t1, t2) \<in> separators (q', q'')
qT \<in> io_targets M' (p_io pR1) (FSM.initial M')

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

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
have "qT \<noteq> qT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qT \<noteq> qT
[PROOF STEP]
using pass_separator_ATC_reduction_distinction[OF \<open>observable M\<close> \<open>observable M'\<close>
                                                          \<open>inputs M' = inputs M\<close> \<open>pass_separator_ATC M' A qT t1\<close>
                                                          \<open>pass_separator_ATC M' A qT t2\<close> \<open>q'' \<in> states M\<close>
                                                          \<open>q' \<in> states M\<close> _ \<open>qT \<in> states M'\<close> \<open>qT \<in> states M'\<close>
                                                          \<open>is_separator M q'' q' A t2 t1\<close> \<open>completely_specified M'\<close>]
              \<open>q' \<noteq> q''\<close>
[PROOF STATE]
proof (prove)
using this:
q'' \<noteq> q' \<Longrightarrow> qT \<noteq> qT
q' \<noteq> q''

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

goal (1 subgoal):
 1. pR1 \<notin> R M q q' pP p \<and> pR2 \<notin> R M q q'' pP p \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qT \<noteq> qT
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
qT \<noteq> qT

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
io_targets M' (p_io pR1) (FSM.initial M') \<inter> io_targets M' (p_io pR2) (FSM.initial M') = {}

goal:
No subgoals!
[PROOF STEP]
qed