Theory Test_Suite_Calculation

section ‹Calculating Sufficient Test Suites›

text ‹This theory describes algorithms to calculate test suites that satisfy the sufficiency
      criterion for a given specification FSM and upper bound m on the number of states in the
      System Under Test.›

theory Test_Suite_Calculation
imports Test_Suite_IO
begin

subsection ‹Calculating Path Prefixes that are to be Extended With Adaptive Cest Cases›

subsubsection ‹Calculating Tests along m-Traversal-Paths›

fun prefix_pair_tests :: "'a  (('a,'b,'c) traversal_path × ('a set × 'a set)) set  ('a × ('a,'b,'c) traversal_path × 'a) set" where
  "prefix_pair_tests q pds 
    = {{(q,p1,(target q p2)), (q,p2,(target q p1))} | p1 p2 . 
           (p,(rd,dr))  pds .  
              (p1,p2)  set (prefix_pairs p)  
              (target q p1)  rd  
              (target q p2)  rd  
              (target q p1)  (target q p2)}"

lemma prefix_pair_tests_code[code] :
  "prefix_pair_tests q pds = ((image (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) pds))"
proof -
  have " tp . tp  prefix_pair_tests q pds  tp  ((image (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) pds))"
  proof -
    fix tp assume "tp  prefix_pair_tests q pds"
    then obtain tps where "tp  tps"
                    and   "tps  {{(q,p1,(target q p2)), (q,p2,(target q p1))} | p1 p2 .  (p,(rd,dr))  pds . (p1,p2)  set (prefix_pairs p)  (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)}"
      unfolding prefix_pair_tests.simps
      by (meson UnionE) 
    then obtain p1 p2 where "tps = {(q,p1,(target q p2)), (q,p2,(target q p1))}"
                      and   " (p,(rd,dr))  pds . (p1,p2)  set (prefix_pairs p)  (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)"
      unfolding mem_Collect_eq by blast

    then obtain p rd dr where "(p,(rd,dr))  pds" and "(p1,p2)  set (prefix_pairs p)" and "(target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)"
      by blast

    have scheme : " f x xs . x  set xs  f x  set (map f xs)" 
      by auto

    have "(p1,p2)  set (filter (λ(p1, p2). target q p1  rd  target q p2  rd  target q p1  target q p2) (prefix_pairs p))"
      using (p1,p2)  set (prefix_pairs p)
            (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2) 
      by auto
    have "{(q,p1,(target q p2)), (q,p2,(target q p1))}  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))"
      using scheme[OF (p1,p2)  set (filter (λ(p1, p2). target q p1  rd  target q p2  rd  target q p1  target q p2) (prefix_pairs p)), of "(λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))})"] 
      by simp

    then show "tp  ((image (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) pds))"
      using tp  tps (p,(rd,dr))  pds
      unfolding tps = {(q,p1,(target q p2)), (q,p2,(target q p1))} 
      by blast
  qed
  moreover have " tp . tp  ((image (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) pds))
                         tp  prefix_pair_tests q pds"
  proof -
    fix tp assume "tp  ((image (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) pds))"
    then obtain prddr where "prddr  pds"
                        and "tp  (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) prddr"
      by blast
    then obtain p rd dr where "prddr = (p,(rd,dr))" by auto

    then have "tp   (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))"
      using tp  (λ (p,(rd,dr)) .  (set (map (λ (p1,p2) . {(q,p1,(target q p2)), (q,p2,(target q p1))}) (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))))) prddr by auto

    then obtain p1 p2 where "(p1,p2)  set (filter (λ (p1,p2) . (target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)) (prefix_pairs p))"
                      and   "tp  {(q,p1,(target q p2)), (q,p2,(target q p1))}" 
      by auto
    then have "(target q p1)  rd  (target q p2)  rd  (target q p1)  (target q p2)" 
         and  "(p1,p2)  set (prefix_pairs p)"
      by auto

    then show "tp  prefix_pair_tests q pds"
      using prddr  pds tp  {(q,p1,(target q p2)), (q,p2,(target q p1))}
      unfolding prefix_pair_tests.simps  prddr = (p,(rd,dr)) 
      by blast
  qed
  ultimately show ?thesis 
    by blast
qed





subsubsection ‹Calculating Tests between Preambles›


fun preamble_prefix_tests' :: "'a  (('a,'b,'c) traversal_path × ('a set × 'a set)) list  'a list  ('a × ('a,'b,'c) traversal_path × 'a) list" where
  "preamble_prefix_tests' q pds drs = 
    concat (map (λ((p,(rd,dr)),q2,p1) . [(q,p1,q2), (q2,[],(target q p1))]) 
                (filter (λ((p,(rd,dr)),q2,p1) . (target q p1)  rd  q2  rd  (target q p1)  q2) 
                        (concat (map (λ((p,(rd,dr)),q2) . map (λp1 . ((p,(rd,dr)),q2,p1)) (prefixes p)) (List.product pds drs)))))"


definition preamble_prefix_tests :: "'a  (('a,'b,'c) traversal_path × ('a set × 'a set)) set  'a set  ('a × ('a,'b,'c) traversal_path × 'a) set" where
  "preamble_prefix_tests q pds drs = {{(q,p1,q2), (q2,[],(target q p1))} | p1 q2 .  (p,(rd,dr))  pds . q2  drs  ( p2 . p = p1@p2)  (target q p1)  rd  q2  rd  (target q p1)  q2}"

lemma preamble_prefix_tests_code[code] :
  "preamble_prefix_tests q pds drs = ((image (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) pds))"
proof -
  have " pp . pp  preamble_prefix_tests q pds drs  pp  ((image (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) pds))"  
  proof -
    fix pp assume "pp  preamble_prefix_tests q pds drs"
    then obtain p1 q2 where "pp  {(q,p1,q2), (q2,[],(target q p1))}"
                      and   " (p,(rd,dr))  pds . q2  drs  ( p2 . p = p1@p2)  (target q p1)  rd  q2  rd  (target q p1)  q2"
      unfolding preamble_prefix_tests_def by blast
    then obtain p rd dr where "(p,(rd,dr))  pds" and "q2  drs" and "( p2 . p = p1@p2)" and "(target q p1)  rd  q2  rd  (target q p1)  q2"
      by auto

    then have "(p1,q2)  (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs))"
      unfolding prefixes_set by force
    then show "pp  ((image (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) pds))"
      using (p,(rd,dr))  pds
            pp  {(q,p1,q2), (q2,[],(target q p1))} by blast
  qed
  moreover have " pp . pp  ((image (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) pds))
                          pp  preamble_prefix_tests q pds drs"
  proof -
    fix pp assume "pp  ((image (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) pds))"
    then obtain prddr where "prddr  pds"
                      and   "pp  (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) prddr"
      by blast

    obtain p rd dr where "prddr = (p,(rd,dr))"
      using prod_cases3 by blast 

    obtain p1 q2 where "(p1,q2)  (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs))"
                 and   "pp  {(q,p1,q2), (q2,[],(target q p1))}"
      using pp  (λ (p,(rd,dr)) . (image (λ (p1,q2) . {(q,p1,q2), (q2,[],(target q p1))}) (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs)))) prddr
      unfolding prddr = (p,(rd,dr)) 
      by blast

    have "q2  drs  ( p2 . p = p1@p2)  (target q p1)  rd  q2  rd  (target q p1)  q2"
      using (p1,q2)  (Set.filter (λ (p1,q2) . (target q p1)  rd  q2  rd  (target q p1)  q2) ((set (prefixes p)) × drs))
      unfolding prefixes_set 
      by auto
    then have "(p, rd, dr)pds. q2  drs  (p2. p = p1 @ p2)  target q p1  rd  q2  rd  target q p1  q2"
      using prddr  pds prddr = (p,(rd,dr)) 
      by blast
    then have *: "{(q,p1,q2), (q2,[],(target q p1))}  {{(q, p1, q2), (q2, [], target q p1)} |p1 q2.
             (p, rd, dr)pds. q2  drs  (p2. p = p1 @ p2)  target q p1  rd  q2  rd  target q p1  q2}" by blast

    show "pp  preamble_prefix_tests q pds drs"
      using UnionI[OF * pp  {(q,p1,q2), (q2,[],(target q p1))}]
      unfolding preamble_prefix_tests_def by assumption
  qed
  ultimately show ?thesis by blast
qed



subsubsection "Calculating Tests between m-Traversal-Paths Prefixes and Preambles"

fun preamble_pair_tests :: "'a set set  ('a × 'a) set  ('a × ('a,'b,'c) traversal_path × 'a) set" where
  "preamble_pair_tests drss rds = ( drs  drss . (λ (q1,q2) . (q1,[],q2)) ` ((drs × drs)  rds))"





subsection ‹Calculating a Test Suite›


definition calculate_test_paths ::
  "('a,'b,'c) fsm
   nat
   'a set
   ('a × 'a) set
   ('a set × 'a set) list
   (('a  ('a,'b,'c) traversal_path set) × (('a × ('a,'b,'c) traversal_path)  'a set))" 
  where
  "calculate_test_paths M m d_reachable_states r_distinguishable_pairs repetition_sets =
    (let
         paths_with_witnesses 
              = (image (λ q . (q,m_traversal_paths_with_witness M q repetition_sets m)) d_reachable_states);
         get_paths                        
              = m2f (set_as_map paths_with_witnesses);
         PrefixPairTests                    
              =  q  d_reachable_states .  mrsps  get_paths q . prefix_pair_tests q mrsps;
         PreamblePrefixTests
              =  q  d_reachable_states .  mrsps  get_paths q . preamble_prefix_tests q mrsps d_reachable_states;
         PreamblePairTests
              = preamble_pair_tests ( (q,pw)  paths_with_witnesses . ((λ (p,(rd,dr)) . dr) ` pw)) r_distinguishable_pairs;
         tests
              = PrefixPairTests  PreamblePrefixTests  PreamblePairTests; 
         tps'  
              = m2f_by  (set_as_map (image (λ (q,p) . (q, image fst p)) paths_with_witnesses));
         tps''  
              = m2f (set_as_map (image (λ (q,p,q') . (q,p)) tests));
         tps  
              = (λ q . tps' q  tps'' q);
         rd_targets 
              = m2f (set_as_map (image (λ (q,p,q') . ((q,p),q')) tests))    
  in 
    ( tps, rd_targets ))"


definition combine_test_suite ::
  "('a,'b,'c) fsm
   nat
   ('a × ('a,'b,'c) preamble) set
   (('a × 'a) × (('d,'b,'c) separator × 'd × 'd)) set
   ('a set × 'a set) list
   ('a,'b,'c,'d) test_suite" 
  where
  "combine_test_suite M m states_with_preambles pairs_with_separators repetition_sets =
    (let drs = image fst states_with_preambles;
        rds = image fst pairs_with_separators;
        tps_and_targets = calculate_test_paths M m drs rds repetition_sets;
        atcs = m2f (set_as_map pairs_with_separators) 
in (Test_Suite states_with_preambles (fst tps_and_targets) (snd tps_and_targets) atcs))"




definition calculate_test_suite_for_repetition_sets :: 
  "('a::linorder,'b::linorder,'c) fsm  nat  ('a set × 'a set) list  ('a,'b,'c, ('a × 'a) + 'a) test_suite" 
  where
  "calculate_test_suite_for_repetition_sets M m repetition_sets = 
    (let
         states_with_preambles = d_reachable_states_with_preambles M;
         pairs_with_separators = image (λ((q1,q2),A) . ((q1,q2),A,Inr q1,Inr q2)) (r_distinguishable_state_pairs_with_separators M)
  in combine_test_suite M m states_with_preambles pairs_with_separators repetition_sets)"




subsection ‹Sufficiency of the Calculated Test Suite›

lemma calculate_test_suite_for_repetition_sets_sufficient_and_finite :
  fixes M :: "('a::linorder,'b::linorder,'c) fsm"
  assumes "observable M"
  and     "completely_specified M"
  and     "inputs M  {}"
  and     "q. q  FSM.states M  dset RepSets. q  fst d"
  and     "d. d  set RepSets  fst d  states M  (snd d = fst d  fst ` d_reachable_states_with_preambles M)" 
  and     " q1 q2 d. d  set RepSets  q1fst d  q2fst d  q1  q2  (q1, q2)  fst ` r_distinguishable_state_pairs_with_separators M"
shows "implies_completeness (calculate_test_suite_for_repetition_sets M m RepSets) M m"
and   "is_finite_test_suite (calculate_test_suite_for_repetition_sets M m RepSets)"
proof -
  obtain states_with_preambles tps rd_targets atcs where "calculate_test_suite_for_repetition_sets M m RepSets 
                                                          = Test_Suite states_with_preambles tps rd_targets atcs"
    using test_suite.exhaust by blast

  have " a b c d . Test_Suite states_with_preambles tps rd_targets atcs = Test_Suite a b c d  tps = b"
    by blast

  have states_with_preambles_def : "states_with_preambles = d_reachable_states_with_preambles M"
    
  
  and tps_def                   : "tps = (λq. (m2f_by  (set_as_map ((λ(q, p). (q, fst ` p)) ` (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M))) q
                                             (m2f (set_as_map ((λ(q, p, q'). (q, p)) `
                                                ((qfst ` d_reachable_states_with_preambles M.  (prefix_pair_tests q ` (m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q))) 
                                                 (qfst ` d_reachable_states_with_preambles M. mrsps m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                                                 preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))))) q)"
  and rd_targets_def            : "rd_targets = m2f (set_as_map
                                              ((λ(q, p, y). ((q, p), y)) `
                                               ((qfst ` d_reachable_states_with_preambles M.  (prefix_pair_tests q ` (m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q))) 
                                                (qfst ` d_reachable_states_with_preambles M. mrsps m2f (set_as_map ((λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M)) q . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                                                preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))))"
  and  atcs_def                 : "atcs = m2f (set_as_map ((λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M))"
    using calculate_test_suite_for_repetition_sets M m RepSets = Test_Suite states_with_preambles tps rd_targets atcs[symmetric]
    unfolding calculate_test_suite_for_repetition_sets_def combine_test_suite_def Let_def calculate_test_paths_def fst_conv snd_conv by force+
  

  have tps_alt_def: " q . q  fst ` d_reachable_states_with_preambles M  
          tps q = (fst ` m_traversal_paths_with_witness M q RepSets m)  
                  {z. (q, z)
                     (λ(q, p, q'). (q, p)) `
                       ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                        (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                        preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
  and rd_targets_alt_def: " q p . q  fst ` d_reachable_states_with_preambles M  
          rd_targets (q,p) = {z. ((q, p), z)
                    (λ(q, p, y). ((q, p), y)) `
                      ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                       (qfst ` d_reachable_states_with_preambles M.
                           mrsps{m_traversal_paths_with_witness M q RepSets m}.
                              preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                       preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
  proof -
    fix q p assume "q  fst ` d_reachable_states_with_preambles M"

  

    have scheme0 : "(case set_as_map
             ((λ(q, p). (q, fst ` p)) `
              (λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
              fst ` d_reachable_states_with_preambles M)
             q of
       None   {} | Some x   x) = image fst (m_traversal_paths_with_witness M q RepSets m)"
    proof -
      have *: "((λ(q, p). (q, fst ` p)) `
              (λq. (q, m_traversal_paths_with_witness M q RepSets m)) `
              fst ` d_reachable_states_with_preambles M)
               = (λ q . (q , image fst (m_traversal_paths_with_witness M q RepSets m))) ` (fst ` d_reachable_states_with_preambles M)"
        by force
      have **: " f q xs . (case set_as_map
                              ((λq. (q, f q)) ` xs)
                              q of
                        None   {} | Some xs   xs) = (if q  xs then  {f q} else  {})" 
      unfolding set_as_map_def by auto

      show ?thesis
        unfolding * **
        using q  fst ` d_reachable_states_with_preambles M
        by auto
    qed
    
    
    have scheme1 : " f q xs . (case set_as_map
                              ((λq. (q, f q)) ` xs)
                              q of
                        None  {} | Some xs  xs) = (if q  xs then {f q} else {})" 
      unfolding set_as_map_def by auto        


    have scheme2: "(qfst ` d_reachable_states_with_preambles M.
                    (prefix_pair_tests q `
                       (if q  fst ` d_reachable_states_with_preambles M
                        then {m_traversal_paths_with_witness M q RepSets m} else {})))
      = (qfst ` d_reachable_states_with_preambles M. ( (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})))"
      unfolding set_as_map_def by auto


    have scheme3: "(qfst ` d_reachable_states_with_preambles M.
                   mrspsif q  fst ` d_reachable_states_with_preambles M
                           then {m_traversal_paths_with_witness M q RepSets m} else {}.
                      preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))
      = (qfst ` d_reachable_states_with_preambles M. (mrsps{m_traversal_paths_with_witness M q RepSets m} . preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)))"
      unfolding set_as_map_def by auto

    have scheme4 : "(fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)
                    = image fst (r_distinguishable_state_pairs_with_separators M)" 
      by force

    have *:"tps q = (fst ` m_traversal_paths_with_witness M q RepSets m)  
                  {z. (q, z)
                     (λ(q, p, q'). (q, p)) `
                       ((qfst ` d_reachable_states_with_preambles M.
                             (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) 
                        (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                        preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
      unfolding tps_def 
      unfolding scheme0 scheme1 scheme2 scheme3 scheme4
      unfolding set_as_map_def
      by auto

    have **: "{z. (q, z)
                     (λ(q, p, q'). (q, p)) `
                       ((qfst ` d_reachable_states_with_preambles M.
                             (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) 
                        (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                        preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}
          = {z. (q, z)
                     (λ(q, p, q'). (q, p)) `
                       ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                        (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                        preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}" 
      (is "{z. (q, z)  ?S1} = {z. (q, z)  ?S2}")
    proof -
      have " z . (q, z)  ?S1  (q, z)  ?S2"
      proof -
        fix z assume "(q, z)  ?S1"
        then consider "(q, z)  (λ(q, p, q'). (q, p)) ` (qfst ` d_reachable_states_with_preambles M.
                             (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
                    | "(q,z)  (λ(q, p, q'). (q, p)) `  (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
                    | "(q,z)  (λ(q, p, q'). (q, p)) ` (preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))"
          by blast
        then show "(q, z)  ?S2" proof cases
          case 1
          have scheme: " f y xs . y  image f xs   x . x  xs  f x = y" by auto

          obtain qzq where "qzq  (qfst ` d_reachable_states_with_preambles M.  (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
                     and   "(λ(q, p, q'). (q, p)) qzq = (q,z)"
            using scheme[OF 1] by blast
          then obtain q' where "q'fst ` d_reachable_states_with_preambles M"
                         and   "qzq   (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})"
            by blast
          then have "fst qzq = q'"
            by auto
          then have "q' = q"
            using (λ(q, p, q'). (q, p)) qzq = (q,z)
            by (simp add: prod.case_eq_if) 
          then have "qzq   (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})"
            using qzq   (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m}) 
            by blast
          then have "(λ(q, p, q'). (q, p)) qzq  ?S2"
            by auto
          then show ?thesis 
            unfolding (λ(q, p, q'). (q, p)) qzq = (q,z) 
            by assumption
        next
          case 2 
          then show ?thesis by blast
        next
          case 3
          then show ?thesis by blast
        qed
      qed
      moreover have " z . (q, z)  ?S2  (q, z)  ?S1"
        using q  fst ` d_reachable_states_with_preambles M by blast
      ultimately show ?thesis
        by meson
    qed

    show "tps q = (fst ` m_traversal_paths_with_witness M q RepSets m)  
                  {z. (q, z)
                     (λ(q, p, q'). (q, p)) `
                       ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                        (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                        preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
     using * unfolding ** by assumption

    have ***: "rd_targets (q,p) = {z. ((q, p), z)
                    (λ(q, p, y). ((q, p), y)) `
                      ((qfst ` d_reachable_states_with_preambles M.
                            (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) 
                       (qfst ` d_reachable_states_with_preambles M.
                           mrsps{m_traversal_paths_with_witness M q RepSets m}.
                              preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                       preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
      unfolding rd_targets_def
      unfolding scheme1 scheme2 scheme3 scheme4
      unfolding set_as_map_def
      by auto


    have ****: "{z. ((q, p), z)
                    (λ(q, p, y). ((q, p), y)) `
                      ((qfst ` d_reachable_states_with_preambles M.
                            (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) 
                       (qfst ` d_reachable_states_with_preambles M.
                           mrsps{m_traversal_paths_with_witness M q RepSets m}.
                              preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                       preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}
          = {z. ((q, p), z)
                    (λ(q, p, y). ((q, p), y)) `
                      ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                       (qfst ` d_reachable_states_with_preambles M.
                           mrsps{m_traversal_paths_with_witness M q RepSets m}.
                              preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                       preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}" 
      (is "{z. ((q, p), z)  ?S1} = {z. ((q, p), z)  ?S2}")
    proof -
      have " z . ((q, p), z)  ?S1  ((q, p), z)  ?S2"
      proof -
        fix z assume "((q, p), z)  ?S1"
        then consider "((q, p), z)  (λ(q, p, y). ((q, p), y)) ` (qfst ` d_reachable_states_with_preambles M.
                             (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
                    | "((q, p), z)  (λ(q, p, y). ((q, p), y)) `  (qfst ` d_reachable_states_with_preambles M.
                            mrsps{m_traversal_paths_with_witness M q RepSets m}.
                               preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))"
                    | "((q, p), z)  (λ(q, p, y). ((q, p), y)) ` (preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))"
          by blast
        then show "((q, p), z)  ?S2" proof cases
          case 1
          have scheme: " f y xs . y  image f xs   x . x  xs  f x = y" by auto

          obtain qzq where "qzq  (qfst ` d_reachable_states_with_preambles M.  (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m}))"
                     and   "(λ(q, p, y). ((q, p), y)) qzq = ((q,p),z)"
            using scheme[OF 1] by blast
          then obtain q' where "q'fst ` d_reachable_states_with_preambles M"
                         and   "qzq   (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m})"
            by blast
          then have "fst qzq = q'"
            by auto
          then have "q' = q"
            using (λ(q, p, y). ((q, p), y)) qzq = ((q,p),z)
            by (simp add: prod.case_eq_if) 
          then have "qzq   (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})"
            using qzq   (prefix_pair_tests q' ` {m_traversal_paths_with_witness M q' RepSets m}) 
            by blast
          then have "(λ(q, p, y). ((q, p), y)) qzq  ?S2"
            by auto
          then show ?thesis 
            unfolding (λ(q, p, y). ((q, p), y)) qzq = ((q,p),z) 
            by assumption
        next
          case 2 
          then show ?thesis by blast
        next
          case 3
          then show ?thesis by blast
        qed
      qed
      moreover have " z . ((q, p), z)  ?S2  ((q, p), z)  ?S1"
        using q  fst ` d_reachable_states_with_preambles M by blast
      ultimately show ?thesis
        by meson
    qed

    show "rd_targets (q,p) = {z. ((q, p), z)
                    (λ(q, p, y). ((q, p), y)) `
                      ((prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)) 
                       (qfst ` d_reachable_states_with_preambles M.
                           mrsps{m_traversal_paths_with_witness M q RepSets m}.
                              preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M)) 
                       preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M))}"
      using ***  unfolding **** by assumption
  qed


  define pps_alt :: "('a × ('a,'b,'c) traversal_path × 'a) set" where pps_alt_def : "pps_alt = {(q1,[],q2) | q1 q2 .  q p rd dr . q  fst ` d_reachable_states_with_preambles M  (p,(rd,dr))  m_traversal_paths_with_witness M q RepSets m  q1  dr  q2  dr  (q1,q2)  fst  ` r_distinguishable_state_pairs_with_separators M}"
  have preamble_pair_tests_alt :
    "preamble_pair_tests ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y) (fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1 :: 'a × 'a + 'a, Inr q2 :: 'a × 'a + 'a)) ` r_distinguishable_state_pairs_with_separators M)
     = pps_alt"
    (is "?PP1 = ?PP2")
  proof -
    have " x . x  ?PP1  x  ?PP2"
    proof -
      fix x assume "x  ?PP1"
      then obtain drs where "drs  ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)"
                      and   "x  (λ(q1, q2). (q1, [], q2)) ` (drs × drs  fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
        unfolding preamble_pair_tests.simps by force

      obtain q y where "(q,y)  (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M"
                 and   "drs  (λ(p, rd, dr). dr) ` y"
        using drs  ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)
        by force

      have "q  fst ` d_reachable_states_with_preambles M"
      and  "y = m_traversal_paths_with_witness M q RepSets m"
        using (q,y)  (λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M
        by force+

      obtain p rd where "(p,(rd,drs))  m_traversal_paths_with_witness M q RepSets m"
        using drs  (λ(p, rd, dr). dr) ` y unfolding y = m_traversal_paths_with_witness M q RepSets m
        by force


      obtain q1 q2 where "(q1,q2)  (drs × drs  fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
                   and   "x = (q1, [], q2)"
        using x  (λ(q1, q2). (q1, [], q2)) ` (drs × drs  fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)
        by force

      have "q1  drs  q2  drs  (q1,q2)  fst  ` r_distinguishable_state_pairs_with_separators M"
        using (q1,q2)  (drs × drs  fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)
        by force

      then show "x  ?PP2"
        unfolding x = (q1, [], q2) pps_alt_def
        using q  fst ` d_reachable_states_with_preambles M (p,(rd,drs))  m_traversal_paths_with_witness M q RepSets m
        by blast
    qed

    moreover have " x . x  ?PP2  x  ?PP1" 
    proof -
      fix x assume "x  ?PP2"
      then obtain q1 q2 where "x = (q1,[],q2)" unfolding pps_alt_def
        by auto
      then obtain q p rd dr where "q  fst ` d_reachable_states_with_preambles M" 
                            and   "(p,(rd,dr))  m_traversal_paths_with_witness M q RepSets m" 
                            and   "q1  dr  q2  dr  (q1,q2)  fst  ` r_distinguishable_state_pairs_with_separators M"
        using x  ?PP2 unfolding pps_alt_def by blast

      have "dr  ((q, y)(λq. (q, m_traversal_paths_with_witness M q RepSets m)) ` fst ` d_reachable_states_with_preambles M. (λ(p, rd, dr). dr) ` y)"
        using q  fst ` d_reachable_states_with_preambles M (p,(rd,dr))  m_traversal_paths_with_witness M q RepSets m by force

      moreover have "x  (λ(q1, q2). (q1, [], q2)) ` (dr × dr  fst ` (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M)"
        unfolding x = (q1,[],q2) using q1  dr  q2  dr  (q1,q2)  fst  ` r_distinguishable_state_pairs_with_separators M by force

      ultimately show "x  ?PP1"
        unfolding preamble_pair_tests.simps by force
    qed

    ultimately show ?thesis by blast
  qed


  have p1: "(initial M,initial_preamble M)  states_with_preambles"
    using fsm_initial[of M]
    unfolding states_with_preambles_def d_reachable_states_with_preambles_def calculate_state_preamble_from_input_choices.simps by force

  have p2a: " q P . (q,P)  states_with_preambles  is_preamble P M q"
    using assms(1) d_reachable_states_with_preambles_soundness(1) states_with_preambles_def by blast

  have p2b: " q P . (q,P)  states_with_preambles  (tps q)  {}"
  proof -
    fix q P assume "(q,P)  states_with_preambles"
    then have "q  (image fst (d_reachable_states_with_preambles M))"
      unfolding states_with_preambles_def
      by (simp add: rev_image_eqI) 
    
    have "q  states M"
      using (q, P)  states_with_preambles assms(1) d_reachable_states_with_preambles_soundness(2) states_with_preambles_def by blast 


    obtain p' d' where  "(p', d')  m_traversal_paths_with_witness M q RepSets m"
      using m_traversal_path_exist[OF assms(2) q  states M assms(3) q. q  FSM.states M  dset RepSets. q  fst d] assms(5) 
      by blast
    then have "p'  image fst (m_traversal_paths_with_witness M q RepSets m)"
      using image_iff by fastforce
    
    have "(q, image fst (m_traversal_paths_with_witness M q RepSets m))  (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M))))"
      using q  (image fst (d_reachable_states_with_preambles M)) by force
    have "(image fst (m_traversal_paths_with_witness M q RepSets m))  (m2f (set_as_map (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M)))))) q"
      using set_as_map_containment[OF (q, image fst (m_traversal_paths_with_witness M q RepSets m))  (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M))))]
      by assumption
    then have "p'  ( ((m2f (set_as_map (image (λ (q,p) . (q, image fst p)) (image (λ q . (q,m_traversal_paths_with_witness M q RepSets m)) (image fst (d_reachable_states_with_preambles M)))))) q))"
      using p'  image fst (m_traversal_paths_with_witness M q RepSets m) by blast

    then show "(tps q)  {}"
      unfolding tps_def m2f_by_from_m2f by blast
  qed

  have p2: "(q P. (q, P)  states_with_preambles  is_preamble P M q  tps q  {})"
    using p2a p2b by blast

  have " q1 q2 A d1 d2 . ((A,d1,d2)  atcs (q1,q2))  ((q1,q2),A)  r_distinguishable_state_pairs_with_separators M  d1 = Inr q1  d2 = Inr q2"
  proof -
    fix q1 q2 A d1 d2 assume "((A,d1,d2)  atcs (q1,q2))"
    then have "atcs (q1,q2) = {z. ((q1, q2), z)  (λ((q1, q2), A). ((q1, q2), A, Inr q1, Inr q2)) ` r_distinguishable_state_pairs_with_separators M}"
      unfolding atcs_def set_as_map_def by auto
    then show "((q1,q2),A)  r_distinguishable_state_pairs_with_separators M  d1 = Inr q1  d2 = Inr q2"
      using ((A,d1,d2)  atcs (q1,q2)) by auto
  qed


  have " 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"
  proof -
    fix q1 q2 A d1 d2 assume "(A,d1,d2)  atcs (q1,q2)"
    then have "((q1,q2),A)  r_distinguishable_state_pairs_with_separators M" and "d1 = Inr q1" and "d2 = Inr q2"
      using  q1 q2 A d1 d2 . ((A,d1,d2)  atcs (q1,q2))  ((q1,q2),A)  r_distinguishable_state_pairs_with_separators M  d1 = Inr q1  d2 = Inr q2
      by blast+
    then have "((q2,q1),A)  r_distinguishable_state_pairs_with_separators M"
      unfolding r_distinguishable_state_pairs_with_separators_def
      by auto  
    then have "(A,d2,d1)  atcs (q2,q1)"
      unfolding atcs_def d1 = Inr q1 d2 = Inr q2 set_as_map_def by force
    moreover have "is_separator M q1 q2 A d1 d2"
      using r_distinguishable_state_pairs_with_separators_elem_is_separator[OF ((q1,q2),A)  r_distinguishable_state_pairs_with_separators M assms(1,2)]
      unfolding d1 = Inr q1 d2 = Inr q2
      by assumption
    ultimately show "(A,d2,d1)  atcs (q2,q1)  is_separator M q1 q2 A d1 d2"
      by simp
  qed
  then have p3 : "(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)"
    by blast

  have p4: " q . q  states M  (d  set RepSets. q  fst d)"
    by (simp add: assms(4))
  
  have p5: " d . d  set RepSets  ((fst d  states M)  (snd d = fst d  fst ` states_with_preambles)  ( q1 q2 . q1  fst d  q2  fst d  q1  q2  atcs (q1,q2)  {}))"
  proof -
    fix d assume "d  set RepSets"
    
    then have " q1 q2 . q1  fst d  q2  fst d  q1  q2  atcs (q1,q2)  {}"
    proof -
      fix q1 q2 assume "q1  fst d" and "q2  fst d" and "q1  q2"
      then have "(q1, q2)  fst ` r_distinguishable_state_pairs_with_separators M" 
        using assms(6)[OF d  set RepSets] by blast
      then obtain A where "((q1,q2),A)  r_distinguishable_state_pairs_with_separators M"
        by auto
      then have "(A,Inr q1,Inr q2)  atcs (q1,q2)"
        unfolding atcs_def set_as_map_def 
        by force
      then show "atcs (q1,q2)  {}"
        by blast
    qed
    then show "((fst d  states M)  (snd d = fst d  fst ` states_with_preambles)  ( q1 q2 . q1  fst d  q2  fst d  q1  q2  atcs (q1,q2)  {}))"
      using assms(5)[OF d  set RepSets] unfolding states_with_preambles_def by blast
  qed

  have p6 : " q . q  image fst states_with_preambles  tps q  {p1 .  p2 d . (p1@p2,d)  m_traversal_paths_with_witness M q RepSets m}  fst ` (m_traversal_paths_with_witness M q RepSets m)  tps q"
  proof 
    fix q assume "q  image fst states_with_preambles"
    then have "q  fst ` d_reachable_states_with_preambles M"
      unfolding states_with_preambles_def by assumption
    then have "q  states M"
      by (metis (no_types, lifting) assms(1) d_reachable_states_with_preambles_soundness(2) image_iff prod.collapse)
    show "fst ` m_traversal_paths_with_witness M q RepSets m  tps q"
      unfolding tps_alt_def[OF q  fst ` d_reachable_states_with_preambles M]
      by blast


    show "tps q  {p1 .  p2 d . (p1@p2,d)  m_traversal_paths_with_witness M q RepSets m}"
    proof
      fix p assume "p  tps q"


      have * : "( q . q  states M  (d  set RepSets. q  fst d))" 
        using p4 by blast

      have  **: "( d . d  set RepSets  (snd d  fst d))"
        using p5 by simp

      from p  tps q consider 
        (a) "p  fst ` m_traversal_paths_with_witness M q RepSets m" |
        (b) "(q, p)  (λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m))" |
        (c) "(q, p)  (λ(q, p, q'). (q, p)) ` (qfst ` d_reachable_states_with_preambles M.
                mrsps{m_traversal_paths_with_witness M q RepSets m}.
                   preamble_prefix_tests q mrsps (fst ` d_reachable_states_with_preambles M))" |
        (d) "(q, p)  (λ(q, p, q'). (q, p)) ` pps_alt"  
        unfolding tps_alt_def[OF q  fst ` d_reachable_states_with_preambles M] preamble_pair_tests_alt by blast

      then show "p  {p1. p2 d. (p1 @ p2, d)  m_traversal_paths_with_witness M q RepSets m}"
      proof cases
        case a
        then obtain d where "(p,d)  m_traversal_paths_with_witness M q RepSets m"
          by auto
        then have "p2 d. (p @ p2, d)  m_traversal_paths_with_witness M q RepSets m"
          by (metis append_eq_append_conv2)
        then show ?thesis 
          by blast
      next
        case b
  
        obtain p1 p2  where "(q,p)  ((λ(q, p, q'). (q, p)) `{(q, p1, target q p2), (q, p2, target q p1)})"
           and "(p, rd, dr)m_traversal_paths_with_witness M q RepSets m.
              (p1, p2)  set (prefix_pairs p)  target q p1  rd  target q p2  rd  target q p1  target q p2"
          using b
          unfolding prefix_pair_tests.simps by blast
  
        obtain p' d where "(p', d)  m_traversal_paths_with_witness M q RepSets m"
                    and   "(p1, p2)  set (prefix_pairs p')"
          using (p, rd, dr)m_traversal_paths_with_witness M q RepSets m.
              (p1, p2)  set (prefix_pairs p)  target q p1  rd  target q p2  rd  target q p1  target q p2
          by blast
  
        have " p'' . p' = p @ p''"
          using (p1, p2)  set (prefix_pairs p') unfolding prefix_pairs_set_alt 
          using (q,p)  ((λ(q, p, q'). (q, p)) `{(q, p1, target q p2), (q, p2, target q p1)}) by auto
        then show ?thesis
          using (p', d)  m_traversal_paths_with_witness M q RepSets m  
          by blast
      next
        case c     
  
        obtain q' where "q'  fst ` d_reachable_states_with_preambles M"
                  and   "(q,p)  (λ(q, p, q'). (q, p)) ` (preamble_prefix_tests q' (m_traversal_paths_with_witness M q' RepSets m) (fst ` d_reachable_states_with_preambles M))"
          using c by blast
  
        obtain p1 q2  where "(q,p)  ((λ(q, p, q'). (q, p)) `{(q', p1, q2), (q2, [], target q' p1)})"
           and "(p, rd, dr)m_traversal_paths_with_witness M q' RepSets m.
              q2  fst ` d_reachable_states_with_preambles M  (p2. p = p1 @ p2)  target q' p1  rd  q2  rd  target q' p1  q2"
          using (q,p)  (λ(q, p, q'). (q, p)) ` (preamble_prefix_tests q' (m_traversal_paths_with_witness M q' RepSets m) (fst ` d_reachable_states_with_preambles M))
          unfolding preamble_prefix_tests_def
          by blast
  
        obtain p2 d where "(p1@p2, d)m_traversal_paths_with_witness M q' RepSets m"
                        and   "q2  fst ` d_reachable_states_with_preambles M"
          using (p, rd, dr)m_traversal_paths_with_witness M q' RepSets m.
              q2  fst ` d_reachable_states_with_preambles M  (p2. p = p1 @ p2)  target q' p1  rd  q2  rd  target q' p1  q2
          by blast
  
        consider (a) "q = q'  p = p1" | (b) "q = q2  p = []"
          using (q,p)  ((λ(q, p, q'). (q, p)) `{(q', p1, q2), (q2, [], target q' p1)}) by auto
        then show ?thesis proof cases
          case a
          then show ?thesis
            using (p1 @ p2, d)  m_traversal_paths_with_witness M q' RepSets m by blast 
  
        next
          case b
  
          then have "q  states M" and "p = []"
            using q2  fst ` d_reachable_states_with_preambles M unfolding d_reachable_states_with_preambles_def by auto
  
          have "p' d'. (p', d')  m_traversal_paths_with_witness M q RepSets m"
            using m_traversal_path_exist[OF assms(2) q  states M assms(3) * **]
            by blast
          then show ?thesis 
            unfolding p = []
            by simp
        qed
      next
        case d 
        then have "p = []" 
          unfolding pps_alt_def by force
        
        have "q  states M"
          using q  fst ` d_reachable_states_with_preambles M unfolding d_reachable_states_with_preambles_def by auto
  
        have "p' d'. (p', d')  m_traversal_paths_with_witness M q RepSets m"
          using m_traversal_path_exist[OF assms(2) q  states M assms(3) * **]
          by blast
        then show ?thesis 
          unfolding p = []
          by simp
      qed
    qed
  qed
 
  have p7 : " q p d . q  image fst states_with_preambles  (p,d)  m_traversal_paths_with_witness M q RepSets m  
            ( ( p1 p2 p3 . p=p1@p2@p3  p2  []  target q p1  fst d  target q (p1@p2)  fst d  target q p1  target q (p1@p2)  (p1  tps q  (p1@p2)  tps q  target q p1  rd_targets (q,(p1@p2))  target q (p1@p2)  rd_targets (q,p1)))
             ( p1 p2 q' . p=p1@p2  q'  image fst states_with_preambles  target q p1  fst d  q'  fst d  target q p1  q'  (p1  tps q  []  tps q'  target q p1  rd_targets (q',[])  q'  rd_targets (q,p1)))
             ( q1 q2 . q1  q2  q1  snd d  q2  snd d  ([]  tps q1  []  tps q2  q1  rd_targets (q2,[])  q2  rd_targets (q1,[]))))"
  proof -
    fix q p d assume "q  image fst states_with_preambles" and "(p,d)  m_traversal_paths_with_witness M q RepSets m"
    then have "(p,(fst d, snd d))  m_traversal_paths_with_witness M q RepSets m" by auto

    have "q  fst ` d_reachable_states_with_preambles M"
      using q  image fst states_with_preambles unfolding states_with_preambles_def by assumption

    have p7c1 : " p1 p2 p3 . p=p1@p2@p3  p2  []  target q p1  fst d  target q (p1@p2)  fst d  target q p1  target q (p1@p2)  (p1  tps q  (p1@p2)  tps q  target q p1  rd_targets (q,(p1@p2))  target q (p1@p2)  rd_targets (q,p1))"
    proof -
      fix p1 p2 p3 assume "p=p1@p2@p3" and "p2  []" and "target q p1  fst d" and "target q (p1@p2)  fst d" and "target q p1  target q (p1@p2)"

      have "(p1,p1@p2)  set (prefix_pairs p)"
        using p=p1@p2@p3 p2  [] unfolding prefix_pairs_set
        by simp 
      then have "(p1,p1@p2)  set (filter (λ(p1, p2). target q p1  fst d  target q p2  fst d  target q p1  target q p2) (prefix_pairs p))"
        using target q p1  fst d target q (p1@p2)  fst d target q p1  target q (p1@p2)
        by auto
      have "{(q, p1, target q (p1@p2)), (q, (p1@p2), target q p1)}  ((set (map (λ(p1, p2). {(q, p1, target q p2), (q, p2, target q p1)})
            (filter (λ(p1, p2). target q p1  fst d  target q p2  fst d  target q p1  target q p2) (prefix_pairs p)))))"
        using map_set[OF (p1,p1@p2)  set (filter (λ(p1, p2). target q p1  fst d  target q p2  fst d  target q p1  target q p2) (prefix_pairs p)), of "(λ(p1, p2). {(q, p1, target q p2), (q, p2, target q p1)})"] 
        by force
      then have "(q, p1, target q (p1@p2))  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
           and  "(q, p1@p2, target q p1)  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
        unfolding prefix_pair_tests_code[of q "m_traversal_paths_with_witness M q RepSets m"]
        using (p,(fst d, snd d))  m_traversal_paths_with_witness M q RepSets m
        by blast+

      have "p1  tps q"
      proof -
        have "(q, p1)  ((λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)))"
          using (q, p1, target q (p1@p2))  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)
          by (simp add: rev_image_eqI)  
        then show ?thesis 
          unfolding tps_alt_def[OF q  fst ` d_reachable_states_with_preambles M] 
          by blast
      qed

      moreover have "(p1@p2)  tps q"
      proof -
        have "(q, p1@p2)  ((λ(q, p, q'). (q, p)) ` (prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)))"
          using (q, p1@p2, target q p1)  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)
          by (simp add: rev_image_eqI) 
        then show ?thesis 
          unfolding tps_alt_def[OF q  fst ` d_reachable_states_with_preambles M] 
          by blast          
      qed

      moreover have "target q p1  rd_targets (q,(p1@p2))"
      proof -
        have "((q, p1@p2), target q p1)  (λ(q, p, y). ((q, p), y)) ` prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
          using (q, p1@p2, target q p1)  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)
          by (simp add: rev_image_eqI)
        then show ?thesis
          unfolding rd_targets_alt_def[OF q  fst ` d_reachable_states_with_preambles M] 
          by blast
      qed

      moreover have "target q (p1@p2)  rd_targets (q,p1)"
      proof -
        have "((q, p1), target q (p1@p2))  (λ(q, p, y). ((q, p), y)) ` prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)"
          using (q, p1, target q (p1@p2))  prefix_pair_tests q (m_traversal_paths_with_witness M q RepSets m)
          by (simp add: rev_image_eqI)
        then show ?thesis
          unfolding rd_targets_alt_def[OF q  fst ` d_reachable_states_with_preambles M] 
          by blast
      qed
      
      ultimately show "(p1  tps q  (p1@p2)  tps q  target q p1  rd_targets (q,(p1@p2))  target q (p1@p2)  rd_targets (q,p1))"
        by blast
    qed

    moreover have p7c2: " p1 p2 q' . p=p1@p2  q'  image fst states_with_preambles  target q p1  fst d  q'  fst d  target q p1  q'  (p1  tps q  []  tps q'  target q p1  rd_targets (q',[])  q'  rd_targets (q,p1))"
    proof -
      fix p1 p2 q' assume "p=p1@p2" and "q'  image fst states_with_preambles" and "target q p1  fst d" and "q'  fst d" and "target q p1  q'"
      then have "q'  fst ` d_reachable_states_with_preambles M"
        unfolding states_with_preambles_def by blast
      
      have "p1  set (prefixes p)"
        using p=p1@p2 unfolding prefixes_set
        by simp 
      then have "(p1,q')  Set.filter (λ(p1, q2). target q p1  fst d  q2  fst d  target q p1  q2) (set (prefixes p) × fst ` d_reachable_states_with_preambles M)"
        using target q p1  fst d q'  fst d q'  image fst states_with_preambles target q p1  q' unfolding states_with_preambles_def
        by force
      then have "{(q, p1, q'), (q', [], target q p1)}  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
        using preamble_prefix_tests_code[of q "m_traversal_paths_with_witness M q RepSets m" "(fst ` d_reachable_states_with_preambles M)"]
        using (p,(fst d, snd d))  m_traversal_paths_with_witness M q RepSets m
        by blast
      then have "(q, p1, q')  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
           and  "(q', [], target q p1)  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)"
        by blast+

      have "p1  tps q"
        using (q, p1, q')  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)        
              q  fst ` d_reachable_states_with_preambles M
        unfolding tps_alt_def[OF q  fst ` d_reachable_states_with_preambles M]
        by force

      moreover have "[]  tps q'"
        using (q', [], target q p1)  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)        
              q  fst ` d_reachable_states_with_preambles M
        unfolding tps_alt_def[OF q'  fst ` d_reachable_states_with_preambles M]
        by force

      moreover have "target q p1  rd_targets (q',[])"
        using (q', [], target q p1)  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)        
              q  fst ` d_reachable_states_with_preambles M
        unfolding rd_targets_alt_def[OF q'  fst ` d_reachable_states_with_preambles M] 
        by force

      moreover have "q'  rd_targets (q,p1)"
        using (q, p1, q')  preamble_prefix_tests q (m_traversal_paths_with_witness M q RepSets m) (fst ` d_reachable_states_with_preambles M)        
              q  fst ` d_reachable_states_with_preambles M
        unfolding rd_targets_alt_def[OF q  fst ` d_reachable_states_with_preambles M]
        by force

      ultimately show "(p1  tps q  []  tps q'  target q p1  rd_targets (q',[])  q'  rd_targets (q,p1))"
        by blast
    qed


    moreover have p7c3: " q1 q2 . q1  q2  q1  snd d  q2  snd d  ([]  tps q1  []  tps q2  q1  rd_targets (q2,[])  q2  rd_targets (q1,[]))"
    proof -
      fix q1 q2 assume "q1  q2" and "q1  snd d" and "q2  snd d"

      have "(d. d  set RepSets  snd d  fst d)"
        using p5 by blast
      have "q  states M"
        by (metis (no_types, lifting) q  fst ` d_reachable_states_with_preambles M assms(1) 
              d_reachable_states_with_preambles_soundness(2) image_iff prod.collapse) 

      have "d  set RepSets" 
        using m_traversal_paths_with_witness_set[OF p4 (d. d  set RepSets  snd d  fst d) q  states M, of m]
        using (p, d)  m_traversal_paths_with_witness M q RepSets m find_set 
        by force 

      have "fst d  states M" 
      and  "snd d = fst d  fst ` states_with_preambles" 
      and  " q1 q2. q1  fst d  q2  fst d  q1  q2  atcs (q1, q2)  {}"
        using p5[OF d  set RepSets] by blast+

      have "q1  fst d" 
       and "q2  fst d" 
       and "q1  fst ` d_reachable_states_with_preambles M" 
       and "q2  fst ` d_reachable_states_with_preambles M"
        using q1  snd d q2  snd d unfolding snd d = fst d  fst ` states_with_preambles 
        unfolding states_with_preambles_def by blast+

      obtain A t1 t2 where "(A,t1,t2)  atcs (q1, q2)"
        using  q1 q2. q1  fst d  q2  fst d  q1  q2  atcs (q1, q2)  {}[OF q1  fst d q2  fst d q1  q2] 
        by auto

      then have "(q1, q2)  fst ` r_distinguishable_state_pairs_with_separators M" 
        unfolding atcs_def using set_as_map_elem by force
      then have "(q1,[],q2)  pps_alt"
        using q  fst ` d_reachable_states_with_preambles M (p,(fst d, snd d))  m_traversal_paths_with_witness M q RepSets m
        unfolding pps_alt_def
        by (metis (mono_tags, lifting) q1  snd d q2  snd d mem_Collect_eq) 
      then have "[]  tps q1" and "q2  rd_targets (q1,[])"
        unfolding tps_alt_def[OF q1  fst ` d_reachable_states_with_preambles M] 
                  rd_targets_alt_def[OF q1  fst ` d_reachable_states_with_preambles M] 
                  preamble_pair_tests_alt 
        by force+

      have "(A,t2,t1)  atcs (q2, q1)"
        using p3 (A,t1,t2)  atcs (q1, q2) by blast
      then have "(q2, q1)  fst ` r_distinguishable_state_pairs_with_separators M" 
        unfolding atcs_def using set_as_map_elem by force
      then have "(q2,[],q1)  pps_alt"
        using q  fst ` d_reachable_states_with_preambles M (p,(fst d, snd d))  m_traversal_paths_with_witness M q RepSets m