[STATEMENT]
lemma handle_state_cover_dynamic_separates_state_cover:
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  fixes M2 :: "('e,'b,'c) fsm"
  fixes cg_insert :: "('d \<Rightarrow> ('b\<times>'c) list \<Rightarrow> 'd)"
  assumes "\<And> \<alpha> \<beta> q1 q2 . q1 \<in> states M1 \<Longrightarrow> q2 \<in> states M1 \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> distinguishes M1 q1 q2 (dist_fun q1 q2)"
  shows "separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
let ?f = "(handle_state_cover_dynamic b c dist_fun)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
have "\<And> (V :: ('a,'b,'c) state_cover_assignment) .
          (V ` reachable_states M1 \<subseteq> set (fst (?f M1 V cg_initial cg_insert cg_lookup)))
            \<and> finite_tree (fst (?f M1 V cg_initial cg_insert cg_lookup))
            \<and> (observable M1 \<longrightarrow>
                observable M2 \<longrightarrow>
                minimal M1 \<longrightarrow>
                minimal M2 \<longrightarrow>
                inputs M2 = inputs M1 \<longrightarrow>
                outputs M2 = outputs M1 \<longrightarrow>
                is_state_cover_assignment M1 V \<longrightarrow>
                convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow>
                convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow>
                L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow>
                (preserves_divergence M1 M2 (V ` reachable_states M1)
                \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (?f M1 V cg_initial cg_insert cg_lookup))))" (is "\<And> V . ?P V")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
fix V :: "('a,'b,'c) state_cover_assignment"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define k where "k = 2 * size M1"
[PROOF STATE]
proof (state)
this:
k = 2 * FSM.size M1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define heuristic where "heuristic = (if c then append_heuristic_input M1 else append_heuristic_io)"
[PROOF STATE]
proof (state)
this:
heuristic = (if c then append_heuristic_input M1 else append_heuristic_io)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define separate_state where "separate_state = (\<lambda> (X,T,G::'d) q . let u = V q;
                                          TG' = spyh_distinguish M1 T G cg_lookup cg_insert dist_fun u X k b heuristic;
                                          X' = u#X
                                      in (X',TG'))"
[PROOF STATE]
proof (state)
this:
separate_state = (\<lambda>(X, T, G) q. let u = V q; TG' = spyh_distinguish M1 T G cg_lookup cg_insert dist_fun u X k b heuristic; X' = u # X in (X', TG'))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define rstates where "rstates = reachable_states_as_list M1"
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define T0' where "T0' = from_list (map V rstates)"
[PROOF STATE]
proof (state)
this:
T0' = from_list (map V rstates)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define T0 where "T0 = (if b
                then Prefix_Tree.combine T0' (from_list (concat (map (\<lambda> q . language_for_input M1 (initial M1) (map fst (V q))) rstates)))
                else T0')"
[PROOF STATE]
proof (state)
this:
T0 = (if b then combine T0' (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) rstates))) else T0')

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
define G0 where "G0 = cg_initial M1 T0"
[PROOF STATE]
proof (state)
this:
G0 = cg_initial M1 T0

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have *:"(?f M1 V cg_initial cg_insert cg_lookup) = snd (foldl separate_state ([],T0,G0) rstates)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup = snd (foldl separate_state ([], T0, G0) rstates)
[PROOF STEP]
unfolding k_def separate_state_def rstates_def heuristic_def T0'_def T0_def G0_def handle_state_cover_dynamic.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (\<lambda>(X, T, G) q. (V q # X, spyh_distinguish M1 T G cg_lookup cg_insert dist_fun (V q) X (2 * FSM.size M1) b (if c then append_heuristic_input M1 else append_heuristic_io))) ([], if b then combine (from_list (map V (reachable_states_as_list M1))) (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) (reachable_states_as_list M1)))) else from_list (map V (reachable_states_as_list M1)), cg_initial M1 (if b then combine (from_list (map V (reachable_states_as_list M1))) (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) (reachable_states_as_list M1)))) else from_list (map V (reachable_states_as_list M1)))) (reachable_states_as_list M1)) = snd (foldl (\<lambda>(X, T, G) q. (V q # X, spyh_distinguish M1 T G cg_lookup cg_insert dist_fun (V q) X (2 * FSM.size M1) b (if c then append_heuristic_input M1 else append_heuristic_io))) ([], if b then combine (from_list (map V (reachable_states_as_list M1))) (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) (reachable_states_as_list M1)))) else from_list (map V (reachable_states_as_list M1)), cg_initial M1 (if b then combine (from_list (map V (reachable_states_as_list M1))) (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) (reachable_states_as_list M1)))) else from_list (map V (reachable_states_as_list M1)))) (reachable_states_as_list M1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup = snd (foldl separate_state ([], T0, G0) rstates)

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have separate_state_subset : "\<And> q X T G . set T \<subseteq> set (fst (snd (separate_state (X,T,G) q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (snd (separate_state (X, T, G) q)))
[PROOF STEP]
using spyh_distinguish_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. \<And>q X T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (snd (separate_state (X, T, G) q)))
[PROOF STEP]
unfolding separate_state_def case_prod_conv Let_def snd_conv
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. \<And>q X T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M1 T G cg_lookup cg_insert dist_fun (V q) X k b heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))
[PROOF STEP]
have "set T0 \<subseteq> set (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
by (induction rstates rule: rev_induct; auto; metis (mono_tags, opaque_lifting) Collect_mono_iff prod.exhaust_sel)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "set T0' \<subseteq> set T0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0
[PROOF STEP]
unfolding T0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set (if b then combine T0' (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) rstates))) else T0')
[PROOF STEP]
using combine_set
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (combine ?t1.0 ?t2.0) = Prefix_Tree.set ?t1.0 \<union> Prefix_Tree.set ?t2.0

goal (1 subgoal):
 1. Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set (if b then combine T0' (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) rstates))) else T0')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "V ` reachable_states M1 \<subseteq> set T0'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'
[PROOF STEP]
unfolding T0'_def rstates_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (from_list (map V (reachable_states_as_list M1)))
[PROOF STEP]
using from_list_subset
[PROOF STATE]
proof (prove)
using this:
list.set ?xs \<subseteq> Prefix_Tree.set (from_list ?xs)

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (from_list (map V (reachable_states_as_list M1)))
[PROOF STEP]
by (metis image_set reachable_states_as_list_set)
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'
[PROOF STEP]
have p1: "V ` reachable_states M1 \<subseteq> set (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "finite_tree T0'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree T0'
[PROOF STEP]
unfolding T0'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (from_list (map V rstates))
[PROOF STEP]
using from_list_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree (from_list ?xs)

goal (1 subgoal):
 1. finite_tree (from_list (map V rstates))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree T0'

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree T0'
[PROOF STEP]
have "finite_tree T0"
[PROOF STATE]
proof (prove)
using this:
finite_tree T0'

goal (1 subgoal):
 1. finite_tree T0
[PROOF STEP]
unfolding T0_def
[PROOF STATE]
proof (prove)
using this:
finite_tree T0'

goal (1 subgoal):
 1. finite_tree (if b then combine T0' (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) rstates))) else T0')
[PROOF STEP]
using combine_finite_tree[OF _ from_list_finite_tree]
[PROOF STATE]
proof (prove)
using this:
finite_tree T0'
finite_tree ?t1.0 \<Longrightarrow> finite_tree (combine ?t1.0 (from_list ?xs1))

goal (1 subgoal):
 1. finite_tree (if b then combine T0' (from_list (concat (map (\<lambda>q. language_for_input M1 (FSM.initial M1) (map fst (V q))) rstates))) else T0')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree T0

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have separate_state_finite : "\<And> q X T G . finite_tree T \<Longrightarrow> finite_tree (fst (snd (separate_state (X,T,G) q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. finite_tree T \<Longrightarrow> finite_tree (fst (snd (separate_state (X, T, G) q)))
[PROOF STEP]
using spyh_distinguish_finite
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. \<And>q X T G. finite_tree T \<Longrightarrow> finite_tree (fst (snd (separate_state (X, T, G) q)))
[PROOF STEP]
unfolding separate_state_def case_prod_conv Let_def snd_conv
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. \<And>q X T G. finite_tree T \<Longrightarrow> finite_tree (fst (spyh_distinguish M1 T G cg_lookup cg_insert dist_fun (V q) X k b heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree ?T1 \<Longrightarrow> finite_tree (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have p2: "finite_tree (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
proof (induction rstates rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) [])))
[PROOF STEP]
using \<open>finite_tree T0\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree T0

goal (1 subgoal):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) [])))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst (snd (foldl separate_state ([], T0, G0) [])))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
case (snoc a rstates)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have *:"foldl separate_state ([], T0, G0) (rstates@[a]) = separate_state (foldl separate_state ([], T0, G0) rstates) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl separate_state ([], T0, G0) (rstates @ [a]) = separate_state (foldl separate_state ([], T0, G0) rstates) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) (rstates @ [a]) = separate_state (foldl separate_state ([], T0, G0) rstates) a

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (snd (foldl separate_state ([], T0, G0) xs))) \<Longrightarrow> finite_tree (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [a]))))
[PROOF STEP]
using separate_state_finite[OF snoc.IH]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (snd (separate_state (?X1, fst (snd (foldl separate_state ([], T0, G0) rstates)), ?G1) ?q1)))

goal (1 subgoal):
 1. finite_tree (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [a]))))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (snd (separate_state (?X1, fst (snd (foldl separate_state ([], T0, G0) rstates)), ?G1) ?q1)))

goal (1 subgoal):
 1. finite_tree (fst (snd (separate_state (foldl separate_state ([], T0, G0) rstates) a)))
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [a]))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have "\<And> q X T G . fst (separate_state (X,T,G) q) = V q # X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. fst (separate_state (X, T, G) q) = V q # X
[PROOF STEP]
unfolding separate_state_def case_prod_conv Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q X T G. V q # X = V q # X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst (separate_state (?X1, ?T1, ?G1) ?q1) = V ?q1 # ?X1

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have heuristic_prop: "(\<And>T w u' uBest lBest. fst (heuristic T w (uBest, lBest) u') \<in> {u', uBest})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T w u' uBest lBest. fst (heuristic T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
unfolding heuristic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T w u' uBest lBest. fst ((if c then append_heuristic_input M1 else append_heuristic_io) T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
using append_heuristic_input_in[of M1] append_heuristic_io_in
[PROOF STATE]
proof (prove)
using this:
fst (append_heuristic_input M1 ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}
fst (append_heuristic_io ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}

goal (1 subgoal):
 1. \<And>T w u' uBest lBest. fst ((if c then append_heuristic_input M1 else append_heuristic_io) T w (uBest, lBest) u') \<in> {u', uBest}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fst (heuristic ?T1 ?w1 (?uBest1, ?lBest1) ?u'1) \<in> {?u'1, ?uBest1}

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
have p3: "observable M1 \<Longrightarrow>
                observable M2 \<Longrightarrow>
                minimal M1 \<Longrightarrow>
                minimal M2 \<Longrightarrow>
                inputs M2 = inputs M1 \<Longrightarrow>
                outputs M2 = outputs M1 \<Longrightarrow>
                is_state_cover_assignment M1 V \<Longrightarrow>
                convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<Longrightarrow>
                convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<Longrightarrow>
                L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) \<Longrightarrow>
                (preserves_divergence M1 M2 (V ` reachable_states M1)
                \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (?f M1 V cg_initial cg_insert cg_lookup)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
assume a0: "observable M1"
         and a1: "observable M2"
         and a2: "minimal M1"
         and a3: "minimal M2"
         and a4: "inputs M2 = inputs M1"
         and a5: "outputs M2 = outputs M1"
         and a6: "is_state_cover_assignment M1 V"
         and a7: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
         and a8: "convergence_graph_initial_invar M1 M2 cg_lookup cg_initial"
         and a9: "L M1 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> set (fst (?f M1 V cg_initial cg_insert cg_lookup))"
[PROOF STATE]
proof (state)
this:
observable M1
observable M2
minimal M1
minimal M2
FSM.inputs M2 = FSM.inputs M1
FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "\<And> rstates . (list.set (fst (foldl separate_state ([],T0,G0) rstates))) = V ` list.set rstates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rstates. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rstates. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
fix rstates
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rstates. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
show "(list.set (fst (foldl separate_state ([],T0,G0) rstates))) = V ` list.set rstates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
proof (induction rstates rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list.set (fst (foldl separate_state ([], T0, G0) [])) = V ` list.set []
 2. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. list.set (fst (foldl separate_state ([], T0, G0) [])) = V ` list.set []
 2. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) [])) = V ` list.set []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) [])) = V ` list.set []

goal (1 subgoal):
 1. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
case (snoc a rstates)
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates

goal (1 subgoal):
 1. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
have *:"(foldl separate_state ([], T0, G0) (rstates@[a])) = separate_state (foldl separate_state ([], T0, G0) rstates) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl separate_state ([], T0, G0) (rstates @ [a]) = separate_state (foldl separate_state ([], T0, G0) rstates) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) (rstates @ [a]) = separate_state (foldl separate_state ([], T0, G0) rstates) a

goal (1 subgoal):
 1. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
have **: "\<And> q XTG . fst (separate_state XTG q) = V q # fst XTG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q XTG. fst (separate_state XTG q) = V q # fst XTG
[PROOF STEP]
using \<open>\<And> q X T G . fst (separate_state (X,T,G) q) = V q # X\<close>
[PROOF STATE]
proof (prove)
using this:
fst (separate_state (?X, ?T, ?G) ?q) = V ?q # ?X

goal (1 subgoal):
 1. \<And>q XTG. fst (separate_state XTG q) = V q # fst XTG
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (separate_state ?XTG1 ?q1) = V ?q1 # fst ?XTG1

goal (1 subgoal):
 1. \<And>x xs. list.set (fst (foldl separate_state ([], T0, G0) xs)) = V ` list.set xs \<Longrightarrow> list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x]))) = V ` list.set (xs @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) (rstates @ [a]))) = V ` list.set (rstates @ [a])
[PROOF STEP]
unfolding * **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (V a # fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set (rstates @ [a])
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates

goal (1 subgoal):
 1. list.set (V a # fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set (rstates @ [a])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) (rstates @ [a]))) = V ` list.set (rstates @ [a])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) ?rstates1)) = V ` list.set ?rstates1

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list.set (fst (foldl separate_state ([], T0, G0) ?rstates1)) = V ` list.set ?rstates1
[PROOF STEP]
have "(list.set (fst (foldl separate_state ([],T0,G0) rstates))) = V ` reachable_states M1"
[PROOF STATE]
proof (prove)
using this:
list.set (fst (foldl separate_state ([], T0, G0) ?rstates1)) = V ` list.set ?rstates1

goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` reachable_states M1
[PROOF STEP]
by (metis reachable_states_as_list_set rstates_def)
[PROOF STATE]
proof (state)
this:
list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` reachable_states M1

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "\<And> q . q \<in> reachable_states M1 \<Longrightarrow> V q \<in> set T0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. q \<in> reachable_states M1 \<Longrightarrow> V q \<in> Prefix_Tree.set T0
[PROOF STEP]
using \<open>Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0\<close> \<open>V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T0' \<subseteq> Prefix_Tree.set T0
V ` reachable_states M1 \<subseteq> Prefix_Tree.set T0'

goal (1 subgoal):
 1. \<And>q. q \<in> reachable_states M1 \<Longrightarrow> V q \<in> Prefix_Tree.set T0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?q1 \<in> reachable_states M1 \<Longrightarrow> V ?q1 \<in> Prefix_Tree.set T0

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "list.set rstates \<subseteq> reachable_states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set rstates \<subseteq> reachable_states M1
[PROOF STEP]
unfolding rstates_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (reachable_states_as_list M1) \<subseteq> reachable_states M1
[PROOF STEP]
using reachable_states_as_list_set
[PROOF STATE]
proof (prove)
using this:
list.set (reachable_states_as_list ?M) = reachable_states ?M

goal (1 subgoal):
 1. list.set (reachable_states_as_list M1) \<subseteq> reachable_states M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set rstates \<subseteq> reachable_states M1

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set rstates \<subseteq> reachable_states M1

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
have "L M1 \<inter> set (fst (snd (foldl separate_state ([],T0,G0) rstates))) = L M2 \<inter> set (fst (snd (foldl separate_state ([],T0,G0) rstates)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
using "*" a9
[PROOF STATE]
proof (prove)
using this:
handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup = snd (foldl separate_state ([], T0, G0) rstates)
L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list.set rstates \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
have "preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([],T0,G0) rstates)))
                        \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([],T0,G0) rstates)))"
[PROOF STATE]
proof (prove)
using this:
list.set rstates \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
proof (induction rstates rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) []))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) [])))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list.set [] \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) []))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) [])))

goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) []))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) [])))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "L M1 \<inter> set T0 = L M2 \<inter> set T0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
[PROOF STEP]
using a9
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
[PROOF STEP]
using \<open>set T0 \<subseteq> set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<close>
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0

goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) []))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) [])))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
[PROOF STEP]
have "convergence_graph_lookup_invar M1 M2 cg_lookup G0"
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup G0
[PROOF STEP]
using a8 \<open>finite_tree T0\<close>
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
convergence_graph_initial_invar M1 M2 cg_lookup cg_initial
finite_tree T0

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup G0
[PROOF STEP]
unfolding G0_def convergence_graph_initial_invar_def
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T0 = L M2 \<inter> Prefix_Tree.set T0
\<forall>T. L M1 \<inter> Prefix_Tree.set T = L M2 \<inter> Prefix_Tree.set T \<longrightarrow> finite_tree T \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (cg_initial M1 T)
finite_tree T0

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (cg_initial M1 T0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G0

goal (2 subgoals):
 1. \<lbrakk>list.set [] \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) []))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) [])))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))
 2. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergence_graph_lookup_invar M1 M2 cg_lookup G0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
convergence_graph_lookup_invar M1 M2 cg_lookup G0

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) []))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) [])))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
case (snoc q rstates)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list.set rstates \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))
list.set (rstates @ [q]) \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
obtain X' T' G' where "foldl separate_state ([],T0,G0) rstates = (X',T',G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X' T' G'. foldl separate_state ([], T0, G0) rstates = (X', T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod_cases3
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c. ?y = (a, b, c) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>X' T' G'. foldl separate_state ([], T0, G0) rstates = (X', T', G') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) rstates = (X', T', G')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
foldl separate_state ([], T0, G0) rstates = (X', T', G')
[PROOF STEP]
have "T' = fst (snd (foldl separate_state ([],T0,G0) rstates))"
             and  "X' = fst (foldl separate_state ([],T0,G0) rstates)"
[PROOF STATE]
proof (prove)
using this:
foldl separate_state ([], T0, G0) rstates = (X', T', G')

goal (1 subgoal):
 1. T' = fst (snd (foldl separate_state ([], T0, G0) rstates)) &&& X' = fst (foldl separate_state ([], T0, G0) rstates)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T' = fst (snd (foldl separate_state ([], T0, G0) rstates))
X' = fst (foldl separate_state ([], T0, G0) rstates)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
define u where "u = V q"
[PROOF STATE]
proof (state)
this:
u = V q

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
define TG'' where "TG'' = spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun u X' k b heuristic"
[PROOF STATE]
proof (state)
this:
TG'' = spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun u X' k b heuristic

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
define X'' where "X'' = u#X'"
[PROOF STATE]
proof (state)
this:
X'' = u # X'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "foldl separate_state ([], T0, G0) (rstates@[q]) = separate_state (X',T',G') q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl separate_state ([], T0, G0) (rstates @ [q]) = separate_state (X', T', G') q
[PROOF STEP]
using \<open>foldl separate_state ([],T0,G0) rstates = (X',T',G')\<close>
[PROOF STATE]
proof (prove)
using this:
foldl separate_state ([], T0, G0) rstates = (X', T', G')

goal (1 subgoal):
 1. foldl separate_state ([], T0, G0) (rstates @ [q]) = separate_state (X', T', G') q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) (rstates @ [q]) = separate_state (X', T', G') q

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) (rstates @ [q]) = separate_state (X', T', G') q

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "separate_state (X',T',G') q = (X'',TG'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separate_state (X', T', G') q = (X'', TG'')
[PROOF STEP]
unfolding separate_state_def u_def TG''_def X''_def case_prod_conv Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V q # X', spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic) = (V q # X', spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
separate_state (X', T', G') q = (X'', TG'')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
foldl separate_state ([], T0, G0) (rstates @ [q]) = (X'', TG'')
[PROOF STEP]
have "foldl separate_state ([], T0, G0) (rstates@[q]) = (X'',TG'')"
[PROOF STATE]
proof (prove)
using this:
foldl separate_state ([], T0, G0) (rstates @ [q]) = (X'', TG'')

goal (1 subgoal):
 1. foldl separate_state ([], T0, G0) (rstates @ [q]) = (X'', TG'')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
foldl separate_state ([], T0, G0) (rstates @ [q]) = (X'', TG'')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "set T' \<subseteq> set (fst (snd (foldl separate_state ([],T0,G0) (rstates@[q]))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
[PROOF STEP]
using separate_state_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
[PROOF STEP]
unfolding \<open>foldl separate_state ([], T0, G0) (rstates@[q]) = separate_state (X',T',G') q\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (separate_state (X', T', G') q)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
[PROOF STEP]
have "L M1 \<inter> set T' = L M2 \<inter> set T'"
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set T' \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'
[PROOF STEP]
have "preserves_divergence M1 M2 (list.set X')"
        and       "convergence_graph_lookup_invar M1 M2 cg_lookup G'"
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set X') &&& convergence_graph_lookup_invar M1 M2 cg_lookup G'
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'
\<lbrakk>list.set rstates \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))
list.set (rstates @ [q]) \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set X') &&& convergence_graph_lookup_invar M1 M2 cg_lookup G'
[PROOF STEP]
unfolding \<open>foldl separate_state ([],T0,G0) rstates = (X',T',G')\<close>
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'
\<lbrakk>list.set rstates \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (X', T', G'))) = L M2 \<inter> Prefix_Tree.set (fst (snd (X', T', G')))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (X', T', G'))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (X', T', G')))
list.set (rstates @ [q]) \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set X') &&& convergence_graph_lookup_invar M1 M2 cg_lookup G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set X')
convergence_graph_lookup_invar M1 M2 cg_lookup G'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "set T0 \<subseteq> set T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
using separate_state_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
unfolding \<open>T' = fst (snd (foldl separate_state ([],T0,G0) rstates))\<close>
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T1 \<subseteq> Prefix_Tree.set (fst (snd (separate_state (?X1, ?T1, ?G1) ?q1)))

goal (1 subgoal):
 1. Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
by (induction rstates rule: rev_induct; auto; metis (mono_tags, opaque_lifting) Collect_mono_iff prod.collapse)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "V q \<in> set T0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V q \<in> Prefix_Tree.set T0
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
list.set (rstates @ [q]) \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal (1 subgoal):
 1. V q \<in> Prefix_Tree.set T0
[PROOF STEP]
using \<open>\<And>q. q \<in> reachable_states M1 \<Longrightarrow> V q \<in> Prefix_Tree.set T0\<close>
[PROOF STATE]
proof (prove)
using this:
list.set (rstates @ [q]) \<subseteq> reachable_states M1
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
?q \<in> reachable_states M1 \<Longrightarrow> V ?q \<in> Prefix_Tree.set T0

goal (1 subgoal):
 1. V q \<in> Prefix_Tree.set T0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V q \<in> Prefix_Tree.set T0

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V q \<in> Prefix_Tree.set T0
[PROOF STEP]
have "V q \<in> set T'"
[PROOF STATE]
proof (prove)
using this:
V q \<in> Prefix_Tree.set T0

goal (1 subgoal):
 1. V q \<in> Prefix_Tree.set T'
[PROOF STEP]
using \<open>set T0 \<subseteq> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
V q \<in> Prefix_Tree.set T0
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. V q \<in> Prefix_Tree.set T'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V q \<in> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V q \<in> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "V q \<in> L M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
have "q \<in> reachable_states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> reachable_states M1
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
list.set (rstates @ [q]) \<subseteq> reachable_states M1

goal (1 subgoal):
 1. q \<in> reachable_states M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> reachable_states M1

goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> reachable_states M1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable_states M1

goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
using is_state_cover_assignment_language[OF a6]
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable_states M1
?q \<in> reachable_states M1 \<Longrightarrow> V ?q \<in> L M1

goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V q \<in> L M1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
V q \<in> L M1

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V q \<in> Prefix_Tree.set T'
V q \<in> L M1
[PROOF STEP]
have "V q \<in> L M2"
[PROOF STATE]
proof (prove)
using this:
V q \<in> Prefix_Tree.set T'
V q \<in> L M1

goal (1 subgoal):
 1. V q \<in> L M2
[PROOF STEP]
using \<open>L M1 \<inter> set T' = L M2 \<inter> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
V q \<in> Prefix_Tree.set T'
V q \<in> L M1
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'

goal (1 subgoal):
 1. V q \<in> L M2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V q \<in> L M2

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "list.set X' = V ` list.set rstates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set X' = V ` list.set rstates
[PROOF STEP]
unfolding \<open>X' = fst (foldl separate_state ([],T0,G0) rstates)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
using \<open>\<And> rstates . (list.set (fst (foldl separate_state ([],T0,G0) rstates))) = V ` list.set rstates\<close>
[PROOF STATE]
proof (prove)
using this:
list.set (fst (foldl separate_state ([], T0, G0) ?rstates)) = V ` list.set ?rstates

goal (1 subgoal):
 1. list.set (fst (foldl separate_state ([], T0, G0) rstates)) = V ` list.set rstates
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list.set X' = V ` list.set rstates

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set X' = V ` list.set rstates

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "list.set rstates \<subseteq> reachable_states M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set rstates \<subseteq> reachable_states M1
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
list.set (rstates @ [q]) \<subseteq> reachable_states M1

goal (1 subgoal):
 1. list.set rstates \<subseteq> reachable_states M1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set rstates \<subseteq> reachable_states M1

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list.set X' = V ` list.set rstates
list.set rstates \<subseteq> reachable_states M1
[PROOF STEP]
have "list.set X' \<subseteq> set T'"
[PROOF STATE]
proof (prove)
using this:
list.set X' = V ` list.set rstates
list.set rstates \<subseteq> reachable_states M1

goal (1 subgoal):
 1. list.set X' \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
using \<open>set T0 \<subseteq> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
list.set X' = V ` list.set rstates
list.set rstates \<subseteq> reachable_states M1
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. list.set X' \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
using \<open>\<And>q. q \<in> reachable_states M1 \<Longrightarrow> V q \<in> Prefix_Tree.set T0\<close>
[PROOF STATE]
proof (prove)
using this:
list.set X' = V ` list.set rstates
list.set rstates \<subseteq> reachable_states M1
Prefix_Tree.set T0 \<subseteq> Prefix_Tree.set T'
?q \<in> reachable_states M1 \<Longrightarrow> V ?q \<in> Prefix_Tree.set T0

goal (1 subgoal):
 1. list.set X' \<subseteq> Prefix_Tree.set T'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list.set X' \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set X' \<subseteq> Prefix_Tree.set T'

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "list.set X' \<subseteq> L M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set X' \<subseteq> L M1
[PROOF STEP]
using \<open>list.set X' = V ` list.set rstates\<close> \<open>list.set rstates \<subseteq> reachable_states M1\<close> a6
[PROOF STATE]
proof (prove)
using this:
list.set X' = V ` list.set rstates
list.set rstates \<subseteq> reachable_states M1
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. list.set X' \<subseteq> L M1
[PROOF STEP]
by (metis dual_order.trans image_mono state_cover_assignment_language)
[PROOF STATE]
proof (state)
this:
list.set X' \<subseteq> L M1

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list.set X' \<subseteq> Prefix_Tree.set T'
list.set X' \<subseteq> L M1
[PROOF STEP]
have "list.set X' \<subseteq> L M2"
[PROOF STATE]
proof (prove)
using this:
list.set X' \<subseteq> Prefix_Tree.set T'
list.set X' \<subseteq> L M1

goal (1 subgoal):
 1. list.set X' \<subseteq> L M2
[PROOF STEP]
using \<open>L M1 \<inter> set T' = L M2 \<inter> set T'\<close>
[PROOF STATE]
proof (prove)
using this:
list.set X' \<subseteq> Prefix_Tree.set T'
list.set X' \<subseteq> L M1
L M1 \<inter> Prefix_Tree.set T' = L M2 \<inter> Prefix_Tree.set T'

goal (1 subgoal):
 1. list.set X' \<subseteq> L M2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list.set X' \<subseteq> L M2

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have *: "L M1 \<inter> set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic)) =
                 L M2 \<inter> set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic)) = L M2 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic))
[PROOF STEP]
using snoc.prems(2) TG''_def \<open>foldl separate_state ([], T0, G0) (rstates@[q]) = separate_state (X', T', G') q\<close> \<open>separate_state (X', T', G') q = (X'', TG'')\<close> u_def
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
TG'' = spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun u X' k b heuristic
foldl separate_state ([], T0, G0) (rstates @ [q]) = separate_state (X', T', G') q
separate_state (X', T', G') q = (X'', TG'')
u = V q

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic)) = L M2 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic)) = L M2 \<inter> Prefix_Tree.set (fst (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))
[PROOF STEP]
using spyh_distinguish_preserves_divergence[OF a0 a1 a2 a3 \<open>V q \<in> L M1\<close> \<open>V q \<in> L M2\<close> assms(1) \<open>convergence_graph_lookup_invar M1 M2 cg_lookup G'\<close> a7 \<open>list.set X' \<subseteq> L M1\<close> \<open>list.set X' \<subseteq> L M2\<close> * heuristic_prop \<open>preserves_divergence M1 M2 (list.set X')\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))
[PROOF STEP]
have "preserves_divergence M1 M2 (list.set X'')"
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (Set.insert (V q) (list.set X'))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set X'')
[PROOF STEP]
by (metis X''_def list.simps(15) u_def)
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set X'')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set X'')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
have "convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')
[PROOF STEP]
using spyh_distinguish_establishes_divergence(2)[OF a0 a1 a2 a3 \<open>V q \<in> L M1\<close> \<open>V q \<in> L M2\<close> assms(1) \<open>convergence_graph_lookup_invar M1 M2 cg_lookup G'\<close> a7 \<open>list.set X' \<subseteq> L M1\<close> \<open>list.set X' \<subseteq> L M2\<close> * heuristic_prop ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (spyh_distinguish M1 T' G' cg_lookup cg_insert dist_fun (V q) X' k b heuristic))

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')
[PROOF STEP]
unfolding u_def[symmetric] TG''_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q2 \<in> FSM.states M1; \<And>\<alpha> \<beta> q1 q2. \<lbrakk>q1 \<in> FSM.states M1; q2 \<in> FSM.states M1; q1 \<noteq> q2\<rbrakk> \<Longrightarrow> q1 \<noteq> q2\<rbrakk> \<Longrightarrow> convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')

goal (1 subgoal):
 1. convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>list.set xs \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) xs)))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) xs))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) xs))); list.set (xs @ [x]) \<subseteq> reachable_states M1; L M1 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x])))) = L M2 \<inter> Prefix_Tree.set (fst (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (xs @ [x])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (xs @ [x]))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preserves_divergence M1 M2 (list.set X'')
convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (list.set X'')
convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (rstates @ [q])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))
[PROOF STEP]
unfolding \<open>foldl separate_state ([], T0, G0) (rstates@[q]) = (X'',TG'')\<close> snd_conv fst_conv
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (list.set X'')
convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')

goal (1 subgoal):
 1. preserves_divergence M1 M2 (list.set X'') \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd TG'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) (rstates @ [q])))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) (rstates @ [q]))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (list.set (fst (foldl separate_state ([], T0, G0) rstates))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding \<open>(list.set (fst (foldl separate_state ([],T0,G0) rstates))) = V ` reachable_states M1\<close>
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))

goal (1 subgoal):
 1. preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (snd (foldl separate_state ([], T0, G0) rstates)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. \<And>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
show "?P V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
using p1 p2 p3
[PROOF STATE]
proof (prove)
using this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))
\<lbrakk>observable M1; observable M2; minimal M1; minimal M2; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.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 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))\<rbrakk> \<Longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup))

goal (1 subgoal):
 1. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup
[PROOF STEP]
unfolding separates_state_cover_def
[PROOF STATE]
proof (prove)
using this:
?V1 ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 ?V1 \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (?V1 ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 ?V1 cg_initial cg_insert cg_lookup)))

goal (1 subgoal):
 1. \<forall>V. V ` reachable_states M1 \<subseteq> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> finite_tree (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<and> (observable M1 \<longrightarrow> observable M2 \<longrightarrow> minimal M1 \<longrightarrow> minimal M2 \<longrightarrow> FSM.inputs M2 = FSM.inputs M1 \<longrightarrow> FSM.outputs M2 = FSM.outputs M1 \<longrightarrow> is_state_cover_assignment M1 V \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<longrightarrow> convergence_graph_initial_invar M1 M2 cg_lookup cg_initial \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) = L M2 \<inter> Prefix_Tree.set (fst (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)) \<longrightarrow> preserves_divergence M1 M2 (V ` reachable_states M1) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_state_cover_dynamic b c dist_fun M1 V cg_initial cg_insert cg_lookup)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
separates_state_cover (handle_state_cover_dynamic b c dist_fun) M1 M2 cg_initial cg_insert cg_lookup

goal:
No subgoals!
[PROOF STEP]
qed