[STATEMENT]
lemma spyh_distinguish_subset :
  "set T \<subseteq> set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
[PROOF STEP]
proof (induction X rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
 2. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
 2. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
case (snoc a X)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
have "set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))
         \<subseteq> set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X@[a]) k completeInputTraces append_heuristic))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
define dh where dh: "dh = (\<lambda> (T,G) v . if after_initial M u = after_initial M v
                                  then (T,G)
                                  else (let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k
                                         in if fst ew = 0
                                              then (T,G)
                                              else (let u' = (u@(snd ew));
                                                        v' = (v@(snd ew));
                                                        w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then (snd ew) else (snd ew)@(get_distinguishing_trace (after_initial M u') (after_initial M v'));
                                                        TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic
                                                    in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)))"
[PROOF STATE]
proof (state)
this:
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)

goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
have "spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X@[a]) k completeInputTraces append_heuristic
                = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a
[PROOF STEP]
unfolding dh spyh_distinguish.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) (X @ [a]) = (case foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X of (T, G) \<Rightarrow> \<lambda>v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) a
[PROOF STEP]
unfolding foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X) [a] = (case foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X of (T, G) \<Rightarrow> \<lambda>v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a

goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a

goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
have "\<And> T G . set T \<subseteq> set (fst (dh (T,G) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
fix T G
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
show "set T \<subseteq> set (fst (dh (T,G) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
proof (cases "after_initial M u = after_initial M a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. after_initial M u = after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
 2. after_initial M u \<noteq> after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
after_initial M u = after_initial M a

goal (2 subgoals):
 1. after_initial M u = after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
 2. after_initial M u \<noteq> after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
after_initial M u = after_initial M a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
after_initial M u = after_initial M a

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
using dh
[PROOF STATE]
proof (prove)
using this:
after_initial M u = after_initial M a
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))

goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
after_initial M u \<noteq> after_initial M a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
proof (cases "fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
 2. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0

goal (2 subgoals):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
 2. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
using False dh
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0
after_initial M u \<noteq> after_initial M a
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
define u' where u': "u' = (u@(snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))"
[PROOF STATE]
proof (state)
this:
u' = u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
define v' where v': "v' = (a@(snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))"
[PROOF STATE]
proof (state)
this:
v' = a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
define w where w: "w = get_distinguishing_trace (after_initial M u') (after_initial M v')"
[PROOF STATE]
proof (state)
this:
w = get_distinguishing_trace (after_initial M u') (after_initial M v')

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
define w' where w': "w' = (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) else (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))@w)"
[PROOF STATE]
proof (state)
this:
w' = (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ w)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
define TG' where TG': "TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic"
[PROOF STATE]
proof (state)
this:
TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
have "dh (T,G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
[PROOF STEP]
using False \<open>FSM.after M (FSM.initial M) u \<noteq> FSM.after M (FSM.initial M) a\<close>
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
[PROOF STEP]
unfolding dh u' v' w w' TG' Let_def case_prod_conv
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. (if after_initial M u = after_initial M a then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert a (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic) = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert a (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
using distribute_extension_subset
[PROOF STATE]
proof (prove)
using this:
dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (distribute_extension ?M ?T ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))
[PROOF STEP]
by (metis (no_types, lifting) subset_trans)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (dh (T, G) a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (dh (?T, ?G) a))

goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (dh (?T, ?G) a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (dh (?T, ?G) a))

goal (1 subgoal):
 1. Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
by (metis eq_fst_iff)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic)) \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spyh_distinguish_finite :
  fixes T :: "('b::linorder\<times>'c::linorder) prefix_tree"
  assumes "finite_tree T"
  shows "finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))"
[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]
proof (induction X rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
 2. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
 2. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u [] k completeInputTraces append_heuristic))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite_tree T

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

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
case (snoc a X)
[PROOF STATE]
proof (state)
this:
finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic))

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
define dh where dh: "dh = (\<lambda> (T,G) v . if after_initial M u = after_initial M v
                                then (T,G)
                                else (let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k
                                       in if fst ew = 0
                                            then (T,G)
                                            else (let u' = (u@(snd ew));
                                                      v' = (v@(snd ew));
                                                      w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then (snd ew) else (snd ew)@(get_distinguishing_trace (after_initial M u') (after_initial M v'));
                                                      TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic
                                                  in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)))"
[PROOF STATE]
proof (state)
this:
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
have *: "spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X@[a]) k completeInputTraces append_heuristic
                = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a
[PROOF STEP]
unfolding dh spyh_distinguish.simps Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) (X @ [a]) = (case foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X of (T, G) \<Rightarrow> \<lambda>v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) a
[PROOF STEP]
unfolding foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X) [a] = (case foldl (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) (T, G) X of (T, G) \<Rightarrow> \<lambda>v. if after_initial M u = after_initial M v then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert v (if does_distinguish M (after_initial M u) (after_initial M v) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k))) (after_initial M (v @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k)))) completeInputTraces append_heuristic) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (X @ [a]) k completeInputTraces append_heuristic = dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
have **:"\<And> T G . finite_tree T \<Longrightarrow> finite_tree (fst (dh (T,G) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T G. finite_tree T \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T G. finite_tree T \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
fix T :: "('b\<times>'c) prefix_tree"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T G. finite_tree T \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
fix G
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T G. finite_tree T \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
assume "finite_tree T"
[PROOF STATE]
proof (state)
this:
finite_tree T

goal (1 subgoal):
 1. \<And>T G. finite_tree T \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
show "finite_tree (fst (dh (T,G) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
proof (cases "after_initial M u = after_initial M a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. after_initial M u = after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
 2. after_initial M u \<noteq> after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
after_initial M u = after_initial M a

goal (2 subgoals):
 1. after_initial M u = after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
 2. after_initial M u \<noteq> after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
after_initial M u = after_initial M a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
after_initial M u = after_initial M a

goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
using dh \<open>finite_tree T\<close>
[PROOF STATE]
proof (prove)
using this:
after_initial M u = after_initial M a
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst (dh (T, G) a))

goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. after_initial M u \<noteq> after_initial M a \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
after_initial M u \<noteq> after_initial M a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
proof (cases "fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
 2. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0

goal (2 subgoals):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
 2. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0

goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
using False dh \<open>finite_tree T\<close>
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0
after_initial M u \<noteq> after_initial M a
dh = (\<lambda>(T, G) v. if after_initial M u = after_initial M v then (T, G) else let ew = get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u v k in if fst ew = 0 then (T, G) else let u' = u @ snd ew; v' = v @ snd ew; w' = if does_distinguish M (after_initial M u) (after_initial M v) (snd ew) then snd ew else snd ew @ get_distinguishing_trace (after_initial M u') (after_initial M v'); TG' = distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic in distribute_extension M (fst TG') (snd TG') cg_lookup cg_insert v w' completeInputTraces append_heuristic)
finite_tree T

goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite_tree (fst (dh (T, G) a))

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
define u' where u': "u' = (u@(snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))"
[PROOF STATE]
proof (state)
this:
u' = u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
define v' where v': "v' = (a@(snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))"
[PROOF STATE]
proof (state)
this:
v' = a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
define w where w: "w = get_distinguishing_trace (after_initial M u') (after_initial M v')"
[PROOF STATE]
proof (state)
this:
w = get_distinguishing_trace (after_initial M u') (after_initial M v')

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
define w' where w': "w' = (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) else (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))@w)"
[PROOF STATE]
proof (state)
this:
w' = (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ w)

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
define TG' where TG': "TG' = distribute_extension M T G cg_lookup cg_insert u w'"
[PROOF STATE]
proof (state)
this:
TG' = distribute_extension M T G cg_lookup cg_insert u w'

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
have *:"dh (T,G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
[PROOF STEP]
using False \<open>FSM.after M (FSM.initial M) u \<noteq> FSM.after M (FSM.initial M) a\<close>
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic
[PROOF STEP]
unfolding dh u' v' w w' TG' Let_def case_prod_conv
[PROOF STATE]
proof (prove)
using this:
fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0
after_initial M u \<noteq> after_initial M a

goal (1 subgoal):
 1. (if after_initial M u = after_initial M a then (T, G) else if fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) = 0 then (T, G) else distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert a (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic) = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic)) cg_lookup cg_insert a (if does_distinguish M (after_initial M u) (after_initial M a) (snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)) then snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) else snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) @ get_distinguishing_trace (after_initial M (u @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k))) (after_initial M (a @ snd (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k)))) completeInputTraces append_heuristic
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dh (T, G) a = distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic

goal (1 subgoal):
 1. \<lbrakk>after_initial M u \<noteq> after_initial M a; fst (get_prefix_of_separating_sequence M T G cg_lookup get_distinguishing_trace u a k) \<noteq> 0\<rbrakk> \<Longrightarrow> finite_tree (fst (dh (T, G) a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (dh (T, G) a))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic))
[PROOF STEP]
using distribute_extension_finite[OF distribute_extension_finite[OF \<open>finite_tree T\<close>]]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (distribute_extension ?M (fst (distribute_extension ?M1 T ?G1 ?cg_lookup1 ?cg_insert1 ?u1 ?w1 ?b1 ?heuristic1)) ?G ?cg_lookup ?cg_insert ?u ?w ?b ?heuristic))

goal (1 subgoal):
 1. finite_tree (fst (distribute_extension M (fst (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) (snd (distribute_extension M T G cg_lookup cg_insert u w' completeInputTraces append_heuristic)) cg_lookup cg_insert a w' completeInputTraces append_heuristic))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite_tree (fst (dh (T, G) a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (dh (T, G) a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_tree (fst (dh (T, G) a))

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

goal (1 subgoal):
 1. \<And>x xs. finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u xs k completeInputTraces append_heuristic)) \<Longrightarrow> finite_tree (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u (xs @ [x]) k completeInputTraces append_heuristic))
[PROOF STEP]
show ?case
[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 @ [a]) k completeInputTraces append_heuristic))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_tree (fst (dh (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic) a))
[PROOF STEP]
using **[OF snoc]
[PROOF STATE]
proof (prove)
using this:
finite_tree (fst (dh (fst (spyh_distinguish M T G cg_lookup cg_insert get_distinguishing_trace u X k completeInputTraces append_heuristic), ?G) a))

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

goal:
No subgoals!
[PROOF STEP]
qed