Theory H_Framework

section ‹H-Framework›

text ‹This theory defines the H-Framework and provides completeness properties.›

theory H_Framework
imports Convergence_Graph "../Prefix_Tree" "../State_Cover"
begin


subsection ‹Abstract H-Condition›

(* assumes that V is a state cover assignment *)
definition satisfies_abstract_h_condition :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ nat ⇒ bool" where
  "satisfies_abstract_h_condition M1 M2 V m = (∀ q γ . 
    q ∈ reachable_states M1 ⟶ 
    length γ ≤ Suc (m-size_r M1) ⟶ 
    list.set γ ⊆ inputs M1 × outputs M1  ⟶ 
    butlast γ ∈ LS M1 q ⟶ 
    (let traces = (V ` reachable_states M1)
                  ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)} 
      in (L M1 ∩ traces = L M2 ∩ traces)
         ∧ preserves_divergence M1 M2 traces))"



lemma abstract_h_condition_exhaustiveness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
  and     "is_state_cover_assignment M V"
  and     "satisfies_abstract_h_condition M I V m"
shows "L M = L I"
proof (rule ccontr)
  assume "L M ≠ L I"

  (* unfold the sufficient condition for easier reference *)

  define Π where Π: "Π = (V ` reachable_states M)"
  define n where n: "n = size_r M"
  define 𝒳 where 𝒳: "𝒳 = (λ q . {io@[(x,y)] | io x y . io ∈ LS M q ∧ length io ≤ m-n ∧ x ∈ inputs M ∧ y ∈ outputs M})"

  have pass_prop: "⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-n) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹
                    (L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                     = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and dist_prop: "⋀ q γ . q ∈ reachable_states M ⟹ length γ ≤ Suc (m-n) ⟹ list.set γ ⊆ inputs M × outputs M  ⟹ butlast γ ∈ LS M q ⟹
                     preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
    using ‹satisfies_abstract_h_condition M I V m› 
    unfolding satisfies_abstract_h_condition_def Let_def Π n  by blast+

  have pass_prop_𝒳 : "⋀ q γ . q ∈ reachable_states M ⟹ γ ∈ 𝒳 q ⟹
                           (L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                            = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
   and dist_prop_𝒳 : "⋀ q γ . q ∈ reachable_states M ⟹ γ ∈ 𝒳 q ⟹
                           preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
  proof -
    fix q γ assume *: "q ∈ reachable_states M" and "γ ∈ 𝒳 q"
    then obtain io x y where "γ = io@[(x,y)]" and "io ∈ LS M q" and "length io ≤ m-n" and "x ∈ inputs M" and "y ∈ outputs M"
      unfolding 𝒳 by blast

    have **:"length γ ≤ Suc (m-n)"
      using ‹γ = io@[(x,y)]› ‹length io ≤ m-n› by auto
    have ***:"list.set γ ⊆ inputs M × outputs M"
      using language_io[OF ‹io ∈ LS M q›] ‹x ∈ inputs M› ‹y ∈ outputs M›
      unfolding ‹γ = io@[(x,y)]› by auto
    have ****:"butlast γ ∈ LS M q"
      unfolding ‹γ = io@[(x,y)]› using ‹io ∈ LS M q› by auto
    
    show "(L M ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                            = L I ∩ (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
      using pass_prop[OF * ** *** ****] .
    show "preserves_divergence M I (Π ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
      using dist_prop[OF * ** *** ****] .
  qed


  (* obtain minimal trace that
      - extends some sequence of the state cover (which contains the empty sequence), and
      - is contained in either L M or L I *)
 
  have "(L M ∩ Π) = (L I ∩ Π)"
    using pass_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
  moreover have "Π ⊆ L M"
    unfolding Π using state_cover_assignment_after(1)[OF assms(1) ‹is_state_cover_assignment M V›]
    by blast
  ultimately have "Π ⊆ L I"
    using ‹Π = (V ` reachable_states M)› by blast

  obtain π τ' where "π ∈ Π"
                and "π @ τ' ∈ (L M - L I) ∪ (L I - L M)"
                and "⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io"
    using ‹(L M ∩ Π) = (L I ∩ Π)›
    using minimal_sequence_to_failure_from_state_cover_assignment_ob[OF ‹L M ≠ L I› ‹is_state_cover_assignment M V›] 
    unfolding Π
    by blast

  obtain q where "q ∈ reachable_states M" and "π = V q"
    using ‹π ∈ Π› unfolding Π by blast
  then have "π ∈ L M" and "after_initial M π = q"
    using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M V›]
    by blast+
  

  have τ'_min: "⋀ π' io . π' ∈ Π ⟹ π'@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io"
  proof -
    fix π' io
    assume "π' ∈ Π" and "π'@io ∈ (L M - L I) ∪ (L I - L M)"
    then obtain q where "q ∈ reachable_states M" and "π' = V q"
      unfolding Π by blast
    then show "length τ' ≤ length io"
      using ‹⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io›
            ‹π'@io ∈ (L M - L I) ∪ (L I - L M)› by auto
  qed


  

  obtain πτ xy τ'' where "π @ τ' = πτ @ [xy] @ τ''"
                      and "πτ ∈ L M ∩ L I"
                      and "πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)"
    using minimal_failure_prefix_ob[OF ‹observable M› ‹observable I› fsm_initial fsm_initial, of "π @ τ'"]
    using minimal_failure_prefix_ob[OF ‹observable I› ‹observable M› fsm_initial fsm_initial, of "π @ τ'"]
    using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
    by (metis Int_commute Un_iff)

  moreover obtain x y where "xy = (x,y)"
    using surjective_pairing by blast

  moreover have "πτ = π @ butlast τ'"
  proof -
    have "length πτ ≥ length π"
    proof (rule ccontr) 
      assume "¬ length π ≤ length πτ"
      then have "length (πτ@[xy]) ≤ length π"
        by auto
      then have "take (length (πτ@[xy])) π = πτ@[xy]"
        using ‹π @ τ' = πτ @ [xy] @ τ''›
        by (metis append_assoc append_eq_append_conv_if) 
      then have "π = (πτ@[xy]) @ (drop (length (πτ@[xy])) π)"
        by (metis append_take_drop_id)          
      then have "πτ@[xy] ∈ L M ∩ L I"
        using ‹π ∈ Π› ‹Π ⊆ L I› ‹Π ⊆ L M› 
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of M "initial M"]
        using language_prefix[of "(πτ@[xy])" "drop (length (πτ@[xy])) π", of I "initial I"]
        by auto
      then show "False"
        using ‹πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)› by blast
    qed

    then have "πτ = π @ (take (length πτ - length π) τ')"
      using ‹π @ τ' = πτ @ [xy] @ τ''›
      by (metis dual_order.refl take_all take_append take_le) 
    then have "π @ ((take (length πτ - length π) τ')@[xy]) ∈ (L I - L M) ∪ (L M - L I)"
      using ‹πτ@[xy] ∈ (L I - L M) ∪ (L M - L I)›
      by (metis append_assoc)        
    then have "length τ' ≤ Suc (length (take (length πτ - length π) τ'))"
      using τ'_min[OF ‹π ∈ Π›]
      by (metis Un_commute length_append_singleton)
    moreover have "length τ' ≥ Suc (length (take (length πτ - length π) τ'))"
      using ‹π @ τ' = πτ @ [xy] @ τ''› ‹πτ = π @ take (length πτ - length π) τ'› not_less_eq_eq by fastforce
    ultimately have "length τ' = Suc (length (take (length πτ - length π) τ'))"
      by simp
    then show ?thesis
    proof -
      have "π @ τ' = (π @ take (length πτ - length π) τ') @ [xy] @ τ''"
        using ‹π @ τ' = πτ @ [xy] @ τ''› ‹πτ = π @ take (length πτ - length π) τ'› by presburger
      then have "take (length πτ - length π) τ' = butlast τ'"
        by (metis (no_types) ‹length τ' = Suc (length (take (length πτ - length π) τ'))› append_assoc append_butlast_last_id append_eq_append_conv diff_Suc_1 length_butlast length_greater_0_conv zero_less_Suc)
      then show ?thesis
        using ‹πτ = π @ take (length πτ - length π) τ'› by fastforce
    qed 
  qed

  ultimately have "π @ (butlast τ') ∈ L M ∩ L I"
              and "(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)"
    by auto

  have "τ' = (butlast τ')@[(x,y)]"
    using ‹π @ τ' = πτ @ [xy] @ τ''› ‹xy = (x,y)› 
    unfolding ‹πτ = π @ butlast τ'›
    by (metis (no_types, opaque_lifting) append_Cons append_butlast_last_id butlast.simps(1) butlast_append last_appendR list.distinct(1) self_append_conv)


  have "x ∈ inputs M" and "y ∈ outputs M"
  proof -
    have *: "(x,y) ∈ list.set ((π @ (butlast τ'))@[(x,y)])"
      by auto

    show "x ∈ inputs M"
      using ‹(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)› 
            language_io(1)[OF _ *, of I]
            language_io(1)[OF _ *, of M]
            ‹inputs I = inputs M›
      by blast

    show "y ∈ outputs M"
      using ‹(π @ (butlast τ'))@[(x,y)] ∈ (L I - L M) ∪ (L M - L I)› 
            language_io(2)[OF _ *, of I]
            language_io(2)[OF _ *, of M]
            ‹outputs I = outputs M›
      by blast
  qed

  have "π @ (butlast τ') ∈ L M"
    using  ‹π @ (butlast τ') ∈ L M ∩ L I› by auto
  have "list.set (π @ τ') ⊆ inputs M × outputs M"
    using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
    using language_io[of ‹π @ τ'› M "initial M"]
    using language_io[of ‹π @ τ'› I "initial I"]
    unfolding assms(6,7) by fast 
  then have "list.set τ' ⊆ inputs M × outputs M"
    by auto
  have "list.set (butlast τ') ⊆ inputs M × outputs M"
    using language_io[OF ‹π @ (butlast τ') ∈ L M›] by force
  have "butlast τ' ∈ LS M q"
    using after_language_iff[OF assms(1) ‹π ∈ L M›] ‹π @ (butlast τ') ∈ L M›
    unfolding ‹after_initial M π = q›
    by blast

  have "length τ' > m - n + 1"
  proof (rule ccontr)
    assume "¬ m - n + 1 < length τ'"
    then have "length τ' ≤ Suc (m - n)"
      by auto

    have "π @ τ' ∈ (Π ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes τ')})"
      unfolding ‹π = V q› using ‹q ∈ reachable_states M›  unfolding prefixes_set by auto
    then have "L M ∩ {π @ τ'} = L I ∩ {π @ τ'}"
      using pass_prop[OF ‹q ∈ reachable_states M› ‹length τ' ≤ Suc (m - n)› ‹list.set τ' ⊆ inputs M × outputs M› ‹butlast τ' ∈ LS M q›]
      by blast
    then show False
      using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)› by blast
  qed



  define τ where τ_def: "τ = (λi . take i (butlast τ'))"

  have "⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q"
  proof -
    fix i assume "i > 0" and "i ≤ m - n + 1"
    
    then have "τ i = (butlast (τ i)) @ [last (τ i)]"
      using τ_def ‹length τ' > m - n + 1›
      by (metis add_less_same_cancel2 append_butlast_last_id length_butlast less_diff_conv list.size(3) not_add_less2 take_eq_Nil) 

    have "length (butlast (τ i)) ≤ m - n" 
      using τ_def ‹length τ' > m - n + 1› ‹i ≤ m - n + 1› by auto


    have "q ∈ io_targets M π (initial M)"
      using ‹is_state_cover_assignment M V› ‹q ∈ reachable_states M› ‹π = V q›
      by simp 
    then have "(butlast τ') ∈ LS M q"
      using ‹π @ (butlast τ') ∈ L M ∩ L I› 
      using observable_io_targets_language[OF _ ‹observable M›] 
      by force
    then have "τ i @ (drop i (butlast τ')) ∈ LS M q"
      using τ_def by auto
    then have "τ i ∈ LS M q"
      using language_prefix
      by fastforce 
    then have "butlast (τ i) ∈ LS M q"
      using language_prefix ‹τ i = (butlast (τ i)) @ [last (τ i)]›
      by metis 

    have "(fst (last (τ i)), snd (last (τ i))) ∈ list.set ((butlast (τ i)) @ [last (τ i)])"
      using ‹τ i = (butlast (τ i)) @ [last (τ i)]›
      using in_set_conv_decomp by fastforce
    then have "fst (last (τ i)) ∈ inputs M" 
          and "snd (last (τ i)) ∈ outputs M"
      using ‹τ i ∈ LS M q› ‹τ i = (butlast (τ i)) @ [last (τ i)]› language_io[of "(butlast (τ i)) @ [last (τ i)]" M q "fst (last (τ i))" "snd (last (τ i))"] 
      by auto
      
    then show "τ i ∈ 𝒳 q"
      unfolding 𝒳 
      using ‹length (butlast (τ i)) ≤ m - n› ‹τ i = (butlast (τ i)) @ [last (τ i)]›
            ‹butlast (τ i) ∈ LS M q›
      by (metis (mono_tags, lifting) mem_Collect_eq surjective_pairing)
  qed

  have "⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I"
  proof -
    fix i assume "i ≤ m-n+1"

    have "butlast τ' = τ i @ (drop i (butlast τ'))"
      unfolding τ_def by auto
    then have ‹(π @ τ i) @ (drop i (butlast τ')) ∈ L M ∩ L I›
      using ‹π @ (butlast τ') ∈ L M ∩ L I›
      by auto
    then show "π @ (τ i) ∈ L M ∩ L I"
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of M "initial M"]
      using language_prefix[of "(π @ τ i)" "(drop i (butlast τ'))", of I "initial I"]
      by blast
  qed

  have B_diff: "Π ∩ (λi . π @ (τ i)) ` {1 .. m-n+1} = {}"
  proof -
    have "⋀ io1 io2 . io1 ∈ Π ⟹ io2 ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹ io1 ≠ io2"
    proof (rule ccontr)
      fix io1 io2 assume "io1 ∈ Π" "io2 ∈ (λi . π @ (τ i)) ` {1 .. m-n+1}" "¬ io1 ≠ io2"

      then obtain i where "io2 = π @ (τ i)" and "i ≥ 1" and "i ≤ m - n + 1" and "π @ (τ i) ∈ Π"
        by auto
      then have "π @ (τ i) ∈ L M"
        using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› by auto
      
      obtain q where "q ∈ reachable_states M" and "V q = π @ (τ i)"
        using ‹π @ (τ i) ∈ Π› Π
        by auto 
      moreover have "(π @ (τ i))@(drop i τ') ∈ (L M - L I) ∪ (L I - L M)"
        using τ_def ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)› ‹length τ' > m - n + 1› ‹i ≤ m - n + 1›
        by (metis append_assoc append_take_drop_id le_iff_sup sup.strict_boundedE take_butlast) 
      ultimately have "length τ' ≤ length (drop i τ')"
        using ‹⋀ io q . q ∈ reachable_states M ⟹ (V q)@io ∈ (L M - L I) ∪ (L I - L M) ⟹ length τ' ≤ length io›
        by presburger
      then show "False"
        using ‹length τ' > m - n + 1› ‹i ≥ 1›
        by (metis One_nat_def ‹i ≤ m - n + 1› diff_diff_cancel diff_is_0_eq' le_trans length_drop less_Suc_eq nat_less_le) 
    qed
    then show ?thesis 
      by blast
  qed


  have same_targets_in_I: "∃ α β . 
                    α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}
                    ∧ β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}
                    ∧ α ≠ β ∧ (after_initial I α = after_initial I β)"
  proof - 
    have "after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}) ⊆ states I"
    proof 
      fix q assume "q ∈ after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})"
      then obtain io where "io ∈ (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})" and "q = after_initial I io"
        by blast
      then have "io ∈ L I"
        using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› ‹Π ⊆ L I› by auto
      then show "q ∈ states I"
        unfolding ‹q = after_initial I io› 
        using observable_after_path[OF ‹observable I›, of io "initial I"] path_target_is_state[of I "initial I"]
        by metis 
    qed
    then have "card (after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})) ≤ m"
      using ‹size I ≤ m› fsm_states_finite[of I] unfolding FSM.size_def
      by (meson card_mono le_trans) 
    moreover have "card (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}) = m+1"
    proof -
      have *: "card Π = n"
        using state_cover_assignment_card[OF ‹is_state_cover_assignment M V› ‹observable M›] unfolding Π n .
      have **: "card ((λi . π @ (τ i)) ` {1 .. m-n+1}) = m-n+1"
      proof -
        have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
          by auto
        moreover have "inj_on (λi . π @ (τ i)) {1 .. m-n+1}" 
        proof 
          fix x y assume "x ∈ {1..m - n + 1}" "y ∈ {1..m - n + 1}" "π @ τ x = π @ τ y"

          then have "take x τ' = take y τ'"
            unfolding τ_def ‹length τ' > m - n + 1›
            by (metis (no_types, lifting) ‹m - n + 1 < length τ'› atLeastAtMost_iff diff_is_0_eq le_trans nat_less_le same_append_eq take_butlast zero_less_diff)
          moreover have "x ≤ length τ'"
            using ‹x ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
          moreover have "y ≤ length τ'"
            using ‹y ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
          ultimately show "x=y"
            by (metis length_take min.absorb2) 
        qed
        moreover have "card {1..m - n + 1} = m - n + 1"
          by auto
        ultimately show ?thesis
          by (simp add: card_image) 
      qed

      have ***: "n + (m - n + 1) = m+1"
        unfolding n using ‹m ≥ size_r M› by auto

      have "finite Π"
        unfolding Π using fsm_states_finite restrict_to_reachable_states_simps(2)
        by (metis finite_imageI) 
      have "finite ((λi . π @ (τ i)) ` {1 .. m-n+1})"
        by auto
      
      show ?thesis
        using card_Un_disjoint[OF ‹finite Π› ‹finite ((λi. π @ τ i) ` {1..m - n + 1})› ‹Π ∩ (λi . π @ (τ i)) ` {1 .. m-n+1} = {}›]
        unfolding * ** *** .
    qed
    ultimately have *: "card (after_initial I ` (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})) < card (Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1})"
      by simp
    
    show ?thesis
      using pigeonhole[OF *] unfolding inj_on_def by blast
  qed

  (* covered converging traces in I must also converge in M *)
  have same_targets_in_M: "⋀ α β . 
                    α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹
                    β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1} ⟹
                    α ≠ β ⟹ 
                    (after_initial I α = after_initial I β) ⟹
                    (after_initial M α = after_initial M β)"
  proof (rule ccontr)
    fix α β assume "α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}"
               and "α ≠ β"
               and "(after_initial I α = after_initial I β)"
               and "(after_initial M α ≠ after_initial M β)"


    have *: "(λi . π @ (τ i)) ` {1 .. m-n+1} ⊆ { (V q) @ τ | q τ . q ∈ reachable_states M ∧ τ ∈ 𝒳 q}"
      using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q› ‹q ∈ reachable_states M› ‹π = V q›
      by force

    have "α ∈ L M" and "β ∈ L M" and "α ∈ L I" and "β ∈ L I"
      using ‹α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}› 
            ‹β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
            ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› 
            ‹Π ⊆ L M› ‹Π ⊆ L I› 
      by auto
    then have "¬ converge M α β" and "converge I α β"
      using ‹after_initial M α ≠ after_initial M β› 
      using ‹minimal M› 
      using after_is_state[OF assms(1) ‹α ∈ L M›]
      using after_is_state[OF assms(1) ‹β ∈ L M›]
      unfolding converge.simps minimal.simps ‹after_initial I α = after_initial I β› by auto
    then have "¬ converge M β α" and "converge I β α"
      using converge_sym by blast+

    
    have split_helper: "⋀ (P :: nat ⇒ nat ⇒ bool) . (∃ i j . P i j ∧ i ≠ j) = ((∃ i j . P i j ∧ i < j) ∨ (∃ i j . P i j ∧ i > j))"
    proof 
      show "⋀ (P :: nat ⇒ nat ⇒ bool) . ∃i j. P i j ∧ i ≠ j ⟹ (∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i)" 
      proof -
        fix P :: "nat ⇒ nat ⇒ bool" 
        assume "∃i j. P i j ∧ i ≠ j"
        then obtain i j where "P i j" and "i ≠ j" by auto
        then have "i < j ∨ i > j" by auto
        then show "(∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i)" using ‹P i j› by auto
      qed
      show "⋀ (P :: nat ⇒ nat ⇒ bool) . (∃i j. P i j ∧ i < j) ∨ (∃i j. P i j ∧ j < i) ⟹ ∃i j. P i j ∧ i ≠ j" by auto
    qed
    have split_scheme:"(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α = π @ (τ i) ∧ β = π @ (τ j))
          = ((∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i < j ∧ α = π @ (τ i) ∧ β = π @ (τ j))
              ∨ (∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i > j ∧ α = π @ (τ i) ∧ β = π @ (τ j)))"
      using ‹α ≠ β›  
      using split_helper[of "λ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α = π @ (τ i) ∧ β = π @ (τ j)"]
      by blast

    consider "(α ∈ Π ∧ β ∈ Π)" |
             "(∃ i . i ∈ {1 .. m-n+1} ∧ α ∈ Π ∧ β = π @ (τ i))" |
             "(∃ i . i ∈ {1 .. m-n+1} ∧ β ∈ Π ∧ α = π @ (τ i))" |
             "(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i < j ∧ α = π @ (τ i) ∧ β = π @ (τ j))" |
             "(∃ i j . i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ i > j ∧ α = π @ (τ i) ∧ β = π @ (τ j))"
      using ‹α ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
            ‹β ∈ Π ∪ (λi . π @ (τ i)) ` {1 .. m-n+1}›
      using split_scheme 
      by blast

    then have "∃ α' β' . α' ∈ L M ∧ β' ∈ L M ∧ ¬converge M α' β' ∧ converge I α' β' ∧
            ( (α' ∈ Π ∧ β' ∈ Π) 
              ∨ (∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i))
              ∨ (∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j)))"
      using ‹α ∈ L M› ‹β ∈ L M› ‹¬ converge M α β› ‹converge I α β› ‹¬ converge M β α› ‹converge I β α› 
      by metis

    then obtain α' β' where "α' ∈ L M" and "β' ∈ L M" and "¬converge M α' β'" and "converge I α' β' "
                        and "(α' ∈ Π ∧ β' ∈ Π) 
                              ∨ (∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i))
                              ∨ (∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j))"
      by blast
    then consider "α' ∈ Π ∧ β' ∈ Π"
      | "∃ i . i ∈ {1 .. m-n+1} ∧ α' ∈ Π ∧ β' = π @ (τ i)"
      | "∃ i j . i < j ∧ i ∈ {1 .. m-n+1} ∧ j ∈ {1 .. m-n+1} ∧ α' = π @ (τ i) ∧ β' = π @ (τ j)"
      by blast

    then show False proof cases
      case 1
      moreover have "preserves_divergence M I Π"
        using dist_prop[OF reachable_states_initial, of "[]"] language_contains_empty_sequence[of M] by auto
      ultimately show ?thesis 
        using ‹¬converge M α' β'› ‹converge I α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        unfolding preserves_divergence.simps 
        by blast
    next
      case 2
      then obtain i where "i ∈ {1 .. m-n+1}" and "α' ∈ Π" and "β' = π @ (τ i)"
        by blast
      then have "τ i ∈ 𝒳 q" 
        using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q›
        by force 

      have "β' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ i))}"
        unfolding ‹β' = π @ (τ i)› ‹π = V q› prefixes_set by auto 
      then have "¬converge I α' β'"
        using ‹α' ∈ Π› ‹¬converge M α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        using dist_prop_𝒳[OF ‹q ∈ reachable_states M› ‹τ i ∈ 𝒳 q›]
        unfolding preserves_divergence.simps by blast
      then show False
        using ‹converge I α' β'› by blast
    next
      case 3
      then obtain i j where "i ∈ {1 .. m-n+1}" and "j ∈ {1 .. m-n+1}" and "α' = π @ (τ i)" and "β' = π @ (τ j)" and "i < j" by blast
      then have "τ j ∈ 𝒳 q" 
        using ‹⋀ i . i > 0 ⟹ i ≤ m - n + 1 ⟹ (τ i) ∈ 𝒳 q›
        by force 

      have "(τ i) = take i (τ j)"
        using ‹i < j› unfolding τ_def
        by simp
      then have "(τ i) ∈ list.set (prefixes (τ j))"
        unfolding prefixes_set
        by (metis (mono_tags) append_take_drop_id mem_Collect_eq)
      then have "α' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ j))}"
        unfolding ‹α' = π @ (τ i)› ‹π = V q›
        by simp
      moreover have "β' ∈ {V q @ ω' |ω'. ω' ∈ list.set (prefixes (τ j))}"
        unfolding ‹β' = π @ (τ j)› ‹π = V q› prefixes_set by auto 
      ultimately have "¬converge I α' β'"
        using ‹¬converge M α' β'› ‹α' ∈ L M› ‹β' ∈ L M›
        using dist_prop_𝒳[OF ‹q ∈ reachable_states M› ‹τ j ∈ 𝒳 q›]
        unfolding preserves_divergence.simps by blast
      then show False
        using ‹converge I α' β'› by blast
    qed
  qed


  have case_helper: "⋀ A B P . (⋀ x y . P x y = P y x) ⟹ 
                                (∃ x y . x ∈ A ∪ B ∧ y ∈ A ∪ B ∧ P x y) =
                                          ((∃ x y . x ∈ A ∧ y ∈ A ∧ P x y)
                                            ∨ (∃ x y . x ∈ A ∧ y ∈ B ∧ P x y)
                                            ∨ (∃ x y . x ∈ B ∧ y ∈ B ∧ P x y))"
    by auto
  have *: "(⋀x y. (x ≠ y ∧ FSM.after I (FSM.initial I) x = FSM.after I (FSM.initial I) y) =
          (y ≠ x ∧ FSM.after I (FSM.initial I) y = FSM.after I (FSM.initial I) x))"
    by auto
    
  consider (a) "∃ α β . α ∈ Π ∧ β ∈ Π ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" | 
           (b) "∃ α β . α ∈ Π ∧ β ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" |
           (c) "∃ α β . α ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ β ∈ (λi . π @ (τ i)) ` {1 .. m-n+1} ∧ α ≠ β ∧ (after_initial I α = after_initial I β)" 
    using same_targets_in_I
    unfolding case_helper[of "λ x y . x ≠ y ∧ (after_initial I x = after_initial I y)" Π "(λi . π @ (τ i)) ` {1 .. m-n+1}", OF *] 
    by blast
  then show "False" proof cases
    case a (* elements of the state cover cannot coincide *)
    then obtain α β  where "α ∈ Π" and "β ∈ Π" and "α ≠ β" and "(after_initial I α = after_initial I β)" by blast
    then have "(after_initial M α = after_initial M β)"
      using same_targets_in_M by blast

    obtain q1 q2 where "q1 ∈ reachable_states M" and "α = V q1"
                   and "q2 ∈ reachable_states M" and "β = V q2"
      using ‹α ∈ Π› ‹β ∈ Π› ‹α ≠ β›
      unfolding Π by blast
    then have "q1 ≠ q2"
      using ‹α ≠ β› by auto

    have "α ∈ L M" 
      using ‹Π ⊆ L M› ‹α ∈ Π› by blast
    have "q1 = after_initial M α"
      using ‹is_state_cover_assignment M V› ‹q1 ∈ reachable_states M› observable_io_targets[OF ‹observable M› ‹α ∈ L M›] 
      unfolding is_state_cover_assignment.simps ‹α = V q1›
      by (metis ‹is_state_cover_assignment M V› assms(1) is_state_cover_assignment_observable_after)

    have "β ∈ L M" 
      using ‹Π ⊆ L M› ‹β ∈ Π› by blast
    have "q2 = after_initial M β"
      using ‹is_state_cover_assignment M V› ‹q2 ∈ reachable_states M› observable_io_targets[OF ‹observable M› ‹β ∈ L M›] 
      unfolding is_state_cover_assignment.simps ‹β = V q2›
      by (metis ‹is_state_cover_assignment M V› assms(1) is_state_cover_assignment_observable_after)

    show "False"
      using ‹q1 ≠ q2› ‹(after_initial M α = after_initial M β)›
      unfolding ‹q1 = after_initial M α› ‹q2 = after_initial M β› 
      by simp
  next
    case b (* state cover and π@(τ i) cannot coincide due to minimality of π@τ' *)
    then obtain α β where "α ∈ Π"
                      and "β ∈ (λi. π @ τ i) ` {1..m - n + 1}"
                      and "α ≠ β" 
                      and "FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β"
      by blast
    then have "FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β"
      using same_targets_in_M by blast

    obtain i where "β = π@(τ i)" and "i ∈ {1..m - n + 1}"
      using ‹β ∈ (λi. π @ τ i) ` {1..m - n + 1}› by auto

    have "α ∈ L M" and "α ∈ L I" 
      using ‹Π ⊆ L M›  ‹Π ⊆ L I› ‹α ∈ Π› by blast+
    have "β ∈ L M" and "β ∈ L I" 
      using ‹β ∈ (λi. π @ τ i) ` {1..m - n + 1}› ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› 
      by auto

    let ?io = "drop i τ'"

    have "τ' = (τ i) @ ?io"
      using ‹i ∈ {1..m - n + 1}› ‹length τ' > m-n+1› 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "β@?io ∈ (L M - L I) ∪ (L I - L M)"
      using ‹β = π@(τ i)›  ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
      by auto
    then have "α@?io ∈ (L M - L I) ∪ (L I - L M)"
      using observable_after_eq[OF ‹observable M› ‹FSM.after M (FSM.initial M) α = FSM.after M (FSM.initial M) β› ‹α ∈ L M› ‹β ∈ L M›]
            observable_after_eq[OF ‹observable I› ‹FSM.after I (FSM.initial I) α = FSM.after I (FSM.initial I) β› ‹α ∈ L I› ‹β ∈ L I›]
      by blast
    then show "False"
      using τ'_min[OF ‹α ∈ Π›, of ?io] ‹length τ' > m - n + 1› ‹i ∈ {1..m - n + 1}›
      by (metis One_nat_def add_diff_cancel_left' atLeastAtMost_iff diff_diff_cancel diff_is_0_eq' length_drop less_Suc_eq nat_le_linear not_add_less2)
  next
    case c (* π@(τ i) and π@(τ j) cannot coincide due to minimality of π@τ' *)
    then have "∃ i j  . i ≠ j ∧ i ∈ {1..m - n + 1} ∧ j ∈ {1..m - n + 1} ∧ (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by force
    then have "∃ i j  . i < j ∧ i ∈ {1..m - n + 1} ∧ j ∈ {1..m - n + 1} ∧ (after_initial I (π@(τ i)) = after_initial I (π@(τ j)))"
      by (metis linorder_neqE_nat)
    then obtain i j  where "i ∈ {1..m - n + 1}"
                       and "j ∈ {1..m - n + 1}"
                       and "i < j"
                       and "FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))"
      by force

    have "(π@(τ i)) ∈ (λi. π @ τ i) ` {1..m - n + 1}" and "(π@(τ j)) ∈ (λi. π @ τ i) ` {1..m - n + 1}"
      using ‹i ∈ {1..m - n + 1}› ‹j ∈ {1..m - n + 1}›
      by auto
    moreover have "(π@(τ i)) ≠ (π@(τ j))"
    proof -
      have "j ≤ length (butlast τ')"
        using ‹j ∈ {1..m - n + 1}› ‹length τ' > m - n + 1› by auto
      moreover have "⋀ xs . j ≤ length xs ⟹ i < j ⟹ take j xs ≠ take i xs"
        by (metis dual_order.strict_implies_not_eq length_take min.absorb2 min_less_iff_conj)
      ultimately show ?thesis
        using ‹i < j› unfolding τ_def
        by fastforce 
    qed
    ultimately have "FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j))"
      using ‹FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))›
            same_targets_in_M 
      by blast

    have "(π@(τ i)) ∈ L M" and "(π@(τ i)) ∈ L I" and "(π@(τ j)) ∈ L M" and "(π@(τ j)) ∈ L I" 
      using ‹⋀ i . i ≤ m-n+1 ⟹ π @ (τ i) ∈ L M ∩ L I› ‹i ∈ {1..m - n + 1}› ‹j ∈ {1..m - n + 1}› 
      by auto

    let ?io = "drop j τ'"
    have "τ' = (τ j) @ ?io"
      using ‹j ∈ {1..m - n + 1}› ‹length τ' > m-n+1› 
      unfolding τ_def
      by (metis (no_types, lifting) antisym_conv append_take_drop_id atLeastAtMost_iff less_or_eq_imp_le linorder_neqE_nat order.trans take_butlast)
    then have "(π@(τ j))@?io ∈ (L M - L I) ∪ (L I - L M)"
      using ‹π @ τ' ∈ (L M - L I) ∪ (L I - L M)›
      by (simp add: τ_def)
    then have "(π@(τ i))@?io ∈ (L M - L I) ∪ (L I - L M)"
      using observable_after_eq[OF ‹observable M› ‹FSM.after M (FSM.initial M) (π@(τ i)) = FSM.after M (FSM.initial M) (π@(τ j))› ‹(π@(τ i)) ∈ L M› ‹(π@(τ j)) ∈ L M›]
            observable_after_eq[OF ‹observable I› ‹FSM.after I (FSM.initial I) (π@(τ i)) = FSM.after I (FSM.initial I) (π@(τ j))› ‹(π@(τ i)) ∈ L I› ‹(π@(τ j)) ∈ L I›]
      by blast
    then have "π@(τ i)@?io ∈ (L M - L I) ∪ (L I - L M)"
      by auto
    moreover have "length τ' > length (τ i @ drop j τ')"
      using ‹length τ' > m - n + 1› ‹j ∈ {1..m - n + 1}› ‹i < j› unfolding τ_def by force
    ultimately show "False"
      using τ'_min[OF ‹π ∈ Π›, of "(τ i) @ ?io"] 
      by simp
  qed
qed



lemma abstract_h_condition_soundness :
  assumes "observable M"
  and     "observable I"
  and     "is_state_cover_assignment M V"
  and     "L M = L I"
shows "satisfies_abstract_h_condition M I V m"
  using assms(3,4) equivalence_preserves_divergence[OF assms(1,2,4)]
  unfolding satisfies_abstract_h_condition_def Let_def by blast
  


lemma abstract_h_condition_completeness :
  assumes "observable M"
  and     "observable I"
  and     "minimal M"
  and     "size I ≤ m"
  and     "m ≥ size_r M"
  and     "inputs I = inputs M"
  and     "outputs I = outputs M"
  and     "is_state_cover_assignment M V"
shows "satisfies_abstract_h_condition M I V m ⟷ (L M = L I)"
  using abstract_h_condition_soundness[OF assms(1,2,8)]
  using abstract_h_condition_exhaustiveness[OF assms]
  by blast


    
subsection ‹Definition of the Framework›


definition h_framework :: "('a::linorder,'b::linorder,'c::linorder) fsm ⇒ 
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment) ⇒                        
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ (('b×'c) prefix_tree × 'd)) ⇒
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('a,'b,'c) transition list ⇒ ('a,'b,'c) transition list) ⇒                              
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒ nat ⇒ ('a,'b,'c) transition ⇒  ('a,'b,'c) transition list ⇒ ( ('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd)) ⇒ 
                              (('a,'b,'c) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ ('b×'c) prefix_tree ⇒ 'd ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 'a ⇒ 'b ⇒ 'c ⇒ (('b×'c) prefix_tree) × 'd) ⇒ 
                              (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
                              ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                              ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
                              ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
                              nat ⇒
                              ('b×'c) prefix_tree" 
  where
  "h_framework M 
               get_state_cover 
               handle_state_cover
               sort_transitions
               handle_unverified_transition
               handle_unverified_io_pair
               cg_initial
               cg_insert
               cg_lookup
               cg_merge
               m
  = (let
      rstates_set = reachable_states M;
      rstates     = reachable_states_as_list M;
      rstates_io  = List.product rstates (List.product (inputs_as_list M) (outputs_as_list M));
      undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M q x y = None) rstates_io;
      V           = get_state_cover M;
      TG1         = handle_state_cover M V cg_initial cg_insert cg_lookup;
      sc_covered_transitions = (⋃ q ∈ rstates_set . covered_transitions M V (V q));
      unverified_transitions = sort_transitions M V (filter (λt . t_source t ∈ rstates_set ∧ t ∉ sc_covered_transitions) (transitions_as_list M));
      verify_transition = (λ (X,T,G) t . handle_unverified_transition M V T G cg_insert cg_lookup cg_merge m t X);
      TG2         = snd (foldl verify_transition (unverified_transitions, TG1) unverified_transitions);
      verify_undefined_io_pair = (λ T (q,(x,y)) . fst (handle_unverified_io_pair M V T (snd TG2) cg_insert cg_lookup q x y))
    in
      foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs)"


subsection ‹Required Conditions on Procedural Parameters›

definition separates_state_cover :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒ ('a,'b,'c) state_cover_assignment ⇒ (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ (('b×'c) prefix_tree × 'd)) ⇒
                                  ('a,'b,'c) fsm ⇒
                                  ('e,'b,'c) fsm ⇒
                                  (('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                  bool"
  where 
  "separates_state_cover f M1 M2 cg_initial cg_insert cg_lookup = 
    (∀ V .
        (V ` reachable_states M1 ⊆ set (fst (f M1 V cg_initial cg_insert cg_lookup)))
        ∧ finite_tree (fst (f M1 V cg_initial cg_insert cg_lookup))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            convergence_graph_initial_invar M1 M2 cg_lookup cg_initial ⟶
            L M1 ∩ set (fst (f M1 V cg_initial cg_insert cg_lookup)) = L M2 ∩ set (fst (f M1 V cg_initial cg_insert cg_lookup)) ⟶
            (preserves_divergence M1 M2 (V ` reachable_states M1)
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V cg_initial cg_insert cg_lookup)))))"


definition handles_transition :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                    ('a,'b,'c) state_cover_assignment ⇒
                                    ('b×'c) prefix_tree ⇒ 
                                    'd ⇒
                                    ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                    ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
                                    ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒ 
                                    nat ⇒
                                    ('a,'b,'c) transition ⇒ 
                                    ('a,'b,'c) transition list ⇒   
                                    (('a,'b,'c) transition list × ('b×'c) prefix_tree × 'd)) ⇒   
                                  ('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                  ('e,'b,'c) fsm ⇒
                                  ('a,'b,'c) state_cover_assignment ⇒    
                                  ('b×'c) prefix_tree ⇒
                                  ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                  ('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
                                  bool"
  where 
  "handles_transition f M1 M2 V T0 cg_insert cg_lookup cg_merge = 
    (∀ T G m t X .
        (set T ⊆ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
        ∧ (finite_tree T ⟶ finite_tree (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            size_r M1 ≤ m ⟶
            size M2 ≤ m ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            preserves_divergence M1 M2 (V ` reachable_states M1) ⟶
            V ` reachable_states M1 ⊆ set T ⟶
            t ∈ transitions M1 ⟶
            t_source t ∈ reachable_states M1 ⟶
            ((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t)) ⟶  
            convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            convergence_graph_merge_invar M1 M2 cg_lookup cg_merge ⟶
            L M1 ∩ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) = L M2 ∩ set (fst (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X))) ⟶
            (set T0 ⊆ set T) ⟶
            (∀ γ . (length γ ≤ (m-size_r M1) ∧ list.set γ ⊆ inputs M1 × outputs M1 ∧ butlast γ ∈ LS M1 (t_target t))
                    ⟶ ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                          = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                         ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})))   
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (f M1 V T G cg_insert cg_lookup cg_merge m t X)))))"


definition handles_io_pair :: "(('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                            ('a,'b,'c) state_cover_assignment ⇒
                                            ('b×'c) prefix_tree ⇒ 
                                            'd ⇒
                                            ('d ⇒ ('b×'c) list ⇒ 'd) ⇒ 
                                            ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒ 
                                            'a ⇒ 'b ⇒ 'c ⇒  
                                            (('b×'c) prefix_tree × 'd)) ⇒
                                          ('a::linorder,'b::linorder,'c::linorder) fsm ⇒
                                          ('e,'b,'c) fsm ⇒
                                          ('d ⇒ ('b×'c) list ⇒ 'd) ⇒
                                          ('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒                                     
                                          bool"
  where 
  "handles_io_pair f M1 M2 cg_insert cg_lookup = 
    (∀ V T G q x y .
        (set T ⊆ set (fst (f M1 V T G cg_insert cg_lookup q x y)))
        ∧ (finite_tree T ⟶ finite_tree (fst (f M1 V T G cg_insert cg_lookup q x y)))
        ∧ (observable M1 ⟶
            observable M2 ⟶
            minimal M1 ⟶
            minimal M2 ⟶
            inputs M2 = inputs M1 ⟶
            outputs M2 = outputs M1 ⟶
            is_state_cover_assignment M1 V ⟶
            L M1 ∩ (V ` reachable_states M1) = L M2 ∩ V ` reachable_states M1 ⟶
            q ∈ reachable_states M1 ⟶
            x ∈ inputs M1 ⟶ 
            y ∈ outputs M1 ⟶ 
            convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶   
            convergence_graph_insert_invar M1 M2 cg_lookup cg_insert ⟶
            L M1 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (f M1 V T G cg_insert cg_lookup q x y)) ⟶
            ( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )
            ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (f M1 V T G cg_insert cg_lookup q x y))))"



subsection ‹Completeness and Finiteness of the Scheme›


lemma unverified_transitions_handle_all_transitions :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: "⋀ t γ . t ∈ transitions M1 ⟹
                                            t_source t ∈ reachable_states M1 ⟹
                                            length γ ≤ k ⟹ 
                                            list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
                                            butlast γ ∈ LS M1 (t_target t) ⟹
                                            (V (t_target t) ≠ (V (t_source t))@[(t_input t, t_output t)]) ⟹
                                            ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                                               = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                                             ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: "⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹ L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}"
  and     "t ∈ transitions M1"
  and     "t_source t ∈ reachable_states M1"
  and     "length γ ≤ k"
  and     "list.set γ ⊆ inputs M1 × outputs M1"
  and     "butlast γ ∈ LS M1 (t_target t)"
shows "(L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
         = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
        ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"
proof (cases "V (t_target t) ≠ V (t_source t) @ [(t_input t, t_output t)]")
  case True
  then show ?thesis 
    using handles_unverified_transitions[OF assms(7-11)] 
    by blast
next
  case False
  then have "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
    by simp
  have "⋀ γ . length γ ≤ k ⟹
             list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
             butlast γ ∈ LS M1 (t_target t) ⟹
             L M1 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) =
               L M2 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ∧
             preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
  proof -
    fix γ assume "length γ ≤ k" and "list.set γ ⊆ inputs M1 × outputs M1" and "butlast γ ∈ LS M1 (t_target t)"
    then show "L M1 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) =
                 L M2 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ∧
               preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)})"
      using ‹t ∈ transitions M1› ‹t_source t ∈ reachable_states M1› ‹V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)›
    proof (induction γ arbitrary: t)
      case Nil
      have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes [])} = {V (t_target t)}"
        unfolding Nil by auto
      then have *: "(V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes [])}) = V ` reachable_states M1"
        using reachable_states_next[OF Nil.prems(5,4)] by blast
      show ?case 
        unfolding *
        using assms(3,4) 
        by blast
    next
      case (Cons xy γ)
      then obtain x y where "xy = (x,y)" by auto
      then have "x ∈ inputs M1" and "y ∈ outputs M1"
        using Cons.prems(2) by auto

      have "t_target t ∈ reachable_states M1"
        using reachable_states_next[OF Cons.prems(5,4)] by blast
      then have "after_initial M1 (V (t_target t)) = t_target t"
        using ‹is_state_cover_assignment M1 V› 
        by (metis assms(1) is_state_cover_assignment_observable_after)

      show ?case proof (cases "[xy] ∈ LS M1 (t_target t)")
        case False
        then have "h_obs M1 (t_target t) x y = None"
          using Cons.prems(4,5) ‹x ∈ inputs M1› ‹y ∈ outputs M1› unfolding ‹xy = (x,y)›
          by (meson assms(1) h_obs_language_single_transition_iff) 
        then have "L M1 ∩ {V (t_target t) @ [(x, y)]} = L M2 ∩ {V (t_target t) @ [(x, y)]}"
          using handles_undefined_io_pairs[OF ‹t_target t ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›] by blast      
        
        have "V (t_target t) @ [(x, y)] ∉ L M1"
          using False ‹after_initial M1 (V (t_target t)) = t_target t› 
          unfolding ‹xy = (x,y)›
          by (metis assms(1) language_prefix observable_after_language_none) 
        then have "preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})"
          using assms(4)
          unfolding preserves_divergence.simps
          by blast 

        have "γ = []"
          using False Cons.prems(3) 
          by (metis (no_types, lifting) LS_single_transition ‹xy = (x, y)› butlast.simps(2) language_next_transition_ob)
        then have "list.set (prefixes (xy#γ)) = {[], [(x,y)]}"
          unfolding ‹xy = (x,y)›
          by force 
        then have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {V (t_target t), V (t_target t) @ [(x, y)]}"
          unfolding Cons by auto
        then have *:"(V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))}) = (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})"
          using reachable_states_next[OF Cons.prems(5,4)] by blast

        

        show ?thesis 
          unfolding *
          using assms(3)
                ‹L M1 ∩ {V (t_target t) @ [(x, y)]} = L M2 ∩ {V (t_target t) @ [(x, y)]}›
                ‹preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V (t_target t) @ [(x, y)]})›    
          by blast
      next
        case True

        then obtain t' where "t_source t' = t_target t" and "t_input t' = x" and "t_output t' = y" and "t' ∈ transitions M1"
          unfolding ‹xy = (x,y)›
          by auto 
        then have "t_target t' ∈ reachable_states M1" and "t_source t' ∈ reachable_states M1"
          using reachable_states_next[OF ‹t_target t ∈ reachable_states M1›, of t'] ‹t_target t ∈ reachable_states M1› by auto

        have *: "length γ ≤ k"
          using Cons.prems(1) by auto
        have **: "list.set γ ⊆ inputs M1 × outputs M1"
          using Cons.prems(2) by auto
        have ***: "butlast γ ∈ LS M1 (t_target t')"
          using Cons.prems(3)
          by (metis True ‹t' ∈ FSM.transitions M1› ‹t_input t' = x› ‹t_output t' = y› ‹t_source t' = t_target t› ‹xy = (x, y)› assms(1) butlast.simps(1) butlast.simps(2) observable_language_transition_target)                
        
        have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∪ {V (t_source t) @ [(t_input t, t_output t)]}"
          by (induction γ; auto) 
        moreover have "{((V (t_source t) @ [(t_input t, t_output t)]) @ [xy]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}"
          unfolding ‹t_source t' = t_target t› ‹t_input t' = x› ‹t_output t' = y› ‹xy = (x,y)›[symmetric] Cons.prems(6)[symmetric] by simp
        ultimately have "{(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))} = {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)} ∪ {V (t_target t)}"
          unfolding Cons by force
        then have ****: "V ` reachable_states M1 ∪ {(V (t_source t') @ [(t_input t', t_output t')]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}
                          = V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes (xy # γ))}"
          using ‹t_source t' = t_target t› ‹t_source t' ∈ reachable_states M1› by force

      

        show ?thesis proof (cases "V (t_source t') @ [(t_input t', t_output t')] = V (t_target t')")
          case True
          show ?thesis
            using Cons.IH[OF * ** *** ‹t' ∈ transitions M1› ‹t_source t' ∈ reachable_states M1› True]
            unfolding **** .
        next
          case False
          then show ?thesis
            using handles_unverified_transitions[OF ‹t' ∈ transitions M1› ‹t_source t' ∈ reachable_states M1› * ** ***]
            unfolding ****
            by presburger
        qed
      qed
    qed
  qed
  then show ?thesis
    using assms(9-11)
    by blast
qed

lemma abstract_h_condition_by_transition_and_io_pair_coverage :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: "⋀ t γ . t ∈ transitions M1 ⟹
                                            t_source t ∈ reachable_states M1 ⟹
                                            length γ ≤ k ⟹ 
                                            list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
                                            butlast γ ∈ LS M1 (t_target t) ⟹
                                            ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                                               = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                                             ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: "⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹ L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}"  
  and     "q ∈ reachable_states M1"
  and     "length γ ≤ Suc k"
  and     "list.set γ ⊆ inputs M1 × outputs M1"
  and     "butlast γ ∈ LS M1 q"
shows "(L M1 ∩ (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
         = L M2 ∩ (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
        ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"   
proof (cases γ)
  case Nil 
  show ?thesis 
    using assms(3,4,7) unfolding Nil by auto
next
  case (Cons xy γ')
  then obtain x y where "xy = (x,y)" using prod.exhaust by metis
  then have "x ∈ inputs M1" and "y ∈ outputs M1"
    using assms(9) Cons by auto

  show ?thesis proof (cases "[xy] ∈ LS M1 q")
    case False
    then have "h_obs M1 q x y = None"
      using assms(7) ‹x ∈ inputs M1› ‹y ∈ outputs M1› unfolding ‹xy = (x,y)›
      by (meson assms(1) h_obs_language_single_transition_iff) 
    then have "L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}"
      using handles_undefined_io_pairs[OF assms(7) ‹x ∈ inputs M1› ‹y ∈ outputs M1›] by blast

    have "V q @ [(x, y)] ∉ L M1"
      using observable_after_language_none[OF assms(1), of "V q" "initial M1" "[(x,y)]"]
      using state_cover_assignment_after[OF assms(1,2,7)]
      by (metis False ‹xy = (x, y)›) 
    then have "preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V q @ [(x, y)]})"
      using assms(4)
      unfolding preserves_divergence.simps
      by blast 


    have "γ' = []"
      using False assms(10) language_prefix[of "[xy]" γ' M1 q]
      unfolding Cons 
      by (metis (no_types, lifting) LS_single_transition ‹xy = (x, y)› butlast.simps(2) language_next_transition_ob)
    then have "γ = [(x,y)]"
      unfolding Cons ‹xy = (x,y)› by auto
    then have *: "(V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}) = V ` reachable_states M1 ∪ {V q @ [(x,y)]}"
      using assms(7) by auto

    show ?thesis
      unfolding *
      using assms(3) ‹L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}› ‹preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V q @ [(x, y)]})›
      by blast
  next
    case True
    moreover have "butlast ((x,y)#γ') ∈ LS M1 q"
      using assms(10) unfolding Cons ‹xy = (x,y)› .
    ultimately have "(x,y) # (butlast γ') ∈ LS M1 q" 
      unfolding  ‹xy = (x,y)› by (cases γ'; auto)
    then obtain q' where "h_obs M1 q x y = Some q'" and "butlast γ' ∈ LS M1 q'"
      using h_obs_language_iff[OF assms(1), of x y "butlast γ'" q]
      by blast
    then have "(q,x,y,q') ∈ transitions M1"
      unfolding h_obs_Some[OF assms(1)] by blast

    

    have "length γ' ≤ k"
      using assms(8) unfolding Cons by auto
    have "list.set γ' ⊆ inputs M1 × outputs M1"    
      using assms(9) unfolding Cons by auto
    
    have *:"(L M1 ∩ (V ` reachable_states M1 ∪ {(V q @ [(x,y)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ')})
         = L M2 ∩ (V ` reachable_states M1 ∪ {(V q @ [(x,y)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ')}))
        ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V q @ [(x,y)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ')})"
      using handles_unverified_transitions[OF ‹(q,x,y,q') ∈ transitions M1› _ ‹length γ' ≤ k› ‹list.set γ' ⊆ inputs M1 × outputs M1›]
            assms(7) ‹butlast γ' ∈ LS M1 q'›
      unfolding fst_conv snd_conv 
      by blast

    have "{V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} = {(V q @ [(x, y)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ')} ∪ {V q}"
      unfolding Cons ‹xy = (x,y)› by auto 
    then have **: "V ` reachable_states M1 ∪ {V q @ ω' |ω'. ω' ∈ list.set (prefixes γ)} 
                    = V ` reachable_states M1 ∪ {(V q @ [(x, y)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ')}"
      using assms(7) by blast

    show ?thesis
      using * unfolding ** .
  qed
qed


lemma abstract_h_condition_by_unverified_transition_and_io_pair_coverage :
  assumes "observable M1"
  and     "is_state_cover_assignment M1 V"
  and     "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
  and     "preserves_divergence M1 M2 (V ` reachable_states M1)"
  and     handles_unverified_transitions: "⋀ t γ . t ∈ transitions M1 ⟹
                                            t_source t ∈ reachable_states M1 ⟹
                                            length γ ≤ k ⟹ 
                                            list.set γ ⊆ inputs M1 × outputs M1 ⟹ 
                                            butlast γ ∈ LS M1 (t_target t) ⟹
                                            (V (t_target t) ≠ (V (t_source t))@[(t_input t, t_output t)]) ⟹ 
                                            ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                                               = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                                             ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))"
  and     handles_undefined_io_pairs: "⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹ L M1 ∩ {V q @ [(x,y)]} = L M2 ∩ {V q @ [(x,y)]}"  
  and     "q ∈ reachable_states M1"
  and     "length γ ≤ Suc k"
  and     "list.set γ ⊆ inputs M1 × outputs M1"
  and     "butlast γ ∈ LS M1 q"
shows "(L M1 ∩ (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
         = L M2 ∩ (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
        ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {V q @ ω' | ω'. ω' ∈ list.set (prefixes γ)})"   
  using unverified_transitions_handle_all_transitions[OF assms(1-6), of k]
  using abstract_h_condition_by_transition_and_io_pair_coverage[OF assms(1-4) _ assms(6-10)]
  by presburger


lemma h_framework_completeness_and_finiteness :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  fixes cg_insert :: "('d ⇒ ('b×'c) list ⇒ 'd)"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "size_r M1 ≤ m"
  and     "size M2 ≤ m"
  and     "inputs M2 = inputs M1"
  and     "outputs M2 = outputs M1"
  and     "is_state_cover_assignment M1 (get_state_cover M1)"
  and     "⋀ xs . List.set xs = List.set (sort_transitions M1 (get_state_cover M1) xs)"
  and     "convergence_graph_initial_invar M1 M2 cg_lookup cg_initial"
  and     "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
  and     "convergence_graph_merge_invar M1 M2 cg_lookup cg_merge"
  and     "separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup"
  and     "handles_transition handle_unverified_transition M1 M2 (get_state_cover M1) (fst (handle_state_cover M1 (get_state_cover M1) cg_initial cg_insert cg_lookup)) cg_insert cg_lookup cg_merge"
  and     "handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m))
                          = (L M2 ∩ set (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m)))"
  (is "(L M1 = L M2) ⟷ ((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))")
and "finite_tree (h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m)"
proof 
  show "(L M1 = L M2) ⟹ ((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
    by blast


  define rstates where rstates: "rstates = reachable_states_as_list M1"
  define rstates_io where rstates_io: "rstates_io = List.product rstates (List.product (inputs_as_list M1) (outputs_as_list M1))"
  define undefined_io_pairs where undefined_io_pairs: "undefined_io_pairs = List.filter (λ (q,(x,y)) . h_obs M1 q x y = None) rstates_io"
  define V where V: "V             = get_state_cover M1"
  define n where n: "n             = size_r M1"
  define TG1 where TG1: "TG1 = handle_state_cover M1 V cg_initial cg_insert cg_lookup"

  define sc_covered_transitions where sc_covered_transitions: "sc_covered_transitions = (⋃ q ∈ reachable_states M1 . covered_transitions M1 V (V q))"
  define unverified_transitions where unverified_transitions: "unverified_transitions = sort_transitions M1 V (filter (λt . t_source t ∈ reachable_states M1 ∧ t ∉ sc_covered_transitions) (transitions_as_list M1))"
  define verify_transition where verify_transition: "verify_transition = (λ (X,T,G) t . handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X)"
  define TG2 where TG2: "TG2 = snd (foldl verify_transition (unverified_transitions, TG1) unverified_transitions)"
  define verify_undefined_io_pair where verify_undefined_io_pair: "verify_undefined_io_pair = (λ T (q,(x,y)) . fst (handle_unverified_io_pair M1 V T (snd TG2) cg_insert cg_lookup q x y))" 
  define T3 where T3: "T3 = foldl verify_undefined_io_pair (fst TG2) undefined_io_pairs"

  have "?TS = T3"
    unfolding rstates rstates_io undefined_io_pairs V TG1 sc_covered_transitions unverified_transitions verify_transition TG2 verify_undefined_io_pair T3
    unfolding h_framework_def Let_def
    by force
  then have "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3"
    by simp

  have "is_state_cover_assignment M1 V"
    unfolding V using assms(9) .

  (* basic properties of T1 and G1 *)

  define T1 where T1: "T1 = fst TG1"
  moreover define G1 where G1: "G1 = snd TG1"
  ultimately have "TG1 = (T1,G1)" 
    by auto 

  have T1_state_cover: "V ` reachable_states M1 ⊆ set T1"
  and  T1_finite: "finite_tree T1"
    using ‹separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup›
    unfolding T1 TG1 separates_state_cover_def
    by blast+
  

  have T1_V_div: "(L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ preserves_divergence M1 M2 (V ` reachable_states M1)"
   and G1_invar: "(L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G1" 
    using ‹separates_state_cover handle_state_cover M1 M2 cg_initial cg_insert cg_lookup›
    unfolding T1 G1 TG1 separates_state_cover_def
    using assms(1-4,7,8) ‹is_state_cover_assignment M1 V› assms(12,11) 
    by blast+

  

  (* properties of transition filtering and sorting *)

  have sc_covered_transitions_alt_def: "sc_covered_transitions = {t . t ∈ transitions M1 ∧ t_source t ∈ reachable_states M1 ∧ (V (t_target t) = (V (t_source t))@[(t_input t, t_output t)])}"
    (is "?A = ?B")
  proof 
    show "?A ⊆ ?B"
    proof 
      fix t assume "t ∈ ?A"
      then obtain q where "t ∈ covered_transitions M1 V (V q)" and "q ∈ reachable_states M1"
        unfolding sc_covered_transitions 
        by blast
      then have "V q ∈ L M1" and "after_initial M1 (V q) = q"
        using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
        by blast+

      then obtain p where "path M1 (initial M1) p" and "p_io p = V q"
        by auto
      then have *: "the_elem (paths_for_io M1 (initial M1) (V q)) = p"
        using observable_paths_for_io[OF assms(1) ‹V q ∈ L M1›]
        unfolding paths_for_io_def
        by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)
      
      have "t ∈ list.set p" and "V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)"
        using ‹t ∈ covered_transitions M1 V (V q)› 
        unfolding covered_transitions_def Let_def * 
        by auto

      have "t ∈ transitions M1"
        using ‹t ∈ list.set p› ‹path M1 (initial M1) p›
        by (meson path_transitions subsetD) 
      moreover have "t_source t ∈ reachable_states M1"
        using reachable_states_path[OF reachable_states_initial ‹path M1 (initial M1) p› ‹t ∈ list.set p›] .
      ultimately show "t ∈ ?B"
        using ‹V (t_source t) @ [(t_input t, t_output t)] = V (t_target t)›
        by auto
    qed

    show "?B ⊆ ?A"
    proof 
      fix t assume "t ∈ ?B"
      then have "t ∈ transitions M1" 
                "t_source t ∈ reachable_states M1" 
                "(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
        by auto
      then have "t_target t ∈ reachable_states M1"
        using reachable_states_next[of "t_source t" M1 t] 
        by blast
      then have "V (t_target t) ∈ L M1" and "after_initial M1 (V (t_target t)) = (t_target t)"
        using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
        by blast+
      then obtain p where "path M1 (initial M1) p" and "p_io p = V (t_target t)"
        by auto
      then have *: "the_elem (paths_for_io M1 (initial M1) (V (t_target t))) = p"
        using observable_paths_for_io[OF assms(1) ‹V (t_target t) ∈ L M1›]
        unfolding paths_for_io_def
        by (metis (mono_tags, lifting) assms(1) mem_Collect_eq observable_path_unique singletonI the_elem_eq)

      
      have "V (t_source t) ∈ L M1" and "after_initial M1 (V (t_source t)) = (t_source t)"
        using ‹t_source t ∈ reachable_states M1›
        using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
        by blast+
      then obtain p' where "path M1 (initial M1) p'" and "p_io p' = V (t_source t)"
        by auto
      
      have "path M1 (initial M1) (p'@[t])"
        using after_path[OF assms(1) ‹path M1 (initial M1) p'›] ‹path M1 (initial M1) p'› ‹t∈transitions M1›
        unfolding ‹p_io p' = V (t_source t)›
        unfolding ‹after_initial M1 (V (t_source t)) = (t_source t)›
        by (metis path_append single_transition_path)
      moreover have "p_io (p'@[t]) = p_io p"
        using ‹p_io p' = V (t_source t)› 
        unfolding ‹p_io p = V (t_target t)›  ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›[symmetric]
        by auto
      ultimately have "p'@[t] = p"
        using observable_path_unique[OF assms(1) _ ‹path M1 (initial M1) p›]
        by force
      then have "t ∈ list.set p"
        by auto
      then have "t ∈ covered_transitions M1 V (V (t_target t))"
        using ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›
        unfolding covered_transitions_def Let_def *
        by auto
      then show "t ∈ ?A"
        using ‹t_target t ∈ reachable_states M1›
        unfolding sc_covered_transitions 
        by blast
    qed
  qed

  have T1_covered_transitions_conv: "⋀ t . (L M1 ∩ set T1 = (L M2 ∩ set T1)) ⟹ t ∈ sc_covered_transitions ⟹ converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
  proof -
    fix t assume "(L M1 ∩ set T1 = (L M2 ∩ set T1))"
                 "t ∈ sc_covered_transitions"

    then have "t ∈ transitions M1" 
              "t_source t ∈ reachable_states M1" 
              "(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)"
      unfolding sc_covered_transitions_alt_def
      by auto
    then have "t_target t ∈ reachable_states M1"
      using reachable_states_next[of "t_source t" M1 t] 
      by blast
    then have "V (t_target t) ∈ L M1"
      using state_cover_assignment_after[OF assms(1) ‹is_state_cover_assignment M1 V›]
      by blast   
    moreover have "V (t_target t) ∈ set T1"
      using T1_state_cover ‹t_target t ∈ reachable_states M1›
      by blast
    ultimately have "V (t_target t) ∈ L M2"
      using ‹(L M1 ∩ set T1 = (L M2 ∩ set T1))›
      by blast
    then show "converge M2 (V (t_target t)) ((V (t_source t))@[(t_input t, t_output t)])"
      unfolding ‹(V (t_source t))@[(t_input t, t_output t)] = V (t_target t)›
      by auto
  qed


  have unverified_transitions_alt_def : "list.set unverified_transitions = {t . t ∈ transitions M1 ∧ t_source t ∈ reachable_states M1 ∧ (V (t_target t) ≠ (V (t_source t))@[(t_input t, t_output t)])}"
    unfolding unverified_transitions sc_covered_transitions_alt_def V
    unfolding assms(10)[symmetric] 
    using transitions_as_list_set[of M1]
    by auto


  (* remaining properties before the computation of TG2 *)

  have cg_insert_invar : "⋀ G γ . γ ∈ L M1 ⟹ γ ∈ L M2 ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G γ)"
    using assms(12)
    unfolding convergence_graph_insert_invar_def
    by blast

  have cg_merge_invar : "⋀ G γ γ'. convergence_graph_lookup_invar M1 M2 cg_lookup G ⟹ converge M1 γ γ' ⟹ converge M2 γ γ' ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_merge G γ γ')"
    using assms(13)
    unfolding convergence_graph_merge_invar_def
    by blast


  (* properties of the computation of TG2 *)

  define T2 where T2: "T2 = fst TG2"
  define G2 where G2: "G2 = snd TG2"

  (* idea: in each application of verify_transition, a further transition of unverified_transitions
           (q,x,y,q') is covered - that is
            - traces α.(x/y), β are added to the test suite such that
              - α converges with V s in both M1 and M2
              - β converges with V s' in both M1 and M2
              - α.(x/y) converges with β in both M1 and M2 
            - the test suite is added as required to establish this convergence
            - the convergence graph is updated, respecting the lookup-invariants due to convergence (in merge)
  *)

  have "handles_transition handle_unverified_transition M1 M2 V T1 cg_insert cg_lookup cg_merge"
    using assms(15)
    unfolding T1 TG1 V .
  then have verify_transition_retains_testsuite: "⋀ t T G X . set T ⊆ set (fst (snd (verify_transition (X,T,G) t)))"
       and  verify_transition_retains_finiteness: "⋀ t T G X . finite_tree T ⟹ finite_tree (fst (snd (verify_transition (X,T,G) t)))"
    unfolding verify_transition case_prod_conv handles_transition_def 
    by presburger+


  define handles_unverified_transition 
    where handles_unverified_transition: "handles_unverified_transition  = (λt .
                                                (∀ γ . (length γ ≤ (m-size_r M1) ∧ list.set γ ⊆ inputs M1 × outputs M1 ∧ butlast γ ∈ LS M1 (t_target t))
                                                          ⟶ ((L M1 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)})
                                                                = L M2 ∩ (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))
                                                               ∧ preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {((V (t_source t))@[(t_input t,t_output t)]) @ ω' | ω'. ω' ∈ list.set (prefixes γ)}))))"


  have verify_transition_cover_prop: "⋀ t T G X . (L M1 ∩ (set (fst (snd (verify_transition (X,T,G) t)))) = L M2 ∩ (set (fst (snd (verify_transition (X,T,G) t)))))
                                          ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G
                                          ⟹ t ∈ transitions M1
                                          ⟹ t_source t ∈ reachable_states M1
                                          ⟹ set T1 ⊆ set T
                                          ⟹ ((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))
                                          ⟹ handles_unverified_transition t ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition (X,T,G) t)))"
  proof -
    fix t T G X
    assume a1: "(L M1 ∩ (set (fst (snd (verify_transition (X,T,G) t)))) = L M2 ∩ (set (fst (snd (verify_transition (X,T,G) t)))))"
    assume a2: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
    assume a3: "t ∈ transitions M1"
    assume a4: "t_source t ∈ reachable_states M1"
    assume a5: "set T1 ⊆ set T"
    assume a6: "((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))"

    

    obtain X' T' G' where TG': "(X',T',G') = handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X"
      using prod.exhaust by metis
    have T':  "T'  = fst (snd (handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X))"
     and G':  "G'  = snd (snd (handle_unverified_transition M1 V T G cg_insert cg_lookup cg_merge m t X))"
      unfolding TG'[symmetric] by auto

    have "verify_transition (X,T,G) t = (X',T',G')"
      using TG'[symmetric]
      unfolding verify_transition G' Let_def case_prod_conv 
      by force
    then have "set T ⊆ set T'"
      using verify_transition_retains_testsuite[of T X G t] unfolding T' 
      by auto
    then have "set T1 ⊆ set T'"
      using a5 by blast
    then have "(L M1 ∩ (set T1) = L M2 ∩ (set T1))"
      using a1 unfolding ‹verify_transition (X,T,G) t = (X',T',G')› fst_conv snd_conv
      by blast
    then have *: "preserves_divergence M1 M2 (V ` reachable_states M1)"
      using T1_V_div
      by auto

    have "L M1 ∩ set T' = L M2 ∩ set T'"
      using a1 ‹set T ⊆ set T'› unfolding T' ‹verify_transition (X,T,G) t = (X',T',G')› fst_conv snd_conv
      by blast

    have **: "V ` reachable_states M1 ⊆ set T"
      using a5 T1_state_cover by blast

    show "handles_unverified_transition t ∧ convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition (X,T,G) t)))"
      unfolding ‹verify_transition (X,T,G) t = (X',T',G')› snd_conv 
      unfolding G'
      using ‹handles_transition handle_unverified_transition M1 M2 V T1 cg_insert cg_lookup cg_merge›
      unfolding handles_transition_def 

      using assms(1-8) ‹is_state_cover_assignment M1 V› * ** a3 a4 a2 a6 ‹convergence_graph_insert_invar M1 M2 cg_lookup cg_insert› ‹convergence_graph_merge_invar M1 M2 cg_lookup cg_merge› ‹L M1 ∩ set T' = L M2 ∩ set T'› a5
      unfolding T'
      unfolding handles_unverified_transition 
      by blast
  qed

  have verify_transition_foldl_invar_1: "⋀ X ts . list.set ts ⊆ list.set unverified_transitions ⟹ 
                set T1 ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ∧ finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
  proof -
    fix X ts assume "list.set ts ⊆ list.set unverified_transitions" 
    then show "set T1 ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ∧ finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
    proof (induction ts rule: rev_induct)
      case Nil
      then show ?case 
        using T1_finite by auto
    next
      case (snoc t ts)
      then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1"
        unfolding unverified_transitions_alt_def 
        by force+

      have p1: "list.set ts ⊆ list.set unverified_transitions"
        using snoc.prems(1) by auto

      have "set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_testsuite 
        unfolding foldl_append
        unfolding foldl.simps 
        by (metis prod.collapse) 

      have **: "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"  
       and ***: "finite_tree (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using snoc.IH[OF p1] 
        by auto          
    
      have "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using ** verify_transition_retains_testsuite ‹set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))› 
        by auto 
      moreover have "finite_tree (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_finiteness[OF ***, of "fst (foldl verify_transition (X, T1, G1) ts)" "snd (snd (foldl verify_transition (X, T1, G1) ts))"] 
        by auto
      ultimately show ?case 
        by simp
    qed
  qed 
  then have T2_invar_1: "set T1 ⊆ set T2"
        and T2_finite : "finite_tree T2"
    unfolding TG2 G2 T2 ‹TG1 = (T1,G1)›
    by auto

  have verify_transition_foldl_invar_2: "⋀ X ts . list.set ts ⊆ list.set unverified_transitions ⟹ 
                L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⟹ 
                convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"
  proof -
    fix X ts assume "list.set ts ⊆ list.set unverified_transitions" 
              and "L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
    then show "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"
    proof (induction ts rule: rev_induct)
      case Nil
      then show ?case 
        using G1_invar by auto
    next
      case (snoc t ts)
      then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1"
        unfolding unverified_transitions_alt_def 
        by force+

      have p1: "list.set ts ⊆ list.set unverified_transitions"
        using snoc.prems(1) by auto

      have "set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
        by (metis fst_conv prod_eq_iff snd_conv)
      then have p2: "L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using snoc.prems(2)
        by blast 

      have *:"convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts)))"                                                           
        using snoc.IH[OF p1 p2] 
        by auto          

      have **: "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
        using verify_transition_foldl_invar_1[OF p1] by blast

      have ***: "((V (t_source t)) @ [(t_input t,t_output t)]) ≠ (V (t_target t))"
        using snoc.prems(1) unfolding unverified_transitions_alt_def by force
    
      have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (verify_transition ((fst (foldl verify_transition (X, T1, G1) ts)), fst (snd (foldl verify_transition (X, T1, G1) ts)), snd (snd (foldl verify_transition (X, T1, G1) ts))) t)))"          
        using verify_transition_cover_prop[OF _ * ‹t ∈ transitions M1› ‹t_source t ∈ reachable_states M1› ** ***, of "(fst (foldl verify_transition (X, T1, G1) ts))"] snoc.prems(2)
        unfolding prod.collapse
        by auto
      then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        by auto
      moreover have "Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t]))))"
        using ** verify_transition_retains_testsuite
        using snoc.prems(1) verify_transition_foldl_invar_1 by blast 
      ultimately show ?case 
        by simp
    qed
  qed 
  then have T2_invar_2: "L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G2"
    unfolding TG2 G2 T2 ‹TG1 = (T1,G1)› by auto

  have T2_cover: "⋀ t . L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ t ∈ list.set unverified_transitions ⟹ handles_unverified_transition t"
  proof -
    have "⋀ X t ts . t ∈ list.set ts ⟹ list.set ts ⊆ list.set unverified_transitions ⟹ L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⟹ handles_unverified_transition t"
    proof -
      fix X t ts
      assume "t ∈ list.set ts" and "list.set ts ⊆ list.set unverified_transitions" and "L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"

      then show "handles_unverified_transition t"
      proof (induction ts rule: rev_induct)
        case Nil
        then show ?case by auto
      next
        case (snoc t' ts)

        then have "t ∈ transitions M1" and "t_source t ∈ reachable_states M1"
          unfolding unverified_transitions_alt_def 
          by blast+

        have "t' ∈ transitions M1" and "t_source t' ∈ reachable_states M1"
          using snoc.prems(2)
          unfolding unverified_transitions_alt_def 
          by auto

        have "set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t']))))"
          using verify_transition_retains_testsuite unfolding foldl_append foldl.simps
          by (metis fst_conv prod_eq_iff snd_conv)
        then have "L M1 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using snoc.prems(3) 
          by blast

        have *: "L M1 ∩ Prefix_Tree.set (fst (snd (verify_transition (foldl verify_transition (X, T1, G1) ts) t'))) = L M2 ∩ Prefix_Tree.set (fst (snd (verify_transition (foldl verify_transition (X, T1, G1) ts) t')))"               
          using snoc.prems(3) by auto

        have **: "V (t_source t') @ [(t_input t', t_output t')] ≠ V (t_target t')"
          using snoc.prems(2) unfolding unverified_transitions_alt_def by force

        have "L M1 ∩ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using ‹set (fst (snd (foldl verify_transition (X, T1, G1) ts))) ⊆ set (fst (snd (foldl verify_transition (X, T1, G1) (ts@[t']))))› snoc.prems(3)
          by auto
        then have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl verify_transition (X, T1, G1) ts))) ∧ Prefix_Tree.set T1 ⊆ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))"
          using snoc.prems(2) verify_transition_foldl_invar_1[of ts] verify_transition_foldl_invar_2[of ts]
          by auto
        then have covers_t': "handles_unverified_transition t'"
          by (metis "*" "**" ‹t' ∈ FSM.transitions M1› ‹t_source t' ∈ reachable_states M1› prod.collapse verify_transition_cover_prop) 

        show ?case proof (cases "t = t'")
          case True
          then show ?thesis 
            using covers_t' by auto
        next
          case False
          then have "t ∈ list.set ts"
            using snoc.prems(1) by auto

          show "handles_unverified_transition t"
            using snoc.IH[OF ‹t ∈ list.set ts›] snoc.prems(2) ‹L M1 ∩ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts))) = L M2 ∩ Prefix_Tree.set (fst (snd (foldl verify_transition (X, T1, G1) ts)))›
            by auto
        qed
      qed
    qed

    then show "⋀ t . L M1 ∩ set T2 = L M2 ∩ set T2 ⟹ t ∈ list.set unverified_transitions ⟹ handles_unverified_transition t"
      unfolding TG2 T2 G2 ‹TG1 = (T1,G1)›
      by simp
  qed


  (* properties of T3 derived from those of T1 and T2 and the assumption that T3 is passed by M2 *)

  have verify_undefined_io_pair_retains_testsuite: "⋀ qxy T . set T ⊆ set (verify_undefined_io_pair T qxy)"
  proof -
    fix qxy :: "('a × 'b × 'c)"
    fix T
    obtain q x y where "qxy = (q,x,y)"
      using prod.exhaust by metis
    show ‹set T ⊆ set (verify_undefined_io_pair T qxy)›
      unfolding ‹qxy = (q,x,y)›
      using ‹handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup›
      unfolding handles_io_pair_def verify_undefined_io_pair case_prod_conv
      by blast
  qed
  have verify_undefined_io_pair_folding_retains_testsuite: "⋀ qxys T . set T ⊆ set (foldl verify_undefined_io_pair T qxys)"
  proof -
    fix qxys T
    show "set T ⊆ set (foldl verify_undefined_io_pair T qxys)"
      using verify_undefined_io_pair_retains_testsuite
      by (induction qxys rule: rev_induct; force) 
  qed

  have verify_undefined_io_pair_retains_finiteness: "⋀ qxy T . finite_tree T ⟹ finite_tree (verify_undefined_io_pair T qxy)"
  proof -
    fix qxy :: "('a × 'b × 'c)"
    fix T :: "('b×'c) prefix_tree"
    assume "finite_tree T"
    obtain q x y where "qxy = (q,x,y)"
      using prod.exhaust by metis
    show ‹finite_tree (verify_undefined_io_pair T qxy)›
      unfolding ‹qxy = (q,x,y)›
      using ‹handles_io_pair handle_unverified_io_pair M1 M2 cg_insert cg_lookup› ‹finite_tree T›
      unfolding handles_io_pair_def verify_undefined_io_pair case_prod_conv
      by blast
  qed
  have verify_undefined_io_pair_folding_retains_finiteness: "⋀ qxys T . finite_tree T ⟹ finite_tree (foldl verify_undefined_io_pair T qxys)"
  proof -
    fix qxys 
    fix T :: "('b×'c) prefix_tree"
    assume "finite_tree T"
    then show "finite_tree (foldl verify_undefined_io_pair T qxys)"
      using verify_undefined_io_pair_retains_finiteness
      by (induction qxys rule: rev_induct; force) 
  qed

  show "finite_tree ?TS"
    using T2 T2_finite T3 ‹h_framework M1 get_state_cover handle_state_cover sort_transitions handle_unverified_transition handle_unverified_io_pair cg_initial cg_insert cg_lookup cg_merge m = T3› verify_undefined_io_pair_folding_retains_finiteness 
    by auto


  (* having finished all but one goal, we may finally assume that M2 passes the test suite *)
  assume "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"
  
  have "set T2 ⊆ set T3"
    unfolding T3 T2
  proof (induction undefined_io_pairs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc x xs)
    then show ?case 
      using verify_undefined_io_pair_retains_testsuite[of "(foldl verify_undefined_io_pair (fst TG2) xs)" x]
      by force
  qed
  then have passes_T2: "L M1 ∩ set T2 = L M2 ∩ set T2"
    using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (L M1 ∩ set T3 = L M2 ∩ set T3)› ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›
    by blast


  have "set T1 ⊆ set T3"
  and  G2_invar: "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ convergence_graph_lookup_invar M1 M2 cg_lookup G2"
    using T2_invar_1 T2_invar_2[OF passes_T2] ‹set T2 ⊆ set T3› 
    by auto
  then have passes_T1: "L M1 ∩ set T1 = L M2 ∩ set T1"
    using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3› ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›
    by blast

  have T3_preserves_divergence : "preserves_divergence M1 M2 (V ` reachable_states M1)"
    using T1_V_div[OF passes_T1] .

  have T3_state_cover : "V ` reachable_states M1 ⊆ set T3"
    using T1_state_cover ‹set T1 ⊆ set T3›
    by blast
  then have T3_passes_state_cover : "L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
    using T1_state_cover passes_T1 by blast 


  (* properties of T3 w.r.t. undefined io pairs *)

  have rstates_io_set : "list.set rstates_io = {(q,(x,y)) . q ∈ reachable_states M1 ∧ x ∈ inputs M1 ∧ y ∈ outputs M1}"
    unfolding rstates_io rstates 
    using reachable_states_as_list_set[of M1] inputs_as_list_set[of M1] outputs_as_list_set[of M1] 
    by force
  then have undefined_io_pairs_set : "list.set undefined_io_pairs = {(q,(x,y)) . q ∈ reachable_states M1 ∧ x ∈ inputs M1 ∧ y ∈ outputs M1 ∧ h_obs M1 q x y = None}"
    unfolding undefined_io_pairs 
    by auto

  have verify_undefined_io_pair_prop : "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ (⋀ q x y T . L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y))) ⟹ 
                                                    q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹
                                                    V ` reachable_states M1 ⊆ set T ⟹
                                                    ( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} ))"
  proof -
    fix q x y T
    assume "L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y)))"
       and "q ∈ reachable_states M1" and "x ∈ inputs M1" and "y ∈ outputs M1"
       and "V ` reachable_states M1 ⊆ set T"
       and "((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))"

    have " L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1"
      using T3_state_cover ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ Prefix_Tree.set T3 = L M2 ∩ Prefix_Tree.set T3› ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› 
      by blast

    have "L M1 ∩ set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y))"
      using ‹L M1 ∩ set (verify_undefined_io_pair T (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair T (q,(x,y)))›
      unfolding verify_undefined_io_pair case_prod_conv combine_set G2
      by blast


    show "( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )"
      using assms(16)
      unfolding handles_io_pair_def 
      using assms(1-4,7,8) ‹is_state_cover_assignment M1 V› ‹L M1 ∩ V ` reachable_states M1 = L M2 ∩ V ` reachable_states M1›
            ‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1›
            G2_invar[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›] ‹convergence_graph_insert_invar M1 M2 cg_lookup cg_insert›
            ‹L M1 ∩ set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y)) = L M2 ∩ set (fst (handle_unverified_io_pair M1 V T G2 cg_insert cg_lookup q x y))› 
      by blast
  qed

  have T3_covers_undefined_io_pairs : "(⋀ q x y . q ∈ reachable_states M1 ⟹ x ∈ inputs M1 ⟹ y ∈ outputs M1 ⟹ h_obs M1 q x y = None ⟹
          ( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} ))" 
  proof -
    fix q x y assume "q ∈ reachable_states M1" and "x ∈ inputs M1" and "y ∈ outputs M1" and "h_obs M1 q x y = None" 

    have "⋀ q x y qxys T . L M1 ∩ set (foldl verify_undefined_io_pair T qxys) = L M2 ∩ set (foldl verify_undefined_io_pair T qxys) ⟹ (V ` reachable_states M1) ⊆ set T ⟹ (q,(x,y)) ∈ list.set qxys ⟹ list.set qxys ⊆ list.set undefined_io_pairs ⟹ 
              ( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )"
      (is "⋀ q x y qxys T . ?P1 qxys T ⟹ (V ` reachable_states M1) ⊆ set T ⟹ (q,(x,y)) ∈ list.set qxys ⟹ list.set qxys ⊆ list.set undefined_io_pairs ⟹ ?P2 q x y qxys T")
    proof -
      fix q x y qxys T
      assume "?P1 qxys T" and "(q,(x,y)) ∈ list.set qxys" and "list.set qxys ⊆ list.set undefined_io_pairs" and "(V ` reachable_states M1) ⊆ set T"
      then show "?P2 q x y qxys T"
      proof (induction qxys rule: rev_induct)
        case Nil
        then show ?case by auto
      next
        case (snoc a qxys)

        have "set (foldl verify_undefined_io_pair T qxys) ⊆ set (foldl verify_undefined_io_pair T (qxys@[a]))"
          using verify_undefined_io_pair_retains_testsuite 
          by auto
        then have *:"L M1 ∩ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys) = L M2 ∩ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
          using snoc.prems(1)
          by blast

        have **: "V ` reachable_states M1 ⊆ Prefix_Tree.set (foldl verify_undefined_io_pair T qxys)"
          using snoc.prems(4) verify_undefined_io_pair_folding_retains_testsuite
          by blast

        show ?case proof (cases "a = (q,(x,y))")
          case True
          then have ***: "q ∈ reachable_states M1"
            using snoc.prems(3) 
            unfolding undefined_io_pairs_set
            by auto 

          have "x ∈ inputs M1" and "y ∈ outputs M1"
            using snoc.prems(2,3) unfolding undefined_io_pairs_set by auto

          have ****: "L M1 ∩ set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y))) = L M2 ∩ set (verify_undefined_io_pair (foldl verify_undefined_io_pair T qxys) (q,(x,y)))"
            using snoc.prems(1) unfolding True by auto
            
          show ?thesis
            using verify_undefined_io_pair_prop[OF ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))› **** *** ‹x ∈ inputs M1› ‹y ∈ outputs M1› **]
            unfolding True 
            by auto
        next
          case False
          then have "(q, x, y) ∈ list.set qxys" and "list.set qxys ⊆ list.set undefined_io_pairs"
            using snoc.prems(2,3) by auto
          then show ?thesis 
            using snoc.IH[OF * _ _  snoc.prems(4)]
            using ‹set (foldl verify_undefined_io_pair T qxys) ⊆ set (foldl verify_undefined_io_pair T (qxys@[a]))›
            by blast
        qed
      qed
    qed
    moreover have "L M1 ∩ set (foldl verify_undefined_io_pair T2 undefined_io_pairs) = L M2 ∩ set (foldl verify_undefined_io_pair T2 undefined_io_pairs)"
      using ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS)) ⟹ L M1 ∩ set T3 = L M2 ∩ set T3›  ‹((L M1 ∩ set ?TS) = (L M2 ∩ set ?TS))›
      unfolding T3 T2 .
    moreover have "(V ` reachable_states M1) ⊆ set T2"
      using T1_state_cover T2 T2_invar_1 passes_T2 by fastforce
    moreover have "(q,(x,y)) ∈ list.set undefined_io_pairs"
      unfolding undefined_io_pairs_set
      using ‹q ∈ reachable_states M1› ‹x ∈ inputs M1› ‹y ∈ outputs M1› ‹h_obs M1 q x y = None›
      by blast
    ultimately show "( L M1 ∩ {(V q)@[(x,y)]} = L M2 ∩ {(V q)@[(x,y)]} )"
      unfolding T3 T2 
      by blast
  qed


  have handles_unverified_transitions: " 
            (⋀t γ. t ∈ FSM.transitions M1 ⟹
              t_source t ∈ reachable_states M1 ⟹
              length γ ≤ m-n ⟹
              list.set γ ⊆ FSM.inputs M1 × FSM.outputs M1 ⟹
              butlast γ ∈ LS M1 (t_target t) ⟹
              V (t_target t) ≠ V (t_source t) @ [(t_input t, t_output t)] ⟹
              L M1 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) =
              L M2 ∩ (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}) ∧
              preserves_divergence M1 M2 (V ` reachable_states M1 ∪ {(V (t_source t) @ [(t_input t, t_output t)]) @ ω' |ω'. ω' ∈ list.set (prefixes γ)}))"
    using T2_cover[OF passes_T2]
    unfolding unverified_transitions_alt_def
    unfolding handles_unverified_transition
    unfolding ‹?TS = T3› n by blast



  have "satisfies_abstract_h_condition M1 M2 V m"
    unfolding satisfies_abstract_h_condition_def Let_def
    using abstract_h_condition_by_unverified_transition_and_io_pair_coverage[where k="m-n",OF assms(1) ‹is_state_cover_assignment M1 V› T3_passes_state_cover T3_preserves_divergence handles_unverified_transitions T3_covers_undefined_io_pairs]
    unfolding ‹?TS = T3› n by blast

  then show "L M1 = L M2"
    using abstract_h_condition_completeness[OF assms(1,2,3,6,5,7,8) ‹is_state_cover_assignment M1 V›]
    by blast  
qed

end