# Theory Traversal_Set

```section ‹Traversal Set›

text ‹This theory defines the calculation of m-traversal paths.
These are paths extended from some state until they visit pairwise r-distinguishable states
a number of times dependent on m.›

theory Traversal_Set
imports Helper_Algorithms
begin

definition m_traversal_paths_with_witness_up_to_length ::
"('a,'b,'c) fsm ⇒ 'a ⇒ ('a set × 'a set) list ⇒ nat ⇒ nat ⇒ (('a×'b×'c×'a) list × ('a set × 'a set)) set"
where
"m_traversal_paths_with_witness_up_to_length M q D m k
= paths_up_to_length_or_condition_with_witness M (λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D) k q"

definition m_traversal_paths_with_witness ::
"('a,'b,'c) fsm ⇒ 'a ⇒ ('a set × 'a set) list ⇒ nat ⇒ (('a×'b×'c×'a) list × ('a set × 'a set)) set"
where
"m_traversal_paths_with_witness M q D m = m_traversal_paths_with_witness_up_to_length M q D m (Suc (size M * m))"

lemma m_traversal_paths_with_witness_finite : "finite (m_traversal_paths_with_witness M q D m)"
unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def
by (simp add: paths_up_to_length_or_condition_with_witness_finite)

lemma m_traversal_paths_with_witness_up_to_length_max_length :
assumes "⋀ q . q ∈ states M ⟹ ∃ d ∈ set D . q ∈ fst d"
and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
and     "q ∈ states M"
and     "(p,d) ∈ (m_traversal_paths_with_witness_up_to_length M q D m k)"
shows "length p ≤ Suc ((size M) * m)"
proof (rule ccontr)
assume "¬ length p ≤ Suc (FSM.size M * m)"

let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

have "path M q []" using assms(3) by auto

have "path M q p"
and "length p ≤ k"
and "?f p = Some d"
and "∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ ?f p' = None"
using assms(4)
unfolding m_traversal_paths_with_witness_up_to_length_def paths_up_to_length_or_condition_with_witness_def
by auto

let ?p = "take (Suc (m * size M)) p"
let ?p' = "drop (Suc (m * size M)) p"
have "path M q ?p"
using ‹path M q p› using path_prefix[of M q ?p "drop (Suc (m * size M)) p"]
by simp
have "?p' ≠ []"
using ‹¬ length p ≤ Suc (FSM.size M * m)›
by (simp add: mult.commute)

have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono)
then have "length ?p ≤ m * (size M)"
using path_length_sum[OF ‹path M q ?p›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹¬ length p ≤ Suc (FSM.size M * m)›
by (simp add: mult.commute)
qed

then obtain q where "q ∈ states M"
and "length (filter (λ t . t_target t = q) ?p) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q ∈ fst d"
using assms(1) by blast
then have "⋀ t . t_target t = q ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q) ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
using filter_length_weakening[of "λ t . t_target t = q" "λ t . t_target t ∈ fst d"] by auto
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
using ‹length (filter (λ t . t_target t = q) ?p) ≥ Suc m› by auto
then have "?f ?p ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
then show ?thesis
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (take (Suc (m * FSM.size M)) p))›
diff_le_self le_trans not_less_eq_eq
by blast
qed
then obtain d' where "?f ?p = Some d'"
by blast

then have "p = ?p@?p' ∧ ?p' ≠ [] ∧ ?f ?p = Some d'"
using ‹?p' ≠ []› by auto

then show "False"
using ‹∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ (?f p') = None›
by (metis (no_types) option.distinct(1))
qed

lemma m_traversal_paths_with_witness_set :
assumes "⋀ q . q ∈ states M ⟹ ∃ d ∈ set D . q ∈ fst d"
and     "⋀ d .  d ∈ set D ⟹ snd d ⊆ fst d"
and     "q ∈ states M"
shows "(m_traversal_paths_with_witness M q D m)
= {(p,d) | p d . path M q p
∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) D = Some d
∧ (∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)}"
(is "?MTP = ?P")
proof -
let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

have "path M q []"
using assms(3) by auto

have "⋀ p . p ∈ ?MTP ⟹ p ∈ ?P"
unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def
paths_up_to_length_or_condition_with_witness_def
by force
moreover have "⋀ p . p ∈ ?P ⟹ p ∈ ?MTP"
proof -
fix px assume "px ∈ ?P"
then obtain p x where "px = (p,x)"
and p1: "path M q p"
and **: "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) D = Some x"
and ***:"(∀p' p''.
p = p' @ p'' ∧ p'' ≠ [] ⟶
find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)"
using prod.collapse by force

then have "(p,x) ∈ (m_traversal_paths_with_witness_up_to_length M q D m (length p))"
unfolding m_traversal_paths_with_witness_up_to_length_def paths_up_to_length_or_condition_with_witness_def
by force
then have "length p ≤ Suc (size M * m)"
using m_traversal_paths_with_witness_up_to_length_max_length[OF assms] by blast

have "(p,x) ∈ ?MTP"
using ‹path M q p› ‹length p ≤ Suc (size M * m)› ‹?f p = Some x›
‹∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ (?f p') = None›
unfolding m_traversal_paths_with_witness_def m_traversal_paths_with_witness_up_to_length_def
paths_up_to_length_or_condition_with_witness_def
by force
then show "px ∈ ?MTP"
using ‹px = (p,x)› by simp
qed
ultimately show ?thesis
by (meson subsetI subset_antisym)
qed

lemma maximal_repetition_sets_from_separators_cover :
assumes "q ∈ states M"
shows "∃ d ∈ (maximal_repetition_sets_from_separators M) . q ∈ fst d"
unfolding maximal_repetition_sets_from_separators_def
using maximal_pairwise_r_distinguishable_state_sets_from_separators_cover[OF assms] by auto

lemma maximal_repetition_sets_from_separators_d_reachable_subset :
shows "⋀ d . d ∈ (maximal_repetition_sets_from_separators M) ⟹ snd d ⊆ fst d"
unfolding maximal_repetition_sets_from_separators_def
by auto

(* Sufficient conditions for a path to be contained in the m-traversal paths *)
lemma m_traversal_paths_with_witness_set_containment :
assumes "q ∈ states M"
and     "path M q p"
and     "d ∈ set repSets"
and     "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)"
and     "⋀ p' p''.
p = p' @ p'' ⟹ p'' ≠ [] ⟹
¬ (∃d∈set repSets.
Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'))"
and     "⋀ q . q∈states M ⟹ ∃d∈set repSets. q ∈ fst d"
and     "⋀ d . d∈set repSets ⟹ snd d ⊆ fst d"
shows "∃ d' . (p,d') ∈ (m_traversal_paths_with_witness M q repSets m)"
proof -
obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p)) repSets = Some d'"
using assms(3,4) find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p))" repSets]
by auto
moreover have "(⋀ p' p''. p = p' @ p'' ⟹ p'' ≠ []
⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) repSets = None)"
using assms(5) find_None_iff[of _ repSets] by force
ultimately show ?thesis
using m_traversal_paths_with_witness_set[of M repSets q m, OF  assms(6,7,1)]
using assms(2) by blast
qed

lemma m_traversal_path_exist :
assumes "completely_specified M"
and     "q ∈ states M"
and     "inputs M ≠ {}"
and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
shows "∃ p' d' . (p',d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -

obtain p where "path M q p" and "length p = Suc ((size M) * m)"
using path_of_length_ex[OF assms(1-3)] by blast

let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

have "∃ q ∈ states M . length (filter (λt . t_target t = q) p) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) p))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) p) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) p) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) p)) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) p) ≤ m› by (meson sum_mono)
then have "length p ≤ m * (size M)"
using path_length_sum[OF ‹path M q p›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹length p = Suc ((size M) * m)›
by (simp add: mult.commute)
qed

then obtain q' where "q' ∈ states M"
and "length (filter (λ t . t_target t = q') p) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q' ∈ fst d"
using assms(4) by blast
then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q') p) ≤ length (filter (λ t . t_target t ∈ fst d) p)"
using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p)"
using ‹length (filter (λ t . t_target t = q') p) ≥ Suc m› by auto
then have "?f p ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p)"
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p)› by linarith
then show ?thesis
using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast
qed
then obtain d' where "?f p = Some d'"
by blast

show ?thesis proof (cases "(∀p' p''. p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
case True
then show ?thesis
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q p› ‹?f p = Some d'›
by blast
next
case False

define ps where ps_def: "ps = {p' . ∃ p''. p = p' @ p'' ∧ p'' ≠ []
∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
have "ps ≠ {}"
using False ps_def
by blast
moreover have "finite ps"
proof -
have "ps ⊆ set (prefixes p)"
unfolding prefixes_set ps_def
by blast
then show ?thesis
by (meson List.finite_set rev_finite_subset)
qed
ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
by (meson leI min_length_elem)
then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ []
⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof -
fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
moreover have "∃p'''. p = p'' @ p''' ∧ p''' ≠ []"
using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
ultimately have "p'' ∈ ps"
unfolding ps_def by auto
moreover have "length p'' < length p'"
using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
ultimately show "False"
using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
using leD by auto
qed
qed

have "path M q p'" and "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
using ‹path M q p› ‹p' ∈ ps› unfolding ps_def by auto
then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
by auto

then have "path M q p' ∧
find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
(∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None›
‹path M q p'›
by blast
then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
then show ?thesis by blast
qed
qed

lemma m_traversal_path_extension_exist :
assumes "completely_specified M"
and     "q ∈ states M"
and     "inputs M ≠ {}"
and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
and     "path M q p1"
and     "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D = None"
shows "∃ p2 d' . (p1@p2,d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -
obtain p2 where "path M (target q p1) p2" and "length p2 = (Suc ((size M) * m)) - length p1"
using path_of_length_ex[OF assms(1) path_target_is_state[OF assms(6)] assms(3)]
by blast

have "path M q (p1@p2)"
using assms(6) ‹path M (target q p1) p2› by auto

let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

have "length p1 < Suc ((size M) * m)"
proof (rule ccontr)
assume "¬ length p1 < Suc (FSM.size M * m)"
then have "length (take (Suc (FSM.size M * m)) p1) = Suc (FSM.size M * m)"
by auto
let ?p = "(take (Suc (FSM.size M * m)) p1)"

have "path M q ?p"
using ‹path M q p1›
by (metis append_take_drop_id path_append_elim)

have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono)
then have "length ?p ≤ m * (size M)"
using path_length_sum[OF ‹path M q ?p›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹length ?p = Suc ((size M) * m)›
by (simp add: mult.commute)
qed
then obtain q' where "q' ∈ states M"
and "length (filter (λ t . t_target t = q') ?p) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q' ∈ fst d"
using assms(4) by blast
then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q') ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
using ‹length (filter (λ t . t_target t = q') ?p) ≥ Suc m› by auto
moreover have "length (filter (λt. t_target t ∈ fst d) ?p) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
proof -
have "⋀ xs P n . length (filter P (take n xs)) ≤ length (filter P xs)"
by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)
then show ?thesis by auto
qed
ultimately have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)"
by auto
then have "?f p1 ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p1)"
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)› by linarith
then show ?thesis
using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast
qed
then obtain d' where "?f p1 = Some d'"
by blast
then show "False"
using assms(7) by simp
qed

have "length (p1@p2) = (Suc ((size M) * m))"
using ‹length p2 = (Suc ((size M) * m)) - length p1›
‹length p1 < Suc ((size M) * m)›
by simp

have "∃ q ∈ states M . length (filter (λt . t_target t = q) (p1@p2)) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) (p1@p2)))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) (p1@p2))) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) (p1@p2)) ≤ m› by (meson sum_mono)
then have "length (p1@p2) ≤ m * (size M)"
using path_length_sum[OF ‹path M q (p1@p2)›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹length (p1@p2) = Suc ((size M) * m)›
by (simp add: mult.commute)
qed
then obtain q' where "q' ∈ states M"
and "length (filter (λ t . t_target t = q') (p1@p2)) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q' ∈ fst d"
using assms(4) by blast
then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q') (p1@p2)) ≤ length (filter (λ t . t_target t ∈ fst d) (p1@p2))"
using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"]
by blast
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) (p1@p2))"
using ‹length (filter (λ t . t_target t = q') (p1@p2)) ≥ Suc m› by auto
then have "?f (p1@p2) ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) (p1@p2))"
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (p1@p2))› by linarith
then show ?thesis
using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast
qed
then obtain d' where "?f (p1@p2) = Some d'"
by blast

show ?thesis proof (cases "(∀p' p''. (p1@p2) = p' @ p'' ∧ p'' ≠ []
⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
case True
then show ?thesis
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q (p1@p2)› ‹?f (p1@p2) = Some d'›
by blast
next
case False

define ps where ps_def: "ps = {p' . ∃ p''. (p1@p2) = p' @ p'' ∧ p'' ≠ []
∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
have "ps ≠ {}" using False ps_def by blast
moreover have "finite ps"
proof -
have "ps ⊆ set (prefixes (p1@p2))"
unfolding prefixes_set ps_def
by auto
then show ?thesis
by (meson List.finite_set rev_finite_subset)
qed
ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
by (meson leI min_length_elem)
then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ []
⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof -
fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
moreover have "∃p'''. (p1@p2) = p'' @ p''' ∧ p''' ≠ []"
using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
ultimately have "p'' ∈ ps"
unfolding ps_def by auto
moreover have "length p'' < length p'"
using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
ultimately show "False"
using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
using leD by auto
qed
qed

obtain p'' where "(p1@p2) = p' @ p''"
and   "p'' ≠ []"
and   "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
using ‹p' ∈ ps› unfolding ps_def by blast
then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
by auto

have "path M q p'"
using ‹path M q (p1@p2)›  unfolding ‹(p1@p2) = p' @ p''› by auto

have "length p' > length p1"
proof (rule ccontr)
assume "¬ length p1 < length p'"
then obtain i where "p' = take i p1"
by (metis ‹p1 @ p2 = p' @ p''› append_eq_append_conv_if less_le)

have "⋀ i . find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D = None"
proof -
fix i
show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))) D ≠ None"
then obtain d where "d ∈ set D"
and   "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1))"
using find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i p1)))" D]
by meson

moreover have "length (filter (λt. t_target t ∈ fst d) (take i p1)) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
using filter_take_length by metis
ultimately have "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
using le_trans by blast
then show "False"
using ‹d ∈ set D› assms(7) unfolding find_None_iff
by blast
qed
qed

then have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
unfolding ‹p' = take i p1› by blast
then show "False"
using ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None›
by auto
qed

moreover have "p' = take (length p') (p1@p2)"
using ‹(p1@p2) = p' @ p''› by auto

ultimately obtain p where "p' = p1 @ p"
by auto

have "path M q p' ∧
find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
(∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None›
‹path M q p'› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'›
by blast
then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
then show ?thesis unfolding ‹p' = p1 @ p› by blast
qed
qed

lemma m_traversal_path_extension_exist_for_transition :
assumes "completely_specified M"
and     "q ∈ states M"
and     "inputs M ≠ {}"
and     "⋀ q . q∈states M ⟹ ∃d∈set D. q ∈ fst d"
and     "⋀ d . d ∈ set D ⟹ snd d ⊆ fst d"
and     "path M q p1"
and     "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D = None"
and     "t ∈ transitions M"
and     "t_source t = target q p1"
shows "∃ p2 d' . (p1@[t]@p2,d') ∈ (m_traversal_paths_with_witness M q D m)"
proof -
let ?q = "(target q (p1 @ [t]))"
let ?p = "p1 @ [t]"

have "path M q ?p"
using ‹path M q p1› ‹t ∈ transitions M› ‹t_source t = target q p1› path_append_transition by simp

obtain p2 where "path M ?q p2" and "length p2 = (Suc ((size M) * m)) - (length ?p)"
using path_of_length_ex[OF assms(1) path_target_is_state[OF ‹path M q (p1@[t])›] assms(3)]
by blast

have "path M q (?p@p2)"
using ‹path M q ?p› ‹path M ?q p2› by auto

let ?f = "(λ p . find (λ d . length (filter (λt . t_target t ∈ fst d) p) ≥ Suc (m - (card (snd d)))) D)"

have "length p1 < Suc ((size M) * m)"
proof (rule ccontr)
assume "¬ length p1 < Suc (FSM.size M * m)"
then have "length (take (Suc (FSM.size M * m)) p1) = Suc (FSM.size M * m)"
by auto
let ?p = "(take (Suc (FSM.size M * m)) p1)"

have "path M q ?p"
using ‹path M q p1›
by (metis append_take_drop_id path_append_elim)

have "∃ q ∈ states M . length (filter (λt . t_target t = q) ?p) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) ?p))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) ?p)) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) ?p) ≤ m› by (meson sum_mono)
then have "length ?p ≤ m * (size M)"
using path_length_sum[OF ‹path M q ?p›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹length ?p = Suc ((size M) * m)›
by (simp add: mult.commute)
qed
then obtain q' where "q' ∈ states M"
and "length (filter (λ t . t_target t = q') ?p) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q' ∈ fst d"
using assms(4) by blast
then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q') ?p) ≤ length (filter (λ t . t_target t ∈ fst d) ?p)"
using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"] by auto
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
using ‹length (filter (λ t . t_target t = q') ?p) ≥ Suc m› by auto
moreover have "length (filter (λt. t_target t ∈ fst d) ?p) ≤ length (filter (λt. t_target t ∈ fst d) p1)"
proof -
have "⋀ xs P n . length (filter P (take n xs)) ≤ length (filter P xs)"
by (metis append_take_drop_id filter_append le0 le_add_same_cancel1 length_append)
then show ?thesis by auto
qed
ultimately have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)"
by auto
then have "?f p1 ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) p1)"
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) p1)› by linarith
then show ?thesis
using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast
qed
then obtain d' where "?f p1 = Some d'"
by blast
then show "False"
using assms(7) by simp
qed

have "length (?p@p2) = (Suc ((size M) * m))"
using ‹length p2 = (Suc ((size M) * m)) - length ?p›
‹length p1 < Suc ((size M) * m)›
by simp

have "∃ q ∈ states M . length (filter (λt . t_target t = q) (?p@p2)) ≥ Suc m"
proof (rule ccontr)
assume "¬ (∃q∈states M. Suc m ≤ length (filter (λt. t_target t = q) (?p@p2)))"
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) < Suc m"
by auto
then have "∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) ≤ m"
by auto

have "(∑q∈states M. length (filter (λt. t_target t = q) (?p@p2))) ≤ (∑q∈states M . m)"
using ‹∀ q ∈ states M . length (filter (λt. t_target t = q) (?p@p2)) ≤ m› by (meson sum_mono)
then have "length (?p@p2) ≤ m * (size M)"
using path_length_sum[OF ‹path M q (?p@p2)›]
using fsm_states_finite[of M]
by (simp add: mult.commute)

then show "False"
using ‹length (?p@p2) = Suc ((size M) * m)›
by (simp add: mult.commute)
qed

then obtain q' where "q' ∈ states M"
and "length (filter (λ t . t_target t = q') (?p@p2)) ≥ Suc m"
by blast
then obtain d where "d ∈ set D"
and "q' ∈ fst d"
using assms(4) by blast
then have "⋀ t . t_target t = q' ⟹ t_target t ∈ fst d" by auto
then have "length (filter (λ t . t_target t = q') (?p@p2)) ≤ length (filter (λ t . t_target t ∈ fst d) (?p@p2))"
using filter_length_weakening[of "λ t . t_target t = q'" "λ t . t_target t ∈ fst d"]
by blast
then have "Suc m ≤ length (filter (λt. t_target t ∈ fst d) (?p@p2))"
using ‹length (filter (λ t . t_target t = q') (?p@p2)) ≥ Suc m› by auto
then have "?f (?p@p2) ≠ None"
using assms(2)
proof -
have "∀p. find p D ≠ None ∨ ¬ p d"
by (metis ‹d ∈ set D› find_from)
have "Suc (m - card (snd d)) ≤ length (filter (λp. t_target p ∈ fst d) (?p@p2))"
using ‹Suc m ≤ length (filter (λt. t_target t ∈ fst d) (?p@p2))› by linarith
then show ?thesis
using ‹∀p. find p D ≠ None ∨ ¬ p d› by blast
qed
then obtain d' where "?f (?p@p2) = Some d'"
by blast

show ?thesis proof (cases "(∀p' p''. (?p@p2) = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)")
case True
obtain d' where "((?p@p2), d') ∈ m_traversal_paths_with_witness M q D m"
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q (?p@p2)› ‹?f (?p@p2) = Some d'› True by force
then show ?thesis
unfolding append.assoc[symmetric] by blast
next
case False

show ?thesis proof (cases "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)) D")
case (Some a)

have *: "(∀p' p''. ?p = p' @ p'' ∧ p'' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None)"
proof -
have "⋀ p' p''. ?p = p' @ p'' ⟹ p'' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
proof -
fix p' p'' assume "?p = p' @ p''" and "p'' ≠ []"
then have "length p' ≤ length p1" by (induction p'' rule: rev_induct; auto)
moreover have "p' = take (length p') ?p"
unfolding ‹?p = p' @ p''› by auto
ultimately have "p' = take (length p') p1"
by auto

show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
moreover have "⋀ x . length (filter (λt. t_target t ∈ fst x) p') ≤ length (filter (λt. t_target t ∈ fst x) p1)"
using ‹p' = take (length p') p1›
by (metis filter_take_length)
ultimately have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p1)) D ≠ None"
unfolding find_None_iff
using le_trans by blast
then show "False"
using assms(7) by simp
qed
qed
then show ?thesis by blast
qed

obtain d' where "(?p, d') ∈ m_traversal_paths_with_witness M q D m"
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] ‹path M q ?p› Some * by force
then show ?thesis
by fastforce
next
case None

define ps where ps_def: "ps = {p' . ∃ p''. (?p@p2) = p' @ p''
∧ p'' ≠ []
∧ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None}"
have "ps ≠ {}" using False ps_def by blast
moreover have "finite ps"
proof -
have "ps ⊆ set (prefixes (?p@p2))"
unfolding prefixes_set ps_def
by auto
then show ?thesis
by (meson List.finite_set rev_finite_subset)
qed
ultimately obtain p' where "p' ∈ ps" and "⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''"
by (meson leI min_length_elem)
then have "⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof -
fix p'' p''' assume "p' = p'' @ p'''" and "p''' ≠ []"
show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D ≠ None"
moreover have "∃p'''. (?p@p2) = p'' @ p''' ∧ p''' ≠ []"
using ‹p' ∈ ps› ‹p' = p'' @ p'''› unfolding ps_def by auto
ultimately have "p'' ∈ ps"
unfolding ps_def by auto
moreover have "length p'' < length p'"
using ‹p''' ≠ []› ‹p' = p'' @ p'''› by auto
ultimately show "False"
using ‹⋀ p'' . p'' ∈ ps ⟹ length p' ≤ length p''›
using leD by auto
qed
qed

obtain p'' where "(?p@p2) = p' @ p''"
and   "p'' ≠ []"
and   "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None"
using ‹p' ∈ ps› unfolding ps_def by blast
then obtain d' where "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'"
by auto

have "path M q p'"
using ‹path M q (?p@p2)›  unfolding ‹(?p@p2) = p' @ p''› by auto

have "length p' > length ?p"
proof (rule ccontr)

assume "¬ length ?p < length p'"
then obtain i where "p' = take i ?p"
by (metis ‹?p @ p2 = p' @ p''› append_eq_append_conv_if less_le)

have "⋀ i . find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D = None"
proof -
fix i
show "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D = None"
proof (rule ccontr)
assume "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))) D ≠ None"
then obtain d where "d ∈ set D"
and   "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p))"
using find_None_iff[of "(λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) (take i ?p)))" D]
by meson

moreover have "length (filter (λt. t_target t ∈ fst d) (take i ?p)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
using filter_take_length by metis
ultimately have "Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) ?p)"
using le_trans by blast
then show "False"
using ‹d ∈ set D› None unfolding find_None_iff
by blast
qed
qed

then have "find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = None"
unfolding ‹p' = take i ?p› by blast
then show "False"
using ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D ≠ None›
by auto
qed

moreover have "p' = take (length p') (?p@p2)"
using ‹(?p@p2) = p' @ p''› by auto

ultimately obtain p where "p' = ?p @ p"
by (metis dual_order.strict_implies_order take_all take_append)

have "path M q p' ∧
find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d' ∧
(∀p'' p'''. p' = p'' @ p''' ∧ p''' ≠ [] ⟶ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None)"
using ‹⋀p'' p''' . p' = p'' @ p''' ⟹ p''' ≠ [] ⟹ find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p'')) D = None› ‹path M q p'› ‹find (λd. Suc (m - card (snd d)) ≤ length (filter (λt. t_target t ∈ fst d) p')) D = Some d'›
by blast
then have "(p',d') ∈ (m_traversal_paths_with_witness M q D m)"
using m_traversal_paths_with_witness_set[OF assms(4,5,2), of m] by blast
then show ?thesis unfolding ‹p' = ?p @ p› by fastforce
qed
qed
qed

end```