# Theory Test_Suite_IO

```section ‹Representing Test Suites as Sets of Input-Output Sequences›

text ‹This theory describes the representation of test suites as sets of input-output sequences
and defines a pass relation for this representation.›

theory Test_Suite_IO
imports Test_Suite Maximal_Path_Trie
begin

fun test_suite_to_io :: "('a,'b,'c) fsm ⇒ ('a,'b,'c,'d) test_suite ⇒ ('b × 'c) list set" where
"test_suite_to_io M (Test_Suite prs tps rd_targets atcs) =
(⋃ (q,P) ∈ prs . L P)
∪ (⋃{(λ io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . ∃ q P . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q})
∪ (⋃{(λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . ∃ P q' t1 t2 . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q,pt) ∧ (A,t1,t2) ∈ atcs (target q pt,q') })"

lemma test_suite_to_io_language :
assumes "implies_completeness T M m"
shows "(test_suite_to_io M T) ⊆ L M"
proof
fix io assume "io ∈ test_suite_to_io M T"

obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs"
by (meson test_suite.exhaust)

then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
using assms(1) unfolding implies_completeness_def
by blast
then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
unfolding implies_completeness_def
by blast

have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q"
using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def]
by blast

have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)"
using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def]
by assumption

have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q"
using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def]
by assumption

have t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d"
using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def]
by blast

from ‹io ∈ test_suite_to_io M T› consider
(a) "io ∈ (⋃ (q,P) ∈ prs . L P)" |
(b) "io ∈ (⋃{(λ io' . p_io p @ io') ` (set (prefixes (p_io pt))) | p pt . ∃ q P . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q})" |
(c) "io ∈ (⋃{(λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A) | p pt q A . ∃ P q' t1 t2 . (q,P) ∈ prs ∧ path P (initial P) p ∧ target (initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q,pt) ∧ (A,t1,t2) ∈ atcs (target q pt,q') })"
unfolding ‹T = Test_Suite prs tps rd_targets atcs› test_suite_to_io.simps
by blast

then show "io ∈ L M" proof cases
case a
then obtain q P  where "(q, P) ∈ prs" and "io ∈ L P"
by blast

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast

show "io ∈ L M"
using submachine_language[OF ‹is_submachine P M›] ‹io ∈ L P› by blast
next
case b
then obtain p pt q P where "io ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
and "(q,P) ∈ prs"
and "path P (initial P) p"
and "target (initial P) p = q"
and "pt ∈ tps q"
by blast

then obtain io' where "io = p_io p @ io'" and "io' ∈ (set (prefixes (p_io pt)))"
by blast

then obtain io'' where "p_io pt = io' @ io''" and "io = p_io p @ io'"
unfolding prefixes_set
proof -
assume a1: "io' ∈ {xs'. ∃xs''. xs' @ xs'' = p_io pt}"
assume "⋀io''. ⟦p_io pt = io' @ io''; io = p_io p @ io'⟧ ⟹ thesis"
then show ?thesis
using a1 ‹io = p_io p @ io'› by moura
qed

have "q ∈ fst ` prs"
using ‹(q,P) ∈ prs›
by force

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›]
unfolding is_preamble_def
by blast
then have "initial P = initial M"
by auto

have "path M (initial M) p"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) p›]
unfolding ‹initial P = initial M›
by assumption

have "target (initial M) p = q"
using ‹target (initial P) p = q›
unfolding ‹initial P = initial M›
by assumption

obtain p2 d where "(pt @ p2, d) ∈ m_traversal_paths_with_witness M q repetition_sets m"
using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q›
by blast
then have "path M q (pt @ p2)"
using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF ‹path M (initial M) p›], of m]
unfolding ‹target (initial M) p = q›
by blast
then have "path M (initial M) (p@pt)"
using ‹path M (initial M) p› ‹target (initial M) p = q›
by auto
then have "p_io p @ p_io pt ∈ L M"
by (metis (mono_tags, lifting) language_intro map_append)

then show "io ∈ L M"
unfolding ‹io = p_io p @ io'› ‹p_io pt = io' @ io''› append.assoc[symmetric]
using language_prefix[of "p_io p @ io'" io'' M "initial M"]
by blast
next
case c

then obtain p pt q A P q' t1 t2 where "io ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
and   "(q,P) ∈ prs"
and   "path P (initial P) p"
and   "target (initial P) p = q"
and   "pt ∈ tps q"
and   "q' ∈ rd_targets (q,pt)"
and   "(A,t1,t2) ∈ atcs (target q pt,q')"
by blast

obtain ioA where "io = p_io p @ p_io pt @ ioA"
and   "ioA ∈ (atc_to_io_set (from_FSM M (target q pt)) A)"
using ‹io ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)›
by blast
then have "ioA ∈ L (from_FSM M (target q pt))"
unfolding atc_to_io_set.simps by blast

have "q ∈ fst ` prs"
using ‹(q,P) ∈ prs› by force

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast
then have "initial P = initial M" by auto

have "path M (initial M) p"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) p›]
unfolding ‹initial P = initial M›
by assumption
have "target (initial M) p = q"
using ‹target (initial P) p = q›
unfolding ‹initial P = initial M›
by assumption

obtain p2 d where "(pt @ p2, d) ∈ m_traversal_paths_with_witness M q repetition_sets m"
using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q› by blast

then have "path M q (pt @ p2)"
using m_traversal_paths_with_witness_set[OF t5 t8 path_target_is_state[OF ‹path M (initial M) p›], of m]
unfolding ‹target (initial M) p = q›
by blast
then have "path M (initial M) (p@pt)"
using ‹path M (initial M) p› ‹target (initial M) p = q›
by auto
moreover have "(target q pt) = target (initial M) (p@pt)"
using ‹target (initial M) p = q›
by auto
ultimately have "(target q pt) ∈ states M"
using path_target_is_state
by metis

have "ioA ∈ LS M (target q pt)"
using from_FSM_language[OF ‹(target q pt) ∈ states M›] ‹ioA ∈ L (from_FSM M (target q pt))›
by blast
then obtain pA where "path M (target q pt) pA" and "p_io pA = ioA"
by auto
then have "path M (initial M) (p @ pt @ pA)"
using ‹path M (initial M) (p@pt)›  unfolding ‹(target q pt) = target (initial M) (p@pt)›
by auto
then have "p_io p @ p_io pt @ ioA ∈ L M"
unfolding ‹p_io pA = ioA›[symmetric]
using language_intro by fastforce
then show "io ∈ L M"
unfolding ‹io = p_io p @ p_io pt @ ioA›
by assumption
qed
qed

lemma minimal_io_seq_to_failure :
assumes "¬ (L M' ⊆ L M)"
and     "inputs M' = inputs M"
and     "completely_specified M"
obtains io x y y' where "io@[(x,y)] ∈ L M" and "io@[(x,y')] ∉  L M" and "io@[(x,y')] ∈ L M'"
proof -
obtain ioF where "ioF ∈ L M'" and "ioF ∉ L M"
using assms(1) by blast

let ?prefs = "{ioF' ∈ set (prefixes ioF) . ioF' ∈ L M' ∧ ioF' ∉ L M}"
have "finite ?prefs"
using prefixes_finite by auto
moreover have "?prefs ≠ {}"
unfolding prefixes_set using ‹ioF ∈ L M'› ‹ioF ∉ L M› by auto
ultimately obtain ioF' where "ioF' ∈ ?prefs" and "⋀ ioF'' . ioF'' ∈ ?prefs ⟹ length ioF' ≤ length ioF''"
by (meson leI min_length_elem)

then have "ioF' ∈ L M'" and "ioF' ∉ L M"
by auto
then have "ioF' ≠ []"
by auto
then have "ioF' = (butlast ioF')@[last ioF']" and "length (butlast ioF') < length ioF'"
by auto
then have "butlast ioF' ∉ ?prefs"
using ‹⋀ ioF'' . ioF'' ∈ ?prefs ⟹ length ioF' ≤ length ioF''› leD by blast
moreover have "butlast ioF' ∈ L M'"
using ‹ioF' ∈ L M'› language_prefix[of "butlast ioF'" "[last ioF']" M' "initial M'"]
unfolding ‹ioF' = (butlast ioF')@[last ioF']›[symmetric] by blast
moreover have "butlast ioF' ∈ set (prefixes ioF)"
using ‹ioF' = (butlast ioF')@[last ioF']› ‹ioF' ∈ ?prefs› prefixes_set
proof -
have "∃ps. (butlast ioF' @ [last ioF']) @ ps = ioF"
using ‹ioF' = butlast ioF' @ [last ioF']› ‹ioF' ∈ {ioF' ∈ set (prefixes ioF). ioF' ∈ L M' ∧ ioF' ∉ L M}›
unfolding prefixes_set
by auto
then show ?thesis
using prefixes_set by fastforce
qed
ultimately have "butlast ioF' ∈ L M"
by blast

have *: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] ∈ L M'"
using ‹ioF' ∈ L M'› ‹ioF' = (butlast ioF')@[last ioF']› by auto
have **: "(butlast ioF')@[(fst (last ioF'), snd (last ioF'))] ∉ L M"
using ‹ioF' ∉ L M› ‹ioF' = (butlast ioF')@[last ioF']› by auto

obtain p where "path M (initial M) p" and "p_io p = butlast ioF'"
using ‹butlast ioF' ∈ L M› by auto
moreover obtain t where "t ∈ transitions M"
and "t_source t = target (initial M) p"
and "t_input t = fst (last ioF')"
proof -
have "fst (last ioF') ∈ inputs M'"
using language_io(1)[OF *, of "fst (last ioF')" "snd (last ioF')"]
by simp
then have "fst (last ioF') ∈ inputs M"
using assms(2) by auto
then show ?thesis
using that ‹completely_specified M› path_target_is_state[OF ‹path M (initial M) p›]
unfolding completely_specified.simps by blast
qed
ultimately have ***: "(butlast ioF')@[(fst (last ioF'), t_output t)] ∈ L M"
proof -
have "p_io (p @ [t]) ∈ L M"
by (metis (no_types) ‹path M (FSM.initial M) p› ‹t ∈ FSM.transitions M› ‹t_source t = target (FSM.initial M) p›
language_intro path_append single_transition_path)
then show ?thesis
by (simp add: ‹p_io p = butlast ioF'› ‹t_input t = fst (last ioF')›)
qed

show ?thesis
using that[OF *** ** *]
by assumption
qed

lemma observable_minimal_path_to_failure :
assumes "¬ (L M' ⊆ L M)"
and     "observable M"
and     "observable M'"
and     "inputs M' = inputs M"
and     "completely_specified M"
and     "completely_specified M'"
obtains p p' t t' where "path M (initial M) (p@[t])"
and   "path M' (initial M') (p'@[t'])"
and   "p_io p' = p_io p"
and   "t_input t' = t_input t"
and   "¬(∃ t'' . t'' ∈ transitions M ∧ t_source t'' = target (initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t')"
proof -

obtain io x y y' where "io@[(x,y)] ∈ L M" and "io@[(x,y')] ∉  L M" and "io@[(x,y')] ∈ L M'"
using minimal_io_seq_to_failure[OF assms(1,4,5)] by blast

obtain p t where "path M (initial M) (p@[t])" and "p_io p = io" and "t_input t = x" and "t_output t = y"
using language_append_path_ob[OF ‹io@[(x,y)] ∈ L M›] by blast

moreover obtain p' t' where "path M' (initial M') (p'@[t'])" and "p_io p' = io" and "t_input t' = x" and "t_output t' = y'"
using language_append_path_ob[OF ‹io@[(x,y')] ∈ L M'›] by blast

moreover have "¬(∃ t'' . t'' ∈ transitions M ∧ t_source t'' = target (initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t')"
proof
assume "∃t''. t'' ∈ FSM.transitions M ∧ t_source t'' = target (FSM.initial M) p ∧ t_input t'' = t_input t ∧ t_output t'' = t_output t'"
then obtain t'' where "t'' ∈ FSM.transitions M" and "t_source t'' = target (FSM.initial M) p" and "t_input t'' = x" and "t_output t'' = y'"
unfolding ‹t_input t = x› ‹t_output t' = y'› by blast

then have "path M (initial M) (p@[t''])"
using ‹path M (initial M) (p@[t])›
by (meson path_append_elim path_append_transition)
moreover have "p_io (p@[t'']) = io@[(x,y')]"
using ‹p_io p = io› ‹t_input t'' = x› ‹t_output t'' = y'› by auto
ultimately have "io@[(x,y')] ∈ L M"
using language_state_containment
by (metis (mono_tags, lifting))
then show "False"
using ‹io@[(x,y')] ∉ L M› by blast
qed

ultimately show ?thesis using that[of p t p' t']
by force
qed

lemma test_suite_to_io_pass :
assumes "implies_completeness T M m"
and     "observable M"
and     "observable M'"
and     "inputs M' = inputs M"
and     "inputs M ≠ {}"
and     "completely_specified M"
and     "completely_specified M'"
shows "pass_io_set M' (test_suite_to_io M T) = passes_test_suite M T M'"
proof -
obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs"
by (meson test_suite.exhaust)
then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
using assms(1) unfolding implies_completeness_def by blast
then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
unfolding implies_completeness_def by blast
then have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⊆ L M"
using test_suite_to_io_language by blast

have t1: "(initial M, initial_preamble M) ∈ prs"
using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def]
by assumption
have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q"
using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def]
by blast
have t3: "⋀ q1 q2 A d1 d2. (A, d1, d2) ∈ atcs (q1, q2) ⟹ (A, d2, d1) ∈ atcs (q2, q1) ∧ is_separator M q1 q2 A d1 d2"
using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def]
by assumption

have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)"
using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def]
by assumption

have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q"
using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def]
by assumption

have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M"
and  t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d"
and  t8':  "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` prs"
and  t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}"
using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def]
by blast+

have "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs)) ⟹ passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'"
proof -
assume "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))"

then have pass_io_prop: "⋀ io x y y' . io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⟹ io @ [(x, y')] ∈ L M' ⟹ io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding pass_io_set_def
by blast

show "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'"
proof (rule ccontr)
assume "¬ passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'"

then consider (a) "¬ (∀q P io x y y'. (q, P) ∈ prs ⟶ io @ [(x, y)] ∈ L P ⟶ io @ [(x, y')] ∈ L M' ⟶ io @ [(x, y')] ∈ L P)" |
(b) "¬ ((∀q P pP ioT pT x y y'.
(q, P) ∈ prs ⟶
path P (FSM.initial P) pP ⟶
target (FSM.initial P) pP = q ⟶
pT ∈ tps q ⟶
ioT @ [(x, y)] ∈ set (prefixes (p_io pT)) ⟶
p_io pP @ ioT @ [(x, y')] ∈ L M' ⟶ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))))" |
(c) "¬ ((∀q P pP pT.
(q, P) ∈ prs ⟶
path P (FSM.initial P) pP ⟶
target (FSM.initial P) pP = q ⟶
pT ∈ tps q ⟶
p_io pP @ p_io pT ∈ L M' ⟶
(∀q' A d1 d2 qT.
q' ∈ rd_targets (q, pT) ⟶
(A, d1, d2) ∈ atcs (target q pT, q') ⟶ qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M') ⟶ pass_separator_ATC M' A qT d2)))"
unfolding passes_test_suite.simps by blast
then show False proof cases
case a
then obtain q P io x y y' where "(q, P) ∈ prs"
and "io @ [(x, y)] ∈ L P"
and "io @ [(x, y')] ∈ L M'"
and "io @ [(x, y')] ∉ L P"
by blast

have "is_preamble P M q"
using t2[OF ‹(q, P) ∈ prs›] by assumption

have "io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps using ‹(q, P) ∈ prs› ‹io @ [(x, y)] ∈ L P›
by fastforce

have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
using pass_io_prop[OF ‹io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› ‹io @ [(x, y')] ∈ L M'›]
by assumption

then have "io @ [(x, y')] ∈ L M"
using test_suite_language_prop
by blast

have "io @ [(x, y')] ∈ L P"
using passes_test_suite_soundness_helper_1[OF ‹is_preamble P M q› ‹observable M› ‹io @ [(x, y)] ∈ L P› ‹io @ [(x, y')] ∈ L M›]
by assumption
then show "False"
using ‹io @ [(x, y')] ∉ L P›
by blast

next
case b
then obtain q P pP ioT pT x y y' where "(q, P) ∈ prs"
and "path P (FSM.initial P) pP"
and "target (FSM.initial P) pP = q"
and "pT ∈ tps q"
and "ioT @ [(x, y)] ∈ set (prefixes (p_io pT))"
and "p_io pP @ ioT @ [(x, y')] ∈ L M'"
and "¬ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))"
by blast

have "∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pT ∈ tps q"
using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pT ∈ tps q› by blast
moreover have "p_io pP @ ioT @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pT))"
using ‹ioT @ [(x, y)] ∈ set (prefixes (p_io pT))› by auto
ultimately have "p_io pP @ ioT @ [(x, y)] ∈ (⋃{(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})"
by blast
then have "p_io pP @ ioT @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps
by blast
then have *: "(p_io pP @ ioT) @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
by auto

have **: "(p_io pP @ ioT) @ [(x, y')] ∈ L M'"
using ‹p_io pP @ ioT @ [(x, y')] ∈ L M'› by auto

have "(p_io pP @ ioT) @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
using pass_io_prop[OF * ** ] by assumption
then have "(p_io pP @ ioT) @ [(x, y')] ∈ L M"
using test_suite_language_prop by blast

have "q ∈ states M"
using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]] by assumption

have "q ∈ fst ` prs"
using ‹(q, P) ∈ prs› by force

obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q› by blast

then have "path M q (pT @ pT')"
and  "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pT @ pT'))) repetition_sets = Some d'"
and  "⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m]
by blast+

obtain ioT' where "p_io pT = ioT @ [(x,y)] @ ioT'"
using prefixes_set_ob[OF ‹ioT @ [(x, y)] ∈ set (prefixes (p_io pT))›]
unfolding prefixes_set append.assoc[symmetric]
by blast

let ?pt = "take (length (ioT @ [(x,y)])) pT"
let ?p  = "butlast ?pt"
let ?t  = "last ?pt"

have "length ?pt > 0"
using ‹p_io pT = ioT @ [(x,y)] @ ioT'›
unfolding length_map[of "(λ t . (t_input t, t_output t))", symmetric]
by auto
then have "?pt = ?p @ [?t]"
by auto
moreover have "path M q ?pt"
using ‹path M q (pT @ pT')›
by (meson path_prefix path_prefix_take)
ultimately have "path M q (?p@[?t])"
by simp

have "p_io ?p = ioT"
proof -
have "p_io ?pt = take (length (ioT @ [(x,y)])) (p_io pT)"
then have "p_io ?pt = ioT @ [(x,y)]"
using ‹p_io pT = ioT @ [(x,y)] @ ioT'› by auto
then show ?thesis
qed

have "path M q ?p"
using path_append_transition_elim[OF ‹path M q (?p@[?t])›] by blast

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast
then have "initial P = initial M" by auto

have "path M (initial M) pP"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›]
unfolding ‹initial P = initial M›
by assumption
moreover have "target (initial M) pP = q"
using ‹target (initial P) pP = q›
unfolding ‹initial P = initial M›
by assumption
ultimately have "path M (initial M) (pP@?p)"
using ‹path M q ?p›
by auto

have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) repetition_sets = None"
proof -
have *: "(pT @ pT') = ?p @ ([?t] @ (drop (length (ioT @ [(x,y)])) pT) @ pT')"
using ‹?pt = ?p @ [?t]›
by (metis append_assoc append_take_drop_id)
have **: "([?t] @ (drop (length (ioT @ [(x,y)])) pT) @ pT') ≠ []"
by simp
show ?thesis
using ‹⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None›[OF * **]
by assumption
qed

(* obtain paths from the transition ending in y' to get a transition from ?p *)
obtain p' t' where "path M (FSM.initial M) (p' @ [t'])" and "p_io p' = p_io pP @ ioT" and "t_input t' = x" and "t_output t' = y'"
using language_append_path_ob[OF ‹(p_io pP @ ioT) @ [(x, y')] ∈ L M›] by blast
then have "path M (FSM.initial M) p'" and "t_source t' = target (initial M) p'" and "t' ∈ transitions M"
by auto

have "p' = pP @ ?p"
using observable_path_unique[OF ‹observable M› ‹path M (FSM.initial M) p'› ‹path M (initial M) (pP@?p)›]
‹p_io ?p = ioT›
unfolding ‹p_io p' = p_io pP @ ioT›
by simp
then have "t_source t' = target q ?p"
unfolding ‹t_source t' = target (initial M) p'› using ‹target (initial M) pP = q›
by auto

obtain pTt' dt' where "(?p @ [t'] @ pTt', dt') ∈ m_traversal_paths_with_witness M q repetition_sets m"
using m_traversal_path_extension_exist_for_transition[OF ‹completely_specified M› ‹q ∈ states M› ‹FSM.inputs M ≠ {}›
t5 t8 ‹path M q ?p› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) repetition_sets = None›
‹t' ∈ transitions M› ‹t_source t' = target q ?p›]
by blast

have "?p @ [t'] @ pTt' ∈ tps q"
using t6[OF ‹q ∈ fst ` prs› ] ‹(?p @ [t'] @ pTt', dt') ∈ m_traversal_paths_with_witness M q repetition_sets m›
by force
moreover have "ioT @ [(x, y')] ∈ set (prefixes (p_io (?p @ [t'] @ pTt')))"
proof -
have "p_io (?p @ [t'] @ pTt') = ioT @ [(x,y')] @ p_io pTt'"
using ‹p_io ?p = ioT› using ‹t_input t' = x› ‹t_output t' = y'›
by auto
then show ?thesis
unfolding prefixes_set
by force
qed

ultimately show "False"
using ‹¬ (∃pT'. pT' ∈ tps q ∧ ioT @ [(x, y')] ∈ set (prefixes (p_io pT')))›
by blast
next
case c

then obtain q P pP pT q' A d1 d2 qT  where "(q, P) ∈ prs"
and   "path P (FSM.initial P) pP"
and   "target (FSM.initial P) pP = q"
and   "pT ∈ tps q"
and   "p_io pP @ p_io pT ∈ L M'"
and   "q' ∈ rd_targets (q, pT)"
and   "(A, d1, d2) ∈ atcs (target q pT, q')"
and   "qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')"
and   "¬pass_separator_ATC M' A qT d2"
by blast

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›]
unfolding is_preamble_def
by blast
then have "initial P = initial M" by auto

have "path M (initial M) pP"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›]
unfolding ‹initial P = initial M›
by assumption
have "target (initial M) pP = q"
using ‹target (initial P) pP = q›
unfolding ‹initial P = initial M›
by assumption

have "q ∈ states M"
using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]]
by assumption

have "q ∈ fst ` prs"
using ‹(q, P) ∈ prs› by force

obtain pT' d' where "(pT @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
using t6[OF ‹q ∈ fst ` prs›] ‹pT ∈ tps q› by blast

then have "path M q (pT @ pT')"
and  "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pT @ pT'))) repetition_sets = Some d'"
and  "⋀ p' p''. (pT @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m]
by blast+
then have "path M q pT"
by auto

have "qT ∈ states M'"
using ‹qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')› io_targets_states subset_iff
by fastforce

have "is_separator M (target q pT) q' A d1 d2"
using  t3[OF ‹(A, d1, d2) ∈ atcs (target q pT, q')›] by blast

have "¬ pass_io_set (FSM.from_FSM M' qT) (atc_to_io_set (FSM.from_FSM M (target q pT)) A)"
using ‹¬pass_separator_ATC M' A qT d2›
pass_separator_pass_io_set_iff[OF ‹is_separator M (target q pT) q' A d1 d2› ‹observable M›
‹observable M'› path_target_is_state[OF ‹path M q pT›]
‹qT ∈ states M'› ‹inputs M' = inputs M› ‹completely_specified M›]
by simp

have "pass_io_set (FSM.from_FSM M' qT) (atc_to_io_set (FSM.from_FSM M (target q pT)) A)"
proof -
have "⋀ io x y y' . io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A ⟹
io @ [(x, y')] ∈ L (FSM.from_FSM M' qT) ⟹
io @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A"
proof -
fix io x y y' assume "io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A"
and    "io @ [(x, y')] ∈ L (FSM.from_FSM M' qT)"

(* subsets of test_suite_to_io *)
define tmp where tmp_def : "tmp = (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})"
define tmp2 where tmp2_def : "tmp2 = ⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}"
have "∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pT ∈ tps q ∧ q' ∈ rd_targets (q, pT) ∧ (A, t1, t2) ∈ atcs (target q pT, q')"
using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pT ∈ tps q› ‹q' ∈ rd_targets (q, pT)› ‹(A, d1, d2) ∈ atcs (target q pT, q')› by blast
then have "(λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A ⊆ tmp"
unfolding tmp_def by blast
then have "(λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A ⊆ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps tmp_def[symmetric] tmp2_def[symmetric] by blast
moreover have "(p_io pP @ p_io pT @ (io @ [(x, y)])) ∈ (λio_atc. p_io pP @ p_io pT @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pT)) A"
using ‹io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A› by auto
ultimately have "(p_io pP @ p_io pT @ (io @ [(x, y)])) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
by blast
then have *: "(p_io pP @ p_io pT @ io) @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
by simp

have "io @ [(x, y')] ∈ LS M' qT"
using ‹io @ [(x, y')] ∈ L (FSM.from_FSM M' qT)› ‹qT ∈ states M'›
by (metis from_FSM_language)
have **: "(p_io pP @ p_io pT @ io) @ [(x, y')] ∈ L M'"
using io_targets_language_append[OF ‹qT ∈ io_targets M' (p_io pP @ p_io pT) (FSM.initial M')› ‹io @ [(x, y')] ∈ LS M' qT›]
by simp

have "(p_io pP @ p_io pT) @ (io @ [(x, y')]) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
using pass_io_prop[OF * ** ] by simp
then have "(p_io pP @ p_io pT) @ (io @ [(x, y')]) ∈ L M"
using test_suite_language_prop by blast

moreover have "target q pT ∈ io_targets M (p_io pP @ p_io pT) (initial M)"
proof -
have "target (initial M) (pP@pT) = target q pT"
unfolding ‹target (initial M) pP = q›[symmetric] by auto
moreover have "path M (initial M) (pP@pT)"
using ‹path M (initial M) pP› ‹path M q pT› unfolding ‹target (initial M) pP = q›[symmetric]
by auto
moreover have "p_io (pP@pT) = (p_io pP @ p_io pT)"
by auto
ultimately show ?thesis
unfolding io_targets.simps
by (metis (mono_tags, lifting) mem_Collect_eq)
qed

ultimately have "io @ [(x, y')] ∈ LS M (target q pT)"
using observable_io_targets_language[OF _ ‹observable M›, of "(p_io pP @ p_io pT)" "(io @ [(x, y')])" "initial M" "target q pT"]
by blast
then have "io @ [(x, y')] ∈ L (FSM.from_FSM M (target q pT))"
unfolding from_FSM_language[OF path_target_is_state[OF ‹path M q pT›]]
by assumption

moreover have "io @ [(x, y')] ∈ L A"
by (metis Int_iff ‹io @ [(x, y')] ∈ LS M (target q pT)› ‹io @ [(x, y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A›
‹is_separator M (target q pT) q' A d1 d2› atc_to_io_set.simps is_separator_simps(9))

ultimately show "io @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pT)) A"
unfolding atc_to_io_set.simps by blast
qed

then show ?thesis unfolding pass_io_set_def by blast
qed

then show "False"
using pass_separator_from_pass_io_set[OF ‹is_separator M (target q pT) q' A d1 d2› _ ‹observable M›
‹observable M'› path_target_is_state[OF ‹path M q pT›]
‹qT ∈ states M'› ‹inputs M' = inputs M› ‹completely_specified M›]
‹¬pass_separator_ATC M' A qT d2›
by simp
qed
qed
qed

moreover have "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M' ⟹ pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))"
proof -
assume "passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'"

(* pass properties *)

have pass1: "⋀ q P io x y y' . (q,P) ∈ prs ⟹ io@[(x,y)] ∈ L P ⟹ io@[(x,y')] ∈ L M' ⟹ io@[(x,y')] ∈ L P"
using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'›
unfolding passes_test_suite.simps
by meson

have pass2: "⋀ q P pP ioT pT x y y' . (q,P) ∈ prs ⟹ path P (initial P) pP ⟹ target (initial P) pP = q ⟹ pT ∈ tps q ⟹ ioT@[(x,y)] ∈ set (prefixes (p_io pT)) ⟹ (p_io pP)@ioT@[(x,y')] ∈ L M' ⟹ (∃ pT' . pT' ∈ tps q ∧ ioT@[(x,y')] ∈ set (prefixes (p_io pT')))"
using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'›
unfolding passes_test_suite.simps by blast

have pass3: "⋀ q P pP pT q' A d1 d2 qT . (q,P) ∈ prs ⟹ path P (initial P) pP ⟹ target (initial P) pP = q ⟹ pT ∈ tps q ⟹ (p_io pP)@(p_io pT) ∈ L M' ⟹ q' ∈ rd_targets (q,pT) ⟹ (A,d1,d2) ∈ atcs (target q pT, q') ⟹ qT ∈ io_targets M' ((p_io pP)@(p_io pT)) (initial M') ⟹ pass_separator_ATC M' A qT d2"
using ‹passes_test_suite M (Test_Suite prs tps rd_targets atcs) M'›
unfolding passes_test_suite.simps by blast

show "pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))"
proof (rule ccontr)
assume "¬ pass_io_set M' (test_suite_to_io M (Test_Suite prs tps rd_targets atcs))"
then obtain io x y y' where "io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
and   "io @ [(x, y')] ∈ L M'"
and   "io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding pass_io_set_def by blast

have preamble_prop: "⋀ q P . (q, P) ∈ prs ⟹ io @ [(x, y)] ∈ L P ⟹ False"
proof -
fix q P assume "(q, P)∈prs" and "io @ [(x, y)] ∈ L P"
have "io @ [(x, y')] ∈ L P" using pass1[OF ‹(q, P)∈prs› ‹io @ [(x, y)] ∈ L P› ‹io @ [(x, y')] ∈ L M'› ]
by assumption
then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps using ‹(q, P)∈prs› by blast
then show "False" using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)›
by simp
qed

have traversal_path_prop : "⋀ pP pt q P .  io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt)) ⟹ (q, P) ∈ prs ⟹ path P (FSM.initial P) pP ⟹ target (FSM.initial P) pP = q ⟹ pt ∈ tps q ⟹ False"
proof -
fix pP pt q P assume "io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))"
and   "(q, P) ∈ prs"
and   "path P (FSM.initial P) pP"
and   "target (FSM.initial P) pP = q"
and   "pt ∈ tps q"

obtain io' io'' where "io @ [(x, y)] = (p_io pP) @ io'" and "io'@io'' = p_io pt"
using ‹io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))›
unfolding prefixes_set
by blast

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›]
unfolding is_preamble_def
by blast
then have "initial P = initial M"
by auto

have "path M (initial M) pP"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›]
unfolding ‹initial P = initial M›
by assumption
have "target (initial M) pP = q"
using ‹target (initial P) pP = q›
unfolding ‹initial P = initial M›
by assumption

have "q ∈ states M"
using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]]
by assumption

have "q ∈ fst ` prs"
using ‹(q, P) ∈ prs› by force

show "False" proof (cases io' rule: rev_cases)
case Nil
then have "p_io pP = io @ [(x, y)]"
using ‹io @ [(x, y)] = (p_io pP) @ io'›
by auto
show ?thesis
using preamble_prop[OF ‹(q,P) ∈ prs› language_state_containment[OF ‹path P (FSM.initial P) pP› ‹p_io pP = io @ [(x, y)]›]]
by assumption
next
case (snoc ioI xy)
then have "xy = (x,y)" and "io = (p_io pP) @ ioI"
using ‹io @ [(x, y)] = (p_io pP) @ io'› by auto
then have "p_io pP @ ioI @ [(x, y')] ∈ L M'"
using ‹io @ [(x, y')] ∈ L M'› by simp

have "ioI @ [(x, y)] ∈ set (prefixes (p_io pt))"
unfolding prefixes_set
using ‹io' @ io'' = p_io pt› ‹xy = (x, y)› snoc
by auto

obtain pT' where "pT' ∈ tps q" and "ioI @ [(x, y')] ∈ set (prefixes (p_io pT'))"
using pass2[OF ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q›
‹ioI @ [(x, y)] ∈ set (prefixes (p_io pt))› ‹p_io pP @ ioI @ [(x, y')] ∈ L M'›] by blast

have "io @ [(x, y')] ∈ (@) (p_io pP) ` set (prefixes (p_io pT'))"
using ‹ioI @ [(x, y')] ∈ set (prefixes (p_io pT'))›
unfolding ‹io = (p_io pP) @ ioI›
by simp

have "io @ [(x, y')] ∈ (⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})"
using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q›
‹pT' ∈ tps q› ‹io @ [(x, y')] ∈ (@) (p_io pP) ` set (prefixes (p_io pT'))›
by blast
then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps
by blast

then show "False"
using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)›
by blast
qed
qed

consider (a) "io @ [(x, y)] ∈ (⋃(q, P)∈prs. L P)" |
(b) "io @ [(x, y)] ∈ (⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q})" |
(c) "io @ [(x, y)] ∈ (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A.
∃P q' t1 t2.
(q, P) ∈ prs ∧
path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})"
using ‹io @ [(x, y)] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)›
unfolding test_suite_to_io.simps by blast

then show "False" proof cases
case a
then show ?thesis using preamble_prop by blast
next
case b
then show ?thesis using traversal_path_prop by blast
next
case c

then obtain pP pt q A P q' t1 t2 where "io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A"
and "(q, P) ∈ prs"
and "path P (FSM.initial P) pP"
and "target (FSM.initial P) pP = q"
and "pt ∈ tps q"
and "q' ∈ rd_targets (q, pt)"
and "(A, t1, t2) ∈ atcs (target q pt, q')"
by blast

obtain ioA where "io @ [(x, y)] = p_io pP @ p_io pt @ ioA"
using ‹io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A›
unfolding prefixes_set
by blast

show "False" proof (cases ioA rule: rev_cases)
case Nil
then have "io @ [(x, y)] = p_io pP @ p_io pt"
using ‹io @ [(x, y)] = p_io pP @ p_io pt @ ioA› by simp
then have "io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))"
unfolding prefixes_set by blast
show ?thesis
using traversal_path_prop[OF ‹io @ [(x, y)] ∈ (@) (p_io pP) ` set (prefixes (p_io pt))› ‹(q, P) ∈ prs›
‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q›]
by assumption
next
case (snoc ioAI xy)
then have "xy = (x,y)" and "io = p_io pP @ p_io pt @ ioAI"
using ‹io @ [(x, y)] = p_io pP @ p_io pt @ ioA› by simp+
then have "p_io pP @ p_io pt @ ioAI @ [(x,y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A"
using ‹io @ [(x, y)] ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A›
by auto
then have "ioAI @ [(x,y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A"
by auto

have "p_io pP @ p_io pt ∈ L M'"
using ‹io @ [(x,y')] ∈ L M'› language_prefix[of "p_io pP @ p_io pt" "ioAI @ [(x, y')]" M' "initial M'"]
unfolding ‹io = p_io pP @ p_io pt @ ioAI›
by simp
then obtain pt' where "path M' (initial M') pt'" and "p_io pt' = p_io pP @ p_io pt"
by auto
then have  "target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')"
by fastforce

have "pass_separator_ATC M' A (target (FSM.initial M') pt') t2"
using pass3[OF ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q›
‹p_io pP @ p_io pt ∈ L M'› ‹q' ∈ rd_targets (q, pt)› ‹(A, t1, t2) ∈ atcs (target q pt, q')›
‹target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')›]
by assumption

have "is_separator M (target q pt) q' A t1 t2"
using  t3[OF ‹(A, t1, t2) ∈ atcs (target q pt, q')›] by blast

have "is_submachine P M"
using t2[OF ‹(q, P) ∈ prs›] unfolding is_preamble_def by blast
then have "initial P = initial M" by auto

have "path M (initial M) pP"
using submachine_path[OF ‹is_submachine P M› ‹path P (initial P) pP›]
unfolding ‹initial P = initial M›
by assumption
have "target (initial M) pP = q"
using ‹target (initial P) pP = q›
unfolding ‹initial P = initial M›
by assumption

have "q ∈ states M"
using is_preamble_is_state[OF t2[OF ‹(q, P) ∈ prs›]]
by assumption

have "q ∈ fst ` prs"
using ‹(q, P) ∈ prs› by force

obtain pT' d' where "(pt @ pT', d') ∈ m_traversal_paths_with_witness M q repetition_sets m"
using t6[OF ‹q ∈ fst ` prs›] ‹pt ∈ tps q›
by blast

then have "path M q (pt @ pT')"
and  "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (pt @ pT'))) repetition_sets = Some d'"
and  "⋀ p' p''. (pt @ pT') = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repetition_sets = None"
using m_traversal_paths_with_witness_set[OF t5 t8 ‹q ∈ states M›, of m]
by blast+
then have "path M q pt"
by auto

have "target (initial M') pt' ∈ states M'"
using ‹target (initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')› io_targets_states
using subset_iff
by fastforce

have "pass_io_set (FSM.from_FSM M' (target (FSM.initial M') pt')) (atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
using  pass_io_set_from_pass_separator[OF ‹is_separator M (target q pt) q' A t1 t2›
‹pass_separator_ATC M' A (target (FSM.initial M') pt') t2›
‹observable M› ‹observable M'› path_target_is_state[OF ‹path M q pt›]
‹target (FSM.initial M') pt' ∈ FSM.states M'› ‹inputs M' = inputs M›]
by assumption
moreover note ‹ioAI @ [(x,y)] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A›
moreover have "ioAI @ [(x, y')] ∈ L (FSM.from_FSM M' (target (FSM.initial M') pt'))"
using ‹io @ [(x,y')] ∈ L M'›   unfolding ‹io = p_io pP @ p_io pt @ ioAI›
by (metis (no_types, lifting) ‹target (FSM.initial M') pt' ∈ FSM.states M'›
‹target (FSM.initial M') pt' ∈ io_targets M' (p_io pP @ p_io pt) (FSM.initial M')›
append_assoc assms(3) from_FSM_language observable_io_targets_language)

ultimately have "ioAI @ [(x,y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A"
unfolding pass_io_set_def by blast

(* subsets of test_suite_to_io *)
define tmp where tmp_def : "tmp = (⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A. ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')})"
define tmp2 where tmp2_def : "tmp2 = ⋃ {(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}"
have "∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) pP ∧ target (FSM.initial P) pP = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')"
using ‹(q, P) ∈ prs› ‹path P (FSM.initial P) pP› ‹target (FSM.initial P) pP = q› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q, pt)› ‹(A, t1, t2) ∈ atcs (target q pt, q')› by blast
then have "(λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A ⊆ tmp"
unfolding tmp_def by blast
then have "(λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A ⊆ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding test_suite_to_io.simps tmp_def[symmetric] tmp2_def[symmetric] by blast
moreover have "(p_io pP @ p_io pt @ (ioAI @ [(x, y')])) ∈ (λio_atc. p_io pP @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A"
using ‹ioAI @ [(x, y')] ∈ atc_to_io_set (FSM.from_FSM M (target q pt)) A› by auto
ultimately have "(p_io pP @ p_io pt @ (ioAI @ [(x, y')])) ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
by blast
then have "io @ [(x, y')] ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
unfolding ‹io = p_io pP @ p_io pt @ ioAI› by auto
then show "False"
using ‹io @ [(x, y')] ∉ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)›
by blast
qed
qed
qed
qed

ultimately show ?thesis
unfolding ‹T = Test_Suite prs tps rd_targets atcs›
by blast
qed

lemma test_suite_to_io_finite :
assumes "implies_completeness T M m"
and     "is_finite_test_suite T"
shows "finite (test_suite_to_io M T)"
proof -
obtain prs tps rd_targets atcs where "T = Test_Suite prs tps rd_targets atcs"
by (meson test_suite.exhaust)
then obtain repetition_sets where repetition_sets_def: "implies_completeness_for_repetition_sets (Test_Suite prs tps rd_targets atcs) M m repetition_sets"
using assms(1)
unfolding implies_completeness_def
by blast
then have "implies_completeness (Test_Suite prs tps rd_targets atcs) M m"
unfolding implies_completeness_def
by blast
then have test_suite_language_prop: "test_suite_to_io M (Test_Suite prs tps rd_targets atcs) ⊆ L M"
using test_suite_to_io_language
by blast

have f1: "(finite prs)"
and  f2: "⋀ q p . q ∈ fst ` prs ⟹ finite (rd_targets (q,p))"
and  f3: "⋀ q q' . finite (atcs (q,q'))"
using assms(2)
unfolding ‹T = Test_Suite prs tps rd_targets atcs› is_finite_test_suite.simps
by blast+

have t1: "(initial M, initial_preamble M) ∈ prs"
using implies_completeness_for_repetition_sets_simps(1)[OF repetition_sets_def]
by assumption
have t2: "⋀ q P. (q, P) ∈ prs ⟹ is_preamble P M q"
using implies_completeness_for_repetition_sets_simps(2)[OF repetition_sets_def]
by blast
have t3: "⋀ q1 q2 A d1 d2. (A, d1, d2) ∈ atcs (q1, q2) ⟹ (A, d2, d1) ∈ atcs (q2, q1) ∧ is_separator M q1 q2 A d1 d2"
using implies_completeness_for_repetition_sets_simps(3)[OF repetition_sets_def]
by assumption

have t5: "⋀q. q ∈ FSM.states M ⟹ (∃d∈set repetition_sets. q ∈ fst d)"
using implies_completeness_for_repetition_sets_simps(4)[OF repetition_sets_def]
by assumption

have t6: "⋀ q. q ∈ fst ` prs ⟹ tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ∧ fst ` (m_traversal_paths_with_witness M q repetition_sets m) ⊆ tps q"
using implies_completeness_for_repetition_sets_simps(7)[OF repetition_sets_def]
by assumption

have t7: "⋀ d. d ∈ set repetition_sets ⟹ fst d ⊆ FSM.states M"
and  t8: "⋀ d. d ∈ set repetition_sets ⟹ snd d ⊆ fst d"
and  t8':  "⋀ d. d ∈ set repetition_sets ⟹ snd d = fst d ∩ fst ` prs"
and  t9: "⋀ d q1 q2. d ∈ set repetition_sets ⟹ q1 ∈ fst d ⟹ q2 ∈ fst d ⟹ q1 ≠ q2 ⟹ atcs (q1, q2) ≠ {}"
using implies_completeness_for_repetition_sets_simps(5,6)[OF repetition_sets_def]
by blast+

have f4: "⋀ q . q ∈ fst ` prs ⟹ finite (tps q)"
proof -
fix q assume "q ∈ fst ` prs"
then have "tps q ⊆ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m}"
using t6 by blast
moreover have "{p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m} ⊆ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
proof
fix p1 assume "p1 ∈ {p1 . ∃ p2 d . (p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m}"
then obtain p2 d where "(p1@p2,d) ∈ m_traversal_paths_with_witness M q repetition_sets m" by blast
then have "p1@p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m" by force
moreover have "p1 ∈ set (prefixes (p1@p2))" unfolding prefixes_set by blast
ultimately show "p1 ∈ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))" by blast
qed
ultimately have "tps q ⊆ (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
by simp
moreover have "finite (⋃ p2 ∈ fst ` m_traversal_paths_with_witness M q repetition_sets m . set (prefixes p2))"
proof -
have "finite (fst ` m_traversal_paths_with_witness M q repetition_sets m)"
using m_traversal_paths_with_witness_finite[of M q repetition_sets m] by auto
moreover have "⋀ p2 . finite (set (prefixes p2))" by auto
ultimately show ?thesis by blast
qed
ultimately show "finite (tps q)"
using finite_subset by blast
qed
then have f4' : "⋀ q P . (q,P) ∈ prs ⟹ finite (tps q)"
by force

define T1 where T1_def : "T1 = (⋃(q, P)∈prs. L P)"
define T2 where T2_def : "T2 = ⋃{(@) (p_io p) ` set (prefixes (p_io pt)) |p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}"
define T3 where T3_def : "T3 = ⋃ {(λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A |p pt q A.
∃P q' t1 t2.
(q, P) ∈ prs ∧
path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}"

have "test_suite_to_io M T = T1 ∪ T2 ∪ T3"
unfolding ‹T = Test_Suite prs tps rd_targets atcs› test_suite_to_io.simps T1_def T2_def T3_def by simp

moreover have "finite T1"
proof -
have "⋀ q P . (q, P)∈prs ⟹ finite (L P)"
proof -
fix q P assume "(q, P)∈prs"
have "acyclic P"
using t2[OF ‹(q, P)∈prs›]
unfolding is_preamble_def
by blast
then show "finite (L P)"
using acyclic_alt_def
by blast
qed
then show ?thesis using f1 unfolding T1_def
by auto
qed

moreover have "finite T2"
proof -
have *: "T2 = (⋃ (p,pt) ∈ {(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q} . ((@) (p_io p) ` set (prefixes (p_io pt))))"
unfolding T2_def
by auto

have "⋀ p pt . finite ((@) (p_io p) ` set (prefixes (p_io pt)))"
by auto
moreover have "finite {(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q}"
proof -
have "{(p,pt) | p pt. ∃q P. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q} ⊆ (⋃ (q,P) ∈ prs . {p . path P (initial P) p} × (tps q))"
by auto
moreover have "finite (⋃ (q,P) ∈ prs . {p . path P (initial P) p} × (tps q))"
proof -
note ‹finite prs›
moreover have "⋀ q P . (q,P) ∈ prs ⟹ finite ({p . path P (initial P) p} × (tps q))"
proof -
fix q P assume "(q,P) ∈ prs"

have "acyclic P" using t2[OF ‹(q, P)∈prs›]
unfolding is_preamble_def
by blast
then have "finite {p . path P (initial P) p}"
using acyclic_paths_finite[of P "initial P"]
unfolding acyclic.simps
by (metis (no_types, lifting) Collect_cong)
then show "finite ({p . path P (initial P) p} × (tps q))"
using f4'[OF ‹(q,P) ∈ prs›]
by simp
qed
ultimately show ?thesis
by force
qed
ultimately show ?thesis
by (meson rev_finite_subset)
qed
ultimately show ?thesis
unfolding * by auto
qed

moreover have "finite T3"
proof -
have scheme: "⋀ f P . (⋃ {f a b c d | a b c d . P a b c d}) = (⋃ (a,b,c,d) ∈ {(a,b,c,d) | a b c d . P a b c d} . f a b c d)"
by blast

have *: "T3 = (⋃ (p,pt,q,A) ∈ {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}
. (λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
unfolding T3_def scheme by blast

have "{(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}
⊆ (⋃ (q,P) ∈ prs . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
by blast
moreover have "finite (⋃ (q,P) ∈ prs . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
proof -
note ‹finite prs›
moreover have "⋀ q P . (q,P) ∈ prs ⟹ finite (⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
proof -
fix q P assume "(q,P) ∈ prs"
then have "q ∈ fst ` prs" by force

have "finite (tps q)" using f4'[OF ‹(q,P) ∈ prs›] by assumption
moreover have "⋀ pt . pt ∈ tps q ⟹ finite (⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
proof -
fix pt assume "pt ∈ tps q"

have "finite (rd_targets (q,pt))" using f2[OF ‹q ∈ fst ` prs›] by blast
moreover have "⋀ q' . q' ∈ rd_targets (q, pt) ⟹ finite (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A})"
proof -
fix q' assume "q' ∈ rd_targets (q, pt)"
have "finite (atcs (target q pt, q'))" using f3 by blast
moreover have "finite {p . path P (initial P) p}"
proof -
have "acyclic P" using t2[OF ‹(q, P)∈prs›] unfolding is_preamble_def by blast
then show ?thesis using acyclic_paths_finite[of P "initial P"] unfolding acyclic.simps by (metis (no_types, lifting) Collect_cong)
qed
ultimately show "finite (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A})"
by force
qed
ultimately show "finite (⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
by force
qed
ultimately show "finite (⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q, pt) . (⋃ (A, t1, t2) ∈ atcs (target q pt, q') . {p . path P (initial P) p} × {pt} × {q} × {A}))"
by force
qed
ultimately show ?thesis by force
qed
ultimately have "finite {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}"
by (meson rev_finite_subset)

moreover have "⋀ p pt q A . (p,pt,q,A) ∈ {(p, pt, q, A) | p pt q A . ∃P q' t1 t2. (q, P) ∈ prs ∧ path P (FSM.initial P) p ∧ target (FSM.initial P) p = q ∧ pt ```