# 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 ⟹ ∃d∈set 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 ⟹ q1∈fst d ⟹ q2∈fst 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)) `
((⋃q∈fst ` 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)))
∪ (⋃q∈fst ` 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)) `
((⋃q∈fst ` 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)))
∪ (⋃q∈fst ` 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)) ∪
(⋃q∈fst ` 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)) ∪
(⋃q∈fst ` 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: "(⋃q∈fst ` 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 {})))
= (⋃q∈fst ` 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: "(⋃q∈fst ` d_reachable_states_with_preambles M.
⋃mrsps∈if 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))
= (⋃q∈fst ` 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)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` 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)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` 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)) ∪
(⋃q∈fst ` 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)) ` (⋃q∈fst ` 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)) `  (⋃q∈fst ` 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 ∈ (⋃q∈fst ` 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)›
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)) ∪
(⋃q∈fst ` 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)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` 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)) `
((⋃q∈fst ` d_reachable_states_with_preambles M.
⋃ (prefix_pair_tests q ` {m_traversal_paths_with_witness M q RepSets m})) ∪
(⋃q∈fst ` 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)) ∪
(⋃q∈fst ` 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)) ` (⋃q∈fst ` 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)) `  (⋃q∈fst ` 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 ∈ (⋃q∈fst ` 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)›
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)) ∪
(⋃q∈fst ` 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

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 ⟹ ∃d∈set 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)"

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)) ` (⋃q∈fst ` 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)›
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)›
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)›
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)›
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›
```