[STATEMENT]
lemma distinguish_from_set_finite :
  fixes T :: "('b::linorder\<times>'c::linorder) prefix_tree "
  assumes "finite_tree T"
  shows "finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
proof (induction depth arbitrary: T G u v X)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
finite_tree T

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define TG' where TG': "TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic"
[PROOF STATE]
proof (state)
this:
TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define vClass where vClass: "vClass = Set.insert v (list.set (cg_lookup (snd TG') v))"
[PROOF STATE]
proof (state)
this:
vClass = Set.insert v (list.set (cg_lookup (snd TG') v))

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define notReferenced where notReferenced: "notReferenced = ((\<not> u_is_v) \<and> (\<forall> q \<in> reachable_states M . V q \<notin> vClass))"
[PROOF STATE]
proof (state)
this:
notReferenced = (\<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> vClass))

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define TG'' where TG'': "TG'' = (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG')"
[PROOF STATE]
proof (state)
this:
TG'' = (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG')

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "finite_tree (fst (TG'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst TG')
[PROOF STEP]
unfolding TG'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
[PROOF STEP]
using spyh_distinguish_finite 0
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree (fst TG')

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst TG')
[PROOF STEP]
have "finite_tree (fst (TG''))"
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG')

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

goal (1 subgoal):
 1. finite_tree (fst (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG'))
[PROOF STEP]
using spyh_distinguish_finite[OF \<open>finite_tree (fst (TG'))\<close>, of M "snd TG'" ]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG')
finite_tree (fst (spyh_distinguish M (fst TG') (snd TG') ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. finite_tree (fst (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst TG'')

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite_tree (fst TG'')

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v= TG''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v = TG''
[PROOF STEP]
apply (subst distinguish_from_set.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic; vClass = Set.insert v (list.set (cg_lookup (snd TG') v)); notReferenced = \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> vClass); TG'' = if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG' in if 0 < 0 then let X' = if notReferenced then v # u # X else u # X; XY = List.product (inputs_as_list M) (outputs_as_list M); handleIO = \<lambda>(T, G) (x, y). let TGu = distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic; TGv = if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic in if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k (0 - 1) completeInputTraces append_heuristic u_is_v else TGv in foldl handleIO TG'' XY else TG'') = TG''
[PROOF STEP]
unfolding TG' vClass notReferenced TG'' Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < 0 then foldl (\<lambda>(T, G) (x, y). if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then v # u # X else u # X) k (0 - 1) completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) (List.product (inputs_as_list M) (outputs_as_list M)) else if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) = (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v = TG''

goal (2 subgoals):
 1. \<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
 2. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst TG'')
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v = TG''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG'')
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v = TG''

goal (1 subgoal):
 1. finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k 0 completeInputTraces append_heuristic u_is_v))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
case (Suc depth)
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V ?T ?G cg_lookup cg_insert get_distinguishing_trace ?u ?v ?X k depth completeInputTraces append_heuristic u_is_v))
finite_tree T

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "(Suc depth - 1) = depth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc depth - 1 = depth
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc depth - 1 = depth

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define TG' where TG': "TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic"
[PROOF STATE]
proof (state)
this:
TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define vClass where vClass: "vClass = Set.insert v (list.set (cg_lookup (snd TG') v))"
[PROOF STATE]
proof (state)
this:
vClass = Set.insert v (list.set (cg_lookup (snd TG') v))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define notReferenced where notReferenced: "notReferenced = ((\<not> u_is_v) \<and> (\<forall> q \<in> reachable_states M . V q \<notin> vClass))"
[PROOF STATE]
proof (state)
this:
notReferenced = (\<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> vClass))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define TG'' where TG'': "TG'' = (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG')"
[PROOF STATE]
proof (state)
this:
TG'' = (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG')

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define X' where X': "X' = (if notReferenced then (v#u#X) else (u#X))"
[PROOF STATE]
proof (state)
this:
X' = (if notReferenced then v # u # X else u # X)

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define XY where XY: "XY = List.product (inputs_as_list M) (outputs_as_list M)"
[PROOF STATE]
proof (state)
this:
XY = List.product (inputs_as_list M) (outputs_as_list M)

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
define handleIO where handleIO: "handleIO = (\<lambda> (T,G) (x,y) . (let TGu = distribute_extension M T G cg_lookup cg_insert u [(x,y)] completeInputTraces append_heuristic;
                                                 TGv = if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x,y)] completeInputTraces append_heuristic
                                             in if is_in_language M (initial M) (u@[(x,y)])
                                                  then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u@[(x,y)]) (v@[(x,y)]) X' k (depth) completeInputTraces append_heuristic u_is_v
                                                  else TGv))"
[PROOF STATE]
proof (state)
this:
handleIO = (\<lambda>(T, G) (x, y). let TGu = distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic; TGv = if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic in if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else TGv)

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "\<And> x y T G . finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T,G) (x,y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
fix T :: "('b::linorder\<times>'c::linorder) prefix_tree "
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
fix x y G
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
assume "finite_tree T"
[PROOF STATE]
proof (state)
this:
finite_tree T

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
define TGu where TGu: "TGu = distribute_extension M T G cg_lookup cg_insert u [(x,y)] completeInputTraces append_heuristic"
[PROOF STATE]
proof (state)
this:
TGu = distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
define TGv where TGv: "TGv = (if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x,y)] completeInputTraces append_heuristic)"
[PROOF STATE]
proof (state)
this:
TGv = (if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
have *: "handleIO (T,G) (x,y) = (if is_in_language M (initial M) (u@[(x,y)])
                                                  then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u@[(x,y)]) (v@[(x,y)]) X' k (depth) completeInputTraces append_heuristic u_is_v
                                                  else TGv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. handleIO (T, G) (x, y) = (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else TGv)
[PROOF STEP]
unfolding handleIO TGu TGv case_prod_conv Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) = (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
handleIO (T, G) (x, y) = (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else TGv)

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
have "finite_tree (fst TGu)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst TGu)
[PROOF STEP]
unfolding TGu
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic))
[PROOF STEP]
using distribute_extension_finite \<open>finite_tree T\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree (fst TGu)

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst TGu)
[PROOF STEP]
have "finite_tree (fst TGv)"
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGu)

goal (1 subgoal):
 1. finite_tree (fst TGv)
[PROOF STEP]
unfolding TGv
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGu)

goal (1 subgoal):
 1. finite_tree (fst (if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic))
[PROOF STEP]
using distribute_extension_finite
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGu)
finite_tree ?T \<Longrightarrow> finite_tree (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. finite_tree (fst (if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite_tree (fst TGv)

goal (1 subgoal):
 1. \<And>x y T G. finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst TGv)
[PROOF STEP]
show "finite_tree (fst (handleIO (T,G) (x,y)))"
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGv)

goal (1 subgoal):
 1. finite_tree (fst (handleIO (T, G) (x, y)))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGv)

goal (1 subgoal):
 1. finite_tree (fst (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else TGv))
[PROOF STEP]
using Suc.IH[of "fst TGv" "snd TGv" "u@[(x,y)]" "v@[(x,y)]" X']
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TGv)
finite_tree (fst TGv) \<Longrightarrow> finite_tree (fst (distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v))

goal (1 subgoal):
 1. finite_tree (fst (if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k depth completeInputTraces append_heuristic u_is_v else TGv))
[PROOF STEP]
by (cases "is_in_language M (initial M) (u@[(x,y)])"; auto)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (handleIO (T, G) (x, y)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleIO (?T, ?G) (?x, ?y)))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "finite_tree (fst TG')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst TG')
[PROOF STEP]
unfolding TG'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
[PROOF STEP]
using spyh_distinguish_finite \<open>finite_tree T\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree ?T \<Longrightarrow> finite_tree (fst (spyh_distinguish ?M ?T ?G ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree (fst TG')

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst TG')
[PROOF STEP]
have "finite_tree (fst TG'')"
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG')

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

goal (1 subgoal):
 1. finite_tree (fst (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG'))
[PROOF STEP]
using spyh_distinguish_finite[OF \<open>finite_tree (fst (TG'))\<close>, of M "snd TG'" ]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG')
finite_tree (fst (spyh_distinguish M (fst TG') (snd TG') ?cg_lookup ?cg_insert ?get_distinguishing_trace ?u ?X ?k ?completeInputTraces ?append_heuristic))

goal (1 subgoal):
 1. finite_tree (fst (if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst TG'')

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "finite_tree (fst (foldl handleIO TG'' XY))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (foldl handleIO TG'' XY))
[PROOF STEP]
proof (induction XY rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (fst (foldl handleIO TG'' []))
 2. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (fst (foldl handleIO TG'' []))
 2. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (foldl handleIO TG'' []))
[PROOF STEP]
using \<open>finite_tree (fst TG'')\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst TG'')

goal (1 subgoal):
 1. finite_tree (fst (foldl handleIO TG'' []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleIO TG'' []))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
case (snoc a XY)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleIO TG'' XY))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
obtain x y where "a = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. a = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x1 x2. ?y = (x1, x2) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>x y. a = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a = (x, y)

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = (x, y)
[PROOF STEP]
have *: "(foldl handleIO TG'' (XY@[a])) = handleIO (fst (foldl handleIO TG'' XY),snd (foldl handleIO TG'' XY)) (x,y)"
[PROOF STATE]
proof (prove)
using this:
a = (x, y)

goal (1 subgoal):
 1. foldl handleIO TG'' (XY @ [a]) = handleIO (fst (foldl handleIO TG'' XY), snd (foldl handleIO TG'' XY)) (x, y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handleIO TG'' (XY @ [a]) = handleIO (fst (foldl handleIO TG'' XY), snd (foldl handleIO TG'' XY)) (x, y)

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (foldl handleIO TG'' xs)) \<Longrightarrow> finite_tree (fst (foldl handleIO TG'' (xs @ [x])))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (foldl handleIO TG'' (XY @ [a])))
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (foldl handleIO TG'' XY))

goal (1 subgoal):
 1. finite_tree (fst (foldl handleIO TG'' (XY @ [a])))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (foldl handleIO TG'' XY))

goal (1 subgoal):
 1. finite_tree (fst (handleIO (fst (foldl handleIO TG'' XY), snd (foldl handleIO TG'' XY)) (x, y)))
[PROOF STEP]
using \<open>\<And> x y T G . finite_tree T \<Longrightarrow> finite_tree (fst (handleIO (T,G) (x,y)))\<close>
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (foldl handleIO TG'' XY))
finite_tree ?T \<Longrightarrow> finite_tree (fst (handleIO (?T, ?G) (?x, ?y)))

goal (1 subgoal):
 1. finite_tree (fst (handleIO (fst (foldl handleIO TG'' XY), snd (foldl handleIO TG'' XY)) (x, y)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleIO TG'' (XY @ [a])))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleIO TG'' XY))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite_tree (fst (foldl handleIO TG'' XY))

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
have "distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v = foldl handleIO TG'' XY"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v = foldl handleIO TG'' XY
[PROOF STEP]
apply (subst distinguish_from_set.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let TG' = spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic; vClass = Set.insert v (list.set (cg_lookup (snd TG') v)); notReferenced = \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> vClass); TG'' = if notReferenced then spyh_distinguish M (fst TG') (snd TG') cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else TG' in if 0 < Suc depth then let X' = if notReferenced then v # u # X else u # X; XY = List.product (inputs_as_list M) (outputs_as_list M); handleIO = \<lambda>(T, G) (x, y). let TGu = distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic; TGv = if u_is_v then TGu else distribute_extension M (fst TGu) (snd TGu) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic in if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst TGv) (snd TGv) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) X' k (Suc depth - 1) completeInputTraces append_heuristic u_is_v else TGv in foldl handleIO TG'' XY else TG'') = foldl handleIO TG'' XY
[PROOF STEP]
unfolding TG' vClass notReferenced TG'' Let_def X' XY handleIO
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < Suc depth then foldl (\<lambda>(T, G) (x, y). if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then v # u # X else u # X) k (Suc depth - 1) completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) (List.product (inputs_as_list M) (outputs_as_list M)) else if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) = foldl (\<lambda>(T, G) (x, y). if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then v # u # X else u # X) k depth completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
unfolding \<open>(Suc depth - 1) = depth\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < Suc depth then foldl (\<lambda>(T, G) (x, y). if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then v # u # X else u # X) k depth completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) (List.product (inputs_as_list M) (outputs_as_list M)) else if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) = foldl (\<lambda>(T, G) (x, y). if is_in_language M (FSM.initial M) (u @ [(x, y)]) then distinguish_from_set M V (fst (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) (snd (if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace (u @ [(x, y)]) (v @ [(x, y)]) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then v # u # X else u # X) k depth completeInputTraces append_heuristic u_is_v else if u_is_v then distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u [(x, y)] completeInputTraces append_heuristic)) cg_lookup cg_insert v [(x, y)] completeInputTraces append_heuristic) (if \<not> u_is_v \<and> (\<forall>q\<in>reachable_states M. V q \<notin> Set.insert v (list.set (cg_lookup (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) v))) then spyh_distinguish M (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) (snd (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) cg_lookup cg_insert get_distinguishing_trace v X k completeInputTraces append_heuristic else spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) (List.product (inputs_as_list M) (outputs_as_list M))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v = foldl handleIO TG'' XY

goal (1 subgoal):
 1. \<And>depth T G u v X. \<lbrakk>\<And>T G u v X. finite_tree T \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k depth completeInputTraces append_heuristic u_is_v)); finite_tree T\<rbrakk> \<Longrightarrow> finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite_tree (fst (foldl handleIO TG'' XY))
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v = foldl handleIO TG'' XY
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (foldl handleIO TG'' XY))
distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v = foldl handleIO TG'' XY

goal (1 subgoal):
 1. finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
finite_tree (fst (distinguish_from_set M V T G cg_lookup cg_insert get_distinguishing_trace u v X k (Suc depth) completeInputTraces append_heuristic u_is_v))

goal:
No subgoals!
[PROOF STEP]
qed