[STATEMENT]
lemma wp_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 \<le> 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 \<Longrightarrow> observable M1 \<and> minimal M1 \<and> reachable_states M1 = states M1" 
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) \<longleftrightarrow> list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
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)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
using wp_method_via_spy_framework_completeness_and_finiteness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> (L ?M1.0 = L ?M2.0) = (L ?M1.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m) = L ?M2.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m))
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> finite_tree (wp_method_via_spy_framework ?M1.0 ?m)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
unfolding wp_method_via_spy_framework_ts_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> (L ?M1.0 = L ?M2.0) = (L ?M1.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m) = L ?M2.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m))
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> finite_tree (wp_method_via_spy_framework ?M1.0 ?m)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
[PROOF STEP]
by metis