[STATEMENT]
lemma spyh_distinguish_preserves_divergence :
  fixes M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
  assumes "observable M1"
  and     "observable M2"
  and     "minimal M1"
  and     "minimal M2"
  and     "u \<in> L M1" and "u \<in> L M2"
  and     "\<And> \<alpha> \<beta> q1 q2 . q1 \<in> states M1 \<Longrightarrow> q2 \<in> states M1 \<Longrightarrow> q1 \<noteq> q2 \<Longrightarrow> distinguishes M1 q1 q2 (get_distinguishing_trace q1 q2)"
  and     "convergence_graph_lookup_invar M1 M2 cg_lookup G"
  and     "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
  and     "list.set X \<subseteq> L M1"
  and     "list.set X \<subseteq> L M2"
  and     "L M1 \<inter> set (fst (spyh_distinguish M1 T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) = L M2 \<inter> set (fst (spyh_distinguish M1 T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))"
  and     "\<And> T w u' uBest lBest . fst (append_heuristic T w (uBest,lBest) u') \<in> {u',uBest}"
  and     "preserves_divergence M1 M2 (list.set X)"
shows "preserves_divergence M1 M2 (Set.insert u (list.set X))"
(is "?P1 X")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preserves_divergence M1 M2 (Set.insert u (list.set X))
[PROOF STEP]
using spyh_distinguish_establishes_divergence(1)[OF assms(1-13)]
[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> \<forall>v. v \<in> list.set X \<longrightarrow> \<not> converge M1 u v \<longrightarrow> \<not> converge M2 u v

goal (1 subgoal):
 1. preserves_divergence M1 M2 (Set.insert u (list.set X))
[PROOF STEP]
using assms(14)
[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> \<forall>v. v \<in> list.set X \<longrightarrow> \<not> converge M1 u v \<longrightarrow> \<not> converge M2 u v
preserves_divergence M1 M2 (list.set X)

goal (1 subgoal):
 1. preserves_divergence M1 M2 (Set.insert u (list.set X))
[PROOF STEP]
unfolding preserves_divergence.simps
[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> \<forall>v. v \<in> list.set X \<longrightarrow> \<not> converge M1 u v \<longrightarrow> \<not> converge M2 u v
\<forall>\<alpha>\<in>L M1 \<inter> list.set X. \<forall>\<beta>\<in>L M1 \<inter> list.set X. \<not> converge M1 \<alpha> \<beta> \<longrightarrow> \<not> converge M2 \<alpha> \<beta>

goal (1 subgoal):
 1. \<forall>\<alpha>\<in>L M1 \<inter> Set.insert u (list.set X). \<forall>\<beta>\<in>L M1 \<inter> Set.insert u (list.set X). \<not> converge M1 \<alpha> \<beta> \<longrightarrow> \<not> converge M2 \<alpha> \<beta>
[PROOF STEP]
by (metis IntD2 Int_iff assms(10) converge.elims(2) converge.elims(3) inf.absorb_iff2 insert_iff)


[STATEMENT]
lemma handle_io_pair_verifies_io_pair : "verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
have *:"\<And> (M::('a::linorder,'b::linorder,'c::linorder) fsm) V T (G::'d) cg_insert cg_lookup q x y . set T \<subseteq> set (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using distribute_extension_subset
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding handle_io_pair_def
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (distribute_extension M T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M else append_heuristic_io)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c ?M ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
have ***:"\<And> (M::('a::linorder,'b::linorder,'c::linorder) fsm) V T (G::'d) cg_insert cg_lookup q x y . finite_tree T \<longrightarrow> finite_tree (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. finite_tree T \<longrightarrow> finite_tree (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using distribute_extension_finite
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. finite_tree T \<longrightarrow> finite_tree (fst (handle_io_pair b c M V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding handle_io_pair_def
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. \<And>M V T G cg_insert cg_lookup q x y. finite_tree T \<longrightarrow> finite_tree (fst (distribute_extension M T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M else append_heuristic_io)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<longrightarrow> finite_tree (fst (handle_io_pair b c ?M ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
have **:"\<And> (M1::('a::linorder,'b::linorder,'c::linorder) fsm) V T (G::'d) cg_insert cg_lookup q x y.
        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>
        L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<Longrightarrow>
        q \<in> reachable_states M1 \<Longrightarrow>
        x \<in> inputs M1 \<Longrightarrow>
        y \<in> outputs M1 \<Longrightarrow>
        convergence_graph_lookup_invar M1 M2 cg_lookup G \<Longrightarrow>
        convergence_graph_insert_invar M1 M2 cg_lookup cg_insert \<Longrightarrow>
        L M1 \<inter> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<Longrightarrow>
        (\<exists> \<alpha> .
             converge M1 \<alpha> (V q) \<and>
             converge M2 \<alpha> (V q) \<and>
             \<alpha> \<in> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and>
             \<alpha>@[(x,y)] \<in> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)))
        \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
fix M1 :: "('a::linorder,'b::linorder,'c::linorder) fsm"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
fix G :: 'd
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
fix V T cg_insert cg_lookup q x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a01: "observable M1"
[PROOF STATE]
proof (state)
this:
observable M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a02: "observable M2"
[PROOF STATE]
proof (state)
this:
observable M2

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a03: "minimal M1"
[PROOF STATE]
proof (state)
this:
minimal M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a04: "minimal M2"
[PROOF STATE]
proof (state)
this:
minimal M2

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a05: "FSM.inputs M2 = FSM.inputs M1"
[PROOF STATE]
proof (state)
this:
FSM.inputs M2 = FSM.inputs M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a06: "FSM.outputs M2 = FSM.outputs M1"
[PROOF STATE]
proof (state)
this:
FSM.outputs M2 = FSM.outputs M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a07: "is_state_cover_assignment M1 V"
[PROOF STATE]
proof (state)
this:
is_state_cover_assignment M1 V

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a09: "L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1"
[PROOF STATE]
proof (state)
this:
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a10: "q \<in> reachable_states M1"
[PROOF STATE]
proof (state)
this:
q \<in> reachable_states M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a11: "x \<in> inputs M1"
[PROOF STATE]
proof (state)
this:
x \<in> FSM.inputs M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a12: "y \<in> outputs M1"
[PROOF STATE]
proof (state)
this:
y \<in> FSM.outputs M1

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a13: "convergence_graph_lookup_invar M1 M2 cg_lookup G"
[PROOF STATE]
proof (state)
this:
convergence_graph_lookup_invar M1 M2 cg_lookup G

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a14: "convergence_graph_insert_invar M1 M2 cg_lookup cg_insert"
[PROOF STATE]
proof (state)
this:
convergence_graph_insert_invar M1 M2 cg_lookup cg_insert

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
assume a15: "L M1 \<inter> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
let ?heuristic = "(if c then append_heuristic_input M1 else append_heuristic_io)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have d1: "V q \<in> L M1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V q \<in> L M1
[PROOF STEP]
using is_state_cover_assignment_language[OF a07 a10]
[PROOF STATE]
proof (prove)
using this:
V q \<in> L M1

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

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have d2: "V q \<in> L M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V q \<in> L M2
[PROOF STEP]
using is_state_cover_assignment_language[OF a07 a10]
[PROOF STATE]
proof (prove)
using this:
V q \<in> L M1

goal (1 subgoal):
 1. V q \<in> L M2
[PROOF STEP]
using a09 a10
[PROOF STATE]
proof (prove)
using this:
V q \<in> L M1
L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1
q \<in> reachable_states M1

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

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have d3: "L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x,y)] b ?heuristic)) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x,y)] b ?heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))
[PROOF STEP]
using a15
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))
[PROOF STEP]
unfolding handle_io_pair_def
[PROOF STATE]
proof (prove)
using this:
L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))

goal (1 subgoal):
 1. L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
L M1 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) = L M2 \<inter> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
have d4: "(\<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 ((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 ((if c then append_heuristic_input M1 else append_heuristic_io) ?T ?w (?uBest, ?lBest) ?u') \<in> {?u', ?uBest}

goal (1 subgoal):
 1. \<And>M1 V T G cg_insert cg_lookup q x y. \<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; L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1; q \<in> reachable_states M1; x \<in> FSM.inputs M1; y \<in> FSM.outputs M1; convergence_graph_lookup_invar M1 M2 cg_lookup G; convergence_graph_insert_invar M1 M2 cg_lookup cg_insert; L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
show "(\<exists> \<alpha> .
             converge M1 \<alpha> (V q) \<and>
             converge M2 \<alpha> (V q) \<and>
             \<alpha> \<in> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and>
             \<alpha>@[(x,y)] \<in> set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)))
        \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
using distribute_extension_adds_sequence[OF a01 a03 d1 d2 a13 a14 d3 d4]
[PROOF STATE]
proof (prove)
using this:
\<exists>u'. converge M1 (V q) u' \<and> u' @ [(x, y)] \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) \<and> converge M2 (V q) u'
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))

goal (1 subgoal):
 1. (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))
[PROOF STEP]
unfolding handle_io_pair_def
[PROOF STATE]
proof (prove)
using this:
\<exists>u'. converge M1 (V q) u' \<and> u' @ [(x, y)] \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) \<and> converge M2 (V q) u'
convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))

goal (1 subgoal):
 1. (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io))) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (distribute_extension M1 T G cg_lookup cg_insert (V q) [(x, y)] b (if c then append_heuristic_input M1 else append_heuristic_io)))
[PROOF STEP]
by (metis converge_sym set_prefix)
[PROOF STATE]
proof (state)
this:
(\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_lookup (snd (handle_io_pair b c M1 V T G cg_insert cg_lookup q x y))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>observable ?M1.0; observable M2; minimal ?M1.0; minimal M2; FSM.inputs M2 = FSM.inputs ?M1.0; FSM.outputs M2 = FSM.outputs ?M1.0; is_state_cover_assignment ?M1.0 ?V; L ?M1.0 \<inter> ?V ` reachable_states ?M1.0 = L M2 \<inter> ?V ` reachable_states ?M1.0; ?q \<in> reachable_states ?M1.0; ?x \<in> FSM.inputs ?M1.0; ?y \<in> FSM.outputs ?M1.0; convergence_graph_lookup_invar ?M1.0 M2 ?cg_lookup ?G; convergence_graph_insert_invar ?M1.0 M2 ?cg_lookup ?cg_insert; L ?M1.0 \<inter> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge ?M1.0 \<alpha> (?V ?q) \<and> converge M2 \<alpha> (?V ?q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y)) \<and> \<alpha> @ [(?x, ?y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))) \<and> convergence_graph_lookup_invar ?M1.0 M2 ?cg_lookup (snd (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
unfolding verifies_io_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y))) \<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> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_insert G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_insert cg_lookup \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_insert (snd (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)))
[PROOF STEP]
using * *** **
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c ?M ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))
finite_tree ?T \<longrightarrow> finite_tree (fst (handle_io_pair b c ?M ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))
\<lbrakk>observable ?M1.0; observable M2; minimal ?M1.0; minimal M2; FSM.inputs M2 = FSM.inputs ?M1.0; FSM.outputs M2 = FSM.outputs ?M1.0; is_state_cover_assignment ?M1.0 ?V; L ?M1.0 \<inter> ?V ` reachable_states ?M1.0 = L M2 \<inter> ?V ` reachable_states ?M1.0; ?q \<in> reachable_states ?M1.0; ?x \<in> FSM.inputs ?M1.0; ?y \<in> FSM.outputs ?M1.0; convergence_graph_lookup_invar ?M1.0 M2 ?cg_lookup ?G; convergence_graph_insert_invar ?M1.0 M2 ?cg_lookup ?cg_insert; L ?M1.0 \<inter> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))\<rbrakk> \<Longrightarrow> (\<exists>\<alpha>. converge ?M1.0 \<alpha> (?V ?q) \<and> converge M2 \<alpha> (?V ?q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y)) \<and> \<alpha> @ [(?x, ?y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))) \<and> convergence_graph_lookup_invar ?M1.0 M2 ?cg_lookup (snd (handle_io_pair b c ?M1.0 ?V ?T ?G ?cg_insert ?cg_lookup ?q ?x ?y))

goal (1 subgoal):
 1. \<forall>V T G q x y. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<and> (finite_tree T \<longrightarrow> finite_tree (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y))) \<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> L M1 \<inter> V ` reachable_states M1 = L M2 \<inter> V ` reachable_states M1 \<longrightarrow> q \<in> reachable_states M1 \<longrightarrow> x \<in> FSM.inputs M1 \<longrightarrow> y \<in> FSM.outputs M1 \<longrightarrow> convergence_graph_lookup_invar M1 M2 cg_insert G \<longrightarrow> convergence_graph_insert_invar M1 M2 cg_insert cg_lookup \<longrightarrow> L M1 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) = L M2 \<inter> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<longrightarrow> (\<exists>\<alpha>. converge M1 \<alpha> (V q) \<and> converge M2 \<alpha> (V q) \<and> \<alpha> \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)) \<and> \<alpha> @ [(x, y)] \<in> Prefix_Tree.set (fst (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y))) \<and> convergence_graph_lookup_invar M1 M2 cg_insert (snd (handle_io_pair b c M1 V T G cg_lookup cg_insert q x y)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
verifies_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma handle_io_pair_handles_io_pair : "handles_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handles_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
using verifies_io_pair_handled[OF handle_io_pair_verifies_io_pair]
[PROOF STATE]
proof (prove)
using this:
handles_io_pair (handle_io_pair ?b1 ?c1) ?M1.0 ?M2.0 ?cg_insert ?cg_lookup

goal (1 subgoal):
 1. handles_io_pair (handle_io_pair b c) M1 M2 cg_lookup cg_insert
[PROOF STEP]
.