[STATEMENT]
lemma get_initial_test_suite_H_2_set_and_finite :
shows  "{(V q)@io@[(x,y)] | q io x y . q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M} \<subseteq> set (get_initial_test_suite_H_2 c V M m)" (is ?P1)
and "finite_tree (get_initial_test_suite_H_2 c V M m)" (is ?P2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) &&& finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m)
 2. finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
have "?P1 \<and> ?P2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
proof (cases c)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
 2. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c

goal (2 subgoals):
 1. c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
 2. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c
[PROOF STEP]
have "get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m"
[PROOF STATE]
proof (prove)
using this:
c

goal (1 subgoal):
 1. get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m
[PROOF STEP]
unfolding get_initial_test_suite_H_2_def
[PROOF STATE]
proof (prove)
using this:
c

goal (1 subgoal):
 1. (if c then get_initial_test_suite_H V M m else let TS = get_initial_test_suite_H V M m; xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS); ys = outputs_as_list M in foldl (\<lambda>t xs. combine t (complete_inputs_to_tree_initial M xs)) TS xss) = get_initial_test_suite_H V M m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m

goal (2 subgoals):
 1. c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
 2. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
using get_initial_test_suite_H_set_and_finite
[PROOF STATE]
proof (prove)
using this:
get_initial_test_suite_H_2 c V M m = get_initial_test_suite_H V M m
{?V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states ?M \<and> io \<in> LS ?M q \<and> length io \<le> ?m - size_r ?M \<and> x \<in> FSM.inputs ?M \<and> y \<in> FSM.outputs ?M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H ?V ?M ?m)
finite_tree (get_initial_test_suite_H ?V ?M ?m)

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> c

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
define TS where "TS = get_initial_test_suite_H V M m"
[PROOF STATE]
proof (state)
this:
TS = get_initial_test_suite_H V M m

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TS = get_initial_test_suite_H V M m

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
define xss where "xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)"
[PROOF STATE]
proof (state)
this:
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
define ys where "ys  = outputs_as_list M"
[PROOF STATE]
proof (state)
this:
ys = outputs_as_list M

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
TS = get_initial_test_suite_H V M m
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)
ys = outputs_as_list M
[PROOF STEP]
have "get_initial_test_suite_H_2 c V M m = foldl (\<lambda> t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss"
[PROOF STATE]
proof (prove)
using this:
TS = get_initial_test_suite_H V M m
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)
ys = outputs_as_list M

goal (1 subgoal):
 1. get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
[PROOF STEP]
unfolding get_initial_test_suite_H_2_def Let_def
[PROOF STATE]
proof (prove)
using this:
TS = get_initial_test_suite_H V M m
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)
ys = outputs_as_list M

goal (1 subgoal):
 1. (if c then get_initial_test_suite_H V M m else foldl (\<lambda>t xs. combine t (complete_inputs_to_tree_initial M xs)) (get_initial_test_suite_H V M m) (map (map fst) (sorted_list_of_maximal_sequences_in_tree (get_initial_test_suite_H V M m)))) = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
TS = get_initial_test_suite_H V M m
xss = map (map fst) (sorted_list_of_maximal_sequences_in_tree TS)
ys = outputs_as_list M
\<not> c

goal (1 subgoal):
 1. (if c then get_initial_test_suite_H V M m else foldl (\<lambda>t xs. combine t (complete_inputs_to_tree_initial M xs)) (get_initial_test_suite_H V M m) (map (map fst) (sorted_list_of_maximal_sequences_in_tree (get_initial_test_suite_H V M m)))) = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
have "set TS \<subseteq> set (foldl (\<lambda> t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[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 TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[PROOF STEP]
by (induction xss rule: rev_induct; auto)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
have "finite_tree (foldl (\<lambda> t xs . combine t (complete_inputs_to_tree M (initial M) ys xs)) TS xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[PROOF STEP]
using complete_inputs_to_tree_finite_tree get_initial_test_suite_H_set_and_finite(2)[of V M m] combine_finite_tree
[PROOF STATE]
proof (prove)
using this:
finite_tree (complete_inputs_to_tree ?M ?q ?ys ?xs)
finite_tree (get_initial_test_suite_H V M m)
\<lbrakk>finite_tree ?t1.0; finite_tree ?t2.0\<rbrakk> \<Longrightarrow> finite_tree (combine ?t1.0 ?t2.0)

goal (1 subgoal):
 1. finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[PROOF STEP]
unfolding TS_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
finite_tree (complete_inputs_to_tree ?M ?q ?ys ?xs)
finite_tree TS
\<lbrakk>finite_tree ?t1.0; finite_tree ?t2.0\<rbrakk> \<Longrightarrow> finite_tree (combine ?t1.0 ?t2.0)

goal (1 subgoal):
 1. finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[PROOF STEP]
by (induction xss rule: rev_induct; auto; blast)
[PROOF STATE]
proof (state)
this:
finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)

goal (1 subgoal):
 1. \<not> c \<Longrightarrow> {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
using get_initial_test_suite_H_set_and_finite(1)[of V M m]
[PROOF STATE]
proof (prove)
using this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H V M m)

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
unfolding TS_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
get_initial_test_suite_H_2 c V M m = foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss
Prefix_Tree.set TS \<subseteq> Prefix_Tree.set (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
finite_tree (foldl (\<lambda>t xs. combine t (complete_inputs_to_tree M (FSM.initial M) ys xs)) TS xss)
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set TS

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)

goal (2 subgoals):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m)
 2. finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
show ?P1 and ?P2
[PROOF STATE]
proof (prove)
using this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) \<and> finite_tree (get_initial_test_suite_H_2 c V M m)

goal (1 subgoal):
 1. {V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m) &&& finite_tree (get_initial_test_suite_H_2 c V M m)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
{V q @ io @ [(x, y)] |q io x y. q \<in> reachable_states M \<and> io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M} \<subseteq> Prefix_Tree.set (get_initial_test_suite_H_2 c V M m)
finite_tree (get_initial_test_suite_H_2 c V M m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_pairs_H_set :
  assumes "observable M"
  and     "is_state_cover_assignment M V"
shows
  "\<And> \<alpha> \<beta> . (\<alpha>,\<beta>) \<in> (V ` reachable_states M) \<times> (V ` reachable_states M)
                      \<union> (V ` reachable_states M) \<times> { (V q) @ \<tau> | q \<tau> . q \<in> reachable_states M \<and> \<tau> \<in> {io@[(x,y)] | io x y . io \<in> LS M q \<and> length io \<le> m-size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M}}
                      \<union> (\<Union> q \<in> reachable_states M . \<Union> \<tau> \<in> {io@[(x,y)] | io x y . io \<in> LS M q \<and> length io \<le> m-size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M} . { (V q) @ \<tau>' | \<tau>' . \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {(V q)@\<tau>}) \<Longrightarrow>
                    \<alpha> \<in> L M \<Longrightarrow> \<beta> \<in> L M \<Longrightarrow> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<Longrightarrow>
                    ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) \<in> list.set (get_pairs_H V M m)"
and "\<And> \<alpha> q' \<beta> q'' . ((\<alpha>,q'),(\<beta>,q'')) \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)) &&& (\<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define rstates where "rstates       = reachable_states_as_list M"
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rstates = reachable_states_as_list M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define n where "n             = size_r M"
[PROOF STATE]
proof (state)
this:
n = size_r M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = size_r M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define iM where "iM            = inputs_as_list M"
[PROOF STATE]
proof (state)
this:
iM = inputs_as_list M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
iM = inputs_as_list M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define hMap' where "hMap'          = mapping_of (map (\<lambda>(q,x) . ((q,x), map (\<lambda>(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) (List.product (states_as_list M) iM))"
[PROOF STATE]
proof (state)
this:
hMap' = mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hMap' = mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define hM' where "hM'            = (\<lambda> q x . case Mapping.lookup hMap' (q,x) of Some ts \<Rightarrow> ts | None \<Rightarrow> [])"
[PROOF STATE]
proof (state)
this:
hM' = (\<lambda>q x. case Mapping.lookup hMap' (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
hMap' = mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))
hM' = (\<lambda>q x. case Mapping.lookup hMap' (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)
[PROOF STEP]
have "get_pairs_H V M m = pairs_to_distinguish M V (\<lambda>q . paths_up_to_length_with_targets q hM' iM ((m-n)+1)) rstates"
[PROOF STATE]
proof (prove)
using this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
hMap' = mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))
hM' = (\<lambda>q x. case Mapping.lookup hMap' (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)

goal (1 subgoal):
 1. get_pairs_H V M m = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM' iM (m - n + 1)) rstates
[PROOF STEP]
unfolding get_pairs_H_def Let_def
[PROOF STATE]
proof (prove)
using this:
rstates = reachable_states_as_list M
n = size_r M
iM = inputs_as_list M
hMap' = mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))
hM' = (\<lambda>q x. case Mapping.lookup hMap' (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)

goal (1 subgoal):
 1. pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q (\<lambda>q x. case Mapping.lookup (mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) (inputs_as_list M)))) (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts) (inputs_as_list M) (m - size_r M + 1)) (reachable_states_as_list M) = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM' iM (m - n + 1)) rstates
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
get_pairs_H V M m = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM' iM (m - n + 1)) rstates

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define hMap where "hMap          = map_of (map (\<lambda>(q,x) . ((q,x), map (\<lambda>(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) (List.product (states_as_list M) iM))"
[PROOF STATE]
proof (state)
this:
hMap = map_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define hM where "hM            = (\<lambda> q x . case hMap (q,x) of Some ts \<Rightarrow> ts | None \<Rightarrow> [])"
[PROOF STATE]
proof (state)
this:
hM = (\<lambda>q x. case hMap (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
have "distinct (List.product (states_as_list M) iM)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (List.product (states_as_list M) iM)
[PROOF STEP]
using states_as_list_distinct inputs_as_list_distinct distinct_product
[PROOF STATE]
proof (prove)
using this:
distinct (states_as_list ?M)
distinct (inputs_as_list ?M)
\<lbrakk>distinct ?xs; distinct ?ys\<rbrakk> \<Longrightarrow> distinct (List.product ?xs ?ys)

goal (1 subgoal):
 1. distinct (List.product (states_as_list M) iM)
[PROOF STEP]
unfolding iM_def
[PROOF STATE]
proof (prove)
using this:
distinct (states_as_list ?M)
distinct (inputs_as_list ?M)
\<lbrakk>distinct ?xs; distinct ?ys\<rbrakk> \<Longrightarrow> distinct (List.product ?xs ?ys)

goal (1 subgoal):
 1. distinct (List.product (states_as_list M) (inputs_as_list M))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (List.product (states_as_list M) iM)

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (List.product (states_as_list M) iM)
[PROOF STEP]
have "Mapping.lookup hMap' = hMap"
[PROOF STATE]
proof (prove)
using this:
distinct (List.product (states_as_list M) iM)

goal (1 subgoal):
 1. Mapping.lookup hMap' = hMap
[PROOF STEP]
using mapping_of_map_of
[PROOF STATE]
proof (prove)
using this:
distinct (List.product (states_as_list M) iM)
distinct (map fst ?kvs) \<Longrightarrow> Mapping.lookup (mapping_of ?kvs) = map_of ?kvs

goal (1 subgoal):
 1. Mapping.lookup hMap' = hMap
[PROOF STEP]
unfolding hMap_def hMap'_def
[PROOF STATE]
proof (prove)
using this:
distinct (List.product (states_as_list M) iM)
distinct (map fst ?kvs) \<Longrightarrow> Mapping.lookup (mapping_of ?kvs) = map_of ?kvs

goal (1 subgoal):
 1. Mapping.lookup (mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))) = map_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))
[PROOF STEP]
using map_pair_fst_helper[of "\<lambda> q x . map (\<lambda>(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x)))"]
[PROOF STATE]
proof (prove)
using this:
distinct (List.product (states_as_list M) iM)
distinct (map fst ?kvs) \<Longrightarrow> Mapping.lookup (mapping_of ?kvs) = map_of ?kvs
map fst (map (\<lambda>(x1, x2). ((x1, x2), map (\<lambda>(y, q'). (x1, x2, y, q')) (sorted_list_of_set (FSM.h M (x1, x2))))) ?xs) = ?xs

goal (1 subgoal):
 1. Mapping.lookup (mapping_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))) = map_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM))
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
Mapping.lookup hMap' = hMap

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Mapping.lookup hMap' = hMap
[PROOF STEP]
have "hM' = hM"
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup hMap' = hMap

goal (1 subgoal):
 1. hM' = hM
[PROOF STEP]
unfolding hM'_def hM_def
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup hMap' = hMap

goal (1 subgoal):
 1. (\<lambda>q x. case Mapping.lookup hMap' (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts) = (\<lambda>q x. case hMap (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
hM' = hM

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hM' = hM

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define pairs where "pairs         = pairs_to_distinguish M V (\<lambda>q . paths_up_to_length_with_targets q hM iM ((m-n)+1)) rstates"
[PROOF STATE]
proof (state)
this:
pairs = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM iM (m - n + 1)) rstates

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hM' = hM
pairs = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM iM (m - n + 1)) rstates
[PROOF STEP]
have res: "get_pairs_H V M m = pairs"
[PROOF STATE]
proof (prove)
using this:
hM' = hM
pairs = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM iM (m - n + 1)) rstates

goal (1 subgoal):
 1. get_pairs_H V M m = pairs
[PROOF STEP]
unfolding \<open>get_pairs_H V M m = pairs_to_distinguish M V (\<lambda>q . paths_up_to_length_with_targets q hM' iM ((m-n)+1)) rstates\<close>
[PROOF STATE]
proof (prove)
using this:
hM' = hM
pairs = pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM iM (m - n + 1)) rstates

goal (1 subgoal):
 1. pairs_to_distinguish M V (\<lambda>q. paths_up_to_length_with_targets q hM' iM (m - n + 1)) rstates = pairs
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
get_pairs_H V M m = pairs

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
have *:"list.set rstates = reachable_states M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set rstates = reachable_states M
[PROOF STEP]
unfolding rstates_def reachable_states_as_list_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_states M = reachable_states M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list.set rstates = reachable_states M

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
define \<X>' where \<X>': "\<X>' = (\<lambda>q . paths_up_to_length_with_targets q hM iM ((m-n)+1))"
[PROOF STATE]
proof (state)
this:
\<X>' = (\<lambda>q. paths_up_to_length_with_targets q hM iM (m - n + 1))

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
have **: "\<And> q p q' . q \<in> reachable_states M \<Longrightarrow> (p,q') \<in> list.set (\<X>' q) \<longleftrightarrow> path M q p \<and> target q p = q' \<and> length p \<le> m-n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
fix q p q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
assume "q \<in> reachable_states M"
[PROOF STATE]
proof (state)
this:
q \<in> reachable_states M

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
define qxPairs where qxPairs: "qxPairs = (List.product (states_as_list M) iM)"
[PROOF STATE]
proof (state)
this:
qxPairs = List.product (states_as_list M) iM

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qxPairs = List.product (states_as_list M) iM

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
define mapList where mapList: "mapList = (map (\<lambda>(q,x) . ((q,x), map (\<lambda>(y,q') . (q,x,y,q')) (sorted_list_of_set (h M (q,x))))) qxPairs)"
[PROOF STATE]
proof (state)
this:
mapList = map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qxPairs = List.product (states_as_list M) iM
mapList = map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs
[PROOF STEP]
have hMap': "hMap = map_of mapList"
[PROOF STATE]
proof (prove)
using this:
qxPairs = List.product (states_as_list M) iM
mapList = map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs

goal (1 subgoal):
 1. hMap = map_of mapList
[PROOF STEP]
unfolding hMap_def
[PROOF STATE]
proof (prove)
using this:
qxPairs = List.product (states_as_list M) iM
mapList = map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs

goal (1 subgoal):
 1. map_of (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) (List.product (states_as_list M) iM)) = map_of mapList
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hMap = map_of mapList

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
have "distinct (states_as_list M)" and "distinct iM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (states_as_list M) &&& distinct iM
[PROOF STEP]
unfolding iM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (states_as_list M) &&& distinct (inputs_as_list M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (states_as_list M)
distinct iM

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (states_as_list M)
distinct iM
[PROOF STEP]
have "distinct qxPairs"
[PROOF STATE]
proof (prove)
using this:
distinct (states_as_list M)
distinct iM

goal (1 subgoal):
 1. distinct qxPairs
[PROOF STEP]
unfolding qxPairs
[PROOF STATE]
proof (prove)
using this:
distinct (states_as_list M)
distinct iM

goal (1 subgoal):
 1. distinct (List.product (states_as_list M) iM)
[PROOF STEP]
by (simp add: distinct_product)
[PROOF STATE]
proof (state)
this:
distinct qxPairs

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct qxPairs

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
have "(map fst mapList) = qxPairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst mapList = qxPairs
[PROOF STEP]
unfolding mapList
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs) = qxPairs
[PROOF STEP]
by (induction qxPairs; auto)
[PROOF STATE]
proof (state)
this:
map fst mapList = qxPairs

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct qxPairs
map fst mapList = qxPairs
[PROOF STEP]
have "distinct (map fst mapList)"
[PROOF STATE]
proof (prove)
using this:
distinct qxPairs
map fst mapList = qxPairs

goal (1 subgoal):
 1. distinct (map fst mapList)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst mapList)

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
have "\<And> q x . hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q x. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q x. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
fix q x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q x. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
show "hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
proof (cases "q \<in> states M \<and> x \<in> inputs M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)
[PROOF STEP]
have "(h M (q, x)) = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)

goal (1 subgoal):
 1. FSM.h M (q, x) = {}
[PROOF STEP]
unfolding h_simps
[PROOF STATE]
proof (prove)
using this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)

goal (1 subgoal):
 1. {(y, q'). (q, x, y, q') \<in> FSM.transitions M} = {}
[PROOF STEP]
using fsm_transition_source fsm_transition_input
[PROOF STATE]
proof (prove)
using this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)
?t \<in> FSM.transitions ?M \<Longrightarrow> t_source ?t \<in> FSM.states ?M
?t \<in> FSM.transitions ?M \<Longrightarrow> t_input ?t \<in> FSM.inputs ?M

goal (1 subgoal):
 1. {(y, q'). (q, x, y, q') \<in> FSM.transitions M} = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
FSM.h M (q, x) = {}

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.h M (q, x) = {}
[PROOF STEP]
have "map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))) = []"
[PROOF STATE]
proof (prove)
using this:
FSM.h M (q, x) = {}

goal (1 subgoal):
 1. map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))) = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))) = []

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
have "q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)

goal (1 subgoal):
 1. q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM
[PROOF STEP]
unfolding states_as_list_set iM_def inputs_as_list_set
[PROOF STATE]
proof (prove)
using this:
\<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M)

goal (1 subgoal):
 1. q \<notin> FSM.states M \<or> x \<notin> FSM.inputs M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM
[PROOF STEP]
have "(q,x) \<notin> list.set qxPairs"
[PROOF STATE]
proof (prove)
using this:
q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM

goal (1 subgoal):
 1. (q, x) \<notin> list.set qxPairs
[PROOF STEP]
unfolding qxPairs
[PROOF STATE]
proof (prove)
using this:
q \<notin> list.set (states_as_list M) \<or> x \<notin> list.set iM

goal (1 subgoal):
 1. (q, x) \<notin> list.set (List.product (states_as_list M) iM)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q, x) \<notin> list.set qxPairs

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, x) \<notin> list.set qxPairs
[PROOF STEP]
have "\<nexists> y . ((q,x),y) \<in> list.set mapList"
[PROOF STATE]
proof (prove)
using this:
(q, x) \<notin> list.set qxPairs

goal (1 subgoal):
 1. \<nexists>y. ((q, x), y) \<in> list.set mapList
[PROOF STEP]
unfolding mapList
[PROOF STATE]
proof (prove)
using this:
(q, x) \<notin> list.set qxPairs

goal (1 subgoal):
 1. \<nexists>y. ((q, x), y) \<in> list.set (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>y. ((q, x), y) \<in> list.set mapList

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>y. ((q, x), y) \<in> list.set mapList
[PROOF STEP]
have "hMap (q,x) = None"
[PROOF STATE]
proof (prove)
using this:
\<nexists>y. ((q, x), y) \<in> list.set mapList

goal (1 subgoal):
 1. hMap (q, x) = None
[PROOF STEP]
unfolding hMap'
[PROOF STATE]
proof (prove)
using this:
\<nexists>y. ((q, x), y) \<in> list.set mapList

goal (1 subgoal):
 1. map_of mapList (q, x) = None
[PROOF STEP]
using map_of_eq_Some_iff[OF \<open>distinct (map fst mapList)\<close>]
[PROOF STATE]
proof (prove)
using this:
\<nexists>y. ((q, x), y) \<in> list.set mapList
(map_of mapList ?x = Some ?y) = ((?x, ?y) \<in> list.set mapList)

goal (1 subgoal):
 1. map_of mapList (q, x) = None
[PROOF STEP]
by (meson option.exhaust)
[PROOF STATE]
proof (state)
this:
hMap (q, x) = None

goal (2 subgoals):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
 2. \<not> (q \<in> FSM.states M \<and> x \<in> FSM.inputs M) \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hMap (q, x) = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hMap (q, x) = None

goal (1 subgoal):
 1. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
using \<open>map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))) = []\<close>
[PROOF STATE]
proof (prove)
using this:
hMap (q, x) = None
map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))) = []

goal (1 subgoal):
 1. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
unfolding hM_def
[PROOF STATE]
proof (prove)
using this:
hMap (q, x) = None
map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))) = []

goal (1 subgoal):
 1. (case hMap (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts) = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M \<and> x \<in> FSM.inputs M

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> FSM.states M \<and> x \<in> FSM.inputs M
[PROOF STEP]
have "q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM"
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M \<and> x \<in> FSM.inputs M

goal (1 subgoal):
 1. q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM
[PROOF STEP]
unfolding states_as_list_set iM_def inputs_as_list_set
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M \<and> x \<in> FSM.inputs M

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM
[PROOF STEP]
have "(q,x) \<in> list.set qxPairs"
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM

goal (1 subgoal):
 1. (q, x) \<in> list.set qxPairs
[PROOF STEP]
unfolding qxPairs
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set (states_as_list M) \<and> x \<in> list.set iM

goal (1 subgoal):
 1. (q, x) \<in> list.set (List.product (states_as_list M) iM)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q, x) \<in> list.set qxPairs

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, x) \<in> list.set qxPairs
[PROOF STEP]
have "((q,x),map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x)))) \<in> list.set mapList"
[PROOF STATE]
proof (prove)
using this:
(q, x) \<in> list.set qxPairs

goal (1 subgoal):
 1. ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList
[PROOF STEP]
unfolding mapList
[PROOF STATE]
proof (prove)
using this:
(q, x) \<in> list.set qxPairs

goal (1 subgoal):
 1. ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set (map (\<lambda>(q, x). ((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))) qxPairs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList
[PROOF STEP]
have "hMap (q,x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))"
[PROOF STATE]
proof (prove)
using this:
((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList

goal (1 subgoal):
 1. hMap (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))
[PROOF STEP]
unfolding hMap'
[PROOF STATE]
proof (prove)
using this:
((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList

goal (1 subgoal):
 1. map_of mapList (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))
[PROOF STEP]
using map_of_eq_Some_iff[OF \<open>distinct (map fst mapList)\<close>]
[PROOF STATE]
proof (prove)
using this:
((q, x), map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))) \<in> list.set mapList
(map_of mapList ?x = Some ?y) = ((?x, ?y) \<in> list.set mapList)

goal (1 subgoal):
 1. map_of mapList (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))
[PROOF STEP]
by (meson option.exhaust)
[PROOF STATE]
proof (state)
this:
hMap (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))

goal (1 subgoal):
 1. q \<in> FSM.states M \<and> x \<in> FSM.inputs M \<Longrightarrow> hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hMap (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hMap (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))

goal (1 subgoal):
 1. hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
unfolding hM_def
[PROOF STATE]
proof (prove)
using this:
hMap (q, x) = Some (map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))

goal (1 subgoal):
 1. (case hMap (q, x) of None \<Rightarrow> [] | Some ts \<Rightarrow> ts) = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hM q x = map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hM ?q ?x = map (\<lambda>(y, q'). (?q, ?x, y, q')) (sorted_list_of_set (FSM.h M (?q, ?x)))

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hM ?q ?x = map (\<lambda>(y, q'). (?q, ?x, y, q')) (sorted_list_of_set (FSM.h M (?q, ?x)))
[PROOF STEP]
have hM_alt_def: "hM = (\<lambda> q x . map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (h M (q, x))))"
[PROOF STATE]
proof (prove)
using this:
hM ?q ?x = map (\<lambda>(y, q'). (?q, ?x, y, q')) (sorted_list_of_set (FSM.h M (?q, ?x)))

goal (1 subgoal):
 1. hM = (\<lambda>q x. map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hM = (\<lambda>q x. map (\<lambda>(y, q'). (q, x, y, q')) (sorted_list_of_set (FSM.h M (q, x))))

goal (1 subgoal):
 1. \<And>q p q'. q \<in> reachable_states M \<Longrightarrow> ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
show "(p,q') \<in> list.set (\<X>' q) \<longleftrightarrow> path M q p \<and> target q p = q' \<and> length p \<le> m-n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
unfolding \<X>' hM_alt_def iM_def
                  paths_up_to_length_with_targets_set[OF reachable_state_is_state[OF \<open>q \<in> reachable_states M\<close>]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((p, q') \<in> {(p, target q p) |p. path M q p \<and> length p \<le> m - n + 1}) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((p, q') \<in> list.set (\<X>' q)) = (path M q p \<and> target q p = q' \<and> length p \<le> m - n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q \<in> reachable_states M \<Longrightarrow> ((?p, ?q') \<in> list.set (\<X>' ?q)) = (path M ?q ?p \<and> target ?q ?p = ?q' \<and> length ?p \<le> m - n + 1)

goal (2 subgoals):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
 2. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
show "\<And> \<alpha> \<beta> . (\<alpha>,\<beta>) \<in> (V ` reachable_states M) \<times> (V ` reachable_states M)
                      \<union> (V ` reachable_states M) \<times> { (V q) @ \<tau> | q \<tau> . q \<in> reachable_states M \<and> \<tau> \<in> {io@[(x,y)] | io x y . io \<in> LS M q \<and> length io \<le> m-size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M}}
                      \<union> (\<Union> q \<in> reachable_states M . \<Union> \<tau> \<in> {io@[(x,y)] | io x y . io \<in> LS M q \<and> length io \<le> m-size_r M \<and> x \<in> inputs M \<and> y \<in> outputs M} . { (V q) @ \<tau>' | \<tau>' . \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {(V q)@\<tau>}) \<Longrightarrow>
                    \<alpha> \<in> L M \<Longrightarrow> \<beta> \<in> L M \<Longrightarrow> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<Longrightarrow>
                    ((\<alpha>,after_initial M \<alpha>),(\<beta>,after_initial M \<beta>)) \<in> list.set (get_pairs_H V M m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
[PROOF STEP]
using pairs_to_distinguish_containment[OF assms(1,2) * **]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; (?\<alpha>, ?\<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); ?\<alpha> \<in> L M; ?\<beta> \<in> L M; after_initial M ?\<alpha> \<noteq> after_initial M ?\<beta>\<rbrakk> \<Longrightarrow> ((?\<alpha>, after_initial M ?\<alpha>), ?\<beta>, after_initial M ?\<beta>) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)

goal (1 subgoal):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (get_pairs_H V M m)
[PROOF STEP]
unfolding res pairs_def \<X>'[symmetric] n_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; (?\<alpha>, ?\<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); ?\<alpha> \<in> L M; ?\<beta> \<in> L M; after_initial M ?\<alpha> \<noteq> after_initial M ?\<beta>\<rbrakk> \<Longrightarrow> ((?\<alpha>, after_initial M ?\<alpha>), ?\<beta>, after_initial M ?\<beta>) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)

goal (1 subgoal):
 1. \<And>\<alpha> \<beta>. \<lbrakk>(\<alpha>, \<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - n \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); \<alpha> \<in> L M; \<beta> \<in> L M; after_initial M \<alpha> \<noteq> after_initial M \<beta>\<rbrakk> \<Longrightarrow> ((\<alpha>, after_initial M \<alpha>), \<beta>, after_initial M \<beta>) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?\<alpha>, ?\<beta>) \<in> V ` reachable_states M \<times> V ` reachable_states M \<union> V ` reachable_states M \<times> {V q @ \<tau> |q \<tau>. q \<in> reachable_states M \<and> \<tau> \<in> {io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}} \<union> (\<Union>q\<in>reachable_states M. \<Union>\<tau>\<in>{io @ [(x, y)] |io x y. io \<in> LS M q \<and> length io \<le> m - size_r M \<and> x \<in> FSM.inputs M \<and> y \<in> FSM.outputs M}. {V q @ \<tau>' |\<tau>'. \<tau>' \<in> list.set (prefixes \<tau>)} \<times> {V q @ \<tau>}); ?\<alpha> \<in> L M; ?\<beta> \<in> L M; after_initial M ?\<alpha> \<noteq> after_initial M ?\<beta>\<rbrakk> \<Longrightarrow> ((?\<alpha>, after_initial M ?\<alpha>), ?\<beta>, after_initial M ?\<beta>) \<in> list.set (get_pairs_H V M m)

goal (1 subgoal):
 1. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
show "\<And> \<alpha> q' \<beta> q'' . ((\<alpha>,q'),(\<beta>,q'')) \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
using pairs_to_distinguish_elems(3,4,5,6,7)[OF assms(1,2) * **]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q1.0 \<noteq> ?q2.0
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?\<alpha> \<in> L M
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?\<beta> \<in> L M
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q1.0 = after_initial M ?\<alpha>
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q2.0 = after_initial M ?\<beta>

goal (1 subgoal):
 1. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
unfolding res pairs_def \<X>'[symmetric] n_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q1.0 \<noteq> ?q2.0
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?\<alpha> \<in> L M
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?\<beta> \<in> L M
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q1.0 = after_initial M ?\<alpha>
\<lbrakk>\<And>q p q'. q \<in> reachable_states M \<Longrightarrow> q \<in> reachable_states M; ((?\<alpha>, ?q1.0), ?\<beta>, ?q2.0) \<in> list.set (pairs_to_distinguish M V \<X>' rstates)\<rbrakk> \<Longrightarrow> ?q2.0 = after_initial M ?\<beta>

goal (1 subgoal):
 1. \<And>\<alpha> q' \<beta> q''. ((\<alpha>, q'), \<beta>, q'') \<in> list.set (pairs_to_distinguish M V \<X>' rstates) \<Longrightarrow> \<alpha> \<in> L M \<and> \<beta> \<in> L M \<and> after_initial M \<alpha> \<noteq> after_initial M \<beta> \<and> q' = after_initial M \<alpha> \<and> q'' = after_initial M \<beta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((?\<alpha>, ?q'), ?\<beta>, ?q'') \<in> list.set (get_pairs_H V M m) \<Longrightarrow> ?\<alpha> \<in> L M \<and> ?\<beta> \<in> L M \<and> after_initial M ?\<alpha> \<noteq> after_initial M ?\<beta> \<and> ?q' = after_initial M ?\<alpha> \<and> ?q'' = after_initial M ?\<beta>

goal:
No subgoals!
[PROOF STEP]
qed