Theory Test_Suite_Generator_Code_Export

section ‹Code Export›

text ‹This theory exports various functions developed in this library.›

theory Test_Suite_Generator_Code_Export
  imports "EquivalenceTesting/H_Method_Implementations"       
          "EquivalenceTesting/HSI_Method_Implementations"
          "EquivalenceTesting/W_Method_Implementations"
          "EquivalenceTesting/Wp_Method_Implementations"
          "EquivalenceTesting/SPY_Method_Implementations"
          "EquivalenceTesting/SPYH_Method_Implementations"
          "EquivalenceTesting/Partial_S_Method_Implementations"
          "AdaptiveStateCounting/Test_Suite_Calculation_Refined"
          "Prime_Transformation"
          "Prefix_Tree_Refined"
          "EquivalenceTesting/Test_Suite_Representations_Refined"
          "HOL-Library.List_Lexorder"
          "HOL-Library.Code_Target_Nat" 
          "HOL-Library.Code_Target_Int"
          "Native_Word.Uint64"
          FSM_Code_Datatype 
begin


subsection ‹Reduction Testing›


definition generate_reduction_test_suite_naive :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ String.literal + (uint64×uint64) list list" where
  "generate_reduction_test_suite_naive M m = (case (calculate_test_suite_naive_as_io_sequences_with_assumption_check M (nat_of_integer m)) of
    Inl err ⇒ Inl err |
    Inr ts ⇒ Inr (sorted_list_of_set ts))"

definition generate_reduction_test_suite_greedy :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ String.literal + (uint64×uint64) list list" where
  "generate_reduction_test_suite_greedy M m = (case (calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m)) of
    Inl err ⇒ Inl err |
    Inr ts ⇒ Inr (sorted_list_of_set ts))"

subsubsection ‹Fault Detection Capabilities of the Test Harness›

text ‹The test harness for reduction testing (see https://bitbucket.org/RobertSachtleben/an-approach-for-the-verification-and-synthesis-of-complete)
      applies a test suite to a system under test (SUT) by repeatedly applying each IO-sequence 
      (test case) in the test suite input by input to the SUT until either the test case has been
      fully applied or the first output is observed that does not correspond to the outputs in the 
      IO-sequence and then checks whether the observed IO-sequence (consisting of a prefix of the 
      test case possibly followed by an IO-pair consisting of the next input in the test case and an
      output that is not the next output in the test case) is prefix of some test case in the test
      suite. If such a prefix exists, then the application passes, else it fails and the overall
      application is aborted, reporting a failure.

      The following lemma shows that the SUT (whose behaviour corresponds to an FSM @{text "M'"}) 
      conforms to the specification (here FSM @{text "M"}) if and only if the above application 
      procedure does not fail. As the following lemma uses quantification over all possible 
      responses of the SUT to each test case, a further testability hypothesis is required to 
      transfer this result to the actual test application process, which by necessity can only
      perform a finite number of applications: we assume that some value @{text "k"} exists such 
      that by applying each test case @{text "k"} times, all responses of the SUT to it can be 
      observed.› 

lemma reduction_test_harness_soundness :
  fixes M :: "(uint64,uint64,uint64) fsm"
  assumes "observable M'"
  and     "FSM.inputs M' = FSM.inputs M"
  and     "completely_specified M'"
  and     "size M' ≤ nat_of_integer m"
  and     "generate_reduction_test_suite_greedy M m = Inr ts"
shows  "(L M' ⊆ L M) ⟷ (list_all  (λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts))) ts)"
proof -

  obtain tss where "calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss"
    using assms(5) unfolding generate_reduction_test_suite_greedy_def 
    by (metis Inr_Inl_False old.sum.exhaust old.sum.simps(5))


  have "FSM.inputs M ≠ {}"
  and  "observable M" 
  and  "completely_specified M"
    using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
    unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def 
    by (meson Inl_Inr_False)+ 
  then have "tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))"
    using ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
    unfolding calculate_test_suite_greedy_as_io_sequences_with_assumption_check_def
    by (metis sum.inject(2)) 

  have  "⋀q. q ∈ FSM.states M ⟹ ∃d∈list.set (maximal_repetition_sets_from_separators_list_greedy M). q ∈ fst d"
    unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def
    using greedy_pairwise_r_distinguishable_state_sets_from_separators_cover[of _ M]
    by simp 
  moreover have "⋀d. d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ fst d ⊆ FSM.states M ∧ (snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)" 
            and "⋀ d q1 q2. d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M) ⟹ q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
  proof 
    fix d assume "d ∈ list.set (maximal_repetition_sets_from_separators_list_greedy M)"
    then have "fst d ∈ list.set (greedy_pairwise_r_distinguishable_state_sets_from_separators M)"
         and  "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)"
      unfolding maximal_repetition_sets_from_separators_list_greedy_def Let_def by force+

    then have "fst d ∈ pairwise_r_distinguishable_state_sets_from_separators M"
      using greedy_pairwise_r_distinguishable_state_sets_from_separators_soundness by blast
    then show "fst d ⊆ FSM.states M" and "(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)" 
          and "⋀ q1 q2 . q1∈fst d ⟹ q2∈fst d ⟹ q1 ≠ q2 ⟹ (q1, q2) ∈ fst ` r_distinguishable_state_pairs_with_separators M"
      using ‹(snd d = fst d ∩ fst ` d_reachable_states_with_preambles M)›
      unfolding pairwise_r_distinguishable_state_sets_from_separators_def
      by force+ 
  qed
  ultimately have "implies_completeness (calculate_test_suite_greedy M (nat_of_integer m)) M (nat_of_integer m)"
             and  "is_finite_test_suite (calculate_test_suite_greedy M (nat_of_integer m))"
    using calculate_test_suite_for_repetition_sets_sufficient_and_finite[OF ‹observable M› ‹completely_specified M› ‹FSM.inputs M ≠ {}›]
    unfolding calculate_test_suite_greedy_def
    by simp+
    
  then have "finite tss" 
    using test_suite_to_io_maximal_finite[OF _ _ ‹observable M›] 
    unfolding ‹tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))›
    by blast 

  have "list.set ts = test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m))"
  and  "ts = sorted_list_of_set tss"
    using sorted_list_of_set(1)[OF ‹finite tss›]
    using assms(5)
    unfolding ‹tss = (test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m)))›
              ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss›
              generate_reduction_test_suite_greedy_def
    by simp+

  then have "(L M' ⊆ L M) = pass_io_set_maximal M' (list.set ts)"
    using calculate_test_suite_greedy_as_io_sequences_with_assumption_check_completeness[OF assms(1,2,3,4)]
          ‹calculate_test_suite_greedy_as_io_sequences_with_assumption_check M (nat_of_integer m) = Inr tss› 
          ‹tss = test_suite_to_io_maximal M (calculate_test_suite_greedy M (nat_of_integer m))›
    by simp

  moreover have "pass_io_set_maximal M' (list.set ts) 
                  = (list_all (λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts))) ts)"
  proof -
    have "⋀ P . list_all P (sorted_list_of_set tss) = (∀ x ∈ tss . P x)"
      by (simp add: ‹finite tss› list_all_iff)
    then have scheme: "⋀ P . list_all P ts = (∀ x ∈ (list.set ts) . P x)"
      unfolding ‹ts = sorted_list_of_set tss› sorted_list_of_set(1)[OF ‹finite tss›] 
      by simp
      
    show ?thesis
      using scheme[of "(λ io . ¬ (∃ ioPre x y y' ioSuf . io = ioPre@[(x,y)]@ioSuf ∧ ioPre@[(x,y')] ∈ L M' ∧ ¬(∃ ioSuf' . ioPre@[(x,y')]@ioSuf' ∈ list.set ts)))"]
      unfolding pass_io_set_maximal_def 
      by fastforce
  qed

  ultimately show ?thesis
    by simp
qed



subsection ‹Equivalence Testing›

subsubsection ‹Test Strategy Application and Transformation›


fun apply_method_to_prime :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ (uint64×uint64) prefix_tree" where
  "apply_method_to_prime M additionalStates isAlreadyPrime f = (let 
    M' = (if isAlreadyPrime then M else to_prime_uint64 M);
    m = size_r M' + (nat_of_integer additionalStates)
  in f M' m)"


lemma apply_method_to_prime_completeness :
  fixes M2 :: "('a,uint64,uint64) fsm"
  assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .  
              observable M1 ⟹
              observable M2 ⟹
              minimal M1 ⟹
              minimal M2 ⟹
              size_r M1 ≤ m ⟹
              size M2 ≤ m ⟹
              FSM.inputs M2 = FSM.inputs M1 ⟹
              FSM.outputs M2 = FSM.outputs M1 ⟹
              (L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m)))"
  and   "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ ((L M1 ∩ set (apply_method_to_prime M1 additionalStates isAlreadyPrime f)) = (L M2 ∩ set (apply_method_to_prime M1 additionalStates isAlreadyPrime f)))"
proof -

  define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
  have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
    unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7) 
    by (metis (full_types))+
  then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
    using assms(5,6) by auto

  have "size_r M' = size_r (to_prime M1)"
    by (metis (no_types) ‹L M1 = L M'› ‹minimal M'› ‹observable M'› minimal_equivalence_size_r to_prime_props(1) to_prime_props(2) to_prime_props(3))
  then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
    by simp

  show ?thesis
    using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
    unfolding apply_method_to_prime.simps Let_def ‹size_r M' = size_r (to_prime M1)›[symmetric] M'_def ‹L M1 = L M'› .
qed


fun apply_to_prime_and_return_io_lists :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ ((uint64×uint64)×bool) list list" where
  "apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime f = (let M' = (if isAlreadyPrime then M else to_prime_uint64 M) in
    sorted_list_of_maximal_sequences_in_tree (test_suite_from_io_tree M' (FSM.initial M') (apply_method_to_prime M additionalStates isAlreadyPrime f)))"


lemma apply_to_prime_and_return_io_lists_completeness :
  fixes M2 :: "('a,uint64,uint64) fsm"
  assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .  
              observable M1 ⟹
              observable M2 ⟹
              minimal M1 ⟹
              minimal M2 ⟹
              size_r M1 ≤ m ⟹
              size M2 ≤ m ⟹
              FSM.inputs M2 = FSM.inputs M1 ⟹
              FSM.outputs M2 = FSM.outputs M1 ⟹
              ((L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m))))
                ∧ finite_tree (f M1 m)"
  and   "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime f)"
proof -

  define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
  have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
    unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7) 
    by (metis (full_types))+
  then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
    using assms(5,6) by auto

  have "L M' = L (to_prime M1)"
    using to_prime_props(1) M'_def
    using ‹L M1 = L M'› by blast
  
  have "size_r M' = size_r (to_prime M1)" 
    using minimal_equivalence_size_r[OF ‹minimal M'› _ ‹observable M'› _ ‹L M' = L (to_prime M1)›]
    using assms(7) to_prime_props(2,3)
    unfolding M'_def
    by blast 
  then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
    by simp

  have *:"(L M1 = L M2) ⟷ ((L M1 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))) = (L M2 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))))"
   and **:"finite_tree (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))"
    using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
    unfolding ‹L M1 = L M'› by blast+

  show ?thesis
    unfolding *
    using passes_test_cases_from_io_tree[OF ‹observable M'› assms(2) fsm_initial[of M'] fsm_initial[of M2] ** ]
    unfolding ‹size_r M' = size_r (to_prime M1)›[symmetric]
    unfolding apply_to_prime_and_return_io_lists.simps apply_method_to_prime.simps Let_def ‹L M1 = L M'›
    unfolding M'_def by blast
qed

     
fun apply_to_prime_and_return_input_lists :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64,uint64,uint64) fsm ⇒ nat ⇒ (uint64×uint64) prefix_tree) ⇒ uint64 list list" where
  "apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime f = test_suite_to_input_sequences (apply_method_to_prime M additionalStates isAlreadyPrime f)"    

lemma apply_to_prime_and_return_input_lists_completeness :
  fixes M2 :: "('a,uint64,uint64) fsm"
  assumes "⋀ M1 m (M2 :: ('a,uint64,uint64) fsm) .  
              observable M1 ⟹
              observable M2 ⟹
              minimal M1 ⟹
              minimal M2 ⟹
              size_r M1 ≤ m ⟹
              size M2 ≤ m ⟹
              FSM.inputs M2 = FSM.inputs M1 ⟹
              FSM.outputs M2 = FSM.outputs M1 ⟹
              ((L M1 = L M2) ⟷ ((L M1 ∩ set (f M1 m)) = (L M2 ∩ set (f M1 m))))
                ∧ finite_tree (f M1 m)"
  and   "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (apply_to_prime_and_return_input_lists M1 additionalStates isAlreadyPrime f). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
proof -
  define M' where "M' = (if isAlreadyPrime then M1 else to_prime_uint64 M1)"
  have "observable M'" and "minimal M'" and "L M1 = L M'" and "FSM.inputs M' = FSM.inputs M1" and "FSM.outputs M' = FSM.outputs M1"
    unfolding M'_def using to_prime_uint64_props[OF assms(8)] assms(7) 
    by (metis (full_types))+
  then have "FSM.inputs M2 = FSM.inputs M'" and "FSM.outputs M2 = FSM.outputs M'"
    using assms(5,6) by auto

  have "L M' = L (to_prime M1)"
    using to_prime_props(1) M'_def ‹L M1 = L M'› by metis
  
  have "size_r M' = size_r (to_prime M1)" 
    using minimal_equivalence_size_r[OF ‹minimal M'› _ ‹observable M'› _ ‹L M' = L (to_prime M1)›]
    using assms(7) to_prime_props(2,3)
    unfolding M'_def
    by blast 
  then have "size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
    by simp

  have *:"(L M1 = L M2) = ((L M1 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))) = (L M2 ∩ set (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))))"
   and **:"finite_tree (f M' (size_r (to_prime M1) + nat_of_integer additionalStates))"
    using assms(1)[OF ‹observable M'› assms(2) ‹minimal M'› assms(3) ‹size_r M' ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)› assms(4) ‹FSM.inputs M2 = FSM.inputs M'› ‹FSM.outputs M2 = FSM.outputs M'›]
    unfolding ‹L M1 = L M'› by blast+

  show ?thesis
    using test_suite_to_input_sequences_pass_alt_def[OF ** *] 
    unfolding ‹size_r M' = size_r (to_prime M1)›[symmetric]
    unfolding apply_to_prime_and_return_input_lists.simps apply_method_to_prime.simps Let_def M'_def .
qed


subsubsection ‹W-Method›

definition w_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "w_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_h_framework"

lemma w_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_h_framework_completeness_and_finiteness
  unfolding w_method_via_h_framework_ts_def
  by metis

definition w_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "w_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_h_framework"

lemma w_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_h_framework_completeness_and_finiteness
  unfolding w_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 

definition w_method_via_h_framework_2_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "w_method_via_h_framework_2_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_h_framework_2"

lemma w_method_via_h_framework_2_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_h_framework_2_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_h_framework_2 and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_h_framework_2_completeness_and_finiteness
  unfolding w_method_via_h_framework_2_ts_def
  by metis

definition w_method_via_h_framework_2_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "w_method_via_h_framework_2_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_h_framework_2"

lemma w_method_via_h_framework_2_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_h_framework_2_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_h_framework_2 and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_h_framework_2_completeness_and_finiteness
  unfolding w_method_via_h_framework_2_input_def[symmetric] 
  by (metis (no_types, lifting))
  
definition w_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "w_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_spy_framework"

lemma w_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_spy_framework_completeness_and_finiteness
  unfolding w_method_via_spy_framework_ts_def
  by metis

definition w_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "w_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_spy_framework"

lemma w_method_via_spy_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_spy_framework_completeness_and_finiteness
  unfolding w_method_via_spy_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 

definition w_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "w_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime w_method_via_pair_framework"

lemma w_method_via_pair_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (w_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=w_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_pair_framework_completeness_and_finiteness
  unfolding w_method_via_pair_framework_ts_def
  by metis

definition w_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "w_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime w_method_via_pair_framework"

lemma w_method_via_pair_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (w_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=w_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using w_method_via_pair_framework_completeness_and_finiteness
  unfolding w_method_via_pair_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 


subsubsection ‹Wp-Method›

definition wp_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "wp_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime wp_method_via_h_framework"

lemma wp_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=wp_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using wp_method_via_h_framework_completeness_and_finiteness
  unfolding wp_method_via_h_framework_ts_def
  by metis

definition wp_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "wp_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime wp_method_via_h_framework"

lemma wp_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (wp_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=wp_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using wp_method_via_h_framework_completeness_and_finiteness
  unfolding wp_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  
definition wp_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "wp_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime wp_method_via_spy_framework"

lemma wp_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=wp_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using wp_method_via_spy_framework_completeness_and_finiteness
  unfolding wp_method_via_spy_framework_ts_def
  by metis

definition wp_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "wp_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime wp_method_via_spy_framework"

lemma wp_method_via_spy_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (wp_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=wp_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using wp_method_via_spy_framework_completeness_and_finiteness
  unfolding wp_method_via_spy_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 


subsubsection ‹HSI-Method›

definition hsi_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "hsi_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_h_framework"

lemma hsi_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_h_framework_completeness_and_finiteness
  unfolding hsi_method_via_h_framework_ts_def
  by metis

definition hsi_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "hsi_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_h_framework"

lemma hsi_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_h_framework_completeness_and_finiteness
  unfolding hsi_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  
definition hsi_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "hsi_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_spy_framework"

lemma hsi_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_spy_framework_completeness_and_finiteness
  unfolding hsi_method_via_spy_framework_ts_def
  by metis

definition hsi_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "hsi_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_spy_framework"

lemma hsi_method_via_spy_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_spy_framework_completeness_and_finiteness
  unfolding hsi_method_via_spy_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 

definition hsi_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "hsi_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime hsi_method_via_pair_framework"

lemma hsi_method_via_pair_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (hsi_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=hsi_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_pair_framework_completeness_and_finiteness
  unfolding hsi_method_via_pair_framework_ts_def
  by metis

definition hsi_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "hsi_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime hsi_method_via_pair_framework"

lemma hsi_method_via_pair_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (hsi_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=hsi_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using hsi_method_via_pair_framework_completeness_and_finiteness
  unfolding hsi_method_via_pair_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 

subsubsection ‹H-Method›

definition h_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "h_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_h_framework M m c b)"

lemma h_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_h_framework_completeness_and_finiteness
  unfolding h_method_via_h_framework_ts_def
  by metis

definition h_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "h_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_h_framework M m c b)"

lemma h_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_h_framework_completeness_and_finiteness
  unfolding h_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  

definition h_method_via_pair_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "h_method_via_pair_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime h_method_via_pair_framework"

lemma h_method_via_pair_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=h_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_completeness_and_finiteness
  unfolding h_method_via_pair_framework_ts_def
  by metis

definition h_method_via_pair_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "h_method_via_pair_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime h_method_via_pair_framework"

lemma h_method_via_pair_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=h_method_via_pair_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_completeness_and_finiteness
  unfolding h_method_via_pair_framework_input_def[symmetric]
  by (metis (no_types, lifting))


definition h_method_via_pair_framework_2_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "h_method_via_pair_framework_2_ts M additionalStates isAlreadyPrime c = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_2 M m c)"

lemma h_method_via_pair_framework_2_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_2_ts M1 additionalStates isAlreadyPrime c)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_pair_framework_2 M m c)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_2_completeness_and_finiteness
  unfolding h_method_via_pair_framework_2_ts_def
  by metis

definition h_method_via_pair_framework_2_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "h_method_via_pair_framework_2_input M additionalStates isAlreadyPrime c = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_2 M m c)"

lemma h_method_via_pair_framework_2_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_2_input M1 additionalStates isAlreadyPrime c). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_pair_framework_2 M m c)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_2_completeness_and_finiteness
  unfolding h_method_via_pair_framework_2_input_def[symmetric]
  by (metis (no_types, lifting))


definition h_method_via_pair_framework_3_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "h_method_via_pair_framework_3_ts M additionalStates isAlreadyPrime c1 c2 = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_3 M m c1 c2)"

lemma h_method_via_pair_framework_3_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (h_method_via_pair_framework_3_ts M1 additionalStates isAlreadyPrime c1 c2)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . h_method_via_pair_framework_3 M m c1 c2)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_3_completeness_and_finiteness
  unfolding h_method_via_pair_framework_3_ts_def
  by metis

definition h_method_via_pair_framework_3_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "h_method_via_pair_framework_3_input M additionalStates isAlreadyPrime c1 c2 = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . h_method_via_pair_framework_3 M m c1 c2)"

lemma h_method_via_pair_framework_3_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (h_method_via_pair_framework_3_input M1 additionalStates isAlreadyPrime c1 c2). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . h_method_via_pair_framework_3 M m c1 c2)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using h_method_via_pair_framework_3_completeness_and_finiteness
  unfolding h_method_via_pair_framework_3_input_def[symmetric]
  by (metis (no_types, lifting))


subsubsection ‹SPY-Method›

definition spy_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "spy_method_via_h_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime spy_method_via_h_framework"

lemma spy_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spy_method_via_h_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=spy_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spy_method_via_h_framework_completeness_and_finiteness
  unfolding spy_method_via_h_framework_ts_def
  by metis

definition spy_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "spy_method_via_h_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime spy_method_via_h_framework"

lemma spy_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spy_method_via_h_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=spy_method_via_h_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spy_method_via_h_framework_completeness_and_finiteness
  unfolding spy_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  
definition spy_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "spy_method_via_spy_framework_ts M additionalStates isAlreadyPrime = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime spy_method_via_spy_framework"

lemma spy_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64" 
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spy_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
  using apply_to_prime_and_return_io_lists_completeness[where f=spy_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spy_method_via_spy_framework_completeness_and_finiteness
  unfolding spy_method_via_spy_framework_ts_def
  by metis

definition spy_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ uint64 list list" where
  "spy_method_via_spy_framework_input M additionalStates isAlreadyPrime = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime spy_method_via_spy_framework"

lemma spy_method_via_spy_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"  
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spy_method_via_spy_framework_input M1 additionalStates isAlreadyPrime). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f=spy_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spy_method_via_spy_framework_completeness_and_finiteness
  unfolding spy_method_via_spy_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 


subsubsection ‹SPYH-Method›

definition spyh_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "spyh_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_h_framework M m c b)"

lemma spyh_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64" 
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spyh_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . spyh_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spyh_method_via_h_framework_completeness_and_finiteness
  unfolding spyh_method_via_h_framework_ts_def
  by metis

definition spyh_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "spyh_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_h_framework M m c b)"

lemma spyh_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64" 
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spyh_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . spyh_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spyh_method_via_h_framework_completeness_and_finiteness
  unfolding spyh_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  
definition spyh_method_via_spy_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "spyh_method_via_spy_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_spy_framework M m c b)"

lemma spyh_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64" 
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (spyh_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime c b)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . spyh_method_via_spy_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spyh_method_via_spy_framework_completeness_and_finiteness
  unfolding spyh_method_via_spy_framework_ts_def
  by metis

definition spyh_method_via_spy_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "spyh_method_via_spy_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . spyh_method_via_spy_framework M m c b)"

lemma spyh_method_via_spy_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64" 
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (spyh_method_via_spy_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . spyh_method_via_spy_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using spyh_method_via_spy_framework_completeness_and_finiteness
  unfolding spyh_method_via_spy_framework_input_def[symmetric]
  by (metis (no_types, lifting)) 


subsubsection ‹Partial S-Method›

definition partial_s_method_via_h_framework_ts :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ ((uint64×uint64)×bool) list list" where
  "partial_s_method_via_h_framework_ts M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_io_lists M additionalStates isAlreadyPrime (λ M m . partial_s_method_via_h_framework M m c b)"

lemma partial_s_method_via_h_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"  
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ list_all (passes_test_case M2 (FSM.initial M2)) (partial_s_method_via_h_framework_ts M1 additionalStates isAlreadyPrime c b)"
  using apply_to_prime_and_return_io_lists_completeness[where f="(λ M m . partial_s_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using partial_s_method_via_h_framework_completeness_and_finiteness
  unfolding partial_s_method_via_h_framework_ts_def
  by metis

definition partial_s_method_via_h_framework_input :: "(uint64,uint64,uint64) fsm ⇒ integer ⇒ bool ⇒ bool ⇒ bool ⇒ uint64 list list" where
  "partial_s_method_via_h_framework_input M additionalStates isAlreadyPrime c b = apply_to_prime_and_return_input_lists M additionalStates isAlreadyPrime (λ M m . partial_s_method_via_h_framework M m c b)"

lemma partial_s_method_via_h_framework_input_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 ≤ size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime ⟹ observable M1 ∧ minimal M1 ∧ reachable_states M1 = states M1"  
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) ⟷ (∀xs∈list.set (partial_s_method_via_h_framework_input M1 additionalStates isAlreadyPrime c b). ∀xs'∈list.set (prefixes xs). {io ∈ L M1. map fst io = xs'} = {io ∈ L M2. map fst io = xs'})"
  using apply_to_prime_and_return_input_lists_completeness[where f="(λ M m . partial_s_method_via_h_framework M m c b)" and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
  using partial_s_method_via_h_framework_completeness_and_finiteness
  unfolding partial_s_method_via_h_framework_input_def[symmetric] 
  by (metis (no_types, lifting)) 
  



subsection ‹New Instances›

(* alternative instantiations for fsets
derive (eq) ceq fset
derive (no) cenum fset
derive (no) ccompare fset
derive (dlist) set_impl fset

instantiation fset :: (infinite_UNIV) finite_UNIV begin
definition "finite_UNIV = Phantom(('a)fset) False"


lemma infinite_UNIV_fset : 
  shows "infinite (UNIV :: ('a :: infinite_UNIV) fset set)"
proof -
  (* if infinitely many elements exist, then infinitely many distinct singletons can be created *)
  define f :: "'a ⇒ ('a) fset" where f_def: "f = (λ q . {| q |})"
  have "inj f" 
  proof 
    fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y" 
    then show "x = y" unfolding f_def by (transfer; auto)
  qed
  moreover have "infinite (UNIV :: 'a set)"
    using infinite_UNIV by auto
  ultimately show ?thesis
    by (meson finite_imageD infinite_iff_countable_subset top_greatest) 
qed

instance by (intro_classes)
            (simp add: finite_UNIV_fset_def infinite_UNIV_fset) 
end

instantiation fset :: (infinite_UNIV) cproper_interval begin
definition cproper_interval_fset :: "(('a) fset) proper_interval" 
  where "cproper_interval_fset _ _ = undefined"
instance by(intro_classes)(simp add: infinite_UNIV_fset)
end

lemma infinite_UNIV_fset : "infinite (UNIV :: ('a :: infinite_UNIV) fset set)"
proof -
  (* if infinitely many elements exist, then infinitely many distinct singletons can be created *)
  define f :: "'a ⇒ ('a) fset" where f_def: "f = (λ q . {| q |})"
  have "inj f" 
  proof 
    fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y" 
    then show "x = y" unfolding f_def by (transfer; auto)
  qed
  moreover have "infinite (UNIV :: 'a set)"
    using infinite_UNIV by auto
  ultimately show ?thesis
    by (meson finite_imageD infinite_iff_countable_subset top_greatest) 
qed
*)

lemma finiteness_fset_UNIV : "finite (UNIV :: 'a fset set) = finite (UNIV :: 'a set)"
proof 

  define f :: "'a ⇒ ('a) fset" where f_def: "f = (λ q . {| q |})"
  have "inj f" 
  proof 
    fix x y assume "x ∈ (UNIV :: 'a set)" and "y ∈ UNIV" and "f x = f y" 
    then show "x = y" unfolding f_def by (transfer; auto)
  qed

  show "finite (UNIV :: 'a fset set) ⟹ finite (UNIV :: 'a set)"
  proof (rule ccontr)
    assume "finite (UNIV :: 'a fset set)" and "¬ finite (UNIV :: 'a set)"

    then have "¬ finite (f ` UNIV)"
      using ‹inj f›
      using finite_imageD by blast 
    then have "¬ finite (UNIV :: 'a fset set)"
      by (meson infinite_iff_countable_subset top_greatest) 
    then show False
      using ‹finite (UNIV :: 'a fset set)› by auto
  qed

  show "finite (UNIV :: 'a set) ⟹ finite (UNIV :: 'a fset set)"
  proof -
    assume "finite (UNIV :: 'a set)"
    then have "finite (UNIV :: 'a set set)"
      by (simp add: Finite_Set.finite_set) 
    moreover have "fset ` (UNIV :: 'a fset set) ⊆ (UNIV :: 'a set set)"
      by auto
    moreover have "inj fset"
      by (meson fset_inject injI) 
    ultimately show ?thesis by (metis inj_on_finite)
  qed
qed

instantiation fset :: (finite_UNIV) finite_UNIV begin
definition "finite_UNIV = Phantom('a fset) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
instance by(intro_classes)(simp add: finite_UNIV_fset_def finite_UNIV finiteness_fset_UNIV)
end

derive (eq) ceq fset
derive (no) cenum fset
derive (no) ccompare fset
derive (dlist) set_impl fset

instantiation fset :: (type) cproper_interval begin
definition cproper_interval_fset :: "(('a) fset) proper_interval" 
  where "cproper_interval_fset _ _ = undefined"
instance by(intro_classes)(simp add: ID_None ccompare_fset_def)
end

lemma card_fPow: "card (Pow (fset A)) = 2 ^ card (fset A)"
  using card_Pow[of "fset A"]
  by simp

 

lemma finite_sets_finite_univ : 
  assumes "finite (UNIV :: 'a set)" 
  shows "finite (xs :: 'a set)"
  by (metis Diff_UNIV Diff_infinite_finite assms finite_Diff) 


lemma card_UNIV_fset: "CARD('a fset) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))"
  apply (simp add: card_eq_0_iff)
proof 

  have "inj fset"
    by (meson fset_inject injI)
  have "card (UNIV :: 'a fset set) = card (fset ` (UNIV :: 'a fset set))"
    by (simp add: ‹inj fset› card_image)


  show "finite (UNIV :: 'a set) ⟶ CARD('a fset) = 2 ^ CARD('a)"
  proof 
    assume "finite (UNIV :: 'a set)"
    then have "CARD('a set) = 2 ^ CARD('a)"
      by (metis Pow_UNIV card_Pow)

    have "finite (UNIV :: 'a set set)" 
      using ‹finite (UNIV :: 'a set)›
      by (simp add: Finite_Set.finite_set) 
    
    have "finite (UNIV :: 'a fset set)"
      using ‹finite (UNIV :: 'a set)› finiteness_fset_UNIV by auto


    have "⋀ xs :: 'a set . finite xs"
      using finite_sets_finite_univ[OF ‹finite (UNIV :: 'a set)›] .
    then have "(UNIV :: 'a set set) = fset ` (UNIV :: 'a fset set)"
      by (metis UNIV_I UNIV_eq_I fset_to_fset image_iff)
    
    have "CARD('a fset) ≤ CARD('a set)"
      unfolding ‹card (UNIV :: 'a fset set) = card (fset ` (UNIV :: 'a fset set))› 
      by (metis ‹finite (UNIV :: 'a set set)› card_mono subset_UNIV)
    moreover have "CARD('a fset) ≥ CARD('a set)" 
      unfolding ‹(UNIV :: 'a set set) = fset ` (UNIV :: 'a fset set)›
      using ‹CARD('a::type fset) = card (range fset)› by linarith
    ultimately have "CARD('a fset) = CARD('a set)"
      by linarith
    then show "CARD('a fset) = (2::nat) ^ CARD('a)"
      by (simp add: ‹CARD('a::type set) = (2::nat) ^ CARD('a::type)›)
  qed 

  show "infinite (UNIV :: 'a set) ⟶ infinite (UNIV :: 'a fset set)"
    by (simp add: finiteness_fset_UNIV)
qed

instantiation fset :: (card_UNIV) card_UNIV begin
definition "card_UNIV = Phantom('a fset)
  (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c = 0 then 0 else 2 ^ c)"
instance by intro_classes (simp add: card_UNIV_fset_def card_UNIV_fset card_UNIV)
end

derive (choose) mapping_impl fset

lemma uint64_range : "range nat_of_uint64 = {..<2 ^ 64}"
proof 
  show "{..<2 ^ 64} ⊆ range nat_of_uint64"
    using uint64_nat_bij
    by (metis lessThan_iff range_eqI subsetI) 
  have "⋀ x . nat_of_uint64 x < 2^64"
    apply transfer using take_bit_nat_eq_self
    by (metis uint64.size_eq_length unsigned_less)
  then show "range nat_of_uint64 ⊆ {..<2 ^ 64}"
    by auto
qed

lemma card_UNIV_uint64: "CARD(uint64) = 2^64" 
proof -
  have "inj nat_of_uint64"
    apply transfer
    by simp 
  then have "bij_betw nat_of_uint64 (UNIV :: uint64 set) {..<2^64}"
    using uint64_range
    unfolding bij_betw_def by blast
  then show ?thesis
    by (simp add: bij_betw_same_card) 
qed

lemma nat_of_uint64_bij_betw : "bij_betw nat_of_uint64  (UNIV :: uint64 set) {..<2 ^ 64}"
  unfolding bij_betw_def
  using uint64_range
  by transfer (auto)


lemma uint64_UNIV : "(UNIV :: uint64 set) = uint64_of_nat ` {..<2 ^ 64}"
  using nat_of_uint64_bij_betw
  by (metis UNIV_I UNIV_eq_I bij_betw_def card_UNIV_uint64 imageI image_eqI inj_on_contraD lessThan_iff rangeI uint64_nat_bij uint64_range)

lemma uint64_of_nat_bij_betw : "bij_betw uint64_of_nat  {..<2 ^ 64} (UNIV :: uint64 set)"  
  unfolding bij_betw_def
proof
  show "inj_on uint64_of_nat {..<2 ^ 64}"
    using nat_of_uint64_bij_betw uint64_nat_bij
    by (metis inj_on_inverseI lessThan_iff) 
  show "uint64_of_nat ` {..<2 ^ 64} = UNIV"
    using uint64_UNIV by blast
qed
    

lemma uint64_finite : "finite (UNIV :: uint64 set)"
  unfolding uint64_UNIV
  by simp 


instantiation uint64 :: finite_UNIV begin
definition "finite_UNIV = Phantom(uint64) True"
instance apply intro_classes
  by (simp add: finite_UNIV_uint64_def uint64_finite) 
end


instantiation uint64 :: card_UNIV begin
definition "card_UNIV = Phantom(uint64) (2^64)"
instance 
  by intro_classes (simp add: card_UNIV_uint64_def card_UNIV_uint64 card_UNIV)
end


instantiation uint64 :: compare
begin
definition compare_uint64 :: "uint64 ⇒ uint64 ⇒ order" where
  "compare_uint64 x y = (case (x < y, x = y) of (True,_) ⇒ Lt | (False,True) ⇒ Eq | (False,False) ⇒ Gt)"

instance 
  apply intro_classes 
proof 
  show "⋀x y::uint64. invert_order (compare x y) = compare y x" 
  proof -
    fix x y::uint64 show "invert_order (compare x y) = compare y x"
    proof (cases "x = y")
      case True
      then show ?thesis unfolding compare_uint64_def by auto
    next
      case False
      then show ?thesis proof (cases "x < y")
        case True
        then show ?thesis unfolding compare_uint64_def using False
          using order_less_not_sym by fastforce 
      next
        case False
        then show ?thesis unfolding compare_uint64_def using ‹x ≠ y›
          using linorder_less_linear by fastforce
      qed
    qed
  qed

  show "⋀x y::uint64. compare x y = Eq ⟹ x = y" 
    unfolding compare_uint64_def
    by (metis (mono_tags) case_prod_conv old.bool.simps(3) old.bool.simps(4) order.distinct(1) order.distinct(3)) 

  show "⋀x y z::uint64. compare x y = Lt ⟹ compare y z = Lt ⟹ compare x z = Lt"
    unfolding compare_uint64_def
    by (metis (full_types, lifting) case_prod_conv old.bool.simps(3) old.bool.simps(4) order.distinct(5) order_less_trans)
qed
end 

instantiation uint64 :: ccompare
begin
definition ccompare_uint64 :: "(uint64 ⇒ uint64 ⇒ order) option" where
  "ccompare_uint64 = Some compare"

instance by (intro_classes; simp add: ccompare_uint64_def comparator_compare)
end

derive (eq) ceq uint64
derive (no) cenum uint64
derive (rbt) set_impl uint64
derive (rbt) mapping_impl uint64


instantiation uint64 :: proper_interval begin
fun proper_interval_uint64 :: "uint64 proper_interval" 
  where 
    "proper_interval_uint64 None None = True" |
    "proper_interval_uint64 None (Some y) = (y > 0)"|
    "proper_interval_uint64 (Some x) None = (x ≠ uint64_of_nat (2^64-1))" | 
    "proper_interval_uint64 (Some x) (Some y) = (x < y ∧ x+1 < y)"

instance apply intro_classes
proof -
  show "proper_interval None (None :: uint64 option) = True" by auto

  show "⋀y. proper_interval None (Some (y::uint64)) = (∃z. z < y)"
    unfolding proper_interval_uint64.simps
    apply transfer
    using word_gt_a_gt_0 by auto
  
  have "⋀ x . (x ≠ uint64_of_nat (2^64-1)) = (nat_of_uint64 x ≠ 2^64-1)"
  proof 
    fix x 
    show "(x ≠ uint64_of_nat (2^64-1)) ⟹ (nat_of_uint64 x ≠ 2^64-1)"
      apply transfer
      by (metis Word.of_nat_unat ucast_id) 
    show "nat_of_uint64 x ≠ 2 ^ 64 - 1 ⟹ x ≠ uint64_of_nat (2 ^ 64 - 1)"
      by (meson diff_less pos2 uint64_nat_bij zero_less_one zero_less_power)
  qed
  then show "⋀x. proper_interval (Some (x::uint64)) None = (∃z. x < z)"
    unfolding proper_interval_uint64.simps
    apply transfer
    by (metis uint64.size_eq_length unat_minus_one_word word_le_less_eq word_le_not_less word_order.extremum)

  show "⋀x y. proper_interval (Some x) (Some (y::uint64)) = (∃z>x. z < y)"
    unfolding proper_interval_uint64.simps
    apply transfer
    using inc_le less_is_non_zero_p1 word_overflow 
    by fastforce
qed
end



                                  
instantiation uint64 :: cproper_interval begin
definition "cproper_interval = (proper_interval :: uint64 proper_interval)"
instance 
  apply intro_classes 
  apply (simp add: cproper_interval_uint64_def ord_defs ccompare_uint64_def ID_Some proper_interval_class.axioms uint64_finite) 
proof 

  fix x y :: uint64

  show "proper_interval None (None :: uint64 option) = True"
    by auto

  have "(∃z. lt_of_comp compare z y) = (∃z. z < y)"
    unfolding compare_uint64_def lt_of_comp_def
    by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(8) order.simps(9)) 
  then show "proper_interval None (Some y) = (∃z. lt_of_comp compare z y)"
    using proper_interval_simps(2) by blast 

  have "(∃z. lt_of_comp compare x z) = (∃z. x < z)"
    unfolding compare_uint64_def lt_of_comp_def
    by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(8) order.simps(9))
  then show "proper_interval (Some x) None = (∃z. lt_of_comp compare x z)"   
    using proper_interval_simps(3) by blast 

  have "(∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y) ⟹ (∃z>x. z < y)"
    unfolding compare_uint64_def lt_of_comp_def
    by (metis bool.case_eq_if case_prod_conv order.simps(7) order.simps(9))
  moreover have "(∃z>x. z < y) ⟹ (∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y)"
    unfolding compare_uint64_def lt_of_comp_def
    unfolding proper_interval_simps(4)[symmetric]
    using compare_uint64_def
    by (metis (mono_tags, lifting) ‹⋀y x. (∃z>x. z < y) = proper_interval (Some x) (Some y)› case_prod_conv old.bool.simps(3) order.simps(8))   
  ultimately show "proper_interval (Some x) (Some y) = (∃z. lt_of_comp compare x z ∧ lt_of_comp compare z y)"
    using proper_interval_simps(4) by blast 
qed
end


subsection ‹Exports›

fun fsm_from_list_uint64 :: "uint64 ⇒ (uint64 × uint64 × uint64 × uint64) list ⇒ (uint64, uint64, uint64) fsm" 
  where "fsm_from_list_uint64 q ts = fsm_from_list q ts"

fun fsm_from_list_integer :: "integer ⇒ (integer × integer × integer × integer) list ⇒ (integer, integer, integer) fsm" 
  where "fsm_from_list_integer q ts = fsm_from_list q ts"




export_code Inl
            fsm_from_list
            fsm_from_list_uint64
            fsm_from_list_integer
            size 
            to_prime
            make_observable
            rename_states
            index_states
            restrict_to_reachable_states
            integer_of_nat 
            generate_reduction_test_suite_naive
            generate_reduction_test_suite_greedy
            w_method_via_h_framework_ts
            w_method_via_h_framework_input
            w_method_via_h_framework_2_ts
            w_method_via_h_framework_2_input
            w_method_via_spy_framework_ts
            w_method_via_spy_framework_input
            w_method_via_pair_framework_ts
            w_method_via_pair_framework_input
            wp_method_via_h_framework_ts
            wp_method_via_h_framework_input
            wp_method_via_spy_framework_ts
            wp_method_via_spy_framework_input
            hsi_method_via_h_framework_ts
            hsi_method_via_h_framework_input
            hsi_method_via_spy_framework_ts
            hsi_method_via_spy_framework_input
            hsi_method_via_pair_framework_ts
            hsi_method_via_pair_framework_input
            h_method_via_h_framework_ts
            h_method_via_h_framework_input
            h_method_via_pair_framework_ts
            h_method_via_pair_framework_input
            h_method_via_pair_framework_2_ts
            h_method_via_pair_framework_2_input
            h_method_via_pair_framework_3_ts
            h_method_via_pair_framework_3_input
            spy_method_via_h_framework_ts
            spy_method_via_h_framework_input
            spy_method_via_spy_framework_ts
            spy_method_via_spy_framework_input
            spyh_method_via_h_framework_ts
            spyh_method_via_h_framework_input
            spyh_method_via_spy_framework_ts
            spyh_method_via_spy_framework_input
            partial_s_method_via_h_framework_ts
            partial_s_method_via_h_framework_input
in Haskell module_name GeneratedCode file_prefix haskell_export


export_code Inl
            fsm_from_list
            fsm_from_list_uint64
            fsm_from_list_integer
            size 
            to_prime
            make_observable
            rename_states
            index_states
            restrict_to_reachable_states
            integer_of_nat 
            generate_reduction_test_suite_naive
            generate_reduction_test_suite_greedy
            w_method_via_h_framework_ts
            w_method_via_h_framework_input
            w_method_via_h_framework_2_ts
            w_method_via_h_framework_2_input
            w_method_via_spy_framework_ts
            w_method_via_spy_framework_input
            w_method_via_pair_framework_ts
            w_method_via_pair_framework_input
            wp_method_via_h_framework_ts
            wp_method_via_h_framework_input
            wp_method_via_spy_framework_ts
            wp_method_via_spy_framework_input
            hsi_method_via_h_framework_ts
            hsi_method_via_h_framework_input
            hsi_method_via_spy_framework_ts
            hsi_method_via_spy_framework_input
            hsi_method_via_pair_framework_ts
            hsi_method_via_pair_framework_input
            h_method_via_h_framework_ts
            h_method_via_h_framework_input
            h_method_via_pair_framework_ts
            h_method_via_pair_framework_input
            h_method_via_pair_framework_2_ts
            h_method_via_pair_framework_2_input
            h_method_via_pair_framework_3_ts
            h_method_via_pair_framework_3_input
            spy_method_via_h_framework_ts
            spy_method_via_h_framework_input
            spy_method_via_spy_framework_ts
            spy_method_via_spy_framework_input
            spyh_method_via_h_framework_ts
            spyh_method_via_h_framework_input
            spyh_method_via_spy_framework_ts
            spyh_method_via_spy_framework_input
            partial_s_method_via_h_framework_ts
            partial_s_method_via_h_framework_input
in Scala module_name GeneratedCode file_prefix scala_export (case_insensitive)


export_code Inl
            fsm_from_list
            fsm_from_list_uint64
            fsm_from_list_integer
            size 
            to_prime
            make_observable
            rename_states
            index_states
            restrict_to_reachable_states
            integer_of_nat 
            generate_reduction_test_suite_naive
            generate_reduction_test_suite_greedy
            w_method_via_h_framework_ts
            w_method_via_h_framework_input
            w_method_via_h_framework_2_ts
            w_method_via_h_framework_2_input
            w_method_via_spy_framework_ts
            w_method_via_spy_framework_input
            w_method_via_pair_framework_ts
            w_method_via_pair_framework_input
            wp_method_via_h_framework_ts
            wp_method_via_h_framework_input
            wp_method_via_spy_framework_ts
            wp_method_via_spy_framework_input
            hsi_method_via_h_framework_ts
            hsi_method_via_h_framework_input
            hsi_method_via_spy_framework_ts
            hsi_method_via_spy_framework_input
            hsi_method_via_pair_framework_ts
            hsi_method_via_pair_framework_input
            h_method_via_h_framework_ts
            h_method_via_h_framework_input
            h_method_via_pair_framework_ts
            h_method_via_pair_framework_input
            h_method_via_pair_framework_2_ts
            h_method_via_pair_framework_2_input
            h_method_via_pair_framework_3_ts
            h_method_via_pair_framework_3_input
            spy_method_via_h_framework_ts
            spy_method_via_h_framework_input
            spy_method_via_spy_framework_ts
            spy_method_via_spy_framework_input
            spyh_method_via_h_framework_ts
            spyh_method_via_h_framework_input
            spyh_method_via_spy_framework_ts
            spyh_method_via_spy_framework_input
            partial_s_method_via_h_framework_ts
            partial_s_method_via_h_framework_input
in SML module_name GeneratedCode file_prefix sml_export


export_code Inl
            fsm_from_list
            fsm_from_list_uint64
            fsm_from_list_integer
            size 
            to_prime
            make_observable
            rename_states
            index_states
            restrict_to_reachable_states
            integer_of_nat 
            generate_reduction_test_suite_naive
            generate_reduction_test_suite_greedy
            w_method_via_h_framework_ts
            w_method_via_h_framework_input
            w_method_via_h_framework_2_ts
            w_method_via_h_framework_2_input
            w_method_via_spy_framework_ts
            w_method_via_spy_framework_input
            w_method_via_pair_framework_ts
            w_method_via_pair_framework_input
            wp_method_via_h_framework_ts
            wp_method_via_h_framework_input
            wp_method_via_spy_framework_ts
            wp_method_via_spy_framework_input
            hsi_method_via_h_framework_ts
            hsi_method_via_h_framework_input
            hsi_method_via_spy_framework_ts
            hsi_method_via_spy_framework_input
            hsi_method_via_pair_framework_ts
            hsi_method_via_pair_framework_input
            h_method_via_h_framework_ts
            h_method_via_h_framework_input
            h_method_via_pair_framework_ts
            h_method_via_pair_framework_input
            h_method_via_pair_framework_2_ts
            h_method_via_pair_framework_2_input
            h_method_via_pair_framework_3_ts
            h_method_via_pair_framework_3_input
            spy_method_via_h_framework_ts
            spy_method_via_h_framework_input
            spy_method_via_spy_framework_ts
            spy_method_via_spy_framework_input
            spyh_method_via_h_framework_ts
            spyh_method_via_h_framework_input
            spyh_method_via_spy_framework_ts
            spyh_method_via_spy_framework_input
            partial_s_method_via_h_framework_ts
            partial_s_method_via_h_framework_input
in OCaml module_name GeneratedCode file_prefix ocaml_export

end