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 using ‹io' ∈ set (prefixes (p_io pt))› prefixes_set_ob 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
    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)"
            by (simp add: take_map) 
          then have "p_io ?pt = ioT @ [(x,y)]"
            using ‹p_io pT = ioT @ [(x,y)] @ ioT'› by auto
          then show ?thesis
            by (simp add: map_butlast) 
        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 ∈ tps q ∧ q' ∈ rd_targets (q, pt) ∧ (A, t1, t2) ∈ atcs (target q pt, q')}
                       ⟹ finite ((λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
    proof -
      fix p pt q A assume "(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')}"
      then obtain P q' t1 t2 where "(q, P) ∈ prs" and "path P (FSM.initial P) p" and "target (FSM.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

      have "is_separator M (target q pt) q' A t1 t2"
        using t3[OF ‹(A, t1, t2) ∈ atcs (target q pt, q')›] by blast
      then have "acyclic A"
        using is_separator_simps(2) by simp
      then have "finite (L A)"
        unfolding acyclic_alt_def by assumption
      then have "finite (atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
        unfolding atc_to_io_set.simps by blast
      then show "finite ((λio_atc. p_io p @ p_io pt @ io_atc) ` atc_to_io_set (FSM.from_FSM M (target q pt)) A)"
        by blast
    qed

    ultimately show ?thesis unfolding * by force
  qed

  ultimately show ?thesis
    by simp 
qed



subsection ‹Calculating the Sets of Sequences›


abbreviation "L_acyclic M ≡ LS_acyclic M (initial M)"

(* collect the prefix-closed IO-sequence representation of a test suite for some reference FSM *)
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_acyclic P 
          ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . 
              ⋃ pt ∈ tps q . 
                ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) 
                ∪ (⋃ q' ∈ rd_targets (q,pt) . 
                    ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . 
                      (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))))"


lemma test_suite_to_io_code :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"  
  and     "observable M"
shows "test_suite_to_io M T = 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

  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 test_suite_to_io'_alt_def: "test_suite_to_io' M T  
    = (⋃ (q,P) ∈ prs . L_acyclic P)
      ∪ (⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt))))) 
      ∪ (⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
    unfolding test_suite_to_io'.simps ‹T = Test_Suite prs tps rd_targets atcs› 
    by fast

  have test_suite_to_io_alt_def: "test_suite_to_io M T =
    (⋃ (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') })"
    unfolding ‹T = Test_Suite prs tps rd_targets atcs› test_suite_to_io.simps
    by force


  have preamble_language_prop: "⋀ q P . (q,P) ∈ prs ⟹ L_acyclic P = 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 "L_acyclic P = L P" using LS_from_LS_acyclic by blast
  qed

  have preamble_path_prop: "⋀ q P ioP . (q,P) ∈ prs ⟹ ioP ∈ remove_proper_prefixes (L_acyclic P) ⟷ (∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP)"
  proof -
    fix q P ioP assume "(q,P) ∈ prs"
    have "is_preamble P M q" using t2[OF ‹(q, P)∈prs›] by assumption

    have "ioP ∈ remove_proper_prefixes (L_acyclic P) ⟹ (∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP)"
    proof -
      assume "ioP ∈ remove_proper_prefixes (L_acyclic P)"
      then have "ioP ∈ L P"  and "∄x'. x' ≠ [] ∧ ioP @ x' ∈ L P"
        unfolding preamble_language_prop[OF ‹(q,P) ∈ prs›] remove_proper_prefixes_def by blast+
      show "(∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP)"
        using preamble_maximal_io_paths_rev[OF ‹is_preamble P M q› ‹observable M› ‹ioP ∈ L P› ‹∄x'. x' ≠ [] ∧ ioP @ x' ∈ L P›] by blast
    qed
    moreover have "(∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP) ⟹ ioP ∈ remove_proper_prefixes (L_acyclic P)"
    proof -
      assume "(∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP)"
      then obtain p where "path P (initial P) p" and "target (initial P) p = q" and "p_io p = ioP"
        by blast
      then have "∄io'. io' ≠ [] ∧ p_io p @ io' ∈ L P"
        using preamble_maximal_io_paths[OF ‹is_preamble P M q› ‹observable M›] by blast
      then show "ioP ∈ remove_proper_prefixes (L_acyclic P)"
        using language_state_containment[OF ‹path P (initial P) p› ‹p_io p = ioP›] unfolding preamble_language_prop[OF ‹(q,P) ∈ prs›] remove_proper_prefixes_def ‹p_io p = ioP› by blast
    qed
    ultimately show "ioP ∈ remove_proper_prefixes (L_acyclic P) ⟷ (∃ p . path P (initial P) p ∧ target (initial P) p = q ∧ p_io p = ioP)"
      by blast
  qed
    

  have eq1: "(⋃ (q,P) ∈ prs . L_acyclic P) = (⋃ (q,P) ∈ prs . L P)"
    using preamble_language_prop by blast

  have eq2: "(⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt))))) = (⋃{(λ 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})"
  proof 
    show "(⋃(q, P)∈prs. ⋃ioP∈remove_proper_prefixes (L_acyclic P). ⋃pt∈tps q. (@) ioP ` set (prefixes (p_io pt))) ⊆ ⋃ {(@) (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}"
    proof 
      fix io assume "io ∈ (⋃ (q,P) ∈ prs . (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt))))))"
      then obtain q P where "(q,P) ∈ prs"
                      and   "io ∈ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))))"
        by blast
      then obtain ioP where "ioP ∈ remove_proper_prefixes (L_acyclic P)"
                      and   "io ∈ (⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))))"
        by blast

      obtain p where "path P (initial P) p" and "target (initial P) p = q" and "ioP = p_io p"
        using preamble_path_prop[OF ‹(q,P) ∈ prs›, of ioP] ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› by auto 

      obtain pt where "pt ∈ tps q" and "io ∈ ((λ io' . p_io p @ io') ` (set (prefixes (p_io pt))))"
        using ‹io ∈ (⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))))› unfolding ‹ioP = p_io p› by blast
      
      show "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})"
        using ‹io ∈ ((λ io' . p_io p @ io') ` (set (prefixes (p_io pt))))› ‹(q,P) ∈ prs› ‹path P (initial P) p› ‹target (initial P) p = q› ‹pt ∈ tps q› by blast
    qed

    show "⋃ {(@) (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} ⊆ (⋃(q, P)∈prs. ⋃ioP∈remove_proper_prefixes (L_acyclic P). ⋃pt∈tps q. (@) ioP ` set (prefixes (p_io pt)))"
    proof 
      fix io assume "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})"
      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 ioP where "ioP ∈ remove_proper_prefixes (L_acyclic P)"
                      and   "p_io p = ioP"
        using preamble_path_prop[OF ‹(q,P) ∈ prs›, of "p_io p"] by blast
      
      
      show "io ∈ (⋃ (q,P) ∈ prs . (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt))))))"
        using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› ‹io ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))›  unfolding ‹p_io p = ioP› by blast
    qed
  qed

  have eq3: "(⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)) = (⋃{(λ 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') })"
  proof
    show "(⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)) ⊆ (⋃{(λ 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') })"    
    proof 
      fix io assume "io ∈ (⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
      then obtain q P ioP pt q' A t1 t2 where "(q,P) ∈ prs" 
                                        and   "ioP ∈ remove_proper_prefixes (L_acyclic P)"
                                        and   "pt ∈ tps q"
                                        and   "q' ∈ rd_targets (q,pt)"
                                        and   "(A,t1,t2) ∈ atcs (target q pt,q')"
                                        and   "io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)"
        by blast

      obtain p where "path P (initial P) p" and "target (initial P) p = q" and "ioP = p_io p"
        using preamble_path_prop[OF ‹(q,P) ∈ prs›, of ioP] ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› by auto 

      have "acyclic A"
        using t3[OF ‹(A,t1,t2) ∈ atcs (target q pt,q')›] is_separator_simps(2) by metis
      have "(acyclic_language_intersection (from_FSM M (target q pt)) A) = (atc_to_io_set (from_FSM M (target q pt)) A)"
        unfolding acyclic_language_intersection_completeness[OF ‹acyclic A›] atc_to_io_set.simps by simp
      have "io ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
        using ‹io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)› unfolding ‹(acyclic_language_intersection (from_FSM M (target q pt)) A) = (atc_to_io_set (from_FSM M (target q pt)) A)› ‹ioP = p_io p› by simp

      then show "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') })"
        using ‹(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')› by blast
    qed

    show "(⋃{(λ 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') }) ⊆ (⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
    proof 
      fix io assume "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') })"
      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

      then obtain ioP where "ioP ∈ remove_proper_prefixes (L_acyclic P)"
                      and   "p_io p = ioP"
        using preamble_path_prop[OF ‹(q,P) ∈ prs›, of "p_io p"] by blast


      have "acyclic A"
        using t3[OF ‹(A,t1,t2) ∈ atcs (target q pt,q')›] is_separator_simps(2) by metis
      have *: "(atc_to_io_set (from_FSM M (target q pt)) A) = (acyclic_language_intersection (from_FSM M (target q pt)) A)"
        unfolding acyclic_language_intersection_completeness[OF ‹acyclic A›] atc_to_io_set.simps by simp
      have "io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (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)› unfolding * ‹p_io p = ioP› by simp

      then show "io ∈ (⋃ (q,P) ∈ prs . ⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
        using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q,pt)› ‹(A,t1,t2) ∈ atcs (target q pt,q')› by force
    qed
  qed

  show ?thesis
    unfolding test_suite_to_io'_alt_def test_suite_to_io_alt_def eq1 eq2 eq3 by simp
qed
  








subsection ‹Using Maximal Sequences Only›



fun test_suite_to_io_maximal :: "('a::linorder,'b::linorder,'c) fsm ⇒ ('a,'b,'c,'d::linorder) test_suite ⇒ ('b × 'c) list set" where
  "test_suite_to_io_maximal M (Test_Suite prs tps rd_targets atcs) = 
      remove_proper_prefixes (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))))"


lemma test_suite_to_io_maximal_code : 
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"  
  and     "observable M"
shows  "{io' ∈ (test_suite_to_io M T) . ¬ (∃ io'' . io'' ≠ [] ∧ io'@io'' ∈ (test_suite_to_io M T))} = test_suite_to_io_maximal M T"
proof -

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

  have t_def: "test_suite_to_io M T = test_suite_to_io' M T"
    using test_suite_to_io_code[OF assms] by assumption

  have t1_def : "test_suite_to_io' M T = (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
    unfolding ‹T = Test_Suite prs tps rd_targets atcs› by simp

  define tmax where tmax_def: "tmax = (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))))"
  have t2_def : "test_suite_to_io_maximal M T = remove_proper_prefixes tmax"
    unfolding ‹T = Test_Suite prs tps rd_targets atcs› tmax_def by simp

  have tmax_sub: "tmax ⊆ (test_suite_to_io M T)"
    unfolding tmax_def t_def t1_def
  proof 
    fix io assume "io ∈ (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))))"
    then obtain q P where "(q,P) ∈ prs"
                    and   "io ∈ L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
      by force
    then consider (a) "io ∈ L_acyclic P" |
                  (b) "io ∈ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
      by blast
    then show "io ∈ (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
    proof cases
      case a
      then show ?thesis using ‹(q,P) ∈ prs› by blast
    next
      case b
      then obtain ioP pt where "ioP ∈ remove_proper_prefixes (L_acyclic P)" 
                         and   "pt ∈ tps q"
                         and   "io ∈ Set.insert (ioP @ p_io pt) (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))"
        by blast
      then consider (b1) "io = (ioP @ p_io pt)" |
                    (b2) "io ∈ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A)))"
        by blast
      then show ?thesis proof cases
        case b1
        then have "io ∈ ((λ io' . ioP @ io') ` (set (prefixes (p_io pt))))" unfolding prefixes_set by blast
        then show ?thesis using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› by blast
      next
        case b2
        then obtain q' A t1 t2 where "q' ∈ rd_targets (q,pt)"
                               and   "(A,t1,t2) ∈ atcs (target q pt,q')"
                               and   "io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))"
          by blast
        then have "io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)"
          unfolding remove_proper_prefixes_def by blast
        then show ?thesis using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q,pt)› ‹(A,t1,t2) ∈ atcs (target q pt,q')› by force
      qed 
    qed
  qed


  have tmax_max: "⋀ io . io ∈ test_suite_to_io M T ⟹ io ∉ tmax ⟹ ∃ io'' . io'' ≠ [] ∧ io@io'' ∈ (test_suite_to_io M T)"
  proof -
    fix io assume "io ∈ test_suite_to_io M T" and "io ∉ tmax"

    then have "io ∈ (⋃ (q,P) ∈ prs . L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
      unfolding t_def t1_def by blast
    then obtain q P where "(q,P) ∈ prs"
                    and   "io ∈ (L_acyclic P ∪ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))))"
      by force
    then consider (a) "io ∈ L_acyclic P" |
                  (b) "io ∈ (⋃ ioP ∈ remove_proper_prefixes (L_acyclic P) . ⋃ pt ∈ tps q . ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)))"
      by blast
    then show "∃ io'' . io'' ≠ [] ∧ io@io'' ∈ (test_suite_to_io M T)" proof cases
      case a
      then have "io ∈ tmax"
        using ‹(q,P) ∈ prs› unfolding tmax_def by blast
      then show ?thesis 
        using ‹io ∉ tmax› by simp
    next
      case b
      then obtain ioP pt where "ioP ∈ remove_proper_prefixes (L_acyclic P)"
                         and   "pt ∈ tps q"
                         and   "io ∈ ((λ io' . ioP @ io') ` (set (prefixes (p_io pt)))) ∪ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
        by blast
      then consider (b1) "io ∈ (λ io' . ioP @ io') ` (set (prefixes (p_io pt)))" |
                    (b2) "io ∈ (⋃ q' ∈ rd_targets (q,pt) . ⋃ (A,t1,t2) ∈ atcs (target q pt,q') . (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A))"
        by blast
      then show ?thesis proof cases
        case b1
        then obtain pt1 pt2 where "io = ioP @ pt1" and "p_io pt = pt1@pt2"
          by (metis (no_types, lifting) b1 image_iff prefixes_set_ob) 

        have "ioP @ (p_io pt) ∈ tmax"
          using ‹io ∉ tmax› ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› unfolding tmax_def by force
        then have "io ≠ ioP @ (p_io pt)"
          using ‹io ∉ tmax› by blast
        then have "pt2 ≠ []" 
          using ‹io = ioP @ pt1› unfolding ‹p_io pt = pt1@pt2› by auto

        have "ioP @ (p_io pt) ∈ test_suite_to_io M T"
          using ‹ioP @ (p_io pt) ∈ tmax› tmax_sub by blast
        then show ?thesis 
          unfolding ‹io = ioP @ pt1› append.assoc ‹p_io pt = pt1@pt2›
          using ‹pt2 ≠ []› by blast
      next
        case b2
        then obtain q' A t1 t2 where "q' ∈ rd_targets (q,pt)"
                               and   "(A,t1,t2) ∈ atcs (target q pt,q')"
                               and   "io ∈ (λ io_atc . ioP @ p_io pt @ io_atc) ` (acyclic_language_intersection (from_FSM M (target q pt)) A)"
          by blast

        then obtain ioA where "io = ioP @ p_io pt @ ioA" 
                        and   "ioA ∈ acyclic_language_intersection (from_FSM M (target q pt)) A"
          by blast

        moreover have "ioA ∉ (remove_proper_prefixes (acyclic_language_intersection (from_FSM M (target q pt)) A))"
        proof 
          assume "ioA ∈ remove_proper_prefixes (acyclic_language_intersection (FSM.from_FSM M (target q pt)) A)"
          then have "io ∈ tmax"
            using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q,pt)› ‹(A,t1,t2) ∈ atcs (target q pt,q')› unfolding tmax_def ‹io = ioP @ p_io pt @ ioA› by force
          then show False
            using ‹io ∉ tmax› by simp
        qed
        ultimately obtain ioA2 where "ioA @ ioA2 ∈ acyclic_language_intersection (from_FSM M (target q pt)) A" 
                               and   "ioA2 ≠ []"
          unfolding remove_proper_prefixes_def by blast
        then have "io@ioA2 ∈ test_suite_to_io M T"
          using ‹(q,P) ∈ prs› ‹ioP ∈ remove_proper_prefixes (L_acyclic P)› ‹pt ∈ tps q› ‹q' ∈ rd_targets (q,pt)› ‹(A,t1,t2) ∈ atcs (target q pt,q')› ‹ioA @ ioA2 ∈ acyclic_language_intersection (from_FSM M (target q pt)) A› unfolding t_def t1_def ‹io = ioP @ p_io pt @ ioA› by force
        
        then show ?thesis 
          using ‹ioA2 ≠ []› by blast
      qed
    qed 
  qed


  show ?thesis unfolding t2_def
  proof 
    show "{io' ∈ test_suite_to_io M T. ∄io''. io'' ≠ [] ∧ io' @ io'' ∈ test_suite_to_io M T} ⊆ remove_proper_prefixes tmax"
    proof 
      fix io assume "io ∈ {io' ∈ test_suite_to_io M T. ∄io''. io'' ≠ [] ∧ io' @ io'' ∈ test_suite_to_io M T}"
      then have "io ∈ test_suite_to_io M T" and "∄io''. io'' ≠ [] ∧ io @ io'' ∈ test_suite_to_io M T" 
        by blast+
      show "io ∈ remove_proper_prefixes tmax"
        using ‹∄io''. io'' ≠ [] ∧ io @ io'' ∈ test_suite_to_io M T›
        using tmax_sub tmax_max[OF ‹io ∈ test_suite_to_io M T›] unfolding remove_proper_prefixes_def
        by auto 
    qed
    show "remove_proper_prefixes tmax ⊆ {io' ∈ test_suite_to_io M T. ∄io''. io'' ≠ [] ∧ io' @ io'' ∈ test_suite_to_io M T}"
    proof 
      fix io assume "io ∈ remove_proper_prefixes tmax"
      then have "io ∈ tmax" and "∄io''. io'' ≠ [] ∧ io @ io'' ∈ remove_proper_prefixes tmax"
        unfolding remove_proper_prefixes_def by blast+
      then have "io ∈ test_suite_to_io M T"
        using tmax_sub by blast
      moreover have "∄io''. io'' ≠ [] ∧ io @ io'' ∈ test_suite_to_io M T"
      proof 
        assume "∃io''. io'' ≠ [] ∧ io @ io'' ∈ test_suite_to_io M T"
        then obtain io'' where "io'' ≠ []" and "io @ io'' ∈ test_suite_to_io M T"
          by blast
        then obtain io''' where "(io @ io'') @ io''' ∈ test_suite_to_io M T" 
                          and   "(∄zs. zs ≠ [] ∧ (io @ io'') @ io''' @ zs ∈ test_suite_to_io M T)"
          using finite_set_elem_maximal_extension_ex[OF ‹io @ io'' ∈ test_suite_to_io M T› test_suite_to_io_finite[OF assms(1,2)]] by blast

        have "io @ (io'' @ io''') ∈ tmax"
          using tmax_max[OF ‹(io @ io'') @ io''' ∈ test_suite_to_io M T›] ‹(∄zs. zs ≠ [] ∧ (io @ io'') @ io''' @ zs ∈ test_suite_to_io M T)› by force
        moreover have "io''@io''' ≠ []"
          using ‹io'' ≠ []› by auto

        ultimately show "False" 
          using ‹∄io''. io'' ≠ [] ∧ io @ io'' ∈ remove_proper_prefixes tmax› 
          by (metis (mono_tags, lifting) ‹io ∈ remove_proper_prefixes tmax› mem_Collect_eq remove_proper_prefixes_def) 
      qed
          

      ultimately show "io ∈ {io' ∈ test_suite_to_io M T. ∄io''. io'' ≠ [] ∧ io' @ io'' ∈ test_suite_to_io M T}"
        by blast
    qed
  qed
qed


lemma test_suite_to_io_pass_maximal :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"  
shows "pass_io_set M' (test_suite_to_io M T) = pass_io_set_maximal M' {io' ∈ (test_suite_to_io M T) . ¬ (∃ io'' . io'' ≠ [] ∧ io'@io'' ∈ (test_suite_to_io M T))}"
proof -

  (* finiteness *)
  have p1: "finite (test_suite_to_io M T)"
    using test_suite_to_io_finite[OF assms] by assumption

  (* prefix closure *)
  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 p2: "⋀io' io''. io' @ io'' ∈ test_suite_to_io M T ⟹ io' ∈ test_suite_to_io M T"
    unfolding ‹T = Test_Suite prs tps rd_targets atcs›
  proof -
    fix io' io'' assume "io' @ io'' ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"

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

    have traversal_path_prop : "⋀ io''' p pt q P . io'@io''' ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt))) ⟹ (q,P) ∈ prs ⟹ path P (initial P) p ⟹ target (initial P) p = q ⟹ pt ∈ tps q ⟹ io' ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
    proof - 
      fix io''' p pt q P assume "io'@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"

      obtain ioP1 where "io'@io''' = p_io p @ ioP1" and "ioP1 ∈ (set (prefixes (p_io pt)))"
        using ‹io'@io''' ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))› by auto
      then obtain ioP2 where "ioP1 @ ioP2 = p_io pt"
         unfolding prefixes_set by blast


      show "io' ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)"
      proof (cases "length io' ≤ length (p_io p)")
        case True
        then have "io' = (take (length io') (p_io p))"
          using ‹io'@io''' = p_io p @ ioP1›
          by (metis (no_types, lifting) order_refl take_all take_le) 
        then have "p_io p = io'@(drop (length io') (p_io p))"
          by (metis (no_types, lifting) append_take_drop_id)
        then have "io'@(drop (length io') (p_io p)) ∈ L P"
          using language_state_containment[OF ‹path P (initial P) p›] by blast
        then show ?thesis 
          using preamble_prop[OF ‹(q,P) ∈ prs›] by blast
      next
        case False
        then have "io' = p_io p @ (take (length io' - length (p_io p)) ioP1)"
          using ‹io'@io''' = p_io p @ ioP1›
          by (metis (no_types, lifting) le_cases take_all take_append take_le) 
        moreover have "(take (length io' - length (p_io p)) ioP1) ∈ (set (prefixes (p_io pt)))"
        proof -
          have "ioP1 = (take (length io' - length (p_io p)) ioP1) @ (drop (length io' - length (p_io p)) ioP1)"
            by auto
          then have "(take (length io' - length (p_io p)) ioP1) @ ((drop (length io' - length (p_io p)) ioP1) @ ioP2) = p_io pt"
            using ‹ioP1 @ ioP2 = p_io pt› by (metis (mono_tags, lifting) append_assoc) 
          then show ?thesis
            unfolding prefixes_set by blast
        qed
        ultimately have "io' ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
          by blast
        then have "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})"
          using ‹(q,P) ∈ prs› ‹path P (initial P) p› ‹target (initial P) p = q› ‹pt ∈ tps q› by blast
        then show ?thesis 
          unfolding test_suite_to_io.simps by blast          
      qed
    qed


    from ‹io' @ io'' ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)› consider
      (a) "io' @ io'' ∈ (⋃ (q,P) ∈ prs . L P)" |
      (b) "io' @ 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'' ∈ (⋃{(λ 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 test_suite_to_io.simps
      by blast

    then show "io' ∈ test_suite_to_io M (Test_Suite prs tps rd_targets atcs)" 
    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 p pt q A  P q' t1 t2  where "io' @ 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' @ io'' = p_io p @ p_io pt @ ioA" 
                   and "ioA ∈ (atc_to_io_set (from_FSM M (target q pt)) A)"
        using ‹io' @ io'' ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)› 
        by blast


      show ?thesis proof (cases "length io' ≤ length (p_io p @ p_io pt)")
        case True
        then have "io' @ (drop (length io') (p_io p @ p_io pt)) = p_io p @ p_io pt"
          using ‹io' @ io'' = p_io p @ p_io pt @ ioA›
          by (simp add: append_eq_conv_conj) 
        moreover have "p_io p @ p_io pt ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
          unfolding prefixes_set by blast
        ultimately have "io'@(drop (length io') (p_io p @ p_io pt)) ∈ (λ io' . p_io p @ io') ` (set (prefixes (p_io pt)))"
          by simp
        then show ?thesis 
          using traversal_path_prop[OF _ ‹(q,P) ∈ prs› ‹path P (initial P) p› ‹target (initial P) p = q› ‹pt ∈ tps q›] by blast
      next
        case False
        then have "io' = (p_io p @ p_io pt) @ (take (length io' - length (p_io p @ p_io pt)) ioA)"
        proof -
          have "io' = take (length io') (io' @ io'')"
            by auto
          then show ?thesis
            using False ‹io' @ io'' = p_io p @ p_io pt @ ioA› by fastforce
        qed
        moreover have "(take (length io' - length (p_io p @ p_io pt)) ioA) ∈ (atc_to_io_set (from_FSM M (target q pt)) A)"
        proof -
          have "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) ∈ L (from_FSM M (target q pt)) ∩ L A"
            using ‹ioA ∈ (atc_to_io_set (from_FSM M (target q pt)) A)› by auto
          then have *: "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) ∈ L (from_FSM M (target q pt))"
               and **: "(take (length io' - length (p_io p @ p_io pt)) ioA)@(drop (length io' - length (p_io p @ p_io pt)) ioA) ∈ L A"
            by blast+
          show ?thesis
            using language_prefix[OF *] language_prefix[OF **]
            unfolding atc_to_io_set.simps by blast
        qed
        ultimately have "io' ∈ (λ io_atc . p_io p @ p_io pt @ io_atc) ` (atc_to_io_set (from_FSM M (target q pt)) A)"
          by force
            
        then have "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') })"
          using ‹(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')› by blast
        then show ?thesis 
          unfolding test_suite_to_io.simps by blast
      qed
    qed
  qed


  then show ?thesis
    using pass_io_set_maximal_from_pass_io_set[OF p1] by blast
qed



lemma passes_test_suite_as_maximal_sequences_completeness :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M" 
  and     "observable M'"
  and     "inputs M' = inputs M"
  and     "inputs M ≠ {}"
  and     "completely_specified M"
  and     "completely_specified M'"
  and     "size M' ≤ m"
shows     "(L M' ⊆ L M) ⟷ pass_io_set_maximal M' (test_suite_to_io_maximal M T)"
  unfolding passes_test_suite_completeness[OF assms(1,3-9)]
  unfolding test_suite_to_io_pass[OF assms(1,3-8),symmetric]
  unfolding test_suite_to_io_pass_maximal[OF assms(1,2)]
  unfolding test_suite_to_io_maximal_code[OF assms(1,2,3)]
  by simp


lemma test_suite_to_io_maximal_finite :
  assumes "implies_completeness T M m"
  and     "is_finite_test_suite T"
  and     "observable M"
shows "finite (test_suite_to_io_maximal M T)"
 using test_suite_to_io_finite[OF assms(1,2)]
 unfolding test_suite_to_io_maximal_code[OF assms, symmetric]
 by simp


end