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  (dset 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  (dset 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  (dset 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 (