Theory ASC_LB

theory ASC_LB
imports "../ATC/ATC" "../FSM/FSM_Product"
begin

section ‹ The lower bound function ›

text ‹
This theory defines the lower bound function @{verbatim LB} and its properties.

Function @{verbatim LB} calculates a lower bound on the number of states of some FSM in order for
some sequence to not contain certain repetitions.
›

subsection ‹ Permutation function Perm ›

text ‹
Function @{verbatim Perm} calculates all possible reactions of an FSM to a set of inputs sequences
such that every set in the calculated set of reactions contains exactly one reaction for each input
sequence.
›

fun Perm :: "'in list set ⇒ ('in, 'out, 'state) FSM ⇒ ('in × 'out) list set set" where
  "Perm V M = {image f V | f . ∀ v ∈ V . f v ∈ language_state_for_input M (initial M) v }"

lemma perm_empty :
  assumes "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
shows "[] ∈ V''"
proof -
  have init_seq : "[] ∈ V" using det_state_cover_empty assms by simp
  obtain f where f_def : "V'' = image f V
                                ∧ (∀ v ∈ V . f v ∈ language_state_for_input M1 (initial M1) v)"
    using assms by auto
  then have "f [] = []"
    using init_seq by (metis language_state_for_input_empty singleton_iff)
  then show ?thesis
    using init_seq f_def by (metis image_eqI)
qed

lemma perm_elem_finite :
  assumes "is_det_state_cover M2 V"
  and     "well_formed M2"
  and     "V'' ∈ Perm V M1"
  shows "finite V''"
proof -
  obtain f where "is_det_state_cover_ass M2 f ∧ V = f ` d_reachable M2 (initial M2)"
    using assms by auto
  moreover have "finite (d_reachable M2 (initial M2))"
  proof -
    have "finite (nodes M2)"
      using assms by auto
    moreover have "nodes M2 = reachable M2 (initial M2)"
      by auto
    ultimately have "finite (reachable M2 (initial M2))"
      by simp
    moreover have "d_reachable M2 (initial M2) ⊆ reachable M2 (initial M2)"
      by auto
    ultimately show ?thesis
      using infinite_super by blast
  qed
  ultimately have "finite V"
    by auto
  moreover obtain f'' where "V'' = image f'' V
                              ∧ (∀ v ∈ V . f'' v ∈ language_state_for_input M1 (initial M1) v)"
    using assms(3) by auto
  ultimately show ?thesis
    by simp
qed

lemma perm_inputs :
  assumes "V'' ∈ Perm V M"
  and     "vs ∈ V''"
shows "map fst vs ∈ V"
proof -
  obtain f where f_def : "V'' = image f V
                          ∧ (∀ v ∈ V . f v ∈ language_state_for_input M (initial M) v)"
    using assms by auto
  then obtain v where v_def : "v ∈ V ∧ f v = vs"
    using assms by auto
  then have "vs ∈ language_state_for_input M (initial M) v"
    using f_def by auto
  then show ?thesis
    using v_def unfolding language_state_for_input.simps by auto
qed

lemma perm_inputs_diff :
  assumes "V'' ∈ Perm V M"
  and     "vs1 ∈ V''"
  and     "vs2 ∈ V''"
  and     "vs1 ≠ vs2"
shows "map fst vs1 ≠ map fst vs2"
proof -
  obtain f where f_def : "V'' = image f V
                          ∧ (∀ v ∈ V . f v ∈ language_state_for_input M (initial M) v)"
    using assms by auto
  then obtain v1 v2 where v_def : "v1 ∈ V ∧ f v1 = vs1 ∧ v2 ∈ V ∧ f v2 = vs2"
    using assms by auto
  then have "vs1 ∈ language_state_for_input M (initial M) v1"
            "vs2 ∈ language_state_for_input M (initial M) v2"
    using f_def by auto
  moreover have "v1 ≠ v2"
    using v_def assms(4) by blast
  ultimately show ?thesis
    by auto
qed

lemma perm_language :
  assumes "V'' ∈ Perm V M"
  and     "vs ∈ V''"
shows "vs ∈ L M"
proof -
  obtain f where f_def : "image f V = V''
                          ∧ (∀ v ∈ V . f v ∈ language_state_for_input M (initial M) v)"
    using assms(1) by auto
  then have "∃ v . f v = vs ∧ f v ∈ language_state_for_input M (initial M) v"
    using assms(2) by blast
  then show ?thesis
    by auto
qed




subsection ‹ Helper predicates ›

text ‹
The following predicates are used to combine often repeated assumption.
›

abbreviation "asc_fault_domain M2 M1 m ≡ (inputs M2 = inputs M1 ∧ card (nodes M1) ≤ m )"

lemma asc_fault_domain_props[elim!] :
  assumes "asc_fault_domain M2 M1 m"
  shows "inputs M2 = inputs M1"
        "card (nodes M1) ≤ m"using assms by auto

abbreviation
  "test_tools M2 M1 FAIL PM V Ω ≡ (
      productF M2 M1 FAIL PM
    ∧ is_det_state_cover M2 V
    ∧ applicable_set M2 Ω
   )"

lemma test_tools_props[elim] :
  assumes "test_tools M2 M1 FAIL PM V Ω"
  and     "asc_fault_domain M2 M1 m"
  shows "productF M2 M1 FAIL PM"
        "is_det_state_cover M2 V"
        "applicable_set M2 Ω"
        "applicable_set M1 Ω"
proof -
  show "productF M2 M1 FAIL PM" using assms(1) by blast
  show "is_det_state_cover M2 V" using assms(1) by blast
  show "applicable_set M2 Ω" using assms(1) by blast
  then show "applicable_set M1 Ω"
    unfolding applicable_set.simps applicable.simps
    using asc_fault_domain_props(1)[OF assms(2)] by simp
qed




lemma perm_nonempty :
  assumes "is_det_state_cover M2 V"
  and "OFSM M1"
  and "OFSM M2"
  and "inputs M1 = inputs M2"
shows "Perm V M1 ≠ {}"
proof -
  have "finite (nodes M2)"
    using assms(3) by auto
  moreover have "d_reachable M2 (initial M2) ⊆ nodes M2"
    by auto
  ultimately have "finite V"
    using det_state_cover_card[OF assms(1)]
    by (metis assms(1) finite_imageI infinite_super is_det_state_cover.elims(2))

  have "[] ∈ V"
    using assms(1) det_state_cover_empty by blast


  have "⋀ VS . VS ⊆ V ∧ VS ≠ {} ⟹ Perm VS M1 ≠ {}"
  proof -
    fix VS assume "VS ⊆ V ∧ VS ≠ {}"
    then have "finite VS" using ‹finite V›
      using infinite_subset by auto
    then show "Perm VS M1 ≠ {}"
      using ‹VS ⊆ V ∧ VS ≠ {}› ‹finite VS›
    proof (induction VS)
      case empty
      then show ?case by auto
    next
      case (insert vs F)
      then have "vs ∈ V" by blast

      obtain q2 where "d_reaches M2 (initial M2) vs q2"
        using det_state_cover_d_reachable[OF assms(1) ‹vs ∈ V›] by blast
      then obtain vs' vsP where io_path : "length vs = length vs'
                                            ∧ length vs = length vsP
                                            ∧ (path M2 ((vs || vs') || vsP) (initial M2))
                                            ∧ target ((vs || vs') || vsP) (initial M2) = q2"
        by auto

      have "well_formed M2"
        using assms by auto

      have "map fst (map fst ((vs || vs') || vsP)) = vs"
      proof -
        have "length (vs || vs') = length vsP"
          using io_path by simp
        then show ?thesis
          using io_path by auto
      qed
      moreover have "set (map fst (map fst ((vs || vs') || vsP))) ⊆ inputs M2"
        using path_input_containment[OF ‹well_formed M2›, of "(vs || vs') || vsP" "initial M2"]
              io_path
        by linarith
      ultimately have "set vs ⊆ inputs M2"
        by presburger

      then have "set vs ⊆ inputs M1"
        using assms by auto

      then have "L⇩i⇩n M1 {vs} ≠ {}"
        using assms(2) language_state_for_inputs_nonempty
        by (metis FSM.nodes.initial)
      then have "language_state_for_input M1 (initial M1) vs ≠ {}"
        by auto
      then obtain vs' where "vs' ∈ language_state_for_input M1 (initial M1) vs"
        by blast

      show ?case
      proof (cases "F = {}")
        case True
        moreover obtain f where "f vs = vs'"
          by moura
        ultimately have "image f (insert vs F) ∈ Perm (insert vs F) M1"
          using Perm.simps ‹vs' ∈ language_state_for_input M1 (initial M1) vs› by blast
        then show ?thesis by blast
      next
        case False
        then obtain F'' where "F'' ∈ Perm F M1"
          using insert.IH insert.hyps(1) insert.prems(1) by blast
        then obtain f where "F'' = image f F"
                            "(∀ v ∈ F . f v ∈ language_state_for_input M1 (initial M1) v)"
          by auto
        let ?f = "f(vs := vs')"
        have "∀ v ∈ (insert vs F) . ?f v ∈ language_state_for_input M1 (initial M1) v"
        proof
          fix v assume "v ∈ insert vs F"
          then show "?f v ∈ language_state_for_input M1 (initial M1) v"
          proof (cases "v = vs")
            case True
            then show ?thesis
              using ‹vs' ∈ language_state_for_input M1 (initial M1) vs› by auto
          next
            case False
            then have "v ∈ F"
              using ‹v ∈ insert vs F› by blast
            then show ?thesis
              using False ‹∀v∈F. f v ∈ language_state_for_input M1 (initial M1) v› by auto
          qed
        qed
        then have "image ?f (insert vs F) ∈ Perm (insert vs F) M1"
          using Perm.simps by blast
        then show ?thesis
          by blast
      qed
    qed
  qed

  then show ?thesis
    using ‹[] ∈ V› by blast
qed



lemma perm_elem :
  assumes "is_det_state_cover M2 V"
  and "OFSM M1"
  and "OFSM M2"
  and "inputs M1 = inputs M2"
  and "vs ∈ V"
  and "vs' ∈ language_state_for_input M1 (initial M1) vs"
obtains V''
where "V'' ∈ Perm V M1" "vs' ∈ V''"
proof -
  obtain V'' where "V'' ∈ Perm V M1"
    using perm_nonempty[OF assms(1-4)] by blast
  then obtain f where "V'' = image f V"
                      "(∀ v ∈ V . f v ∈ language_state_for_input M1 (initial M1) v)"
    by auto

  let ?f = "f(vs := vs')"

  have "∀ v ∈ V . (?f v) ∈ (language_state_for_input M1 (initial M1) v)"
    using ‹∀v∈V. (f v) ∈ (language_state_for_input M1 (initial M1) v)› assms(6) by fastforce

  then have "(image ?f V) ∈ Perm V M1"
    unfolding Perm.simps by blast
  moreover have "vs' ∈ image ?f V"
    by (metis assms(5) fun_upd_same imageI)
  ultimately show ?thesis
    using that by blast
qed



subsection ‹ Function R ›

text ‹
Function @{verbatim R} calculates the set of suffixes of a sequence that reach a given state if
applied after a given other sequence.
›


fun R :: "('in, 'out, 'state) FSM ⇒ 'state ⇒ ('in × 'out) list
          ⇒ ('in × 'out) list ⇒ ('in × 'out) list set"
  where
  "R M s vs xs = { vs@xs' | xs' . xs' ≠ []
                                ∧ prefix xs' xs
                                ∧ s ∈ io_targets M (initial M) (vs@xs') }"

lemma finite_R : "finite (R M s vs xs)"
proof -
  have "R M s vs xs ⊆ { vs @ xs' | xs' .prefix xs' xs }"
    by auto
  then have "R M s vs xs ⊆ image (λ xs' . vs @ xs') {xs' . prefix xs' xs}"
    by auto
  moreover have "{xs' . prefix xs' xs} = {take n xs | n . n ≤ length xs}"
  proof
    show "{xs'. prefix xs' xs} ⊆ {take n xs |n. n ≤ length xs}"
    proof
      fix xs' assume "xs' ∈ {xs'. prefix xs' xs}"
      then obtain zs' where "xs' @ zs' = xs"
        by (metis (full_types) mem_Collect_eq prefixE)
      then obtain i where "xs' = take i xs ∧ i ≤ length xs"
        by (metis (full_types) append_eq_conv_conj le_cases take_all)
      then show "xs' ∈ {take n xs |n. n ≤ length xs}"
        by auto
    qed
    show "{take n xs |n. n ≤ length xs} ⊆ {xs'. prefix xs' xs}"
      using take_is_prefix by force
  qed
  moreover have "finite {take n xs | n . n ≤ length xs}"
    by auto
  ultimately show ?thesis
    by auto
qed



lemma card_union_of_singletons :
  assumes "∀ S ∈ SS . (∃ t . S = {t})"
shows "card (⋃ SS) = card SS"
proof -
  let ?f = "λ x . {x}"
  have "bij_betw ?f (⋃ SS) SS"
    unfolding bij_betw_def inj_on_def using assms by fastforce
  then show ?thesis
    using bij_betw_same_card by blast
qed

lemma card_union_of_distinct :
  assumes "∀ S1 ∈ SS . ∀ S2 ∈ SS . S1 = S2 ∨ f S1 ∩ f S2 = {}"
  and     "finite SS"
  and     "∀ S ∈ SS . f S ≠ {}"
shows "card (image f SS) = card SS"
proof -
  from assms(2) have "∀ S1 ∈ SS . ∀ S2 ∈ SS . S1 = S2 ∨ f S1 ∩ f S2 = {}
                      ⟹ ∀ S ∈ SS . f S ≠ {} ⟹ ?thesis"
  proof (induction SS)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    then have "¬ (∃ y ∈ F . f y = f x)"
      by auto
    then have "f x ∉ image f F"
      by auto
    then have "card (image f (insert x F)) = Suc (card (image f F))"
      using insert by auto
    moreover have "card (f ` F) = card F"
      using insert by auto
    moreover have "card (insert x F) = Suc (card F)"
      using insert by auto
    ultimately show ?case
      by simp
  qed
  then show ?thesis
    using assms by simp
qed

lemma R_count :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "s ∈ nodes M2"
  and "productF M2 M1 FAIL PM"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "distinct (states (xs || tr) (q2,q1))"
shows "card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))) = card (R M2 s vs xs)"
  ― ‹each sequence in the set calculated by R reaches a different state in M1›
proof -

  ― ‹Proof sketch:
       - states of PM reached by the sequences calculated by R can differ only in their second value
       - the sequences in the set calculated by R reach different states in PM due to distinctness›

  have obs_PM : "observable PM" using observable_productF assms(2) assms(3) assms(7) by blast

  have state_component_2 : "∀ io ∈ (R M2 s vs xs) . io_targets M2 (initial M2) io = {s}"
  proof
    fix io assume "io ∈ R M2 s vs xs"
    then have "s ∈ io_targets M2 (initial M2) io"
      by auto
    moreover have "io ∈ language_state M2 (initial M2)"
      using calculation by auto
    ultimately show "io_targets M2 (initial M2) io = {s}"
      using assms(3) io_targets_observable_singleton_ex by (metis singletonD)
  qed

  moreover have "∀ io ∈ R M2 s vs xs . io_targets PM (initial PM) io
                    = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
  proof
    fix io assume io_assm : "io ∈ R M2 s vs xs"
    then have io_prefix : "prefix io (vs @ xs)"
      by auto
    then have io_lang_subs : "io ∈ L M1 ∧ io ∈ L M2"
      using assms(1) unfolding prefix_def by (metis IntE language_state language_state_split)
    then have io_lang_inter : "io ∈ L M1 ∩ L M2"
      by simp
    then have io_lang_pm : "io ∈ L PM"
      using productF_language assms by blast
    moreover obtain p2 p1 where "(p2,p1) ∈ io_targets PM (initial PM) io"
      by (metis assms(2) assms(3) assms(7) calculation insert_absorb insert_ident insert_not_empty
          io_targets_observable_singleton_ob observable_productF singleton_insert_inj_eq subrelI)
    ultimately have targets_pm : "io_targets PM (initial PM) io = {(p2,p1)}"
      using assms io_targets_observable_singleton_ex singletonD by (metis observable_productF)
    then obtain trP where trP_def : "target (io || trP) (initial PM) = (p2,p1)
                                      ∧ path PM (io || trP) (initial PM)
                                      ∧ length io = length trP"
      proof -
        assume a1: "⋀trP. target (io || trP) (initial PM) = (p2, p1)
                            ∧ path PM (io || trP) (initial PM)
                            ∧ length io = length trP ⟹ thesis"
        have "∃ps. target (io || ps) (initial PM) = (p2, p1)
                    ∧ path PM (io || ps) (initial PM) ∧ length io = length ps"
          using ‹(p2, p1) ∈ io_targets PM (initial PM) io› by auto
        then show ?thesis
          using a1 by blast
      qed
      then have trP_unique : "{ tr . path PM (io || tr) (initial PM) ∧ length io = length tr }
                              = { trP }"
        using observable_productF observable_path_unique_ex[of PM io "initial PM"]
              io_lang_pm assms(2) assms(3) assms(7)
      proof -
        obtain pps :: "('d × 'c) list" where
          f1: "{ps. path PM (io || ps) (initial PM) ∧ length io = length ps} = {pps}
                ∨ ¬ observable PM"
          by (metis (no_types) ‹⋀thesis. ⟦observable PM; io ∈ L PM; ⋀tr.
                                          {t. path PM (io || t) (initial PM)
                                          ∧ length io = length t} = {tr} ⟹ thesis⟧ ⟹ thesis›
              io_lang_pm)
        have f2: "observable PM"
          by (meson ‹observable M1› ‹observable M2› ‹productF M2 M1 FAIL PM› observable_productF)
        then have "trP ∈ {pps}"
          using f1 trP_def by blast
        then show ?thesis
          using f2 f1 by force
      qed


    obtain trIO2 where trIO2_def : "{tr . path M2 (io||tr) (initial M2) ∧ length io = length tr}
                                    = { trIO2 }"
      using observable_path_unique_ex[of M2 io "initial M2"] io_lang_subs assms(3) by blast
    obtain trIO1 where trIO1_def : "{tr . path M1 (io||tr) (initial M1) ∧ length io = length tr}
                                    = { trIO1 }"
      using observable_path_unique_ex[of M1 io "initial M1"] io_lang_subs assms(2) by blast

    have "path PM (io || trIO2 || trIO1) (initial M2, initial M1)
          ∧ length io = length trIO2
          ∧ length trIO2 = length trIO1"
    proof -
      have f1: "path M2 (io || trIO2) (initial M2) ∧ length io = length trIO2"
        using trIO2_def by auto
      have f2: "path M1 (io || trIO1) (initial M1) ∧ length io = length trIO1"
        using trIO1_def by auto
      then have "length trIO2 = length trIO1"
        using f1 by presburger
      then show ?thesis
        using f2 f1 assms(4) assms(5) assms(7) by blast
    qed
    then have trP_split : "path PM (io || trIO2 || trIO1) (initial PM)
                            ∧ length io = length trIO2
                            ∧ length trIO2 = length trIO1"
      using assms(7) by auto
    then have trP_zip : "trIO2 || trIO1 = trP"
      using trP_def trP_unique using length_zip by fastforce

    have "target (io || trIO2) (initial M2) = p2
          ∧ path M2 (io || trIO2) (initial M2)
          ∧ length io = length trIO2"
      using trP_zip trP_split assms(7) trP_def trIO2_def by auto
    then have "p2 ∈ io_targets M2 (initial M2) io"
      by auto
    then have targets_2 : "io_targets M2 (initial M2) io = {p2}"
      by (metis state_component_2 io_assm singletonD)

    have "target (io || trIO1) (initial M1) = p1
            ∧ path M1 (io || trIO1) (initial M1)
            ∧ length io = length trIO1"
      using trP_zip trP_split assms(7) trP_def trIO1_def by auto
    then have "p1 ∈ io_targets M1 (initial M1) io"
      by auto
    then have targets_1 : "io_targets M1 (initial M1) io = {p1}"
      by (metis io_lang_subs assms(2) io_targets_observable_singleton_ex singletonD)

    have "io_targets M2 (initial M2) io × io_targets M1 (initial M1) io = {(p2,p1)}"
      using targets_2 targets_1 by simp
    then show "io_targets PM (initial PM) io
                = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
      using targets_pm by simp
  qed

  ultimately have state_components : "∀ io ∈ R M2 s vs xs . io_targets PM (initial PM) io
                                      = {s} × io_targets M1 (initial M1) io"
    by auto

  then have "⋃ (image (io_targets PM (initial PM)) (R M2 s vs xs))
              = ⋃ (image (λ io . {s} × io_targets M1 (initial M1) io) (R M2 s vs xs))"
    by auto
  then have "⋃ (image (io_targets PM (initial PM)) (R M2 s vs xs))
              = {s} × ⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))"
    by auto
  then have "card (⋃ (image (io_targets PM (initial PM)) (R M2 s vs xs)))
              = card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs)))"
    by (metis (no_types) card_cartesian_product_singleton)

  moreover have "card (⋃ (image (io_targets PM (initial PM)) (R M2 s vs xs)))
                  = card (R M2 s vs xs)"
  proof (rule ccontr)
    assume assm : "card (⋃ (io_targets PM (initial PM) ` R M2 s vs xs) ) ≠ card (R M2 s vs xs)"

    have "∀ io ∈ R M2 s vs xs . io ∈ L PM"
    proof
      fix io assume io_assm : "io ∈ R M2 s vs xs"
      then have "prefix io (vs @ xs)"
        by auto
      then have "io ∈ L M1 ∧ io ∈ L M2"
        using assms(1) unfolding prefix_def by (metis IntE language_state language_state_split)
      then show "io ∈ L PM"
        using productF_language assms by blast
    qed
    then have singletons : "∀ io ∈ R M2 s vs xs . (∃ t . io_targets PM (initial PM) io = {t})"
      using io_targets_observable_singleton_ex observable_productF assms by metis
    then have card_targets : "card (⋃(io_targets PM (initial PM) ` R M2 s vs xs))
                              = card (image (io_targets PM (initial PM)) (R M2 s vs xs))"
      using finite_R card_union_of_singletons
            [of "image (io_targets PM (initial PM)) (R M2 s vs xs)"]
      by simp

    moreover have "card (image (io_targets PM (initial PM)) (R M2 s vs xs)) ≤ card (R M2 s vs xs)"
      using finite_R by (metis card_image_le)
    ultimately have card_le : "card (⋃(io_targets PM (initial PM) ` R M2 s vs xs))
                                < card (R M2 s vs xs)"
      using assm by linarith

    have "∃ io1 ∈ (R M2 s vs xs) . ∃ io2 ∈ (R M2 s vs xs) . io1 ≠ io2
            ∧ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2 ≠ {}"
    proof (rule ccontr)
      assume "¬ (∃io1∈R M2 s vs xs. ∃io2∈R M2 s vs xs. io1 ≠ io2
                  ∧ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2 ≠ {})"
      then have "∀io1∈R M2 s vs xs. ∀io2∈R M2 s vs xs. io1 = io2
                  ∨ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2 = {}"
        by blast
      moreover have "∀io∈R M2 s vs xs. io_targets PM (initial PM) io ≠ {}"
        by (metis insert_not_empty singletons)
      ultimately have "card (image (io_targets PM (initial PM)) (R M2 s vs xs))
                        = card (R M2 s vs xs)"
        using finite_R[of M2 s vs xs] card_union_of_distinct
              [of "R M2 s vs xs" "(io_targets PM (initial PM))"]
        by blast
      then show "False"
        using card_le card_targets by linarith
    qed

    then have "∃ io1 io2 . io1 ∈ (R M2 s vs xs)
                            ∧ io2 ∈ (R M2 s vs xs)
                            ∧ io1 ≠ io2
                            ∧ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2 ≠ {}"
      by blast
    moreover have "∀ io1 io2 . (io1 ∈ (R M2 s vs xs) ∧ io2 ∈ (R M2 s vs xs) ∧ io1 ≠ io2)
                                ⟶ length io1 ≠ length io2"
    proof (rule ccontr)
      assume " ¬ (∀io1 io2. io1 ∈ R M2 s vs xs ∧ io2 ∈ R M2 s vs xs ∧ io1 ≠ io2
                  ⟶ length io1 ≠ length io2)"
      then obtain io1 io2 where io_def : "io1 ∈ R M2 s vs xs
                                          ∧ io2 ∈ R M2 s vs xs
                                          ∧ io1 ≠ io2
                                          ∧ length io1 = length io2"
        by auto
      then have "prefix io1 (vs @ xs) ∧ prefix io2 (vs @ xs)"
        by auto
      then have "io1 = take (length io1) (vs @ xs) ∧ io2 = take (length io2) (vs @ xs)"
        by (metis append_eq_conv_conj prefixE)
      then show "False"
        using io_def by auto
    qed

    ultimately obtain io1 io2 where rep_ios_def :
      "io1 ∈ (R M2 s vs xs)
        ∧ io2 ∈ (R M2 s vs xs)
        ∧ length io1 < length io2
        ∧ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2 ≠ {}"
      by (metis inf_sup_aci(1) linorder_neqE_nat)

    obtain rep where "(s,rep) ∈ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2"
    proof -
      assume a1: "⋀rep. (s, rep) ∈ io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2
                        ⟹ thesis"
      have "∃f. Sigma {s} f ∩ (io_targets PM (initial PM) io1 ∩ io_targets PM (initial PM) io2)
                 ≠ {}"
        by (metis (no_types) inf.left_idem rep_ios_def state_components)
      then show ?thesis
        using a1 by blast
    qed
    then have rep_state : "io_targets PM (initial PM) io1 = {(s,rep)}
                            ∧ io_targets PM (initial PM) io2 = {(s,rep)}"
      by (metis Int_iff rep_ios_def singletonD singletons)

    obtain io1X io2X where rep_ios_split : "io1 = vs @ io1X
                                            ∧ prefix io1X xs
                                            ∧ io2 = vs @ io2X
                                            ∧ prefix io2X xs"
      using rep_ios_def by auto
    then have "length io1 > length vs"
      using rep_ios_def by auto


    ― ‹get a path from (initial PM) to (q2,q1)›

    have "vs@xs ∈ L PM"
      by (metis (no_types) assms(1) assms(4) assms(5) assms(7) inf_commute productF_language)
    then have "vs ∈ L PM"
      by (meson language_state_prefix)
    then obtain trV where trV_def : "{tr . path PM (vs || tr) (initial PM) ∧ length vs = length tr}
                                      = { trV }"
      using observable_path_unique_ex[of PM vs "initial PM"]
            assms(2) assms(3) assms(7) observable_productF
      by blast
    let ?qv = "target (vs || trV) (initial PM)"

    have "?qv ∈ io_targets PM (initial PM) vs"
      using trV_def by auto
    then have qv_simp[simp] : "?qv = (q2,q1)"
      using singletons assms by blast
    then have "?qv ∈ nodes PM"
      using trV_def assms by blast


    ― ‹get a path using io1X from the state reached by vs in PM›

    obtain tr1X_all where tr1X_all_def : "path PM (vs @ io1X || tr1X_all) (initial PM)
                                          ∧ length (vs @ io1X) = length tr1X_all"
      using rep_ios_def rep_ios_split by auto
    let ?tr1X = "drop (length vs) tr1X_all"
    have "take (length vs) tr1X_all = trV"
    proof -
      have "path PM (vs || take (length vs) tr1X_all) (initial PM)
            ∧ length vs = length (take (length vs) tr1X_all)"
        using tr1X_all_def trV_def
        by (metis (no_types, lifting) FSM.path_append_elim append_eq_conv_conj
            length_take zip_append1)
      then show "take (length vs) tr1X_all = trV"
        using trV_def by blast
    qed
    then have tr1X_def : "path PM (io1X || ?tr1X) ?qv ∧ length io1X = length ?tr1X"
    proof -
      have "length tr1X_all = length vs + length io1X"
        using tr1X_all_def by auto
      then have "length io1X = length tr1X_all - length vs"
        by presburger
      then show ?thesis
        by (metis (no_types) FSM.path_append_elim ‹take (length vs) tr1X_all = trV›
            length_drop tr1X_all_def zip_append1)
    qed
    then have io1X_lang : "io1X ∈ language_state PM ?qv"
      by auto
    then obtain tr1X' where tr1X'_def : "{tr . path PM (io1X || tr) ?qv ∧ length io1X = length tr}
                                          = { tr1X' }"
      using observable_path_unique_ex[of PM io1X ?qv]
            assms(2) assms(3) assms(7) observable_productF
      by blast
    moreover have "?tr1X ∈ { tr . path PM (io1X || tr) ?qv ∧ length io1X = length tr }"
      using tr1X_def by auto
    ultimately have tr1x_unique : "tr1X' = ?tr1X"
      by simp

    ― ‹get a path using io2X from the state reached by vs in PM›

    obtain tr2X_all where tr2X_all_def : "path PM (vs @ io2X || tr2X_all) (initial PM)
                                          ∧ length (vs @ io2X) = length tr2X_all"
      using rep_ios_def rep_ios_split by auto
    let ?tr2X = "drop (length vs) tr2X_all"
    have "take (length vs) tr2X_all = trV"
    proof -
      have "path PM (vs || take (length vs) tr2X_all) (initial PM)
            ∧ length vs = length (take (length vs) tr2X_all)"
        using tr2X_all_def trV_def
        by (metis (no_types, lifting) FSM.path_append_elim append_eq_conv_conj
            length_take zip_append1)
      then show "take (length vs) tr2X_all = trV"
        using trV_def by blast
    qed
    then have tr2X_def : "path PM (io2X || ?tr2X) ?qv ∧ length io2X = length ?tr2X"
    proof -
      have "length tr2X_all = length vs + length io2X"
        using tr2X_all_def by auto
      then have "length io2X = length tr2X_all - length vs"
        by presburger
      then show ?thesis
        by (metis (no_types) FSM.path_append_elim ‹take (length vs) tr2X_all = trV›
            length_drop tr2X_all_def zip_append1)
    qed
    then have io2X_lang : "io2X ∈ language_state PM ?qv" by auto
    then obtain tr2X' where tr2X'_def : "{tr . path PM (io2X || tr) ?qv ∧ length io2X = length tr}
                                          = { tr2X' }"
      using observable_path_unique_ex[of PM io2X ?qv] assms(2) assms(3) assms(7) observable_productF
      by blast
    moreover have "?tr2X ∈ { tr . path PM (io2X || tr) ?qv ∧ length io2X = length tr }"
      using tr2X_def by auto
    ultimately have tr2x_unique : "tr2X' = ?tr2X"
      by simp

    ― ‹both paths reach the same state›

    have "io_targets PM (initial PM) (vs @ io1X) = {(s,rep)}"
      using rep_state rep_ios_split by auto
    moreover have "io_targets PM (initial PM) vs = {?qv}"
      using assms(8) by auto
    ultimately have rep_via_1 : "io_targets PM ?qv io1X = {(s,rep)}"
      by (meson obs_PM observable_io_targets_split)
    then have rep_tgt_1 : "target (io1X || tr1X') ?qv = (s,rep)"
      using obs_PM observable_io_target_unique_target[of PM ?qv io1X "(s,rep)"] tr1X'_def by blast
    have length_1 : "length (io1X || tr1X') > 0"
      using ‹length vs < length io1› rep_ios_split tr1X_def tr1x_unique by auto

    have tr1X_alt_def : "tr1X' = take (length io1X) tr"
      by (metis (no_types) assms(10) assms(9) obs_PM observable_path_prefix qv_simp
          rep_ios_split tr1X_def tr1x_unique)
    moreover have "io1X = take (length io1X) xs"
      using rep_ios_split by (metis append_eq_conv_conj prefixE)
    ultimately have "(io1X || tr1X') = take (length io1X) (xs || tr)"
      by (metis take_zip)
    moreover have "length (xs || tr) ≥ length (io1X || tr1X')"
      by (metis (no_types) ‹io1X = take (length io1X) xs› assms(10) length_take length_zip
          nat_le_linear take_all tr1X_def tr1x_unique)
    ultimately have rep_idx_1 : "(states (xs || tr) ?qv) ! ((length io1X) - 1) = (s,rep)"
      by (metis (no_types, lifting) One_nat_def Suc_less_eq Suc_pred rep_tgt_1 length_1
          less_Suc_eq_le map_snd_zip scan_length scan_nth states_alt_def tr1X_def tr1x_unique)


    have "io_targets PM (initial PM) (vs @ io2X) = {(s,rep)}"
      using rep_state rep_ios_split by auto
    moreover have "io_targets PM (initial PM) vs = {?qv}"
      using assms(8) by auto
    ultimately have rep_via_2 : "io_targets PM ?qv io2X = {(s,rep)}"
      by (meson obs_PM observable_io_targets_split)
    then have rep_tgt_2 : "target (io2X || tr2X') ?qv = (s,rep)"
      using obs_PM observable_io_target_unique_target[of PM ?qv io2X "(s,rep)"] tr2X'_def by blast
    moreover have length_2 : "length (io2X || tr2X') > 0"
      by (metis ‹length vs < length io1› append.right_neutral length_0_conv length_zip less_asym min.idem neq0_conv rep_ios_def rep_ios_split tr2X_def tr2x_unique)

    have tr2X_alt_def : "tr2X' = take (length io2X) tr"
      by (metis (no_types) assms(10) assms(9) obs_PM observable_path_prefix qv_simp rep_ios_split tr2X_def tr2x_unique)
    moreover have "io2X = take (length io2X) xs"
      using rep_ios_split by (metis append_eq_conv_conj prefixE)
    ultimately have "(io2X || tr2X') = take (length io2X) (xs || tr)"
      by (metis take_zip)
    moreover have "length (xs || tr) ≥ length (io2X || tr2X')"
      using calculation by auto
    ultimately have rep_idx_2 : "(states (xs || tr) ?qv) ! ((length io2X) - 1) = (s,rep)"
      by (metis (no_types, lifting) One_nat_def Suc_less_eq Suc_pred rep_tgt_2 length_2
          less_Suc_eq_le map_snd_zip scan_length scan_nth states_alt_def tr2X_def tr2x_unique)


    ― ‹thus the distinctness assumption is violated›

    have "length io1X ≠ length io2X"
      by (metis ‹io1X = take (length io1X) xs› ‹io2X = take (length io2X) xs› less_irrefl
          rep_ios_def rep_ios_split)
    moreover have "(states (xs || tr) ?qv) ! ((length io1X) - 1)
                    = (states (xs || tr) ?qv) ! ((length io2X) - 1)"
      using rep_idx_1 rep_idx_2 by simp
    ultimately have "¬ (distinct (states (xs || tr) ?qv))"
      by (metis Suc_less_eq ‹io1X = take (length io1X) xs›
          ‹io1X || tr1X' = take (length io1X) (xs || tr)› ‹io2X = take (length io2X) xs›
          ‹io2X || tr2X' = take (length io2X) (xs || tr)›
          ‹length (io1X || tr1X') ≤ length (xs || tr)› ‹length (io2X || tr2X') ≤ length (xs || tr)›
          assms(10) diff_Suc_1 distinct_conv_nth gr0_conv_Suc le_imp_less_Suc length_1 length_2
          length_take map_snd_zip scan_length states_alt_def)
    then show "False"
      by (metis assms(11) states_alt_def)
  qed

  ultimately show ?thesis
    by linarith
qed



lemma R_state_component_2 :
  assumes "io ∈ (R M2 s vs xs)"
  and     "observable M2"
shows "io_targets M2 (initial M2) io = {s}"
proof -
  have "s ∈ io_targets M2 (initial M2) io"
    using assms(1) by auto
  moreover have "io ∈ language_state M2 (initial M2)"
    using calculation by auto
  ultimately show "io_targets M2 (initial M2) io = {s}"
    using assms(2) io_targets_observable_singleton_ex by (metis singletonD)
qed


lemma R_union_card_is_suffix_length :
  assumes "OFSM M2"
  and     "io@xs ∈ L M2"
shows "sum (λ q . card (R M2 q io xs)) (nodes M2) = length xs"
using assms proof (induction xs rule: rev_induct)
  case Nil
  show ?case
    by (simp add: sum.neutral)
next
  case (snoc x xs)

  have "finite (nodes M2)"
    using assms by auto

  have R_update : "⋀ q . R M2 q io (xs@[x]) = (if (q ∈ io_targets M2 (initial M2) (io @ xs @ [x]))
                                    then insert (io@xs@[x]) (R M2 q io xs)
                                    else R M2 q io xs)"
    by auto

  obtain q where "io_targets M2 (initial M2) (io @ xs @ [x]) = {q}"
    by (meson assms(1) io_targets_observable_singleton_ex snoc.prems(2))

  then have "R M2 q io (xs@[x]) = insert (io@xs@[x]) (R M2 q io xs)"
    using R_update by auto
  moreover have "(io@xs@[x]) ∉ (R M2 q io xs)"
    by auto
  ultimately have "card (R M2 q io (xs@[x])) = Suc (card (R M2 q io xs))"
    by (metis card_insert_disjoint finite_R)

  have "q ∈ nodes M2"
    by (metis (full_types) FSM.nodes.initial ‹io_targets M2 (initial M2) (io@xs @ [x]) = {q}›
        insertI1 io_targets_nodes)

  have "∀ q' . q' ≠ q ⟶ R M2 q' io (xs@[x]) = R M2 q' io xs"
    using ‹io_targets M2 (initial M2) (io@xs @ [x]) = {q}› R_update
    by auto
  then have "∀ q' . q' ≠ q ⟶ card (R M2 q' io (xs@[x])) = card (R M2 q' io xs)"
    by auto

  then have "(∑q∈(nodes M2 - {q}). card (R M2 q io (xs@[x])))
              = (∑q∈(nodes M2 - {q}). card (R M2 q io xs))"
    by auto
  moreover have "(∑q∈nodes M2. card (R M2 q io (xs@[x])))
                  = (∑q∈(nodes M2 - {q}). card (R M2 q io (xs@[x]))) + (card (R M2 q io (xs@[x])))"
                "(∑q∈nodes M2. card (R M2 q io xs))
                  = (∑q∈(nodes M2 - {q}). card (R M2 q io xs)) + (card (R M2 q io xs))"
  proof -
    have "∀C c f. (infinite C ∨ (c::'c) ∉ C) ∨ sum f C = (f c::nat) + sum f (C - {c})"
      by (meson sum.remove)
    then show "(∑q∈nodes M2. card (R M2 q io (xs@[x])))
                = (∑q∈(nodes M2 - {q}). card (R M2 q io (xs@[x]))) + (card (R M2 q io (xs@[x])))"
              "(∑q∈nodes M2. card (R M2 q io xs))
                = (∑q∈(nodes M2 - {q}). card (R M2 q io xs)) + (card (R M2 q io xs))"
      using ‹finite (nodes M2)› ‹q ∈ nodes M2› by presburger+
  qed
  ultimately have "(∑q∈nodes M2. card (R M2 q io (xs@[x])))
                    = Suc (∑q∈nodes M2. card (R M2 q io xs))"
    using ‹card (R M2 q io (xs@[x])) = Suc (card (R M2 q io xs))›
    by presburger

  have "(∑q∈nodes M2. card (R M2 q io xs)) = length xs"
    using snoc.IH snoc.prems language_state_prefix[of "io@xs" "[x]" M2 "initial M2"]
  proof -
    show ?thesis
      by (metis (no_types) ‹(io @ xs) @ [x] ∈ L M2 ⟹ io @ xs ∈ L M2›
          ‹OFSM M2› ‹io @ xs @ [x] ∈ L M2› append.assoc snoc.IH)
  qed

  show ?case
  proof -
    show ?thesis
      by (metis (no_types)
          ‹(∑q∈nodes M2. card (R M2 q io (xs @ [x]))) = Suc (∑q∈nodes M2. card (R M2 q io xs))›
          ‹(∑q∈nodes M2. card (R M2 q io xs)) = length xs› length_append_singleton)
  qed
qed

lemma R_state_repetition_via_long_sequence :
  assumes "OFSM M"
  and     "card (nodes M) ≤ m"
  and     "Suc (m * m) ≤ length xs"
  and     "vs@xs ∈ L M"
shows "∃ q ∈ nodes M . card (R M q vs xs) > m"
proof (rule ccontr)
  assume "¬ (∃q∈nodes M. m < card (R M q vs xs))"
  then have "∀ q ∈ nodes M . card (R M q vs xs) ≤ m"
    by auto
  then have "sum (λ q . card (R M q vs xs)) (nodes M) ≤ sum (λ q . m) (nodes M)"
    by (meson sum_mono)
  moreover have "sum (λ q . m) (nodes M) ≤ m * m"
    using assms(2) by auto
  ultimately have "sum (λ q . card (R M q vs xs)) (nodes M) ≤ m * m"
    by presburger

  moreover have "Suc (m*m) ≤ sum (λ q . card (R M q vs xs)) (nodes M)"
    using R_union_card_is_suffix_length[OF assms(1), of vs xs] assms(4,3) by auto
  ultimately show "False" by simp
qed

lemma R_state_repetition_distribution :
  assumes "OFSM M"
  and     "Suc (card (nodes M) * m) ≤ length xs"
  and     "vs@xs ∈ L M"
shows "∃ q ∈ nodes M . card (R M q vs xs) > m"
proof (rule ccontr)
  assume "¬ (∃q∈nodes M. m < card (R M q vs xs))"
  then have "∀ q ∈ nodes M . card (R M q vs xs) ≤ m"
    by auto
  then have "sum (λ q . card (R M q vs xs)) (nodes M) ≤ sum (λ q . m) (nodes M)"
    by (meson sum_mono)
  moreover have "sum (λ q . m) (nodes M) ≤ card (nodes M) * m"
    using assms(2) by auto
  ultimately have "sum (λ q . card (R M q vs xs)) (nodes M) ≤ card (nodes M) * m"
    by presburger

  moreover have "Suc (card (nodes M)*m) ≤ sum (λ q . card (R M q vs xs)) (nodes M)"
    using R_union_card_is_suffix_length[OF assms(1), of vs xs] assms(3,2) by auto
  ultimately show "False"
    by simp
qed



subsection ‹ Function RP ›

text ‹
Function @{verbatim RP} extends function @{verbatim MR} by adding all elements from a set of
IO-sequences that also reach the given state.
›


fun RP :: "('in, 'out, 'state) FSM ⇒ 'state ⇒ ('in × 'out) list
            ⇒ ('in × 'out) list ⇒ ('in × 'out) list set
            ⇒ ('in × 'out) list set"
  where
  "RP M s vs xs V'' = R M s vs xs
                      ∪ {vs' ∈ V'' . io_targets M (initial M) vs' = {s}}"

lemma RP_from_R:
  assumes "is_det_state_cover M2 V"
  and     "V'' ∈ Perm V M1"
shows "RP M2 s vs xs V'' = R M2 s vs xs
        ∨ (∃ vs' ∈ V'' . vs' ∉ R M2 s vs xs ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs))"
proof (rule ccontr)
  assume assm : "¬ (RP M2 s vs xs V'' = R M2 s vs xs ∨
        (∃vs'∈V''. vs' ∉ R M2 s vs xs ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs)))"

  moreover have "R M2 s vs xs ⊆ RP M2 s vs xs V''"
    by simp
  moreover have "RP M2 s vs xs V'' ⊆ R M2 s vs xs ∪ V''"
    by auto
  ultimately obtain vs1 vs2 where vs_def :
       "vs1 ≠ vs2 ∧ vs1 ∈ V'' ∧ vs2 ∈ V''
        ∧ vs1 ∉ R M2 s vs xs ∧ vs2 ∉ R M2 s vs xs
        ∧ vs1 ∈ RP M2 s vs xs V'' ∧ vs2 ∈ RP M2 s vs xs V''"
    by blast

  then have "io_targets M2 (initial M2) vs1 = {s} ∧ io_targets M2 (initial M2) vs2 = {s}"
    by (metis (mono_tags, lifting) RP.simps Un_iff mem_Collect_eq)
  then have "io_targets M2 (initial M2) vs1 = io_targets M2 (initial M2) vs2"
    by simp

  obtain f where f_def : "is_det_state_cover_ass M2 f ∧ V = f ` d_reachable M2 (initial M2)"
    using assms by auto
  moreover have "V = image f (d_reachable M2 (initial M2))"
    using f_def by blast
  moreover have "map fst vs1 ∈ V ∧ map fst vs2 ∈ V"
    using assms(2) perm_inputs vs_def by blast
  ultimately obtain r1 r2 where r_def :
    "f r1 = map fst vs1 ∧ r1 ∈ d_reachable M2 (initial M2)"
    "f r2 = map fst vs2 ∧ r2 ∈ d_reachable M2 (initial M2)"
    by force
  then have "d_reaches M2 (initial M2) (map fst vs1) r1"
            "d_reaches M2 (initial M2) (map fst vs2) r2"
    by (metis f_def is_det_state_cover_ass.elims(2))+

  then have "io_targets M2 (initial M2) vs1 ⊆ {r1}"
    using d_reaches_io_target[of M2 "initial M2" "map fst vs1" r1 "map snd vs1"] by simp
  moreover have "io_targets M2 (initial M2) vs2 ⊆ {r2}"
    using d_reaches_io_target[of M2 "initial M2" "map fst vs2" r2 "map snd vs2"]
          ‹d_reaches M2 (initial M2) (map fst vs2) r2› by auto
  ultimately have "r1 = r2"
    using ‹io_targets M2 (initial M2) vs1 = {s} ∧ io_targets M2 (initial M2) vs2 = {s}› by auto

  have "map fst vs1 ≠ map fst vs2"
    using assms(2) perm_inputs_diff vs_def by blast
  then have "r1 ≠ r2"
    using r_def(1) r_def(2) by force

  then show "False"
    using ‹r1 = r2› by auto
qed

lemma finite_RP :
  assumes "is_det_state_cover M2 V"
  and     "V'' ∈ Perm V M1"
shows "finite (RP M2 s vs xs V'')"
  using assms RP_from_R finite_R by (metis finite_insert)




lemma RP_count :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "s ∈ nodes M2"
  and "productF M2 M1 FAIL PM"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "distinct (states (xs || tr) (q2,q1))"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "∀ s' ∈ set (states (xs || map fst tr) q2) . ¬ (∃ v ∈ V . d_reaches M2 (initial M2) v s')"
shows "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) = card (RP M2 s vs xs V'')"
  ― ‹each sequence in the set calculated by RP reaches a different state in M1›
proof -

  ― ‹Proof sketch:
     - RP calculates either the same set as R or the set of R and an additional element
     - in the first case, the result for R applies
     - in the second case, the additional element is not contained in the set calcualted by R due to
       the assumption that no state reached by a non-empty prefix of xs after vs is also reached by
       some sequence in V (see the last two assumptions)›


  have RP_cases : "RP M2 s vs xs V'' = R M2 s vs xs
                    ∨ (∃ vs' ∈ V'' . vs' ∉ R M2 s vs xs
                                      ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs))"
    using RP_from_R assms by metis
  show ?thesis
  proof (cases "RP M2 s vs xs V'' = R M2 s vs xs")
    case True
    then show ?thesis using R_count assms by metis
  next
    case False
    then obtain vs' where vs'_def : "vs' ∈ V''
                                      ∧ vs' ∉ R M2 s vs xs
                                      ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs)"
      using RP_cases by auto

    have obs_PM : "observable PM"
      using observable_productF assms(2) assms(3) assms(7) by blast

    have state_component_2 : "∀ io ∈ (R M2 s vs xs) . io_targets M2 (initial M2) io = {s}"
    proof
      fix io assume "io ∈ R M2 s vs xs"
      then have "s ∈ io_targets M2 (initial M2) io"
        by auto
      moreover have "io ∈ language_state M2 (initial M2)"
        using calculation by auto
      ultimately show "io_targets M2 (initial M2) io = {s}"
        using assms(3) io_targets_observable_singleton_ex by (metis singletonD)
    qed

    have "vs' ∈ L M1"
      using assms(13) perm_language vs'_def by blast
    then obtain s' where s'_def : "io_targets M1 (initial M1) vs' = {s'}"
      by (meson assms(2) io_targets_observable_singleton_ob)

    moreover have "s' ∉ ⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))"
    proof (rule ccontr)
      assume "¬ s' ∉ ⋃(io_targets M1 (initial M1) ` R M2 s vs xs)"
      then obtain xs' where xs'_def : "vs @ xs' ∈ R M2 s vs xs ∧ s' ∈ io_targets M1 (initial M1) (vs @ xs')"
      proof -
        assume a1: "⋀xs'. vs @ xs' ∈ R M2 s vs xs ∧ s' ∈ io_targets M1 (initial M1) (vs @ xs')
                          ⟹ thesis"
        obtain pps :: "('a × 'b) list set ⇒ (('a × 'b) list ⇒ 'c set) ⇒ 'c ⇒ ('a × 'b) list"
          where
          "∀x0 x1 x2. (∃v3. v3 ∈ x0 ∧ x2 ∈ x1 v3) = (pps x0 x1 x2 ∈ x0 ∧ x2 ∈ x1 (pps x0 x1 x2))"
          by moura
        then have f2: "pps (R M2 s vs xs) (io_targets M1 (initial M1)) s' ∈ R M2 s vs xs
                        ∧ s' ∈ io_targets M1 (initial M1) (pps (R M2 s vs xs)
                                              (io_targets M1 (initial M1)) s')"
          using ‹¬ s' ∉ ⋃(io_targets M1 (initial M1) ` R M2 s vs xs)› by blast
        then have "∃ps. pps (R M2 s vs xs) (io_targets M1 (initial M1)) s' = vs @ ps
                        ∧ ps ≠ [] ∧ prefix ps xs ∧ s ∈ io_targets M2 (initial M2) (vs @ ps)"
          by simp
        then show ?thesis
          using f2 a1 by (metis (no_types))
      qed
      then obtain tr' where tr'_def : "path M2 (vs @ xs' || tr') (initial M2)
                                        ∧ length tr' = length (vs @ xs')"
        by auto

      then obtain trV' trX' where tr'_split : "trV' = take (length vs) tr'"
                                              "trX' = drop (length vs) tr'"
                                              "tr' = trV' @ trX'"
        by fastforce
      then have "path M2 (vs || trV') (initial M2) ∧ length trV' = length vs"
        by (metis (no_types) FSM.path_append_elim ‹trV' = take (length vs) tr'›
            append_eq_conv_conj length_take tr'_def zip_append1)




      have "initial PM = (initial M2, initial M1)"
        using assms(7) by simp
      moreover have "vs ∈ L M2" "vs ∈ L M1"
        using assms(1) language_state_prefix by auto
      ultimately have "io_targets M1 (initial M1) vs = {q1}"
                      "io_targets M2 (initial M2) vs = {q2}"
        using productF_path_io_targets[of M2 M1 FAIL PM "initial M2" "initial M1" vs q2 q1]
        by (metis FSM.nodes.initial assms(7) assms(8) assms(2) assms(3) assms(4) assms(5)
            io_targets_observable_singleton_ex singletonD)+

      then have "target (vs || trV') (initial M2) = q2"
        using ‹path M2 (vs || trV') (initial M2) ∧ length trV' = length vs› io_target_target
        by metis
      then have path_xs' : "path M2 (xs' || trX') q2 ∧ length trX' = length xs'"
        by (metis (no_types) FSM.path_append_elim
            ‹path M2 (vs || trV') (initial M2) ∧ length trV' = length vs›
            ‹target (vs || trV') (initial M2) = q2› append_eq_conv_conj length_drop tr'_def
            tr'_split(1) tr'_split(2) zip_append2)


      have "io_targets M2 (initial M2) (vs @ xs') = {s}"
        using state_component_2 xs'_def by blast
      then have "io_targets M2 q2 xs' = {s}"
        by (meson assms(3) observable_io_targets_split ‹io_targets M2 (initial M2) vs = {q2}›)
      then have target_xs' : "target (xs' || trX') q2 = s"
        using io_target_target path_xs' by metis
      moreover have "length xs' > 0"
        using xs'_def by auto
      ultimately have "last (states (xs' || trX') q2) = s"
        using path_xs' target_in_states by metis
      moreover have "length (states (xs' || trX') q2) > 0"
        using ‹0 < length xs'› path_xs' by auto
      ultimately have states_xs' : "s ∈ set (states (xs' || trX') q2)"
        using last_in_set by blast

      have "vs @ xs ∈ L M2"
        using assms by simp
      then obtain q' where "io_targets M2 (initial M2) (vs@xs) = {q'}"
        using io_targets_observable_singleton_ob[of M2 "vs@xs" "initial M2"] assms(3) by auto
      then have "xs ∈ language_state M2 q2"
        using assms(3) ‹io_targets M2 (initial M2) vs = {q2}›
              observable_io_targets_split[of M2 "initial M2" vs xs q' q2]
        by auto

      moreover have "path PM (xs || map fst tr || map snd tr) (q2,q1)
                      ∧ length xs = length (map fst tr)"
        using assms(7) assms(9) assms(10) productF_path_unzip by simp
      moreover have "xs ∈ language_state PM (q2,q1)"
        using assms(9) assms(10) by auto
      moreover have "q2 ∈ nodes M2"
        using ‹io_targets M2 (initial M2) vs = {q2}› io_targets_nodes
        by (metis FSM.nodes.initial insertI1)
      moreover have "q1 ∈ nodes M1"
        using ‹io_targets M1 (initial M1) vs = {q1}› io_targets_nodes
        by (metis FSM.nodes.initial insertI1)
      ultimately have path_xs : "path M2 (xs || map fst tr) q2"
        using productF_path_reverse_ob_2(1)[of xs "map fst tr" "map snd tr" M2 M1 FAIL PM q2 q1]
              assms(2,3,4,5,7)
        by simp



      moreover have "prefix xs' xs"
        using xs'_def by auto
      ultimately have "trX' = take (length xs') (map fst tr)"
        using ‹path PM (xs || map fst tr || map snd tr) (q2, q1) ∧ length xs = length (map fst tr)›
              assms(3) path_xs'
        by (metis observable_path_prefix)

      then have states_xs : "s ∈ set (states (xs || map fst tr) q2)"
        by (metis assms(10) in_set_takeD length_map map_snd_zip path_xs' states_alt_def states_xs')



      have "d_reaches M2 (initial M2) (map fst vs') s"
      proof -
        obtain fV where fV_def : "is_det_state_cover_ass M2 fV
                                  ∧ V = fV ` d_reachable M2 (initial M2)"
          using assms(12) by auto
        moreover have "V = image fV (d_reachable M2 (initial M2))"
          using fV_def by blast
        moreover have "map fst vs' ∈ V"
          using perm_inputs vs'_def assms(13) by metis
        ultimately obtain qv where qv_def : "fV qv = map fst vs' ∧ qv∈ d_reachable M2 (initial M2)"
          by force
        then have "d_reaches M2 (initial M2) (map fst vs') qv"
          by (metis fV_def is_det_state_cover_ass.elims(2))
        then have "io_targets M2 (initial M2) vs' ⊆ {qv}"
          using d_reaches_io_target[of M2 "initial M2" "map fst vs'" qv "map snd vs'"] by simp
        moreover have "io_targets M2 (initial M2) vs' = {s}"
          using vs'_def by (metis (mono_tags, lifting) RP.simps Un_iff insertI1 mem_Collect_eq)
        ultimately have "qv = s"
          by simp
        then show ?thesis
          using ‹d_reaches M2 (initial M2) (map fst vs') qv› by blast
      qed

      then show "False"  by (meson assms(14) assms(13) perm_inputs states_xs vs'_def)
    qed

    moreover have "⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs)))
                    = insert s' (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs)))"
      using s'_def by simp

    moreover have "finite (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs)))"
    proof
      show "finite (R M2 s vs xs)"
        using finite_R by simp
      show "⋀a. a ∈ R M2 s vs xs ⟹ finite (io_targets M1 (initial M1) a)"
      proof -
        fix a assume "a ∈ R M2 s vs xs"
        then have "prefix a (vs@xs)"
          by auto
        then have "a ∈ L M1"
          using language_state_prefix by (metis IntD1 assms(1) prefix_def)
        then obtain p where "io_targets M1 (initial M1) a = {p}"
          using assms(2) io_targets_observable_singleton_ob by metis
        then show "finite (io_targets M1 (initial M1) a)"
          by simp
      qed
    qed

    ultimately have "card (⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs))))
                     = Suc (card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))))"
      by (metis (no_types) card_insert_disjoint)


    moreover have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                    = card (⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs))))"
      using vs'_def by simp

    ultimately have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                      = Suc (card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))))"
      by linarith

    then have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                = Suc (card (R M2 s vs xs))"
      using R_count[of vs xs M1 M2 s FAIL PM q2 q1 tr] assms(1,10,11,2-9) by linarith

    moreover have "card (RP M2 s vs xs V'') = Suc (card (R M2 s vs xs))"
      using vs'_def by (metis card_insert_if finite_R)

    ultimately show ?thesis
      by linarith
  qed
qed


lemma RP_state_component_2 :
  assumes "io ∈ (RP M2 s vs xs V'')"
  and     "observable M2"
shows "io_targets M2 (initial M2) io = {s}"
  by (metis (mono_tags, lifting) RP.simps R_state_component_2 Un_iff assms mem_Collect_eq)


lemma RP_io_targets_split :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "productF M2 M1 FAIL PM"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "io ∈ RP M2 s vs xs V''"
shows "io_targets PM (initial PM) io
        = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
proof -
  have RP_cases : "RP M2 s vs xs V'' = R M2 s vs xs
                    ∨ (∃ vs' ∈ V'' . vs' ∉ R M2 s vs xs
                                      ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs))"
    using RP_from_R assms by metis
  show ?thesis
  proof (cases "io ∈ R M2 s vs xs")
    case True
    then have io_prefix : "prefix io (vs @ xs)"
      by auto
    then have io_lang_subs : "io ∈ L M1 ∧ io ∈ L M2"
      using assms(1) unfolding prefix_def by (metis IntE language_state language_state_split)
    then have io_lang_inter : "io ∈ L M1 ∩ L M2"
      by simp
    then have io_lang_pm : "io ∈ L PM"
      using productF_language assms by blast
    moreover obtain p2 p1 where "(p2,p1) ∈ io_targets PM (initial PM) io"
      by (metis assms(2) assms(3) assms(6) calculation insert_absorb insert_ident insert_not_empty
          io_targets_observable_singleton_ob observable_productF singleton_insert_inj_eq subrelI)
    ultimately have targets_pm : "io_targets PM (initial PM) io = {(p2,p1)}"
      using assms io_targets_observable_singleton_ex singletonD
      by (metis observable_productF)
    then obtain trP where trP_def : "target (io || trP) (initial PM) = (p2,p1)
                                      ∧ path PM (io || trP) (initial PM) ∧ length io = length trP"
    proof -
      assume a1: "⋀trP. target (io || trP) (initial PM) = (p2, p1)
                          ∧ path PM (io || trP) (initial PM) ∧ length io = length trP ⟹ thesis"
      have "∃ps. target (io || ps) (initial PM) = (p2, p1) ∧ path PM (io || ps) (initial PM)
                                                           ∧ length io = length ps"
        using ‹(p2, p1) ∈ io_targets PM (initial PM) io› by auto
      then show ?thesis
        using a1 by blast
    qed
    then have trP_unique : "{tr . path PM (io || tr) (initial PM) ∧ length io = length tr} = {trP}"
      using observable_productF observable_path_unique_ex[of PM io "initial PM"]
            io_lang_pm assms(2) assms(3) assms(7)
    proof -
      obtain pps :: "('d × 'c) list" where
        f1: "{ps. path PM (io || ps) (initial PM) ∧ length io = length ps} = {pps}
              ∨ ¬ observable PM"
        by (metis (no_types) ‹⋀thesis. ⟦observable PM; io ∈ L PM; ⋀tr.
                              {t. path PM (io || t) (initial PM) ∧ length io = length t} = {tr}
                               ⟹ thesis⟧ ⟹ thesis›
            io_lang_pm)
      have f2: "observable PM"
        by (meson ‹observable M1› ‹observable M2› ‹productF M2 M1 FAIL PM› observable_productF)
      then have "trP ∈ {pps}"
        using f1 trP_def by blast
      then show ?thesis
        using f2 f1 by force
    qed


    obtain trIO2 where trIO2_def : "{tr . path M2 (io || tr) (initial M2) ∧ length io = length tr}
                                    = { trIO2 }"
      using observable_path_unique_ex[of M2 io "initial M2"] io_lang_subs assms(3) by blast
    obtain trIO1 where trIO1_def : "{tr . path M1 (io || tr) (initial M1) ∧ length io = length tr}
                                    = { trIO1 }"
      using observable_path_unique_ex[of M1 io "initial M1"] io_lang_subs assms(2) by blast

    have "path PM (io || trIO2 || trIO1) (initial M2, initial M1)
          ∧ length io = length trIO2 ∧ length trIO2 = length trIO1"
    proof -
      have f1: "path M2 (io || trIO2) (initial M2) ∧ length io = length trIO2"
        using trIO2_def by auto
      have f2: "path M1 (io || trIO1) (initial M1) ∧ length io = length trIO1"
        using trIO1_def by auto
      then have "length trIO2 = length trIO1"
        using f1 by presburger
      then show ?thesis
        using f2 f1 assms(4) assms(5) assms(6) by blast
    qed
    then have trP_split : "path PM (io || trIO2 || trIO1) (initial PM)
                           ∧ length io = length trIO2 ∧ length trIO2 = length trIO1"
      using assms(6) by auto
    then have trP_zip : "trIO2 || trIO1 = trP"
      using trP_def trP_unique length_zip by fastforce

    have "target (io || trIO2) (initial M2) = p2
            ∧ path M2 (io || trIO2) (initial M2)
            ∧ length io = length trIO2"
      using trP_zip trP_split assms(6) trP_def trIO2_def by auto
    then have "p2 ∈ io_targets M2 (initial M2) io"
      by auto
    then have targets_2 : "io_targets M2 (initial M2) io = {p2}"
      by (meson assms(3) observable_io_target_is_singleton)

    have "target (io || trIO1) (initial M1) = p1
          ∧ path M1 (io || trIO1) (initial M1)
          ∧ length io = length trIO1"
      using trP_zip trP_split assms(6) trP_def trIO1_def by auto
    then have "p1 ∈ io_targets M1 (initial M1) io"
      by auto
    then have targets_1 : "io_targets M1 (initial M1) io = {p1}"
      by (metis io_lang_subs assms(2) io_targets_observable_singleton_ex singletonD)

    have "io_targets M2 (initial M2) io × io_targets M1 (initial M1) io = {(p2,p1)}"
      using targets_2 targets_1 by simp
    then show "io_targets PM (initial PM) io
                = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
      using targets_pm by simp

  next
    case False
    then have "io ∉ R M2 s vs xs ∧ RP M2 s vs xs V'' = insert io (R M2 s vs xs)"
      using RP_cases assms(9) by (metis insertE)

    have "io ∈ L M1" using assms(8) perm_language assms(9)
      using False by auto
    then obtain s' where s'_def : "io_targets M1 (initial M1) io = {s'}"
      by (meson assms(2) io_targets_observable_singleton_ob)
    then obtain tr1 where tr1_def : "target (io || tr1) (initial M1) = s'
                                      ∧ path M1 (io || tr1) (initial M1) ∧ length tr1 = length io"
      by (metis io_targets_elim singletonI)

    have "io_targets M2 (initial M2) io = {s}"
      using assms(9) assms(3) RP_state_component_2 by simp
    then obtain tr2 where tr2_def : "target (io || tr2) (initial M2) = s
                                      ∧ path M2 (io || tr2) (initial M2) ∧ length tr2 = length io"
      by (metis io_targets_elim singletonI)
    then have paths : "path M2 (io || tr2) (initial M2) ∧ path M1 (io || tr1) (initial M1)"
      using tr1_def by simp


    have "length io = length tr2"
      using tr2_def by simp
    moreover have "length tr2 = length tr1"
      using tr1_def tr2_def by simp
    ultimately have "path PM (io || tr2 || tr1) (initial M2, initial M1)"
      using assms(6) assms(5) assms(4) paths
            productF_path_forward[of io tr2 tr1 M2 M1 FAIL PM "initial M2" "initial M1"]
      by blast

    moreover have "target (io || tr2 || tr1) (initial M2, initial M1) = (s,s')"
      by (simp add: tr1_def tr2_def)
    moreover have "length (tr2 || tr2) = length io"
      using tr1_def tr2_def by simp
    moreover have "(initial M2, initial M1) = initial PM"
      using assms(6) by simp
    ultimately have "(s,s') ∈ io_targets PM (initial PM) io"
      by (metis io_target_from_path length_zip tr1_def tr2_def)
    moreover have "observable PM"
      using assms(2) assms(3) assms(6) observable_productF by blast
    then have "io_targets PM (initial PM) io = {(s,s')}"
      by (meson calculation observable_io_target_is_singleton)

    then show ?thesis
      using ‹io_targets M2 (initial M2) io = {s}› ‹io_targets M1 (initial M1) io = {s'}›
      by simp
  qed
qed





lemma RP_io_targets_finite_M1 :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
shows "finite (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))"
proof
  show "finite (RP M2 s vs xs V'')" using finite_RP assms(3) assms(4) by simp
  show "⋀a. a ∈ RP M2 s vs xs V'' ⟹ finite (io_targets M1 (initial M1) a)"
  proof -
    fix a assume "a ∈ RP M2 s vs xs V''"

    have RP_cases : "RP M2 s vs xs V'' = R M2 s vs xs
                      ∨ (∃ vs' ∈ V'' . vs' ∉ R M2 s vs xs
                                        ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs))"
      using RP_from_R assms by metis
    have "a ∈ L M1"
    proof (cases "a ∈ R M2 s vs xs")
      case True
      then have "prefix a (vs@xs)"
        by auto
      then show "a ∈ L M1"
        using language_state_prefix by (metis IntD1 assms(1) prefix_def)
    next
      case False
      then have "a ∈ V'' ∧ RP M2 s vs xs V'' = insert a (R M2 s vs xs)"
        using RP_cases ‹a ∈ RP M2 s vs xs V''› by (metis insertE)
      then show "a ∈ L M1"
        by (meson assms(4) perm_language)
    qed
    then obtain p where "io_targets M1 (initial M1) a = {p}"
      using assms(2) io_targets_observable_singleton_ob by metis
    then show "finite (io_targets M1 (initial M1) a)"
      by simp
  qed
qed

lemma RP_io_targets_finite_PM :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "productF M2 M1 FAIL PM"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
shows "finite (⋃ (image (io_targets PM (initial PM)) (RP M2 s vs xs V'')))"
proof -
  have "∀ io ∈ RP M2 s vs xs V'' . io_targets PM (initial PM) io
                                    = {s} × io_targets M1 (initial M1) io"
  proof
    fix io assume "io ∈ RP M2 s vs xs V''"
    then have "io_targets PM (initial PM) io
                = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
      using assms RP_io_targets_split[of vs xs M1 M2 FAIL PM V V'' io s] by simp
    moreover have "io_targets M2 (initial M2) io = {s}"
      using ‹io ∈ RP M2 s vs xs V''› assms(3) RP_state_component_2[of io M2 s vs xs V'']
      by blast
    ultimately show "io_targets PM (initial PM) io = {s} × io_targets M1 (initial M1) io"
      by auto
  qed
  then have "⋃ (image (io_targets PM (initial PM)) (RP M2 s vs xs V''))
              = ⋃ (image (λ io . {s} × io_targets M1 (initial M1) io) (RP M2 s vs xs V''))"
    by simp
  moreover have "⋃ (image (λ io . {s} × io_targets M1 (initial M1) io) (RP M2 s vs xs V''))
                  = {s} × ⋃ (image (λ io . io_targets M1 (initial M1) io) (RP M2 s vs xs V''))"
    by blast
  ultimately have "⋃ (image (io_targets PM (initial PM)) (RP M2 s vs xs V''))
                    = {s} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))"
    by auto
  moreover have "finite ({s} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))"
    using assms(1,2,7,8) RP_io_targets_finite_M1[of vs xs M1 M2 V V'' s] by simp
  ultimately show ?thesis
    by simp
qed



lemma RP_union_card_is_suffix_length :
  assumes "OFSM M2"
  and     "io@xs ∈ L M2"
  and     "is_det_state_cover M2 V"
  and     "V'' ∈ Perm V M1"
shows "⋀ q . card (R M2 q io xs) ≤ card (RP M2 q io xs V'')"
      "sum (λ q . card (RP M2 q io xs V'')) (nodes M2) ≥ length xs"
proof -
  have "sum (λ q . card (R M2 q io xs)) (nodes M2) = length xs"
    using R_union_card_is_suffix_length[OF assms(1,2)] by assumption
  show "⋀ q . card (R M2 q io xs) ≤ card (RP M2 q io xs V'')"
    by (metis RP_from_R assms(3) assms(4) card_insert_le eq_iff finite_R)
  show "sum (λ q . card (RP M2 q io xs V'')) (nodes M2) ≥ length xs"
    by (metis (no_types, lifting) ‹(∑q∈nodes M2. card (R M2 q io xs)) = length xs›
        ‹⋀q. card (R M2 q io xs) ≤ card (RP M2 q io xs V'')› sum_mono)
qed

lemma RP_state_repetition_distribution_productF :
  assumes "OFSM M2"
  and     "OFSM M1"
  and     "(card (nodes M2) * m) ≤ length xs"
  and     "card (nodes M1) ≤ m"
  and     "vs@xs ∈ L M2 ∩ L M1"
  and     "is_det_state_cover M2 V"
  and     "V'' ∈ Perm V M1"
shows "∃ q ∈ nodes M2 . card (RP M2 q vs xs V'') > m"
proof -
  have "finite (nodes M1)"
       "finite (nodes M2)"
    using assms(1,2) by auto
  then have "card(nodes M2 × nodes M1) = card (nodes M2) * card (nodes M1)"
    using card_cartesian_product by blast

  have "nodes (product M2 M1) ⊆ nodes M2 × nodes M1"
    using product_nodes by auto

  have "card (nodes (product M2 M1)) ≤ card (nodes M2) * card (nodes M1)"
    by (metis (no_types) ‹card (nodes M2 × nodes M1) = |M2| * |M1|› ‹finite (nodes M1)›
        ‹finite (nodes M2)› ‹nodes (product M2 M1) ⊆ nodes M2 × nodes M1›
        card_mono finite_cartesian_product)


  have "(∀ q ∈ nodes M2 . card (R M2 q vs xs) = m) ∨ (∃ q ∈ nodes M2 . card (R M2 q vs xs) > m)"
  proof (rule ccontr)
    assume "¬ ((∀q∈nodes M2. card (R M2 q vs xs) = m) ∨ (∃q∈nodes M2. m < card (R M2 q vs xs)))"

    then have "∀ q ∈ nodes M2 . card (R M2 q vs xs) ≤ m"
      by auto
    moreover obtain q' where "q'∈nodes M2" "card (R M2 q' vs xs) < m"
      using ‹¬ ((∀q∈nodes M2. card (R M2 q vs xs) = m) ∨ (∃q∈nodes M2. m < card (R M2 q vs xs)))›
            nat_neq_iff
      by blast

    have "sum (λ q . card (R M2 q vs xs)) (nodes M2)
          = sum (λ q . card (R M2 q vs xs)) (nodes M2 - {q'})
            + sum (λ q . card (R M2 q vs xs)) {q'}"
      using ‹q'∈nodes M2›
      by (meson ‹finite (nodes M2)› empty_subsetI insert_subset sum.subset_diff)
    moreover have "sum (λ q . card (R M2 q vs xs)) (nodes M2 - {q'})
                    ≤ sum (λ q . m) (nodes M2 - {q'})"
      using ‹∀ q ∈ nodes M2 . card (R M2 q vs xs) ≤ m›
      by (meson sum_mono DiffD1)
    moreover have "sum (λ q . card (R M2 q vs xs)) {q'} < m"
      using ‹card (R M2 q' vs xs) < m› by auto
    ultimately have "sum (λ q . card (R M2 q vs xs)) (nodes M2) < sum (λ q . m) (nodes M2)"
    proof -
      have "∀C c f. infinite C ∨ (c::'c) ∉ C ∨ sum f C = (f c::nat) + sum f (C - {c})"
        by (meson sum.remove)
      then have "(∑c∈nodes M2. m) = m + (∑c∈nodes M2 - {q'}. m)"
        using ‹finite (nodes M2)› ‹q' ∈ nodes M2› by blast
      then show ?thesis
        using ‹(∑q∈nodes M2 - {q'}. card (R M2 q vs xs)) ≤ (∑q∈nodes M2 - {q'}. m)›
              ‹(∑q∈nodes M2. card (R M2 q vs xs)) = (∑q∈nodes M2 - {q'}. card (R M2 q vs xs))
                + (∑q∈{q'}. card (R M2 q vs xs))›
              ‹(∑q∈{q'}. card (R M2 q vs xs)) < m›
        by linarith
    qed


    moreover have "sum (λ q . m) (nodes M2) ≤ card (nodes M2) * m"
      using assms(2) by auto
    ultimately have "sum (λ q . card (R M2 q vs xs)) (nodes M2) < card (nodes M2) * m"
      by presburger

    moreover have "Suc (card (nodes M2)*m) ≤ sum (λ q . card (R M2 q vs xs)) (nodes M2)"
      using R_union_card_is_suffix_length[OF assms(1), of vs xs] assms(5,3)
      by (metis Int_iff ‹vs @ xs ∈ L M2 ⟹ (∑q∈nodes M2. card (R M2 q vs xs)) = length xs›
          ‹vs @ xs ∈ L M2 ∩ L M1› ‹|M2| * m ≤ length xs› calculation less_eq_Suc_le not_less_eq_eq)

    ultimately show "False" by simp
  qed
  then show ?thesis
  proof
    let ?q = "initial M2"

    assume "∀q∈nodes M2. card (R M2 q vs xs) = m"
    then have "card (R M2 ?q vs xs) = m"
      by auto

    have "[] ∈ V''"
      by (meson assms(6) assms(7) perm_empty)
    then have "[] ∈ RP M2 ?q vs xs V''"
      by auto
    have "[] ∉ R M2 ?q vs xs"
      by auto
    have "card (RP M2 ?q vs xs V'') ≥ card (R M2 ?q vs xs)"
      using finite_R[of M2 ?q vs xs] finite_RP[OF assms(6,7),of ?q vs xs] unfolding RP.simps
      by (simp add: card_mono)

    have "card (RP M2 ?q vs xs V'') > card (R M2 ?q vs xs)"
    proof -
      have f1: "∀n na. (¬ (n::nat) ≤ na ∨ n = na) ∨ n < na"
        by (meson le_neq_trans)
      have "RP M2 (initial M2) vs xs V'' ≠ R M2 (initial M2) vs xs"
        using ‹[] ∈ RP M2 (initial M2) vs xs V''› ‹[] ∉ R M2 (initial M2) vs xs› by blast
      then show ?thesis
        using f1 by (metis (no_types) RP_from_R
                     ‹card (R M2 (initial M2) vs xs) ≤ card (RP M2 (initial M2) vs xs V'')›
                     assms(6) assms(7) card_insert_disjoint finite_R le_simps(2))
    qed

    then show ?thesis
      using ‹card (R M2 ?q vs xs) = m›
      by blast
  next
    assume "∃q∈nodes M2. m < card (R M2 q vs xs)"
    then obtain q where "q∈nodes M2" "m < card (R M2 q vs xs)"
      by blast
    moreover have "card (RP M2 q vs xs V'') ≥ card (R M2 q vs xs)"
      using finite_R[of M2 q vs xs] finite_RP[OF assms(6,7),of q vs xs] unfolding RP.simps
      by (simp add: card_mono)
    ultimately have "m < card (RP M2 q vs xs V'')"
      by simp

    show ?thesis
      using ‹q ∈ nodes M2›  ‹m < card (RP M2 q vs xs V'')› by blast
  qed
qed



subsection ‹ Conditions for the result of LB to be a valid lower bound ›

text ‹
The following predicates describe the assumptions necessary to show that the value calculated by
@{verbatim LB} is a lower bound on the number of states of a given FSM.
›

fun Prereq :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM ⇒ ('in × 'out) list
              ⇒ ('in × 'out) list ⇒ 'in list set ⇒ 'state1 set ⇒ ('in, 'out) ATC set
              ⇒ ('in × 'out) list set ⇒ bool"
  where
  "Prereq M2 M1 vs xs T S Ω V'' = (
    (finite T)
    ∧ (vs @ xs) ∈ L M2 ∩ L M1
    ∧ S ⊆ nodes M2
    ∧ (∀ s1 ∈ S . ∀ s2 ∈ S . s1 ≠ s2
        ⟶ (∀ io1 ∈ RP M2 s1 vs xs V'' .
               ∀ io2 ∈ RP M2 s2 vs xs V'' .
                 B M1 io1 Ω ≠ B M1 io2 Ω )))"


fun Rep_Pre :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM ⇒ ('in × 'out) list
                ⇒ ('in × 'out) list ⇒ bool" where
  "Rep_Pre M2 M1 vs xs = (∃ xs1 xs2 . prefix xs1 xs2 ∧ prefix xs2 xs ∧ xs1 ≠ xs2
    ∧ (∃ s2 . io_targets M2 (initial M2) (vs @ xs1) = {s2}
              ∧ io_targets M2 (initial M2) (vs @ xs2) = {s2})
    ∧ (∃ s1 . io_targets M1 (initial M1) (vs @ xs1) = {s1}
              ∧ io_targets M1 (initial M1) (vs @ xs2) = {s1}))"


fun Rep_Cov :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM ⇒ ('in × 'out) list set
                ⇒ ('in × 'out) list ⇒ ('in × 'out) list ⇒ bool" where
  "Rep_Cov M2 M1 V'' vs xs = (∃ xs' vs' . xs' ≠ [] ∧ prefix xs' xs ∧ vs' ∈ V''
    ∧ (∃ s2 . io_targets M2 (initial M2) (vs @ xs') = {s2}
              ∧ io_targets M2 (initial M2) (vs') = {s2})
    ∧ (∃ s1 . io_targets M1 (initial M1) (vs @ xs') = {s1}
              ∧ io_targets M1 (initial M1) (vs') = {s1}))"



lemma distinctness_via_Rep_Pre :
  assumes "¬ Rep_Pre M2 M1 vs xs"
  and "productF M2 M1 FAIL PM"
  and "observable M1"
  and "observable M2"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "(vs @ xs) ∈ L M1 ∩ L M2"
  and "well_formed M1"
  and "well_formed M2"
shows "distinct (states (xs || tr) (q2, q1))"
proof (rule ccontr)
  assume assm : "¬ distinct (states (xs || tr) (q2, q1))"
  then obtain i1 i2 where index_def :
     "i1 ≠ 0
      ∧ i1 ≠ i2
      ∧ i1 < length (states (xs || tr) (q2, q1))
      ∧ i2 < length (states (xs || tr) (q2, q1))
      ∧ (states (xs || tr) (q2, q1)) ! i1 = (states (xs || tr) (q2, q1)) ! i2"
    by (metis distinct_conv_nth)
  then have "length xs > 0" by auto

  let ?xs1 = "take (Suc i1) xs"
  let ?xs2 = "take (Suc i2) xs"
  let ?tr1 = "take (Suc i1) tr"
  let ?tr2 = "take (Suc i2) tr"
  let ?st  = "(states (xs || tr) (q2, q1)) ! i1"

  have obs_PM : "observable PM"
    using observable_productF assms(2) assms(3) assms(4) by blast

  have "initial PM = (initial M2, initial M1)"
    using assms(2) by simp
  moreover have "vs ∈ L M2" "vs ∈ L M1"
    using assms(8) language_state_prefix by auto
  ultimately have "io_targets M1 (initial M1) vs = {q1}" "io_targets M2 (initial M2) vs = {q2}"
    using productF_path_io_targets[of M2 M1 FAIL PM "initial M2" "initial M1" vs q2 q1]
    by (metis FSM.nodes.initial assms(2) assms(3) assms(4) assms(5) assms(9) assms(10)
        io_targets_observable_singleton_ex singletonD)+

  ― ‹paths for ?xs1›

  have "(states (xs || tr) (q2, q1)) ! i1 ∈ io_targets PM (q2, q1) ?xs1"
    by (metis ‹0 < length xs› assms(6) assms(7) index_def map_snd_zip states_alt_def
        states_index_io_target)
  then have "io_targets PM (q2, q1) ?xs1 = {?st}"
    using obs_PM by (meson observable_io_target_is_singleton)

  have "path PM (?xs1 || ?tr1) (q2,q1)"
    by (metis FSM.path_append_elim append_take_drop_id assms(6) assms(7) length_take zip_append)
  then have "path PM (?xs1 || map fst ?tr1 || map snd ?tr1) (q2,q1)"
    by auto

  have "vs @ ?xs1 ∈ L M2"
    by (metis (no_types) IntD2 append_assoc append_take_drop_id assms(8) language_state_prefix)
  then obtain q2' where "io_targets M2 (initial M2) (vs@?xs1) = {q2'}"
    using io_targets_observable_singleton_ob[of M2 "vs@?xs1" "initial M2"] assms(4) by auto
  then have "q2' ∈ io_targets M2 q2 ?xs1"
    using assms(4) ‹io_targets M2 (initial M2) vs = {q2}›
          observable_io_targets_split[of M2 "initial M2" vs ?xs1 q2' q2]
    by simp
  then have "?xs1 ∈ language_state M2 q2"
    by auto
  moreover have "length ?xs1 = length (map snd ?tr1)"
    using assms(7) by auto
  moreover have "length (map fst ?tr1) = length (map snd ?tr1)"
    by auto
  moreover have "q2 ∈ nodes M2"
    using ‹io_targets M2 (initial M2) vs = {q2}› io_targets_nodes
    by (metis FSM.nodes.initial insertI1)
  moreover have "q1 ∈ nodes M1"
    using ‹io_targets M1 (initial M1) vs = {q1}› io_targets_nodes
    by (metis FSM.nodes.initial insertI1)
  ultimately have
     "path M1 (?xs1 || map snd ?tr1) q1"
     "path M2 (?xs1 || map fst ?tr1) q2"
     "target (?xs1 || map snd ?tr1) q1 = snd (target (?xs1 || map fst ?tr1 || map snd ?tr1) (q2,q1))"
     "target (?xs1 || map fst ?tr1) q2 = fst (target (?xs1 || map fst ?tr1 || map snd ?tr1) (q2,q1))"
    using assms(2) assms(9) assms(10) ‹path PM (?xs1 || map fst ?tr1 || map snd ?tr1) (q2,q1)›
          assms(4)
          productF_path_reverse_ob_2[of ?xs1 "map fst ?tr1" "map snd ?tr1" M2 M1 FAIL PM q2 q1]
    by simp+
  moreover have "target (?xs1 || map fst ?tr1 || map snd ?tr1) (q2,q1) = ?st"
    by (metis (no_types) index_def scan_nth take_zip zip_map_fst_snd)
  ultimately have
     "target (?xs1 || map snd ?tr1) q1 = snd ?st"
     "target (?xs1 || map fst ?tr1) q2 = fst ?st"
    by simp+

  ― ‹paths for ?xs2›

  have "(states (xs || tr) (q2, q1)) ! i2 ∈ io_targets PM (q2, q1) ?xs2"
    by (metis ‹0 < length xs› assms(6) assms(7) index_def map_snd_zip states_alt_def states_index_io_target)
  then have "io_targets PM (q2, q1) ?xs2 = {?st}"
    using obs_PM by (metis index_def observable_io_target_is_singleton)

  have "path PM (?xs2 || ?tr2) (q2,q1)"
    by (metis FSM.path_append_elim append_take_drop_id assms(6) assms(7) length_take zip_append)
  then have "path PM (?xs2 || map fst ?tr2 || map snd ?tr2) (q2,q1)"
    by auto

  have "vs @ ?xs2 ∈ L M2"
    by (metis (no_types) IntD2 append_assoc append_take_drop_id assms(8) language_state_prefix)
  then obtain q2'' where "io_targets M2 (initial M2) (vs@?xs2) = {q2''}"
    using io_targets_observable_singleton_ob[of M2 "vs@?xs2" "initial M2"] assms(4)
    by auto
  then have "q2'' ∈ io_targets M2 q2 ?xs2"
    using assms(4) ‹io_targets M2 (initial M2) vs = {q2}›
          observable_io_targets_split[of M2 "initial M2" vs ?xs2 q2'' q2]
    by simp
  then have "?xs2 ∈ language_state M2 q2"
    by auto
  moreover have "length ?xs2 = length (map snd ?tr2)" using assms(7)
    by auto
  moreover have "length (map fst ?tr2) = length (map snd ?tr2)"
    by auto
  moreover have "q2 ∈ nodes M2"
    using ‹io_targets M2 (initial M2) vs = {q2}› io_targets_nodes
    by (metis FSM.nodes.initial insertI1)
  moreover have "q1 ∈ nodes M1"
    using ‹io_targets M1 (initial M1) vs = {q1}› io_targets_nodes
    by (metis FSM.nodes.initial insertI1)
  ultimately have
     "path M1 (?xs2 || map snd ?tr2) q1"
     "path M2 (?xs2 || map fst ?tr2) q2"
     "target (?xs2 || map snd ?tr2) q1 = snd(target (?xs2 || map fst ?tr2 || map snd ?tr2) (q2,q1))"
     "target (?xs2 || map fst ?tr2) q2 = fst(target (?xs2 || map fst ?tr2 || map snd ?tr2) (q2,q1))"
    using assms(2) assms(9) assms(10) ‹path PM (?xs2 || map fst ?tr2 || map snd ?tr2) (q2,q1)›
          assms(4)
          productF_path_reverse_ob_2[of ?xs2 "map fst ?tr2" "map snd ?tr2" M2 M1 FAIL PM q2 q1]
    by simp+
  moreover have "target (?xs2 || map fst ?tr2 || map snd ?tr2) (q2,q1) = ?st"
    by (metis (no_types) index_def scan_nth take_zip zip_map_fst_snd)
  ultimately have
     "target (?xs2 || map snd ?tr2) q1 = snd ?st"
     "target (?xs2 || map fst ?tr2) q2 = fst ?st"
    by simp+



  have "io_targets M1 q1 ?xs1 = {snd ?st}"
    using ‹path M1 (?xs1 || map snd ?tr1) q1› ‹target (?xs1 || map snd ?tr1) q1 = snd ?st›
          ‹length ?xs1 = length (map snd ?tr1)› assms(3) obs_target_is_io_targets[of M1 ?xs1
          "map snd ?tr1" q1]
    by simp
  then have tgt_1_1 : "io_targets M1 (initial M1) (vs @ ?xs1) = {snd ?st}"
    by (meson ‹io_targets M1 (initial M1) vs = {q1}› assms(3) observable_io_targets_append)

  have "io_targets M2 q2 ?xs1 = {fst ?st}"
    using ‹path M2 (?xs1 || map fst ?tr1) q2› ‹target (?xs1 || map fst ?tr1) q2 = fst ?st›
          ‹length ?xs1 = length (map snd ?tr1)› assms(4)
          obs_target_is_io_targets[of M2 ?xs1 "map fst ?tr1" q2]
    by simp
  then have tgt_1_2 : "io_targets M2 (initial M2) (vs @ ?xs1) = {fst ?st}"
    by (meson ‹io_targets M2 (initial M2) vs = {q2}› assms(4) observable_io_targets_append)

  have "io_targets M1 q1 ?xs2 = {snd ?st}"
    using ‹path M1 (?xs2 || map snd ?tr2) q1› ‹target (?xs2 || map snd ?tr2) q1 = snd ?st›
          ‹length ?xs2 = length (map snd ?tr2)› assms(3)
          obs_target_is_io_targets[of M1 ?xs2 "map snd ?tr2" q1]
    by simp
  then have tgt_2_1 : "io_targets M1 (initial M1) (vs @ ?xs2) = {snd ?st}"
    by (meson ‹io_targets M1 (initial M1) vs = {q1}› assms(3) observable_io_targets_append)

  have "io_targets M2 q2 ?xs2 = {fst ?st}"
    using ‹path M2 (?xs2 || map fst ?tr2) q2› ‹target (?xs2 || map fst ?tr2) q2 = fst ?st›
          ‹length ?xs2 = length (map snd ?tr2)› assms(4)
          obs_target_is_io_targets[of M2 ?xs2 "map fst ?tr2" q2]
    by simp
  then have tgt_2_2 : "io_targets M2 (initial M2) (vs @ ?xs2) = {fst ?st}"
    by (meson ‹io_targets M2 (initial M2) vs = {q2}› assms(4) observable_io_targets_append)

  have "?xs1 ≠ []" using ‹0 < length xs›
    by auto
  have "prefix ?xs1 xs"
    using take_is_prefix by blast
  have "prefix ?xs2 xs"
    using take_is_prefix by blast
  have "?xs1 ≠ ?xs2"
  proof -
    have f1: "∀n na. ¬ n < na ∨ Suc n ≤ na"
      by presburger
    have f2: "Suc i1 ≤ length xs"
      using index_def by force
    have "Suc i2 ≤ length xs"
      using f1 by (metis index_def length_take map_snd_zip_take min_less_iff_conj states_alt_def)
    then show ?thesis
      using f2 by (metis (no_types) index_def length_take min.absorb2 nat.simps(1))
  qed
  have "Rep_Pre M2 M1 vs xs"
  proof (cases "length ?xs1 < length ?xs2")
    case True
    then have "prefix ?xs1 ?xs2"
      by (meson ‹prefix (take (Suc i1) xs) xs› ‹prefix (take (Suc i2) xs) xs› leD prefix_length_le
          prefix_same_cases)
    show ?thesis
      by (meson Rep_Pre.elims(3) ‹prefix (take (Suc i1) xs) (take (Suc i2) xs)›
          ‹prefix (take (Suc i2) xs) xs› ‹take (Suc i1) xs ≠ take (Suc i2) xs›
          tgt_1_1 tgt_1_2 tgt_2_1 tgt_2_2)
  next
    case False
    moreover have "length ?xs1 ≠ length ?xs2"
      by (metis (no_types) ‹take (Suc i1) xs ≠ take (Suc i2) xs› append_eq_conv_conj
          append_take_drop_id)
    ultimately have "length ?xs2 < length ?xs1"
      by auto
    then have "prefix ?xs2 ?xs1"
      using ‹prefix (take (Suc i1) xs) xs› ‹prefix (take (Suc i2) xs) xs› less_imp_le_nat
            prefix_length_prefix
      by blast
    show ?thesis
      by (metis Rep_Pre.elims(3) ‹prefix (take (Suc i1) xs) xs›
          ‹prefix (take (Suc i2) xs) (take (Suc i1) xs)› ‹take (Suc i1) xs ≠ take (Suc i2) xs›
          tgt_1_1 tgt_1_2 tgt_2_1 tgt_2_2)
  qed

  then show "False"
    using assms(1) by simp
qed





lemma RP_count_via_Rep_Cov :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "s ∈ nodes M2"
  and "productF M2 M1 FAIL PM"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "distinct (states (xs || tr) (q2,q1))"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "¬ Rep_Cov M2 M1 V'' vs xs"
shows "card (⋃(image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) = card (RP M2 s vs xs V'')"
proof -
  have RP_cases : "RP M2 s vs xs V'' = R M2 s vs xs
                    ∨ (∃ vs' ∈ V'' . vs' ∉ R M2 s vs xs
                                      ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs))"
    using RP_from_R assms by metis
  show ?thesis
  proof (cases "RP M2 s vs xs V'' = R M2 s vs xs")
    case True
    then show ?thesis
      using R_count assms by metis
  next
    case False
    then obtain vs' where vs'_def : "vs' ∈ V''
                                      ∧ vs' ∉ R M2 s vs xs
                                      ∧ RP M2 s vs xs V'' = insert vs' (R M2 s vs xs)"
      using RP_cases by auto

    have state_component_2 : "∀ io ∈ (R M2 s vs xs) . io_targets M2 (initial M2) io = {s}"
    proof
      fix io assume "io ∈ R M2 s vs xs"
      then have "s ∈ io_targets M2 (initial M2) io"
        by auto
      moreover have "io ∈ language_state M2 (initial M2)"
        using calculation by auto
      ultimately show "io_targets M2 (initial M2) io = {s}"
        using assms(3) io_targets_observable_singleton_ex by (metis singletonD)
    qed

    have "vs' ∈ L M1"
      using assms(13) perm_language vs'_def by blast
    then obtain s' where s'_def : "io_targets M1 (initial M1) vs' = {s'}"
      by (meson assms(2) io_targets_observable_singleton_ob)

    moreover have "s' ∉ ⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))"
    proof (rule ccontr)
      assume "¬ s' ∉ ⋃(io_targets M1 (initial M1) ` R M2 s vs xs)"
      then obtain xs' where xs'_def : "vs @ xs' ∈ R M2 s vs xs
                                        ∧ s' ∈ io_targets M1 (initial M1) (vs @ xs')"
      proof -
        assume a1: "⋀xs'. vs @ xs' ∈ R M2 s vs xs
                          ∧ s' ∈ io_targets M1 (initial M1) (vs @ xs') ⟹ thesis"
        obtain pps :: "('a × 'b) list set ⇒ (('a × 'b) list ⇒ 'c set) ⇒ 'c ⇒ ('a × 'b) list"
          where
          "∀x0 x1 x2. (∃v3. v3 ∈ x0 ∧ x2 ∈ x1 v3) = (pps x0 x1 x2 ∈ x0 ∧ x2 ∈ x1 (pps x0 x1 x2))"
          by moura
        then have f2: "pps (R M2 s vs xs) (io_targets M1 (initial M1)) s' ∈ R M2 s vs xs
                        ∧ s' ∈ io_targets M1 (initial M1)
                                              (pps (R M2 s vs xs) (io_targets M1 (initial M1)) s')"
          using ‹¬ s' ∉ ⋃(io_targets M1 (initial M1) ` R M2 s vs xs)› by blast
        then have "∃ps. pps (R M2 s vs xs) (io_targets M1 (initial M1)) s' = vs @ ps ∧ ps ≠ []
                        ∧ prefix ps xs ∧ s ∈ io_targets M2 (initial M2) (vs @ ps)"
          by simp
        then show ?thesis
          using f2 a1 by (metis (no_types))
      qed

      have "vs @ xs' ∈ L M1"
        using xs'_def by blast
      then have "io_targets M1 (initial M1) (vs@xs') = {s'}"
        by (metis assms(2) io_targets_observable_singleton_ob singletonD xs'_def)
      moreover have "io_targets M1 (initial M1) (vs') = {s'}"
        using s'_def by blast
      moreover have "io_targets M2 (initial M2) (vs @ xs') = {s}"
        using state_component_2 xs'_def by blast
      moreover have "io_targets M2 (initial M2) (vs') = {s}"
        by (metis (mono_tags, lifting) RP.simps Un_iff insertI1 mem_Collect_eq vs'_def)
      moreover have "xs' ≠ []"
        using xs'_def by simp
      moreover have "prefix xs' xs"
        using xs'_def by simp
      moreover have "vs' ∈ V''"
        using vs'_def by simp
      ultimately have "Rep_Cov M2 M1 V'' vs xs"
        by auto

      then show "False"
        using assms(14) by simp
    qed

    moreover have "⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs)))
                    = insert s' (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs)))"
      using s'_def by simp

    moreover have "finite (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs)))"
    proof
      show "finite (R M2 s vs xs)"
        using finite_R by simp
      show "⋀a. a ∈ R M2 s vs xs ⟹ finite (io_targets M1 (initial M1) a)"
      proof -
        fix a assume "a ∈ R M2 s vs xs"
        then have "prefix a (vs@xs)"
          by auto
        then have "a ∈ L M1"
          using language_state_prefix by (metis IntD1 assms(1) prefix_def)
        then obtain p where "io_targets M1 (initial M1) a = {p}"
          using assms(2) io_targets_observable_singleton_ob by metis
        then show "finite (io_targets M1 (initial M1) a)"
          by simp
      qed
    qed

    ultimately have "card (⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs))))
                      = Suc (card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))))"
      by (metis (no_types) card_insert_disjoint)


    moreover have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                    = card (⋃ (image (io_targets M1 (initial M1)) (insert vs' (R M2 s vs xs))))"
      using vs'_def by simp

    ultimately have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                      = Suc (card (⋃ (image (io_targets M1 (initial M1)) (R M2 s vs xs))))"
      by linarith

    then have "card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))
                  = Suc (card (R M2 s vs xs))"
      using R_count[of vs xs M1 M2 s FAIL PM q2 q1 tr] using assms(1,10,11,2-9)
      by linarith

    moreover have "card (RP M2 s vs xs V'') = Suc (card (R M2 s vs xs))"
      using vs'_def by (metis card_insert_if finite_R)

    ultimately show ?thesis
      by linarith
  qed
qed


lemma RP_count_alt_def :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "s ∈ nodes M2"
  and "productF M2 M1 FAIL PM"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "¬ Rep_Pre M2 M1 vs xs"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "¬ Rep_Cov M2 M1 V'' vs xs"
shows "card (⋃(image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) = card (RP M2 s vs xs V'')"
proof -
  have "distinct (states (xs || tr) (q2,q1))"
    using distinctness_via_Rep_Pre[of M2 M1 vs xs FAIL PM q2 q1 tr] assms by simp
  then show ?thesis
    using RP_count_via_Rep_Cov[of vs xs M1 M2 s FAIL PM q2 q1 tr V V'']
    using assms(1,10,12-14,2-9) by blast
qed




subsection ‹ Function LB ›

text ‹
@{verbatim LB} adds together the number of elements in sets calculated via RP for a given set of
states and the number of ATC-reaction known to exist but not produced by a state reached by any of
the above elements.
›

fun LB :: "('in, 'out, 'state1) FSM ⇒ ('in, 'out, 'state2) FSM
          ⇒ ('in × 'out) list ⇒ ('in × 'out) list ⇒ 'in list set
          ⇒ 'state1 set ⇒ ('in, 'out) ATC set
          ⇒ ('in × 'out) list set ⇒ nat"
  where
  "LB M2 M1 vs xs T S Ω V'' =
    (sum (λ s . card (RP M2 s vs xs V'')) S)
    + card ((D M1 T Ω) -
            {B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''})"



lemma LB_count_helper_RP_disjoint_and_cards :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "productF M2 M1 FAIL PM"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "s1 ≠ s2"
shows "⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V''))
        ∩ ⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')) = {}"
      "card (⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V'')))
        = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))"
      "card (⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')))
        = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
proof -
  have "∀ io ∈ RP M2 s1 vs xs V'' . io_targets PM (initial PM) io
                                      = {s1} × io_targets M1 (initial M1) io"
  proof
    fix io assume "io ∈ RP M2 s1 vs xs V''"
    then have "io_targets PM (initial PM) io
                = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
      using assms RP_io_targets_split[of vs xs M1 M2 FAIL PM V V'' io s1] by simp
    moreover have "io_targets M2 (initial M2) io = {s1}"
      using ‹io ∈ RP M2 s1 vs xs V''› assms(3) RP_state_component_2[of io M2 s1 vs xs V'']
      by blast
    ultimately show "io_targets PM (initial PM) io = {s1} × io_targets M1 (initial M1) io"
      by auto
  qed
  then have "⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V''))
              = ⋃ (image (λ io . {s1} × io_targets M1 (initial M1) io) (RP M2 s1 vs xs V''))"
    by simp
  moreover have "⋃ (image (λ io . {s1} × io_targets M1 (initial M1) io) (RP M2 s1 vs xs V''))
                  = {s1} × ⋃ (image (λ io . io_targets M1 (initial M1) io) (RP M2 s1 vs xs V''))"
    by blast
  ultimately have image_split_1 :
    "⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V'') )
      = {s1} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))"
    by simp
  then show "card (⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V'')))
              = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))"
    by (metis (no_types)  card_cartesian_product_singleton)




  have "∀ io ∈ RP M2 s2 vs xs V'' . io_targets PM (initial PM) io
                                      = {s2} × io_targets M1 (initial M1) io"
  proof
    fix io assume "io ∈ RP M2 s2 vs xs V''"
    then have "io_targets PM (initial PM) io
                  = io_targets M2 (initial M2) io × io_targets M1 (initial M1) io"
      using assms RP_io_targets_split[of vs xs M1 M2 FAIL PM V V'' io s2] by simp
    moreover have "io_targets M2 (initial M2) io = {s2}"
      using ‹io ∈ RP M2 s2 vs xs V''› assms(3) RP_state_component_2[of io M2 s2 vs xs V'']
      by blast
    ultimately show "io_targets PM (initial PM) io = {s2} × io_targets M1 (initial M1) io"
      by auto
  qed
  then have "⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V''))
              = ⋃ (image (λ io . {s2} × io_targets M1 (initial M1) io) (RP M2 s2 vs xs V''))"
    by simp
  moreover have "⋃ (image (λ io . {s2} × io_targets M1 (initial M1) io) (RP M2 s2 vs xs V''))
                  = {s2} × ⋃ (image (λ io . io_targets M1 (initial M1) io) (RP M2 s2 vs xs V''))"
    by blast
  ultimately have image_split_2 :
    "⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V''))
      = {s2} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V''))" by simp
  then show "card (⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')))
              = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
    by (metis (no_types)  card_cartesian_product_singleton)


  have "⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V''))
          ∩ ⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V''))
        = {s1} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))
          ∩ {s2} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V''))"
    using image_split_1 image_split_2 by blast
  moreover have "{s1} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))
                  ∩ {s2} × ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')) = {}"
    using assms(9) by auto
  ultimately show "⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V''))
                    ∩ ⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')) = {}"
    by presburger
qed


lemma LB_count_helper_RP_disjoint_card_M1 :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "productF M2 M1 FAIL PM"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "s1 ≠ s2"
shows "card (⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V''))
              ∪ ⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')))
       = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))
          + card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
proof -
  have "finite (⋃ (image (io_targets PM (initial PM)) (RP M2 s1 vs xs V'')))"
    using RP_io_targets_finite_PM[OF assms(1-8)] by simp
  moreover have "finite (⋃ (image (io_targets PM (initial PM)) (RP M2 s2 vs xs V'')))"
    using RP_io_targets_finite_PM[OF assms(1-8)] by simp
  ultimately show ?thesis
    using LB_count_helper_RP_disjoint_and_cards[OF assms]
    by (metis (no_types) card_Un_disjoint)
qed

lemma LB_count_helper_RP_disjoint_M1_pair :
  assumes "(vs @ xs) ∈ L M1 ∩ L M2"
  and "observable M1"
  and "observable M2"
  and "well_formed M1"
  and "well_formed M2"
  and "productF M2 M1 FAIL PM"
  and "io_targets PM (initial PM) vs = {(q2,q1)}"
  and "path PM (xs || tr) (q2,q1)"
  and "length xs = length tr"
  and "¬ Rep_Pre M2 M1 vs xs"
  and "is_det_state_cover M2 V"
  and "V'' ∈ Perm V M1"
  and "¬ Rep_Cov M2 M1 V'' vs xs"
  and "Prereq M2 M1 vs xs T S Ω V''"
  and "s1 ≠ s2"
  and "s1 ∈ S"
  and "s2 ∈ S"
  and "applicable_set M1 Ω"
  and "completely_specified M1"
shows "card (RP M2 s1 vs xs V'') + card (RP M2 s2 vs xs V'')
        = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))
          + card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
      "⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))
          ∩ ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V''))
        = {}"
proof -
  have "s1 ∈ nodes M2"
    using assms(14,16) unfolding Prereq.simps by blast
  have "s2 ∈ nodes M2"
    using assms(14,17) unfolding Prereq.simps by blast
  have "card (RP M2 s1 vs xs V'')
          = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))"
    using RP_count_alt_def[OF assms(1-5) ‹s1 ∈ nodes M2› assms(6-13)]
    by linarith
  moreover have "card (RP M2 s2 vs xs V'')
                  = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
    using RP_count_alt_def[OF assms(1-5) ‹s2 ∈ nodes M2› assms(6-13)]
    by linarith

  moreover show "⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))
                  ∩ ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')) = {}"
  proof (rule ccontr)
    assume "⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V''))
              ∩ ⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')) ≠ {}"
    then obtain io1 io2 t where shared_elem_def :
      "io1 ∈ (RP M2 s1 vs xs V'')"
      "io2 ∈ (RP M2 s2 vs xs V'')"
      "t ∈ io_targets M1 (initial M1) io1"
      "t ∈ io_targets M1 (initial M1) io2"
      by blast


    have dist_prop: "(∀ s1 ∈ S . ∀ s2 ∈ S . s1 ≠ s2
            ⟶ (∀ io1 ∈ RP M2 s1 vs xs V'' .
                       ∀ io2 ∈ RP M2 s2 vs xs V'' .
                         B M1 io1 Ω ≠ B M1 io2 Ω ))"
      using assms(14) by simp

    have "io_targets M1 (initial M1) io1 ∩ io_targets M1 (initial M1) io2 = {}"
    proof (rule ccontr)
      assume "io_targets M1 (initial M1) io1 ∩ io_targets M1 (initial M1) io2 ≠ {}"
      then have "io_targets M1 (initial M1) io1 ≠ {}" "io_targets M1 (initial M1) io2 ≠ {}"
        by blast+

      then obtain s1 s2 where "s1 ∈ io_targets M1 (initial M1) io1"
                              "s2 ∈ io_targets M1 (initial M1) io2"
        by blast

      then have "io_targets M1 (initial M1) io1 = {s1}"
                "io_targets M1 (initial M1) io2 = {s2}"
        by (meson assms(2) observable_io_target_is_singleton)+

      then have "s1 = s2"
        using ‹io_targets M1 (initial M1) io1 ∩ io_targets M1 (initial M1) io2 ≠ {}›
        by auto

      then have "B M1 io1 Ω = B M1 io2 Ω"
        using ‹io_targets M1 (initial M1) io1 = {s1}› ‹io_targets M1 (initial M1) io2 = {s2}›
        by auto
      then show "False"
        using assms(15-17) dist_prop shared_elem_def(1,2) by blast
    qed
    then show "False"
      using shared_elem_def(3,4) by blast
  qed

  ultimately show "card (RP M2 s1 vs xs V'') + card (RP M2 s2 vs xs V'')
       = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s1 vs xs V'')))
          + card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s2 vs xs V'')))"
    by linarith
qed






lemma LB_count_helper_RP_card_union :
  assumes "observable M2"
  and     "s1 ≠ s2"
shows "RP M2 s1 vs xs V'' ∩ RP M2 s2 vs xs V'' = {}"
proof (rule ccontr)
  assume "RP M2 s1 vs xs V'' ∩ RP M2 s2 vs xs V'' ≠ {}"
  then obtain io where "io ∈ RP M2 s1 vs xs V'' ∧ io ∈ RP M2 s2 vs xs V''"
    by blast
  then have "s1 ∈ io_targets M2 (initial M2) io"
            "s2 ∈ io_targets M2 (initial M2) io"
    by auto
  then have "s1 = s2"
    using assms(1) by (metis observable_io_target_is_singleton singletonD)
  then show "False"
    using assms(2) by simp
qed



lemma LB_count_helper_RP_inj :
obtains f
where "∀ q ∈ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S)) .
          f q ∈ nodes M1"
      "inj_on f (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
proof -
  let ?f =
    "λ q . if (q ∈ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S)))
      then q
      else (initial M1)"

  have "(⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S)) ⊆ nodes M1"
    by blast

  then have "∀ q ∈ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S)) .
              ?f q ∈ nodes M1"
    by (metis Un_iff  sup.order_iff)

  moreover have "inj_on ?f (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1))
                                                      (RP M2 s vs xs V''))) S))"
  proof
    fix x assume "x ∈ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
    then have "?f x = x"
      by presburger

    fix y assume "y ∈ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
    then have "?f y = y"
      by presburger

    assume "?f x = ?f y"
    then show "x = y" using ‹?f x = x› ‹?f y = y›
      by presburger
  qed

  ultimately show ?thesis
    using that by presburger
qed

abbreviation (input) UNION :: "'a set ⇒ ('a ⇒ 'b set) ⇒ 'b set"
  where "UNION A f ≡ ⋃ (f ` A)"


lemma LB_count_helper_RP_card_union_sum :
  assumes "(vs @ xs) ∈ L M2 ∩ L M1"
  and     "OFSM M1"
  and     "OFSM M2"
  and     "asc_fault_domain M2 M1 m"
  and     "test_tools M2 M1 FAIL PM V Ω"
  and     "V'' ∈ Perm V M1"
  and     "Prereq M2 M1 vs xs T S Ω V''"
  and     "¬ Rep_Pre M2 M1 vs xs"
  and     "¬ Rep_Cov M2 M1 V'' vs xs"
shows "sum (λ s . card (RP M2 s vs xs V'')) S
        = sum (λ s . card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))) S"
using assms proof -
  have "finite (nodes M2)"
    using assms(3) by auto
  moreover have "S ⊆ nodes M2"
    using assms(7) by simp
  ultimately have "finite S"
    using infinite_super by blast

  then have "sum (λ s . card (RP M2 s vs xs V'')) S
              = sum (λ s . card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))) S"
  using assms proof (induction S)
    case empty
    show ?case by simp
  next
    case (insert s S)

    have "(insert s S) ⊆ nodes M2"
      using insert.prems(7) by simp
    then have "s ∈ nodes M2"
      by simp

    have "Prereq M2 M1 vs xs T S Ω V''"
      using ‹Prereq M2 M1 vs xs T (insert s S) Ω V''› by simp
    then have "(∑s∈S. card (RP M2 s vs xs V''))
                = (∑s∈S. card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a))"
      using insert.IH[OF insert.prems(1-6) _ assms(8,9)] by metis
    moreover have "(∑s'∈(insert s S). card (RP M2 s' vs xs V''))
                    = (∑s'∈S. card (RP M2 s' vs xs V'')) + card (RP M2 s vs xs V'')"
      by (simp add: add.commute insert.hyps(1) insert.hyps(2))
    ultimately have S_prop : "(∑s'∈(insert s S). card (RP M2 s' vs xs V''))
                               = (∑s∈S. card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a))
                                  + card (RP M2 s vs xs V'')"
      by presburger

    have "vs@xs ∈ L M1 ∩ L M2"
      using insert.prems(1) by simp

    obtain q2 q1 tr where suffix_path : "io_targets PM (initial PM) vs = {(q2,q1)}"
                          "path PM (xs || tr) (q2,q1)"
                          "length xs = length tr"
      using productF_language_state_intermediate[OF insert.prems(1)
            test_tools_props(1)[OF insert.prems(5,4)] OFSM_props(2,1)[OF insert.prems(3)]
                                    OFSM_props(2,1)[OF insert.prems(2)]]
      by blast



    have "card (RP M2 s vs xs V'')
            = card (⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V'')))"
      using OFSM_props(2,1)[OF insert.prems(3)] OFSM_props(2,1)[OF insert.prems(2)]
            RP_count_alt_def[OF ‹vs@xs ∈ L M1 ∩ L M2› _ _ _ _
                                ‹s∈nodes M2› test_tools_props(1)[OF insert.prems(5,4)]
                                suffix_path insert.prems(8)
                                test_tools_props(2)[OF insert.prems(5,4)] assms(6) insert.prems(9)]
      by linarith

    show "(∑s∈insert s S. card (RP M2 s vs xs V'')) =
                  (∑s∈insert s S. card (UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1))))"
    proof -
      have "(∑c∈insert s S. card (UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1))))
            = card (UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))
              + (∑c∈S. card (UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1))))"
        by (meson insert.hyps(1) insert.hyps(2) sum.insert)
      then show ?thesis
        using ‹(∑s'∈insert s S. card (RP M2 s' vs xs V''))
                = (∑s∈S. card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a))
                    + card (RP M2 s vs xs V'')›
              ‹card (RP M2 s vs xs V'')
                = card (UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))›
        by presburger
    qed
  qed

  then show ?thesis
    using assms by blast
qed


lemma finite_insert_card :
  assumes "finite (⋃SS)"
  and     "finite S"
  and     "S ∩ (⋃SS) = {}"
shows "card (⋃ (insert S SS)) = card (⋃SS) + card S"
  by (simp add: assms(1) assms(2) assms(3) card_Un_disjoint)

lemma LB_count_helper_RP_disjoint_M1_union :
  assumes "(vs @ xs) ∈ L M2 ∩ L M1"
  and     "OFSM M1"
  and     "OFSM M2"
  and     "asc_fault_domain M2 M1 m"
  and     "test_tools M2 M1 FAIL PM V Ω"
  and     "V'' ∈ Perm V M1"
  and     "Prereq M2 M1 vs xs T S Ω V''"
  and     "¬ Rep_Pre M2 M1 vs xs"
  and     "¬ Rep_Cov M2 M1 V'' vs xs"
shows "sum (λ s . card (RP M2 s vs xs V'')) S
        = card (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
using assms proof -
  have "finite (nodes M2)"
    using assms(3) by auto
  moreover have "S ⊆ nodes M2"
    using assms(7) by simp
  ultimately have "finite S"
    using infinite_super by blast

  then show "sum (λ s . card (RP M2 s vs xs V'')) S
              = card (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
  using assms proof (induction S)
    case empty
    show ?case by simp
  next
    case (insert s S)

    have "(insert s S) ⊆ nodes M2"
      using insert.prems(7) by simp
    then have "s ∈ nodes M2"
      by simp

    have "Prereq M2 M1 vs xs T S Ω V''"
      using ‹Prereq M2 M1 vs xs T (insert s S) Ω V''› by simp
    then have applied_IH : "(∑s∈S. card (RP M2 s vs xs V''))
                              = card (⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)"
      using insert.IH[OF insert.prems(1-6) _ insert.prems(8,9)] by metis

    obtain q2 q1 tr where suffix_path : "io_targets PM (initial PM) vs = {(q2,q1)}"
                              "path PM (xs || tr) (q2,q1)"
                              "length xs = length tr"
      using productF_language_state_intermediate
            [OF insert.prems(1) test_tools_props(1)[OF insert.prems(5,4)]
                OFSM_props(2,1)[OF insert.prems(3)] OFSM_props(2,1)[OF insert.prems(2)]]
      by blast

    have "s ∈ insert s S"
      by simp

    have "vs@xs ∈ L M1 ∩ L M2"
      using insert.prems(1) by simp

    have "∀ s' ∈ S . (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
                        ∩ (⋃a∈RP M2 s' vs xs V''. io_targets M1 (initial M1) a) = {}"
    proof
      fix s' assume "s' ∈ S"

      have "s ≠ s'"
        using insert.hyps(2) ‹s' ∈ S› by blast
      have "s' ∈ insert s S"
        using ‹s' ∈ S› by simp

      show "(⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
              ∩ (⋃a∈RP M2 s' vs xs V''. io_targets M1 (initial M1) a) = {}"
        using OFSM_props(2,1)[OF assms(3)] OFSM_props(2,1,3)[OF assms(2)]
              LB_count_helper_RP_disjoint_M1_pair(2)
                [OF ‹vs@xs ∈ L M1 ∩ L M2› _ _ _ _ test_tools_props(1)[OF insert.prems(5,4)]
                    suffix_path insert.prems(8) test_tools_props(2)[OF insert.prems(5,4)]
                    insert.prems(6,9,7) ‹s ≠ s'› ‹s ∈ insert s S› ‹s' ∈ insert s S›
                    test_tools_props(4)[OF insert.prems(5,4)]]
        by linarith
    qed
    then have disj_insert : "(⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
                                ∩ (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a) = {}"
      by blast
    have finite_S : "finite (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)"
      using RP_io_targets_finite_M1[OF insert.prems(1)]
      by (meson RP_io_targets_finite_M1 ‹vs @ xs ∈ L M1 ∩ L M2› assms(2) assms(5) insert.prems(6))
    have finite_s : "finite (⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)"
      by (meson RP_io_targets_finite_M1 ‹vs @ xs ∈ L M1 ∩ L M2› assms(2) assms(5)
          finite_UN_I insert.hyps(1) insert.prems(6))


    have "card (⋃s∈insert s S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
          = card (⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
            + card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)"
    proof -
      have f1: "insert (UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))
                    ((λc. UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1))) ` S)
                = (λc. UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1))) ` insert s S"
        by blast
      have "∀c. c ∈ S ⟶ UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1))
                          ∩ UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1)) = {}"
        by (meson ‹∀s'∈S. (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
                              ∩ (⋃a∈RP M2 s' vs xs V''. io_targets M1 (initial M1) a) = {}›)
      then have "UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1))
                  ∩ (⋃c∈S. UNION (RP M2 c vs xs V'') (io_targets M1 (initial M1))) = {}"
        by blast
      then show ?thesis
        using f1 by (metis finite_S finite_insert_card finite_s)
    qed

    have "card (RP M2 s vs xs V'')
          = card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)"
      using assms(2) assms(3)
            RP_count_alt_def[OF ‹vs@xs ∈ L M1 ∩ L M2› _ _ _ _ ‹s ∈ nodes M2›
                                test_tools_props(1)[OF insert.prems(5,4)] suffix_path
                                insert.prems(8) test_tools_props(2)[OF insert.prems(5,4)]
                                insert.prems(6,9)]
      by metis

    show ?case
    proof -
      have "(∑c∈insert s S. card (RP M2 c vs xs V''))
              = card (RP M2 s vs xs V'') + (∑c∈S. card (RP M2 c vs xs V''))"
        by (meson insert.hyps(1) insert.hyps(2) sum.insert)
      then show ?thesis
        using ‹card (RP M2 s vs xs V'')
                = card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)›
              ‹card (⋃s∈insert s S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
                = card (⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)
                  + card (⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a)› applied_IH
        by presburger
    qed
  qed
qed





lemma LB_count_helper_LB1 :
  assumes "(vs @ xs) ∈ L M2 ∩ L M1"
  and     "OFSM M1"
  and     "OFSM M2"
  and     "asc_fault_domain M2 M1 m"
  and     "test_tools M2 M1 FAIL PM V Ω"
  and     "V'' ∈ Perm V M1"
  and     "Prereq M2 M1 vs xs T S Ω V''"
  and     "¬ Rep_Pre M2 M1 vs xs"
  and     "¬ Rep_Cov M2 M1 V'' vs xs"
shows "(sum (λ s . card (RP M2 s vs xs V'')) S) ≤ card (nodes M1)"
proof -
  have "(⋃s∈S. UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1))) ⊆ nodes M1"
    by blast
  moreover have "finite (nodes M1)"
    using assms(2) OFSM_props(1) unfolding well_formed.simps finite_FSM.simps by simp
  ultimately have "card (⋃s∈S. UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))
                    ≤ card (nodes M1)"
    by (meson card_mono)

  moreover have "(∑s∈S. card (RP M2 s vs xs V''))
                    = card (⋃s∈S. UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))"
    using LB_count_helper_RP_disjoint_M1_union[OF assms]
    by linarith

  ultimately show ?thesis
    by linarith
qed




lemma LB_count_helper_D_states :
  assumes "observable M"
  and     "RS ∈ (D M T Ω)"
obtains q
where "q ∈ nodes M ∧ RS = IO_set M q Ω"
proof -
  have "RS ∈ image (λ io . B M io Ω) (LS⇩i⇩n M (initial M) T)"
    using assms by simp
  then obtain io where "RS = B M io Ω" "io ∈ LS⇩i⇩n M (initial M) T"
    by blast
  then have "io ∈ language_state M (initial M)"
    using language_state_for_inputs_in_language_state[of M "initial M" T] by blast
  then obtain q where "{q} = io_targets M (initial M) io"
    by (metis assms(1) io_targets_observable_singleton_ob)
  then have "B M io Ω = ⋃ (image (λ s . IO_set M s Ω) {q})"
    by simp
  then have "B M io Ω = IO_set M q Ω"
    by simp
  then have "RS = IO_set M q Ω" using ‹RS = B M io Ω›
    by simp
  moreover have "q ∈ nodes M" using ‹{q} = io_targets M (initial M) io›
    by (metis FSM.nodes.initial insertI1 io_targets_nodes)
  ultimately show ?thesis
    using that by simp
qed


lemma LB_count_helper_LB2 :
  assumes "observable M1"
  and     "IO_set M1 q Ω ∈ (D M1 T Ω) - {B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''}"
shows "q ∉ (⋃ (image (λ s . ⋃ (image (io_targets M1 (initial M1)) (RP M2 s vs xs V''))) S))"
proof
  assume "q ∈ (⋃s∈S. UNION (RP M2 s vs xs V'') (io_targets M1 (initial M1)))"
  then obtain s' where "s' ∈ S" "q ∈ (⋃ (image (io_targets M1 (initial M1)) (RP M2 s' vs xs V'')))"
    by blast
  then obtain xs' where "q ∈ io_targets M1 (initial M1) xs'" "xs' ∈ RP M2 s' vs xs V''"
    by blast
  then have "{q} = io_targets M1 (initial M1) xs'"
    by (metis assms(1) observable_io_target_is_singleton)
  then have "B M1 xs' Ω = ⋃ (image (λ s . IO_set M1 s Ω) {q})"
    by simp
  then have "B M1 xs' Ω = IO_set M1 q Ω"
    by simp
  moreover have "B M1 xs' Ω ∈ {B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''}"
    using ‹s' ∈ S› ‹xs' ∈ RP M2 s' vs xs V''› by blast
  ultimately have "IO_set M1 q Ω ∈ {B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''}"
    by blast
  moreover have "IO_set M1 q Ω ∉ {B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''}"
    using assms(2) by blast
  ultimately show "False"
    by simp
qed




subsection ‹ Validity of the result of LB constituting a lower bound ›


lemma LB_count :
assumes "(vs @ xs) ∈ L M1"
  and     "OFSM M1"
  and     "OFSM M2"
  and     "asc_fault_domain M2 M1 m"
  and     "test_tools M2 M1 FAIL PM V Ω"
  and     "V'' ∈ Perm V M1"
  and     "Prereq M2 M1 vs xs T S Ω V''"
  and     "¬ Rep_Pre M2 M1 vs xs"
  and     "¬ Rep_Cov M2 M1 V'' vs xs"
shows "LB M2 M1 vs xs T S Ω V'' ≤ |M1|"
proof -

  let ?D = "D M1 T Ω"
  let ?B = "{B M1 xs' Ω | xs' s' . s' ∈ S ∧ xs' ∈ RP M2 s' vs xs V''}"
  let ?DB = "?D - ?B"
  let ?RP = "⋃s∈S. ⋃a∈RP M2 s vs xs V''. io_targets M1 (initial M1) a"

  have "finite (nodes M1)"
    using OFSM_props[OF assms(2)] unfolding well_formed.simps finite_FSM.simps by simp
  then have "finite ?D"
    using OFSM_props[OF assms(2)] assms(7) D_bound[of M1 T Ω] unfolding Prereq.simps by linarith
  then have "finite ?DB"
    by simp

  ― ‹Proof sketch:
      Construct a function f (via induction) that maps each response set in ?DB to some state
      that produces that response set.
      This is then used to show that each response sets in ?DB indicates the existence of
      a distinct state in M1 not reached via the RP-sequences.›

  have states_f : "⋀ DB' . DB' ⊆ ?DB ⟹ ∃ f . inj_on f DB'
                                                ∧ image f DB' ⊆ (nodes M1) - ?RP
                                                ∧ (∀ RS ∈ DB' . IO_set M1 (f RS) Ω = RS)"
  proof -
    fix DB' assume "DB' ⊆ ?DB"
    have "finite DB'"
    proof (rule ccontr)
      assume "infinite DB'"
      have "infinite ?DB"
        using infinite_super[OF ‹DB' ⊆ ?DB› ‹infinite DB'› ] by simp
      then show "False"
        using ‹finite ?DB› by simp
    qed
    then show "∃ f . inj_on f DB' ∧ image f DB' ⊆ (nodes M1) - ?RP
                                  ∧ (∀ RS ∈ DB' . IO_set M1 (f RS) Ω = RS)"
    using assms ‹DB' ⊆ ?DB› proof (induction DB')
      case empty
      show ?case by simp
    next
      case (insert RS DB')

      have "DB' ⊆ ?DB"
        using insert.prems(10) by blast
      obtain f' where "inj_on f' DB'"
                      "image f' DB' ⊆ (nodes M1) - ?RP"
                      "∀ RS ∈ DB' . IO_set M1 (f' RS) Ω = RS"
        using insert.IH[OF insert.prems(1-9) ‹DB' ⊆ ?DB›]
        by blast

      have "RS ∈ D M1 T Ω"
        using insert.prems(10) by blast
      obtain q where "q ∈ nodes M1" "RS = IO_set M1 q Ω"
        using insert.prems(2)  LB_count_helper_D_states[OF _ ‹RS ∈ D M1 T Ω›]
        by blast
      then have "IO_set M1 q Ω ∈ ?DB"
        using insert.prems(10) by blast

      have "q ∉ ?RP"
        using insert.prems(2) LB_count_helper_LB2[OF _ ‹IO_set M1 q Ω ∈ ?DB›]
        by blast

      let ?f = "f'(RS := q)"
      have "inj_on ?f (insert RS DB')"
      proof
        have "?f RS ∉ ?f ` (DB' - {RS})"
        proof
          assume "?f RS ∈ ?f ` (DB' - {RS})"
          then have "q ∈ ?f ` (DB' - {RS})" by auto
          have "RS ∈ DB'"
          proof -
            have "∀P c f. ∃Pa. ((c::'c) ∉ f ` P ∨ (Pa::('a × 'b) list set) ∈ P)
                                ∧ (c ∉ f ` P ∨ f Pa = c)"
              by auto
            moreover
            { assume "q ∉ f' ` DB'"
              moreover
              { assume "q ∉ f'(RS := q) ` DB'"
                then have ?thesis
                  using ‹q ∈ f'(RS := q) ` (DB' - {RS})› by blast }
              ultimately have ?thesis
                by (metis fun_upd_image) }
            ultimately show ?thesis
              by (metis (no_types) ‹RS = IO_set M1 q Ω› ‹∀RS∈DB'. IO_set M1 (f' RS) Ω = RS›)
          qed
          then show "False" using insert.hyps(2) by simp
        qed
        then show "inj_on ?f DB' ∧ ?f RS ∉ ?f ` (DB' - {RS})"
          using ‹inj_on f' DB'› inj_on_fun_updI by fastforce
      qed
      moreover have "image ?f (insert RS DB') ⊆ (nodes M1) - ?RP"
      proof -
        have "image ?f {RS} = {q}" by simp
        then have "image ?f {RS} ⊆ (nodes M1) - ?RP"
          using ‹q ∈ nodes M1› ‹q ∉ ?RP› by auto
        moreover have "image ?f (insert RS DB') = image ?f {RS} ∪ image ?f DB'"
          by auto
        ultimately show ?thesis
          by (metis (no_types, lifting) ‹image f' DB' ⊆ (nodes M1) - ?RP› fun_upd_other image_cong
              image_insert insert.hyps(2) insert_subset)
      qed
      moreover have "∀ RS ∈ (insert RS DB') . IO_set M1 (?f RS) Ω = RS"
        using ‹RS = IO_set M1 q Ω› ‹∀RS∈DB'. IO_set M1 (f' RS) Ω = RS› by auto

      ultimately show ?case
        by blast
    qed
  qed

  have "?DB ⊆ ?DB"
    by simp
  obtain f where "inj_on f ?DB" "image f ?DB ⊆ (nodes M1) - ?RP"
    using states_f[OF ‹?DB ⊆ ?DB›] by blast
  have "finite (nodes M1 - ?RP)"
    using ‹finite (nodes M1)› by simp
  have "card ?DB ≤ card (nodes M1 - ?RP)"
    using card_inj_on_le[OF ‹inj_on f ?DB› ‹image f ?DB ⊆ (nodes M1) - ?RP›
                            ‹finite (nodes M1 - ?RP)›]
    by assumption

  have "?RP ⊆ nodes M1"
    by blast
  then have "card (nodes M1 - ?RP) = card (nodes M1) - card ?RP"
    by (meson ‹finite (nodes M1)› card_Diff_subset infinite_subset)
  then have "card ?DB ≤ card (nodes M1) - card ?RP"
    using ‹card ?DB ≤ card (nodes M1 - ?RP)› by linarith

  have "vs @ xs ∈ L M2 ∩ L M1"
    using assms(7) by simp
  have "(sum (λ s . card (RP M2 s vs xs V'')) S) = card ?RP"
    using LB_count_helper_RP_disjoint_M1_union[OF ‹vs @ xs ∈ L M2 ∩ L M1› assms(2-9)] by simp
  moreover have "card ?RP ≤ card (nodes M1)"
    using card_mono[OF ‹finite (nodes M1)› ‹?RP ⊆ nodes M1›] by assumption
  ultimately show ?thesis
    unfolding LB.simps using ‹card ?DB ≤ card (nodes M1) - card ?RP›
    by linarith
qed



lemma contradiction_via_LB :
assumes "(vs @ xs) ∈ L M1"
  and     "OFSM M1"
  and     "OFSM M2"
  and     "asc_fault_domain M2 M1 m"
  and     "test_tools M2 M1 FAIL PM V Ω"
  and     "V'' ∈ Perm V M1"
  and     "Prereq M2 M1 vs xs T S Ω V''"
  and     "¬ Rep_Pre M2 M1 vs xs"
  and     "¬ Rep_Cov M2 M1 V'' vs xs"
  and     "LB M2 M1 vs xs T S Ω V'' > m"
shows  "False"
proof -
  have "LB M2 M1 vs xs T S Ω V'' ≤ card (nodes M1)"
    using LB_count[OF assms(1-9)] by assumption
  moreover have "card (nodes M1) ≤ m"
    using assms(4) by auto
  ultimately show "False"
    using assms(10) by linarith
qed



end