[STATEMENT]
lemma complement_4_language_1: "language (complement_3 A) \<subseteq> language (complement_4 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement_3 A) \<subseteq> language (complement_4 A)
[PROOF STEP]
proof (rule simulation_language)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. alphabet (complement_3 A) \<subseteq> alphabet (complement_4 A)
 2. \<And>p. p \<in> initial (complement_3 A) \<Longrightarrow> \<exists>q\<in>initial (complement_4 A). (p, q) \<in> ?R
 3. \<And>a p p' q. \<lbrakk>p' \<in> transition (complement_3 A) a p; (p, q) \<in> ?R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition (complement_4 A) a q. (p', q') \<in> ?R
 4. \<And>p q. \<lbrakk>(p, q) \<in> ?R; accepting (complement_3 A) p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) q
[PROOF STEP]
show "alphabet (complement_3 A) \<subseteq> alphabet (complement_4 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (complement_3 A) \<subseteq> alphabet (complement_4 A)
[PROOF STEP]
unfolding complement_3_def complement_4_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_3 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c)) \<subseteq> alphabet (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
alphabet (complement_3 A) \<subseteq> alphabet (complement_4 A)

goal (3 subgoals):
 1. \<And>p. p \<in> initial (complement_3 A) \<Longrightarrow> \<exists>q\<in>initial (complement_4 A). (p, q) \<in> ?R
 2. \<And>a p p' q. \<lbrakk>p' \<in> transition (complement_3 A) a p; (p, q) \<in> ?R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition (complement_4 A) a q. (p', q') \<in> ?R
 3. \<And>p q. \<lbrakk>(p, q) \<in> ?R; accepting (complement_3 A) p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) q
[PROOF STEP]
show "\<exists> q \<in> initial (complement_4 A). (p, q) \<in> R" if "p \<in> initial (complement_3 A)" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q\<in>initial (complement_4 A). (p, q) \<in> R
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
p \<in> initial (complement_3 A)

goal (1 subgoal):
 1. \<exists>q\<in>initial (complement_4 A). (p, q) \<in> R
[PROOF STEP]
unfolding complement_3_def complement_4_def R_def
[PROOF STATE]
proof (prove)
using this:
p \<in> initial (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_3 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c))

goal (1 subgoal):
 1. \<exists>q\<in>initial (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c)). (p, q) \<in> {(f, g). dom f = dom g \<and> (\<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p))) \<and> (\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p)))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?p \<in> initial (complement_3 A) \<Longrightarrow> \<exists>q\<in>initial (complement_4 A). (?p, q) \<in> R

goal (2 subgoals):
 1. \<And>a p p' q. \<lbrakk>p' \<in> transition (complement_3 A) a p; (p, q) \<in> R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition (complement_4 A) a q. (p', q') \<in> R
 2. \<And>p q. \<lbrakk>(p, q) \<in> R; accepting (complement_3 A) p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) q
[PROOF STEP]
show "\<exists> g' \<in> transition (complement_4 A) a g. (f', g') \<in> R"
      if "f' \<in> transition (complement_3 A) a f" "(f, g) \<in> R"
      for a f f' g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have 1: "f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
using that(1)
[PROOF STATE]
proof (prove)
using this:
f' \<in> transition (complement_3 A) a f

goal (1 subgoal):
 1. f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
unfolding complement_3_def complement_succ_3_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> transition (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (\<lambda>a. ((expand_map \<circ>\<circ> get_3) A \<circ>\<circ>\<circ> bounds_3) A a \<circ> refresh_1) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c)) a f

goal (1 subgoal):
 1. f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have 2:
        "dom f = dom g"
        "\<forall> p \<in> dom f. fst (the (f p)) \<le> fst (the (g p))"
        "\<forall> p \<in> dom f. snd (the (f p)) \<longleftrightarrow> snd (the (g p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom f = dom g &&& \<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p)) &&& \<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
[PROOF STEP]
using that(2)
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> R

goal (1 subgoal):
 1. dom f = dom g &&& \<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p)) &&& \<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). dom f = dom g \<and> (\<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p))) \<and> (\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p)))}

goal (1 subgoal):
 1. dom f = dom g &&& \<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p)) &&& \<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom f = dom g
\<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p))
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have "dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
using expand_map_dom 1
[PROOF STATE]
proof (prove)
using this:
?g \<in> expand_map ?f \<Longrightarrow> dom ?g = dom ?f
f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have "\<dots> = dom (bounds_3 A a (refresh_1 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (get_3 A (bounds_3 A a (refresh_1 f))) = dom (bounds_3 A a (refresh_1 f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (get_3 A (bounds_3 A a (refresh_1 f))) = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dom f' = dom (bounds_3 A a (refresh_1 f))
[PROOF STEP]
have 3: "dom f' = dom (bounds_3 A a (refresh_1 f))"
[PROOF STATE]
proof (prove)
using this:
dom f' = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. dom f' = dom (bounds_3 A a (refresh_1 f))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom f' = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
define g' where "g' p \<equiv> do
      {
        (k, c) \<leftarrow> bounds_3 A a (refresh_1 g) p;
        (l, d) \<leftarrow> f' p;
        Some (if even k = even l then k else k - 1, d)
      }" for p
[PROOF STATE]
proof (state)
this:
g' ?p \<equiv> bounds_3 A a (refresh_1 g) ?p \<bind> (\<lambda>(k, c). f' ?p \<bind> (\<lambda>(l, d). Some (if even k = even l then k else k - 1, d)))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have 4: "g' p = do
      {
        kc \<leftarrow> bounds_3 A a (refresh_1 g) p;
        ld \<leftarrow> f' p;
        Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)
      }" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' p = bounds_3 A a (refresh_1 g) p \<bind> (\<lambda>kc. f' p \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))
[PROOF STEP]
unfolding g'_def case_prod_beta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_3 A a (refresh_1 g) p \<bind> (\<lambda>pa. f' p \<bind> (\<lambda>p. Some (if even (fst pa) = even (fst p) then fst pa else fst pa - 1, snd p))) = bounds_3 A a (refresh_1 g) p \<bind> (\<lambda>kc. f' p \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
g' ?p = bounds_3 A a (refresh_1 g) ?p \<bind> (\<lambda>kc. f' ?p \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have "dom g' = dom (bounds_3 A a (refresh_1 g)) \<inter> dom f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g' = dom (bounds_3 A a (refresh_1 g)) \<inter> dom f'
[PROOF STEP]
using 4 bind_eq_Some_conv
[PROOF STATE]
proof (prove)
using this:
g' ?p = bounds_3 A a (refresh_1 g) ?p \<bind> (\<lambda>kc. f' ?p \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))
(?f \<bind> ?g = Some ?x) = (\<exists>y. ?f = Some y \<and> ?g y = Some ?x)

goal (1 subgoal):
 1. dom g' = dom (bounds_3 A a (refresh_1 g)) \<inter> dom f'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
dom g' = dom (bounds_3 A a (refresh_1 g)) \<inter> dom f'

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dom g' = dom (bounds_3 A a (refresh_1 g)) \<inter> dom f'

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have "\<dots> = dom f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (bounds_3 A a (refresh_1 g)) \<inter> dom f' = dom f'
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p))
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
dom f' = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. dom (bounds_3 A a (refresh_1 g)) \<inter> dom f' = dom f'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (bounds_3 A a (refresh_1 g)) \<inter> dom f' = dom f'

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dom g' = dom f'
[PROOF STEP]
have 5: "dom g' = dom f'"
[PROOF STATE]
proof (prove)
using this:
dom g' = dom f'

goal (1 subgoal):
 1. dom g' = dom f'
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom g' = dom f'

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
have 6: "(l, d) \<in> items_3 A p (k, c)"
        if "bounds_3 A a (refresh_1 f) p = Some (k, c)" "f' p = Some (l, d)" for p k c l d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (k, c)
[PROOF STEP]
using 1 that
[PROOF STATE]
proof (prove)
using this:
f' \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))
bounds_3 A a (refresh_1 f) p = Some (k, c)
f' p = Some (l, d)

goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (k, c)
[PROOF STEP]
unfolding expand_map_alt_def get_3_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {g. dom g = dom (\<lambda>p. map_option (items_3 A p) (bounds_3 A a (refresh_1 f) p)) \<and> (\<forall>x S y. map_option (items_3 A x) (bounds_3 A a (refresh_1 f) x) = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S)}
bounds_3 A a (refresh_1 f) p = Some (k, c)
f' p = Some (l, d)

goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (k, c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>bounds_3 A a (refresh_1 f) ?p = Some (?k, ?c); f' ?p = Some (?l, ?d)\<rbrakk> \<Longrightarrow> (?l, ?d) \<in> items_3 A ?p (?k, ?c)

goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R
[PROOF STEP]
unfolding complement_4_def nba.sel complement_succ_4_def comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g'\<in>expand_map (get_4 A (bounds_3 A a (refresh_1 g))). (f', g') \<in> R
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (f', ?g') \<in> R
 2. ?g' \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 g)))
[PROOF STEP]
show "(f', g') \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f', g') \<in> R
[PROOF STEP]
unfolding R_def mem_Collect_eq prod.case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom f' = dom g' \<and> (\<forall>p\<in>dom f'. fst (the (f' p)) \<le> fst (the (g' p))) \<and> (\<forall>p\<in>dom f'. snd (the (f' p)) = snd (the (g' p)))
[PROOF STEP]
proof (intro conjI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dom f' = dom g'
 2. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 3. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
show "dom f' = dom g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom f' = dom g'
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
dom g' = dom f'

goal (1 subgoal):
 1. dom f' = dom g'
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
dom f' = dom g'

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
assume 10: "p \<in> dom f'"
[PROOF STATE]
proof (state)
this:
p \<in> dom f'

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 11: "p \<in> dom (bounds_3 A a (refresh_1 g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> dom (bounds_3 A a (refresh_1 g))
[PROOF STEP]
using 2(1) 3 10
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
dom f' = dom (bounds_3 A a (refresh_1 f))
p \<in> dom f'

goal (1 subgoal):
 1. p \<in> dom (bounds_3 A a (refresh_1 g))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<in> dom (bounds_3 A a (refresh_1 g))

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k c. bounds_3 A a (refresh_1 g) p = Some (k, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 11
[PROOF STATE]
proof (prove)
using this:
p \<in> dom (bounds_3 A a (refresh_1 g))

goal (1 subgoal):
 1. (\<And>k c. bounds_3 A a (refresh_1 g) p = Some (k, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
obtain l d where 13: "f' p = Some (l, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l d. f' p = Some (l, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f'

goal (1 subgoal):
 1. (\<And>l d. f' p = Some (l, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' p = Some (l, d)

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n e. bounds_3 A a (refresh_1 f) p = Some (n, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 10 3
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f'
dom f' = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. (\<And>n e. bounds_3 A a (refresh_1 f) p = Some (n, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
bounds_3 A a (refresh_1 f) p = Some (n, e)

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 15: "(l, d) \<in> items_3 A p (n, e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (n, e)
[PROOF STEP]
using 6 14 13
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bounds_3 A a (refresh_1 f) ?p = Some (?k, ?c); f' ?p = Some (?l, ?d)\<rbrakk> \<Longrightarrow> (?l, ?d) \<in> items_3 A ?p (?k, ?c)
bounds_3 A a (refresh_1 f) p = Some (n, e)
f' p = Some (l, d)

goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (n, e)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
(l, d) \<in> items_3 A p (n, e)

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 16: "n \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
using bounds_R(1) that(2) 14 12
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f, ?g) \<in> R; bounds_3 ?A ?a (refresh_1 ?f) ?p = Some (?n, ?e); bounds_3 ?A ?a (refresh_1 ?g) ?p = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?n \<le> ?k
(f, g) \<in> R
bounds_3 A a (refresh_1 f) p = Some (n, e)
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
n \<le> k

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 17: "l \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> k
[PROOF STEP]
using 15 16
[PROOF STATE]
proof (prove)
using this:
(l, d) \<in> items_3 A p (n, e)
n \<le> k

goal (1 subgoal):
 1. l \<le> k
[PROOF STEP]
unfolding items_3_def
[PROOF STATE]
proof (prove)
using this:
(l, d) \<in> (case (n, e) of (k, c) \<Rightarrow> {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A p \<longrightarrow> even l)})
n \<le> k

goal (1 subgoal):
 1. l \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> k

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 18: "even k \<longleftrightarrow> odd l \<Longrightarrow> l \<le> k \<Longrightarrow> l \<le> k - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even k = odd l; l \<le> k\<rbrakk> \<Longrightarrow> l \<le> k - 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<lbrakk>even k = odd l; l \<le> k\<rbrakk> \<Longrightarrow> l \<le> k - 1

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
have 19: "e \<longleftrightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = c
[PROOF STEP]
using bounds_R(2) that(2) 14 12
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f, ?g) \<in> R; bounds_3 ?A ?a (refresh_1 ?f) ?p = Some (?n, ?e); bounds_3 ?A ?a (refresh_1 ?g) ?p = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?e = ?c
(f, g) \<in> R
bounds_3 A a (refresh_1 f) p = Some (n, e)
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. e = c
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
e = c

goal (2 subgoals):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> fst (the (f' p)) \<le> fst (the (g' p))
 2. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
show "fst (the (f' p)) \<le> fst (the (g' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (f' p)) \<le> fst (the (g' p))
[PROOF STEP]
using 17 18
[PROOF STATE]
proof (prove)
using this:
l \<le> k
\<lbrakk>even k = odd l; l \<le> k\<rbrakk> \<Longrightarrow> l \<le> k - 1

goal (1 subgoal):
 1. fst (the (f' p)) \<le> fst (the (g' p))
[PROOF STEP]
unfolding 4 12 13
[PROOF STATE]
proof (prove)
using this:
l \<le> k
\<lbrakk>even k = odd l; l \<le> k\<rbrakk> \<Longrightarrow> l \<le> k - 1

goal (1 subgoal):
 1. fst (the (Some (l, d))) \<le> fst (the (Some (k, c) \<bind> (\<lambda>kc. Some (l, d) \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (the (f' p)) \<le> fst (the (g' p))

goal (1 subgoal):
 1. \<And>p. p \<in> dom f' \<Longrightarrow> snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
show "snd (the (f' p)) \<longleftrightarrow> snd (the (g' p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
using 19
[PROOF STATE]
proof (prove)
using this:
e = c

goal (1 subgoal):
 1. snd (the (f' p)) = snd (the (g' p))
[PROOF STEP]
unfolding 4 12 13
[PROOF STATE]
proof (prove)
using this:
e = c

goal (1 subgoal):
 1. snd (the (Some (l, d))) = snd (the (Some (k, c) \<bind> (\<lambda>kc. Some (l, d) \<bind> (\<lambda>ld. Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd (the (f' p)) = snd (the (g' p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f', g') \<in> R

goal (1 subgoal):
 1. g' \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 g)))
[PROOF STEP]
show "g' \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 g)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 g)))
[PROOF STEP]
unfolding expand_map_alt_def mem_Collect_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g))) \<and> (\<forall>x S y. get_4 A (bounds_3 A a (refresh_1 g)) x = Some S \<longrightarrow> g' x = Some y \<longrightarrow> y \<in> S)
[PROOF STEP]
proof (intro conjI allI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))
 2. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
show "dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))
[PROOF STEP]
using 2(1) 3 5
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
dom f' = dom (bounds_3 A a (refresh_1 f))
dom g' = dom f'

goal (1 subgoal):
 1. dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
fix p S xy
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
assume 10: "get_4 A (bounds_3 A a (refresh_1 g)) p = Some S"
[PROOF STATE]
proof (state)
this:
get_4 A (bounds_3 A a (refresh_1 g)) p = Some S

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
assume 11: "g' p = Some xy"
[PROOF STATE]
proof (state)
this:
g' p = Some xy

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)" "S = items_4 A p (k, c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k c. \<lbrakk>bounds_3 A a (refresh_1 g) p = Some (k, c); S = items_4 A p (k, c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
get_4 A (bounds_3 A a (refresh_1 g)) p = Some S

goal (1 subgoal):
 1. (\<And>k c. \<lbrakk>bounds_3 A a (refresh_1 g) p = Some (k, c); S = items_4 A p (k, c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding get_4_def
[PROOF STATE]
proof (prove)
using this:
map_option (items_4 A p) (bounds_3 A a (refresh_1 g) p) = Some S

goal (1 subgoal):
 1. (\<And>k c. \<lbrakk>bounds_3 A a (refresh_1 g) p = Some (k, c); S = items_4 A p (k, c)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounds_3 A a (refresh_1 g) p = Some (k, c)
S = items_4 A p (k, c)

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
obtain l d where 13: "f' p = Some (l, d)" "xy = (if even k \<longleftrightarrow> even l then k else k - 1, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l d. \<lbrakk>f' p = Some (l, d); xy = (if even k = even l then k else k - 1, d)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 11 12
[PROOF STATE]
proof (prove)
using this:
g' p = Some xy
bounds_3 A a (refresh_1 g) p = Some (k, c)
S = items_4 A p (k, c)

goal (1 subgoal):
 1. (\<And>l d. \<lbrakk>f' p = Some (l, d); xy = (if even k = even l then k else k - 1, d)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding g'_def
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 g) p \<bind> (\<lambda>(k, c). f' p \<bind> (\<lambda>(l, d). Some (if even k = even l then k else k - 1, d))) = Some xy
bounds_3 A a (refresh_1 g) p = Some (k, c)
S = items_4 A p (k, c)

goal (1 subgoal):
 1. (\<And>l d. \<lbrakk>f' p = Some (l, d); xy = (if even k = even l then k else k - 1, d)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: bind_splits)
[PROOF STATE]
proof (state)
this:
f' p = Some (l, d)
xy = (if even k = even l then k else k - 1, d)

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n e. bounds_3 A a (refresh_1 f) p = Some (n, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 13(1) 3
[PROOF STATE]
proof (prove)
using this:
f' p = Some (l, d)
dom f' = dom (bounds_3 A a (refresh_1 f))

goal (1 subgoal):
 1. (\<And>n e. bounds_3 A a (refresh_1 f) p = Some (n, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
bounds_3 A a (refresh_1 f) p = Some (n, e)

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
have 15: "(l, d) \<in> items_3 A p (n, e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (n, e)
[PROOF STEP]
using 6 14 13(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bounds_3 A a (refresh_1 f) ?p = Some (?k, ?c); f' ?p = Some (?l, ?d)\<rbrakk> \<Longrightarrow> (?l, ?d) \<in> items_3 A ?p (?k, ?c)
bounds_3 A a (refresh_1 f) p = Some (n, e)
f' p = Some (l, d)

goal (1 subgoal):
 1. (l, d) \<in> items_3 A p (n, e)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
(l, d) \<in> items_3 A p (n, e)

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
have 16: "n \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
using bounds_R(1) that(2) 14 12(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f, ?g) \<in> R; bounds_3 ?A ?a (refresh_1 ?f) ?p = Some (?n, ?e); bounds_3 ?A ?a (refresh_1 ?g) ?p = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?n \<le> ?k
(f, g) \<in> R
bounds_3 A a (refresh_1 f) p = Some (n, e)
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
n \<le> k

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
have 17: "e \<longleftrightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = c
[PROOF STEP]
using bounds_R(2) that(2) 14 12(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f, ?g) \<in> R; bounds_3 ?A ?a (refresh_1 ?f) ?p = Some (?n, ?e); bounds_3 ?A ?a (refresh_1 ?g) ?p = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?e = ?c
(f, g) \<in> R
bounds_3 A a (refresh_1 f) p = Some (n, e)
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. e = c
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
e = c

goal (1 subgoal):
 1. \<And>x S y. \<lbrakk>get_4 A (bounds_3 A a (refresh_1 g)) x = Some S; g' x = Some y\<rbrakk> \<Longrightarrow> y \<in> S
[PROOF STEP]
show "xy \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xy \<in> S
[PROOF STEP]
using 15 16 17
[PROOF STATE]
proof (prove)
using this:
(l, d) \<in> items_3 A p (n, e)
n \<le> k
e = c

goal (1 subgoal):
 1. xy \<in> S
[PROOF STEP]
unfolding 12(2) 13(2) items_3_def items_4_def
[PROOF STATE]
proof (prove)
using this:
(l, d) \<in> (case (n, e) of (k, c) \<Rightarrow> {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A p \<longrightarrow> even l)})
n \<le> k
e = c

goal (1 subgoal):
 1. (if even k = even l then k else k - 1, d) \<in> (case (k, c) of (k, c) \<Rightarrow> {(l, c \<and> even l) |l. k \<le> Suc l \<and> l \<le> k \<and> (accepting A p \<longrightarrow> even l)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xy \<in> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g' \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 g)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>g'\<in>transition (complement_4 A) a g. (f', g') \<in> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?f' \<in> transition (complement_3 A) ?a ?f; (?f, ?g) \<in> R\<rbrakk> \<Longrightarrow> \<exists>g'\<in>transition (complement_4 A) ?a ?g. (?f', g') \<in> R

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>(p, q) \<in> R; accepting (complement_3 A) p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) q
[PROOF STEP]
show "\<And> p q. (p, q) \<in> R \<Longrightarrow> accepting (complement_3 A) p \<Longrightarrow> accepting (complement_4 A) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>(p, q) \<in> R; accepting (complement_3 A) p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) q
[PROOF STEP]
unfolding complement_3_def complement_4_def R_def map_to_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>(p, q) \<in> {(f, g). dom f = dom g \<and> (\<forall>p\<in>dom f. fst (the (f p)) \<le> fst (the (g p))) \<and> (\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p)))}; accepting (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_3 A) (\<lambda>f. \<forall>(p, k, c)\<in>{(k, v). f k = Some v}. \<not> c)) p\<rbrakk> \<Longrightarrow> accepting (nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, c)\<in>{(k, v). f k = Some v}. \<not> c)) q
[PROOF STEP]
by (auto) (metis domIff eq_snd_iff option.exhaust_sel option.sel)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?p, ?q) \<in> R; accepting (complement_3 A) ?p\<rbrakk> \<Longrightarrow> accepting (complement_4 A) ?q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_4_less: "complement_4 A \<le> complement_3 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complement_4 A \<le> complement_3 A
[PROOF STEP]
unfolding less_eq_nba_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (complement_4 A) \<subseteq> alphabet (complement_3 A) \<and> initial (complement_4 A) \<subseteq> initial (complement_3 A) \<and> transition (complement_4 A) \<le> transition (complement_3 A) \<and> accepting (complement_4 A) \<le> accepting (complement_3 A)
[PROOF STEP]
unfolding complement_4_def complement_3_def nba.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet A \<subseteq> alphabet A \<and> {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} \<subseteq> {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} \<and> complement_succ_4 A \<le> complement_succ_3 A \<and> (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y) \<le> (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y)
[PROOF STEP]
unfolding complement_succ_4_def complement_succ_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet A \<subseteq> alphabet A \<and> {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} \<subseteq> {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} \<and> (\<lambda>a. ((expand_map \<circ>\<circ> get_4) A \<circ>\<circ>\<circ> bounds_3) A a \<circ> refresh_1) \<le> (\<lambda>a. ((expand_map \<circ>\<circ> get_3) A \<circ>\<circ>\<circ> bounds_3) A a \<circ> refresh_1) \<and> (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y) \<le> (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y)
[PROOF STEP]
proof (safe intro!: le_funI, unfold comp_apply)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. xb \<in> expand_map (get_4 A (bounds_3 A x (refresh_1 xa))) \<Longrightarrow> xb \<in> expand_map (get_3 A (bounds_3 A x (refresh_1 xa)))
[PROOF STEP]
fix a f g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. xb \<in> expand_map (get_4 A (bounds_3 A x (refresh_1 xa))) \<Longrightarrow> xb \<in> expand_map (get_3 A (bounds_3 A x (refresh_1 xa)))
[PROOF STEP]
assume "g \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 f)))"
[PROOF STATE]
proof (state)
this:
g \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. \<And>x xa xb. xb \<in> expand_map (get_4 A (bounds_3 A x (refresh_1 xa))) \<Longrightarrow> xb \<in> expand_map (get_3 A (bounds_3 A x (refresh_1 xa)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
show "g \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
[PROOF STATE]
proof (prove)
using this:
g \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 f)))

goal (1 subgoal):
 1. g \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))
[PROOF STEP]
unfolding get_4_def get_3_def items_4_def items_3_def expand_map_alt_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = dom (\<lambda>p. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. k \<le> Suc l \<and> l \<le> k \<and> (accepting A p \<longrightarrow> even l)}) (bounds_3 A a (refresh_1 f) p)) \<and> (\<forall>x S y. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. k \<le> Suc l \<and> l \<le> k \<and> (accepting A x \<longrightarrow> even l)}) (bounds_3 A a (refresh_1 f) x) = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S)}

goal (1 subgoal):
 1. g \<in> {g. dom g = dom (\<lambda>p. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A p \<longrightarrow> even l)}) (bounds_3 A a (refresh_1 f) p)) \<and> (\<forall>x S y. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A x \<longrightarrow> even l)}) (bounds_3 A a (refresh_1 f) x) = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_4_language_2: "language (complement_4 A) \<subseteq> language (complement_3 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement_4 A) \<subseteq> language (complement_3 A)
[PROOF STEP]
using language_mono complement_4_less
[PROOF STATE]
proof (prove)
using this:
mono language
complement_4 ?A \<le> complement_3 ?A

goal (1 subgoal):
 1. language (complement_4 A) \<subseteq> language (complement_3 A)
[PROOF STEP]
by (auto dest: monoD)


[STATEMENT]
lemma complement_4_language: "language (complement_3 A) = language (complement_4 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement_3 A) = language (complement_4 A)
[PROOF STEP]
using complement_4_language_1 complement_4_language_2
[PROOF STATE]
proof (prove)
using this:
language (complement_3 ?A) \<subseteq> language (complement_4 ?A)
language (complement_4 ?A) \<subseteq> language (complement_3 ?A)

goal (1 subgoal):
 1. language (complement_3 A) = language (complement_4 A)
[PROOF STEP]
by blast


[STATEMENT]
lemma complement_4_finite[simp]:
    assumes "finite (nodes A)"
    shows "finite (nodes (complement_4 A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have "(nodes (complement_3 A), nodes (complement_2 A)) \<in> \<langle>Id\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nodes (complement_3 A), nodes (complement_2 A)) \<in> \<langle>Id\<rangle>set_rel
[PROOF STEP]
using complement_3_refine
[PROOF STATE]
proof (prove)
using this:
(complement_3, complement_2) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel

goal (1 subgoal):
 1. (nodes (complement_3 A), nodes (complement_2 A)) \<in> \<langle>Id\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(nodes (complement_3 A), nodes (complement_2 A)) \<in> \<langle>Id\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(nodes (complement_3 A), nodes (complement_2 A)) \<in> \<langle>Id\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have "(nodes (complement_2 A), nodes (complement_1 A)) \<in> \<langle>Id\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nodes (complement_2 A), nodes (complement_1 A)) \<in> \<langle>Id\<rangle>set_rel
[PROOF STEP]
using complement_2_refine
[PROOF STATE]
proof (prove)
using this:
(complement_2, complement_1) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel

goal (1 subgoal):
 1. (nodes (complement_2 A), nodes (complement_1 A)) \<in> \<langle>Id\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(nodes (complement_2 A), nodes (complement_1 A)) \<in> \<langle>Id\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(nodes (complement_2 A), nodes (complement_1 A)) \<in> \<langle>Id\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have "(nodes (complement_1 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nodes (complement_1 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel
[PROOF STEP]
using complement_1_refine
[PROOF STATE]
proof (prove)
using this:
(complement_1, complement) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, cs_rel\<rangle>nba_rel

goal (1 subgoal):
 1. (nodes (complement_1 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(nodes (complement_1 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(nodes (complement_3 A), nodes (complement A)) \<in> (\<langle>Id\<rangle>set_rel O \<langle>Id\<rangle>set_rel) O \<langle>cs_rel\<rangle>set_rel
[PROOF STEP]
have 1: "(nodes (complement_3 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
using this:
(nodes (complement_3 A), nodes (complement A)) \<in> (\<langle>Id\<rangle>set_rel O \<langle>Id\<rangle>set_rel) O \<langle>cs_rel\<rangle>set_rel

goal (1 subgoal):
 1. (nodes (complement_3 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(nodes (complement_3 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have 2: "finite (nodes (complement A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (complement A))
[PROOF STEP]
using complement_finite assms(1)
[PROOF STATE]
proof (prove)
using this:
finite (nodes ?A) \<Longrightarrow> finite (nodes (complement ?A))
finite (nodes A)

goal (1 subgoal):
 1. finite (nodes (complement A))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
finite (nodes (complement A))

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have 3: "finite (nodes (complement_3 A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (complement_3 A))
[PROOF STEP]
using finite_set_rel_transfer_back 1 cs_rel_inv_single_valued 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?s, ?s') \<in> \<langle>?R\<rangle>set_rel; single_valued (?R\<inverse>); finite ?s'\<rbrakk> \<Longrightarrow> finite ?s
(nodes (complement_3 A), nodes (complement A)) \<in> \<langle>cs_rel\<rangle>set_rel
single_valued (cs_rel\<inverse>)
finite (nodes (complement A))

goal (1 subgoal):
 1. finite (nodes (complement_3 A))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
finite (nodes (complement_3 A))

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
have 4: "nodes (complement_4 A) \<subseteq> nodes (complement_3 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (complement_4 A) \<subseteq> nodes (complement_3 A)
[PROOF STEP]
using nodes_mono complement_4_less
[PROOF STATE]
proof (prove)
using this:
mono nodes
complement_4 ?A \<le> complement_3 ?A

goal (1 subgoal):
 1. nodes (complement_4 A) \<subseteq> nodes (complement_3 A)
[PROOF STEP]
by (auto dest: monoD)
[PROOF STATE]
proof (state)
this:
nodes (complement_4 A) \<subseteq> nodes (complement_3 A)

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
show "finite (nodes (complement_4 A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
using finite_subset 4 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
nodes (complement_4 A) \<subseteq> nodes (complement_3 A)
finite (nodes (complement_3 A))

goal (1 subgoal):
 1. finite (nodes (complement_4 A))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
finite (nodes (complement_4 A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_4_correct:
    assumes "finite (nodes A)"
    shows "language (complement_4 A) = streams (alphabet A) - language A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
have "language (complement_4 A) = language (complement_3 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement_4 A) = language (complement_3 A)
[PROOF STEP]
using complement_4_language
[PROOF STATE]
proof (prove)
using this:
language (complement_3 ?A) = language (complement_4 ?A)

goal (1 subgoal):
 1. language (complement_4 A) = language (complement_3 A)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
language (complement_4 A) = language (complement_3 A)

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
language (complement_4 A) = language (complement_3 A)

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
have "(language (complement_3 A), language (complement_2 A)) \<in> \<langle>\<langle>Id\<rangle> stream_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language (complement_3 A), language (complement_2 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
using complement_3_refine
[PROOF STATE]
proof (prove)
using this:
(complement_3, complement_2) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel

goal (1 subgoal):
 1. (language (complement_3 A), language (complement_2 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(language (complement_3 A), language (complement_2 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(language (complement_3 A), language (complement_2 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
have "(language (complement_2 A), language (complement_1 A)) \<in> \<langle>\<langle>Id\<rangle> stream_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language (complement_2 A), language (complement_1 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
using complement_2_refine
[PROOF STATE]
proof (prove)
using this:
(complement_2, complement_1) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel

goal (1 subgoal):
 1. (language (complement_2 A), language (complement_1 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(language (complement_2 A), language (complement_1 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(language (complement_2 A), language (complement_1 A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
have "(language (complement_1 A), language (complement A)) \<in> \<langle>\<langle>Id\<rangle> stream_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language (complement_1 A), language (complement A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
using complement_1_refine
[PROOF STATE]
proof (prove)
using this:
(complement_1, complement) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, cs_rel\<rangle>nba_rel

goal (1 subgoal):
 1. (language (complement_1 A), language (complement A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(language (complement_1 A), language (complement A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(language (complement_1 A), language (complement A)) \<in> \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
have "language (complement A) = streams (alphabet A) - language A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language (complement A) = streams (alphabet A) - language A
[PROOF STEP]
using complement_language assms(1)
[PROOF STATE]
proof (prove)
using this:
finite (nodes ?A) \<Longrightarrow> language (complement ?A) = streams (alphabet ?A) - language ?A
finite (nodes A)

goal (1 subgoal):
 1. language (complement A) = streams (alphabet A) - language A
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
language (complement A) = streams (alphabet A) - language A

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(language (complement_4 A), streams (alphabet A) - language A) \<in> (\<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel O \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel) O \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
show "language (complement_4 A) = streams (alphabet A) - language A"
[PROOF STATE]
proof (prove)
using this:
(language (complement_4 A), streams (alphabet A) - language A) \<in> (\<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel O \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel) O \<langle>\<langle>Id\<rangle>stream_rel\<rangle>set_rel

goal (1 subgoal):
 1. language (complement_4 A) = streams (alphabet A) - language A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
language (complement_4 A) = streams (alphabet A) - language A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounds_3_empty: "bounds_3 A a Map.empty = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_3 A a Map.empty = Map.empty
[PROOF STEP]
unfolding bounds_3_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>q. if Some -` Map.empty ` pred A a q = {} then None else Some (\<Sqinter> (fst ` Some -` Map.empty ` pred A a q), \<Squnion> (snd ` Some -` Map.empty ` pred A a q))) = Map.empty
[PROOF STEP]
by auto


[STATEMENT]
lemma bounds_3_update: "bounds_3 A a (f (p \<mapsto> s)) =
    override_on (bounds_3 A a f) (Some \<circ> merge_5 s \<circ> bounds_3 A a (f (p := None))) (transition A a p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_3 A a (f(p \<mapsto> s)) = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bounds_3 A a (f(p \<mapsto> s)) x = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) x
[PROOF STEP]
note fun_upd_image[simp]
[PROOF STATE]
proof (state)
this:
?f(?x := ?y) ` ?A = (if ?x \<in> ?A then insert ?y (?f ` (?A - {?x})) else ?f ` ?A)

goal (1 subgoal):
 1. \<And>x. bounds_3 A a (f(p \<mapsto> s)) x = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) x
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bounds_3 A a (f(p \<mapsto> s)) x = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) x
[PROOF STEP]
show "bounds_3 A a (f (p \<mapsto> s)) q =
      override_on (bounds_3 A a f) (Some \<circ> merge_5 s \<circ> bounds_3 A a (f (p := None))) (transition A a p) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
proof (cases "q \<in> transition A a p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q \<in> transition A a p

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
define S where "S \<equiv> Some -` f ` (pred A a q - {p})"
[PROOF STATE]
proof (state)
this:
S \<equiv> Some -` f ` (pred A a q - {p})

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
have 1: "Some -` f (p := Some s) ` pred A a q = insert s S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some -` f(p \<mapsto> s) ` pred A a q = insert s S
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
q \<in> transition A a p

goal (1 subgoal):
 1. Some -` f(p \<mapsto> s) ` pred A a q = insert s S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
using this:
q \<in> transition A a p

goal (1 subgoal):
 1. Some -` f(p \<mapsto> s) ` pred A a q = insert s (Some -` f ` (pred A a q - {p}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some -` f(p \<mapsto> s) ` pred A a q = insert s S

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
have 2: "Some -` f (p := None) ` pred A a q = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some -` f(p := None) ` pred A a q = S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some -` f(p := None) ` pred A a q = Some -` f ` (pred A a q - {p})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some -` f(p := None) ` pred A a q = S

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
have "bounds_3 A a (f (p \<mapsto> s)) q = Some (\<Sqinter>(fst ` (insert s S)), \<Squnion>(snd ` (insert s S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_3 A a (f(p \<mapsto> s)) q = Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S))
[PROOF STEP]
unfolding bounds_3_def 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let S = insert s S in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bounds_3 A a (f(p \<mapsto> s)) q = Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S))

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bounds_3 A a (f(p \<mapsto> s)) q = Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S))

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
have "\<dots> = Some (merge_5 s (bounds_3 A a (f (p := None)) q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S)) = Some (merge_5 s (bounds_3 A a (f(p := None)) q))
[PROOF STEP]
unfolding 2 bounds_3_def merge_5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S)) = Some ((case s of (k, c) \<Rightarrow> \<lambda>x. case x of None \<Rightarrow> (k, c) | Some (l, d) \<Rightarrow> (k \<sqinter> l, c \<squnion> d)) (let S = S in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))))
[PROOF STEP]
by (cases s) (simp_all add: cInf_insert)
[PROOF STATE]
proof (state)
this:
Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S)) = Some (merge_5 s (bounds_3 A a (f(p := None)) q))

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Some (\<Sqinter> (fst ` insert s S), \<Squnion> (snd ` insert s S)) = Some (merge_5 s (bounds_3 A a (f(p := None)) q))

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
have "\<dots> = override_on (bounds_3 A a f) (Some \<circ> merge_5 s \<circ> bounds_3 A a (f (p := None)))
        (transition A a p) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (merge_5 s (bounds_3 A a (f(p := None)) q)) = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
q \<in> transition A a p

goal (1 subgoal):
 1. Some (merge_5 s (bounds_3 A a (f(p := None)) q)) = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (merge_5 s (bounds_3 A a (f(p := None)) q)) = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q

goal (2 subgoals):
 1. q \<in> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
 2. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q

goal (1 subgoal):
 1. bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q

goal (1 subgoal):
 1. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
q \<notin> transition A a p

goal (1 subgoal):
 1. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<notin> transition A a p
[PROOF STEP]
have "pred A a q \<inter> {x. x \<noteq> p} = pred A a q"
[PROOF STATE]
proof (prove)
using this:
q \<notin> transition A a p

goal (1 subgoal):
 1. pred A a q \<inter> {x. x \<noteq> p} = pred A a q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pred A a q \<inter> {x. x \<noteq> p} = pred A a q

goal (1 subgoal):
 1. q \<notin> transition A a p \<Longrightarrow> bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
q \<notin> transition A a p
pred A a q \<inter> {x. x \<noteq> p} = pred A a q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<notin> transition A a p
pred A a q \<inter> {x. x \<noteq> p} = pred A a q

goal (1 subgoal):
 1. bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q
[PROOF STEP]
by (simp add: bounds_3_def)
[PROOF STATE]
proof (state)
this:
bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bounds_3 A a (f(p \<mapsto> s)) q = override_on (bounds_3 A a f) (((Some \<circ>\<circ> merge_5) s \<circ>\<circ>\<circ> bounds_3 A) a (f(p := None))) (transition A a p) q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma refresh_5_refine: "(refresh_5, \<lambda> f. RETURN (refresh_1 f)) \<in> Id \<rightarrow> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (refresh_5, \<lambda>f. RETURN (refresh_1 f)) \<in> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (refresh_5 a', RETURN (refresh_1 a')) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
fix f :: "'a \<Rightarrow> item option"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (refresh_5 a', RETURN (refresh_1 a')) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
have 1: "(\<exists> (p, k, c) \<in> map_to_set f. c) \<longleftrightarrow> True \<in> snd ` ran f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>(p, k, c)\<in>map_to_set f. c) = (True \<in> snd ` ran f)
[PROOF STEP]
unfolding image_def map_to_set_def ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>(p, k, c)\<in>{(k, v). f k = Some v}. c) = (True \<in> {y. \<exists>x\<in>{b. \<exists>a. f a = Some b}. y = snd x})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<exists>(p, k, c)\<in>map_to_set f. c) = (True \<in> snd ` ran f)

goal (1 subgoal):
 1. \<And>a a'. (refresh_5 a', RETURN (refresh_1 a')) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
show "(refresh_5 f, RETURN (refresh_1 f)) \<in> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (refresh_5 f, RETURN (refresh_1 f)) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding refresh_5_def refresh_1_def 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if True \<in> snd ` ran f then RETURN f else ASSUME (finite (dom f)) \<bind> (\<lambda>_. FOREACH (map_to_set f) (\<lambda>(p, k, c) m. ASSERT (p \<notin> dom m) \<bind> (\<lambda>_. RETURN (m(p \<mapsto> (k, True))))) Map.empty), RETURN (if True \<in> snd ` ran f then f else map_option (apsnd \<top>) \<circ> f)) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by (refine_vcg FOREACH_rule_map_eq[where X = "\<lambda> m. map_option (apsnd \<top>) \<circ> m"]) (auto)
[PROOF STATE]
proof (state)
this:
(refresh_5 f, RETURN (refresh_1 f)) \<in> \<langle>Id\<rangle>nres_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounds_5_refine: "(bounds_5 A a, \<lambda> f. RETURN (bounds_3 A a f)) \<in> Id \<rightarrow> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bounds_5 A a, \<lambda>f. RETURN (bounds_3 A a f)) \<in> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding bounds_5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. ASSUME (\<forall>p. finite (transition A a p)) \<bind> (\<lambda>_. FOREACH (map_to_set f) (\<lambda>(p, s). FOREACH (transition A a p) (\<lambda>q f. RETURN (f(q \<mapsto> merge_5 s (f q))))) Map.empty)), \<lambda>f. RETURN (bounds_3 A a f)) \<in> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by
      (refine_vcg FOREACH_rule_map_eq[where X = "bounds_3 A a"] FOREACH_rule_insert_eq)
      (auto simp: override_on_insert bounds_3_empty bounds_3_update)


[STATEMENT]
lemma items_5_refine: "items_5 = items_4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. items_5 = items_4
[PROOF STEP]
unfolding items_5_def items_4_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A p (k, c). let values = if accepting A p then Set.filter even {k - 1..k} else {k - 1..k}; item = \<lambda>l. (l, c \<and> even l) in item ` values) = (\<lambda>A p (k, c). {(l, c \<and> even l) |l. k \<le> Suc l \<and> l \<le> k \<and> (accepting A p \<longrightarrow> even l)})
[PROOF STEP]
by (intro ext) (auto split: if_splits)


[STATEMENT]
lemma get_5_refine: "get_5 = get_4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_5 = get_4
[PROOF STEP]
unfolding get_5_def get_4_def items_5_refine
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A f p. map_option (items_4 A p) (f p)) = (\<lambda>A f p. map_option (items_4 A p) (f p))
[PROOF STEP]
by rule


[STATEMENT]
lemma expand_5_refine: "(expand_5 f, ASSERT (finite (dom f)) \<then> RETURN (expand_map f)) \<in> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (expand_5 f, ASSERT (finite (dom f)) \<bind> (\<lambda>_. RETURN (expand_map f))) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding expand_5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FOREACH (map_to_set f) (\<lambda>(x, S) X. ASSERT (\<forall>g\<in>X. x \<notin> dom g) \<bind> (\<lambda>_. ASSERT (\<forall>a\<in>S. \<forall>b\<in>S. a \<noteq> b \<longrightarrow> (\<lambda>g. g(x \<mapsto> a)) ` X \<inter> (\<lambda>g. g(x \<mapsto> b)) ` X = {}) \<bind> (\<lambda>_. RETURN (\<Union>y\<in>S. (\<lambda>g. g(x \<mapsto> y)) ` X)))) {Map.empty}, ASSERT (finite (dom f)) \<bind> (\<lambda>_. RETURN (expand_map f))) \<in> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by (refine_vcg FOREACH_rule_map_eq[where X = expand_map]) (auto dest!: expand_map_dom map_upd_eqD1)


[STATEMENT]
lemma complement_succ_5_refine: "(complement_succ_5, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in>
    Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_succ_5, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding complement_succ_5_def complement_succ_4_def get_5_refine comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A a f. refresh_5 f \<bind> (\<lambda>f. bounds_5 A a f \<bind> (\<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. expand_5 (get_4 A f)))), \<lambda>x xa xb. RETURN (expand_map (get_4 x (bounds_3 x xa (refresh_1 xb))))) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by (refine_vcg vcg1[OF refresh_5_refine] vcg1[OF bounds_5_refine] vcg0[OF expand_5_refine]) (auto)


[STATEMENT]
lemma expand_map_get_6_refine: "(expand_map_get_6, expand_5 \<circ>\<circ> get_5) \<in> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (expand_map_get_6, expand_5 \<circ>\<circ> get_5) \<in> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding expand_map_get_6_def expand_5_def get_5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A f. FOREACH (map_to_set f) (\<lambda>(k, v) X. ASSERT (\<forall>g\<in>X. k \<notin> dom g) \<bind> (\<lambda>_. ASSERT (\<forall>a\<in>items_5 A k v. \<forall>b\<in>items_5 A k v. a \<noteq> b \<longrightarrow> (\<lambda>g. g(k \<mapsto> a)) ` X \<inter> (\<lambda>g. g(k \<mapsto> b)) ` X = {}) \<bind> (\<lambda>_. RETURN (\<Union>y\<in>items_5 A k v. (\<lambda>g. g(k \<mapsto> y)) ` X)))) {Map.empty}, \<lambda>x. (\<lambda>f. FOREACH (map_to_set f) (\<lambda>(x, S) X. ASSERT (\<forall>g\<in>X. x \<notin> dom g) \<bind> (\<lambda>_. ASSERT (\<forall>a\<in>S. \<forall>b\<in>S. a \<noteq> b \<longrightarrow> (\<lambda>g. g(x \<mapsto> a)) ` X \<inter> (\<lambda>g. g(x \<mapsto> b)) ` X = {}) \<bind> (\<lambda>_. RETURN (\<Union>y\<in>S. (\<lambda>g. g(x \<mapsto> y)) ` X)))) {Map.empty}) \<circ> (\<lambda>f p. map_option (items_5 x p) (f p))) \<in> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by (auto intro: FOREACH_rule_map_map[param_fo])


[STATEMENT]
lemma complement_succ_6_refine:
    "(complement_succ_6, complement_succ_5) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_succ_6, complement_succ_5) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
unfolding complement_succ_6_def complement_succ_5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A a f. refresh_5 f \<bind> (\<lambda>f. bounds_5 A a f \<bind> (\<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. expand_map_get_6 A f))), \<lambda>A a f. refresh_5 f \<bind> (\<lambda>f. bounds_5 A a f \<bind> (\<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. expand_5 (get_5 A f))))) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel
[PROOF STEP]
by (refine_vcg vcg2[OF expand_map_get_6_refine]) (auto intro: refine_IdI)


[STATEMENT]
lemma [simp]: "finite (dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
using list_map_rel_finite fi
[PROOF STATE]
proof (prove)
using this:
finite_map_rel (\<langle>?Rk, ?Rv\<rangle>list_map_rel)
(fi, f) \<in> state_rel

goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
unfolding finite_map_rel_def
[PROOF STATE]
proof (prove)
using this:
Range (\<langle>?Rk, ?Rv\<rangle>list_map_rel) \<subseteq> Collect (finite \<circ> dom)
(fi, f) \<in> state_rel

goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
by force


[STATEMENT]
lemma refresh_7_refine: "(\<lambda> f. RETURN (refresh_7 f), refresh_5) \<in> state_rel \<rightarrow> \<langle>state_rel\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f. RETURN (refresh_7 f), refresh_5) \<in> state_rel \<rightarrow> \<langle>state_rel\<rangle>nres_rel
[PROOF STEP]
using refresh_7.refine
[PROOF STATE]
proof (prove)
using this:
(?fi, ?f) \<in> state_rel \<Longrightarrow> (RETURN (refresh_7 ?fi), refresh_5 ?f) \<in> \<langle>state_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (\<lambda>f. RETURN (refresh_7 f), refresh_5) \<in> state_rel \<rightarrow> \<langle>state_rel\<rangle>nres_rel
[PROOF STEP]
by fast


[STATEMENT]
lemma [simp]: "finite (transition A a p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (transition A a p)
[PROOF STEP]
using list_set_rel_finite succi[param_fo]
[PROOF STATE]
proof (prove)
using this:
finite_set_rel (\<langle>?R\<rangle>list_set_rel)
(?x, ?x') \<in> nat_rel \<Longrightarrow> (succi ?x, transition A a ?x') \<in> \<langle>nat_rel\<rangle>list_set_rel

goal (1 subgoal):
 1. finite (transition A a p)
[PROOF STEP]
unfolding finite_set_rel_def
[PROOF STATE]
proof (prove)
using this:
Range (\<langle>?R\<rangle>list_set_rel) \<subseteq> Collect finite
(?x, ?x') \<in> nat_rel \<Longrightarrow> (succi ?x, transition A a ?x') \<in> \<langle>nat_rel\<rangle>list_set_rel

goal (1 subgoal):
 1. finite (transition A a p)
[PROOF STEP]
by blast


[STATEMENT]
lemma [simp]: "finite (dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
using fi
[PROOF STATE]
proof (prove)
using this:
(fi, f) \<in> state_rel

goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
by force


[STATEMENT]
lemma [autoref_rules]: "(min, min) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (min, min) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma bounds_7_refine: "(si, transition A a) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle> list_set_rel \<Longrightarrow>
    (\<lambda> p. RETURN (bounds_7 si p), bounds_5 A a) \<in>
    state_rel \<rightarrow> \<langle>\<langle>nat_rel, item_rel\<rangle> dflt_ahm_rel\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (si, transition A a) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>list_set_rel \<Longrightarrow> (\<lambda>p. RETURN (bounds_7 si p), bounds_5 A a) \<in> state_rel \<rightarrow> \<langle>\<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel\<rangle>nres_rel
[PROOF STEP]
using bounds_7.refine
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?succi, transition ?A ?a) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>list_set_rel; (?fi, ?f) \<in> state_rel\<rbrakk> \<Longrightarrow> (RETURN (bounds_7 ?succi ?fi), bounds_5 ?A ?a ?f) \<in> \<langle>\<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (si, transition A a) \<in> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>list_set_rel \<Longrightarrow> (\<lambda>p. RETURN (bounds_7 si p), bounds_5 A a) \<in> state_rel \<rightarrow> \<langle>\<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel\<rangle>nres_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma [autoref_op_pat]: "accepting A \<equiv> OP (accepting A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accepting A \<equiv> OP (accepting A)
[PROOF STEP]
by simp


[STATEMENT]
lemma [autoref_rules]: "((dvd), (dvd)) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((dvd), (dvd)) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> bool_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma [autoref_rules]: "(\<lambda> k l. upt k (Suc l), atLeastAtMost) \<in>
      nat_rel \<rightarrow> nat_rel \<rightarrow> \<langle>nat_rel\<rangle> list_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k l. [k..<Suc l], atLeastAtMost) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> \<langle>nat_rel\<rangle>list_set_rel
[PROOF STEP]
by (auto simp: list_set_rel_def in_br_conv)


[STATEMENT]
lemma [simp]: "finite (dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
using dflt_ahm_rel_finite_nat fi
[PROOF STATE]
proof (prove)
using this:
finite_map_rel (\<langle>nat_rel, ?V\<rangle>dflt_ahm_rel)
(fi, f) \<in> \<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel

goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
unfolding finite_map_rel_def
[PROOF STATE]
proof (prove)
using this:
Range (\<langle>nat_rel, ?V\<rangle>dflt_ahm_rel) \<subseteq> Collect (finite \<circ> dom)
(fi, f) \<in> \<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel

goal (1 subgoal):
 1. finite (dom f)
[PROOF STEP]
by force


[STATEMENT]
lemma [simp]:
      assumes "\<And> m. m \<in> S \<Longrightarrow> x \<notin> dom m"
      shows "inj_on (\<lambda> m. m (x \<mapsto> y)) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>m. m(x \<mapsto> y)) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?m \<in> S \<Longrightarrow> x \<notin> dom ?m

goal (1 subgoal):
 1. inj_on (\<lambda>m. m(x \<mapsto> y)) S
[PROOF STEP]
unfolding dom_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
?m \<in> S \<Longrightarrow> x \<notin> {a. ?m a \<noteq> None}

goal (1 subgoal):
 1. \<forall>xa\<in>S. \<forall>ya\<in>S. xa(x \<mapsto> y) = ya(x \<mapsto> y) \<longrightarrow> xa = ya
[PROOF STEP]
by (auto) (metis fun_upd_triv fun_upd_upd)


[STATEMENT]
lemma [autoref_op_pat]: "items_5 A \<equiv> OP (items_5 A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. items_5 A \<equiv> OP (items_5 A)
[PROOF STEP]
by simp


[STATEMENT]
lemma expand_map_get_7_refine:
    assumes "(ai, accepting A) \<in> nat_rel \<rightarrow> bool_rel"
    shows "(\<lambda> fi. RETURN (expand_map_get_7 ai fi),
      \<lambda> f. ASSUME (finite (dom f)) \<then> expand_map_get_6 A f) \<in>
      \<langle>nat_rel, item_rel\<rangle> dflt_ahm_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle> list_set_rel\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>fi. RETURN (expand_map_get_7 ai fi), \<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. expand_map_get_6 A f)) \<in> \<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel
[PROOF STEP]
using expand_map_get_7.refine[OF assms]
[PROOF STATE]
proof (prove)
using this:
(?fi, ?f) \<in> \<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel \<Longrightarrow> (RETURN (expand_map_get_7 ai ?fi), expand_map_get_6 A ?f) \<in> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (\<lambda>fi. RETURN (expand_map_get_7 ai fi), \<lambda>f. ASSUME (finite (dom f)) \<bind> (\<lambda>_. expand_map_get_6 A f)) \<in> \<langle>nat_rel, item_rel\<rangle>dflt_ahm_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma [autoref_op_pat]: "(\<lambda> g. ASSUME (finite (dom g)) \<then> expand_map_get_6 A g) \<equiv>
      OP (\<lambda> g. ASSUME (finite (dom g)) \<then> expand_map_get_6 A g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>g. ASSUME (finite (dom g)) \<bind> (\<lambda>_. expand_map_get_6 A g) \<equiv> OP (\<lambda>g. ASSUME (finite (dom g)) \<bind> (\<lambda>_. expand_map_get_6 A g))
[PROOF STEP]
by simp


[STATEMENT]
lemma [autoref_op_pat]: "bounds_5 A a \<equiv> OP (bounds_5 A a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounds_5 A a \<equiv> OP (bounds_5 A a)
[PROOF STEP]
by simp


[STATEMENT]
lemma complement_succ_7_refine:
    "(RETURN \<circ>\<circ>\<circ> complement_succ_7, complement_succ_6) \<in>
      \<langle>Id, Id\<rangle> nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow>
      \<langle>\<langle>state_rel\<rangle> list_set_rel\<rangle> nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RETURN \<circ>\<circ>\<circ> complement_succ_7, complement_succ_6) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel
[PROOF STEP]
using complement_succ_7.refine
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?Ai, ?A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel; (?ai, ?a) \<in> Id; (?pi, ?p) \<in> state_rel\<rbrakk> \<Longrightarrow> (RETURN (complement_succ_7 ?Ai ?ai ?pi), complement_succ_6 ?A ?a ?p) \<in> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (RETURN \<circ>\<circ>\<circ> complement_succ_7, complement_succ_6) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel
[PROOF STEP]
unfolding comp_apply
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?Ai, ?A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel; (?ai, ?a) \<in> Id; (?pi, ?p) \<in> state_rel\<rbrakk> \<Longrightarrow> (RETURN (complement_succ_7 ?Ai ?ai ?pi), complement_succ_6 ?A ?a ?p) \<in> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (\<lambda>x xa xb. RETURN (complement_succ_7 x xa xb), complement_succ_6) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma [autoref_op_pat]: "initial A \<equiv> OP (initial A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. initial A \<equiv> OP (initial A)
[PROOF STEP]
by simp


[STATEMENT]
lemma complement_7_refine[autoref_rules]:
    assumes "(Ai, A) \<in> \<langle>Id, Id\<rangle> nbai_nba_rel"
    assumes "(ni,
      (OP card ::: \<langle>Id\<rangle> ahs_rel bhc \<rightarrow> nat_rel) $
      ((OP nodes ::: \<langle>Id, Id\<rangle> nbai_nba_rel \<rightarrow> \<langle>Id\<rangle> ahs_rel bhc) $ A)) \<in> nat_rel"
    shows "(complement_7 Ai ni, (OP complement_4 :::
      \<langle>Id, Id\<rangle> nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle> nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle> nbai_nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
note complement_succ_7_refine
[PROOF STATE]
proof (state)
this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, complement_succ_6) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, complement_succ_6) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
note complement_succ_6_refine
[PROOF STATE]
proof (state)
this:
(complement_succ_6, complement_succ_5) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(complement_succ_6, complement_succ_5) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
note complement_succ_5_refine
[PROOF STATE]
proof (state)
this:
(complement_succ_5, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> (\<langle>Id, nat_rel\<rangle>nbai_nba_rel O Id) O Id \<rightarrow> (Id O Id) O Id \<rightarrow> (state_rel O Id) O Id \<rightarrow> (\<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel O \<langle>Id\<rangle>nres_rel) O \<langle>Id\<rangle>nres_rel
[PROOF STEP]
have 1: "(complement_succ_7, complement_succ_4) \<in>
      \<langle>Id, Id\<rangle> nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle> list_set_rel"
[PROOF STATE]
proof (prove)
using this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> (\<langle>Id, nat_rel\<rangle>nbai_nba_rel O Id) O Id \<rightarrow> (Id O Id) O Id \<rightarrow> (state_rel O Id) O Id \<rightarrow> (\<langle>\<langle>state_rel\<rangle>list_set_rel\<rangle>nres_rel O \<langle>Id\<rangle>nres_rel) O \<langle>Id\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel
[PROOF STEP]
unfolding nres_rel_comp
[PROOF STATE]
proof (prove)
using this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> (\<langle>Id, nat_rel\<rangle>nbai_nba_rel O Id) O Id \<rightarrow> (Id O Id) O Id \<rightarrow> (state_rel O Id) O Id \<rightarrow> \<langle>(\<langle>state_rel\<rangle>list_set_rel O Id) O Id\<rangle>nres_rel

goal (1 subgoal):
 1. (complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel
[PROOF STEP]
unfolding nres_rel_def
[PROOF STATE]
proof (prove)
using this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> (\<langle>Id, nat_rel\<rangle>nbai_nba_rel O Id) O Id \<rightarrow> (Id O Id) O Id \<rightarrow> (state_rel O Id) O Id \<rightarrow> {(c, a). c \<le> \<Down> ((\<langle>state_rel\<rangle>list_set_rel O Id) O Id) a}

goal (1 subgoal):
 1. (complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel
[PROOF STEP]
unfolding fun_rel_def
[PROOF STATE]
proof (prove)
using this:
(RETURN \<circ>\<circ>\<circ> complement_succ_7, RETURN \<circ>\<circ>\<circ> complement_succ_4) \<in> {(f, f'). \<forall>(a, a')\<in>(\<langle>Id, nat_rel\<rangle>nbai_nba_rel O Id) O Id. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>(Id O Id) O Id. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>(state_rel O Id) O Id. (f a, f' a') \<in> {(c, a). c \<le> \<Down> ((\<langle>state_rel\<rangle>list_set_rel O Id) O Id) a}}}}

goal (1 subgoal):
 1. (complement_succ_7, complement_succ_4) \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>Id, nat_rel\<rangle>nbai_nba_rel. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>Id. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>state_rel. (f a, f' a') \<in> \<langle>state_rel\<rangle>list_set_rel}}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel

goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
unfolding complement_7_def complement_4_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbai (alphabeti Ai) (complement_initial_7 Ai ni) (complement_succ_7 Ai) complement_accepting_7, (OP (\<lambda>A. nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c)) ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
using 1 complement_initial_7.refine complement_accepting_7.refine assms
[PROOF STATE]
proof (prove)
using this:
(complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel
\<lbrakk>(?Ai, ?A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel; (?ni, ?n) \<in> nat_rel\<rbrakk> \<Longrightarrow> (complement_initial_7 ?Ai ?ni, {(Some \<circ> (\<lambda>_. (2 * ?n, False))) |` initial ?A}) \<in> \<langle>state_rel\<rangle>list_set_rel
(complement_accepting_7, \<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c) \<in> state_rel \<rightarrow> bool_rel
(Ai, A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel
(ni, (OP card ::: \<langle>nat_rel\<rangle>ahs_rel bhc \<rightarrow> nat_rel) $ ((OP nodes ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>nat_rel\<rangle>ahs_rel bhc) $ A)) \<in> nat_rel

goal (1 subgoal):
 1. (nbai (alphabeti Ai) (complement_initial_7 Ai ni) (complement_succ_7 Ai) complement_accepting_7, (OP (\<lambda>A. nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c)) ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
unfolding autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
(complement_succ_7, complement_succ_4) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> Id \<rightarrow> state_rel \<rightarrow> \<langle>state_rel\<rangle>list_set_rel
\<lbrakk>(?Ai, ?A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel; (?ni, ?n) \<in> nat_rel\<rbrakk> \<Longrightarrow> (complement_initial_7 ?Ai ?ni, {(Some \<circ> (\<lambda>_. (2 * ?n, False))) |` initial ?A}) \<in> \<langle>state_rel\<rangle>list_set_rel
(complement_accepting_7, \<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c) \<in> state_rel \<rightarrow> bool_rel
(Ai, A) \<in> \<langle>Id, nat_rel\<rangle>nbai_nba_rel
(ni, card (nodes A)) \<in> nat_rel

goal (1 subgoal):
 1. (nbai (alphabeti Ai) (complement_initial_7 Ai ni) (complement_succ_7 Ai) complement_accepting_7, nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_4 A) (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y)) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(complement_7 Ai ni, (OP complement_4 ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, state_rel\<rangle>nbai_nba_rel) $ A) \<in> \<langle>Id, state_rel\<rangle>nbai_nba_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_slice_aux_length: "\<And>xs. length (list_slice_aux xs k n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. length (list_slice_aux xs k n) = n
[PROOF STEP]
by (induct n, simp+)


[STATEMENT]
lemma list_slice_aux_nth: "
 \<And>m xs. m < n \<Longrightarrow> (list_slice_aux xs k n) ! m = (xs \<up> (m * k) \<down> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m xs. m < n \<Longrightarrow> list_slice_aux xs k n ! m = xs \<up> (m * k) \<down> k
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m xs. m < 0 \<Longrightarrow> list_slice_aux xs k 0 ! m = xs \<up> (m * k) \<down> k
 2. \<And>n m xs. \<lbrakk>\<And>m xs. m < n \<Longrightarrow> list_slice_aux xs k n ! m = xs \<up> (m * k) \<down> k; m < Suc n\<rbrakk> \<Longrightarrow> list_slice_aux xs k (Suc n) ! m = xs \<up> (m * k) \<down> k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m xs. \<lbrakk>\<And>m xs. m < n \<Longrightarrow> list_slice_aux xs k n ! m = xs \<up> (m * k) \<down> k; m < Suc n\<rbrakk> \<Longrightarrow> list_slice_aux xs k (Suc n) ! m = xs \<up> (m * k) \<down> k
[PROOF STEP]
apply (simp add: nth_Cons' diff_mult_distrib)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_length: "length (list_slice xs k) = length xs div k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_slice xs k) = length xs div k
[PROOF STEP]
by (simp add: list_slice_def list_slice_aux_length)


[STATEMENT]
lemma list_slice_0: "list_slice xs 0 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice xs 0 = []
[PROOF STEP]
by (simp add: list_slice_def)


[STATEMENT]
lemma list_slice_1: "list_slice xs (Suc 0) = map (\<lambda>x. [x]) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice xs (Suc 0) = map (\<lambda>x. [x]) xs
[PROOF STEP]
by (fastforce simp: list_eq_iff list_slice_def list_slice_aux_nth list_slice_aux_length)


[STATEMENT]
lemma list_slice_less: "length xs < k \<Longrightarrow> list_slice xs k = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs < k \<Longrightarrow> list_slice xs k = []
[PROOF STEP]
by (simp add: list_slice_def)


[STATEMENT]
lemma list_slice_Nil: "list_slice [] k = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_slice [] k = []
[PROOF STEP]
by (simp add: list_slice_def)


[STATEMENT]
lemma list_slice_nth: "
  m < length xs div k \<Longrightarrow> list_slice xs k ! m = xs \<up> (m * k) \<down> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> list_slice xs k ! m = xs \<up> (m * k) \<down> k
[PROOF STEP]
by (simp add: list_slice_def list_slice_aux_nth)


[STATEMENT]
lemma list_slice_nth_length: "
  m < length xs div k \<Longrightarrow> length ((list_slice xs k) ! m) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> length (list_slice xs k ! m) = k
[PROOF STEP]
apply (case_tac "length xs < k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m < length xs div k; length xs < k\<rbrakk> \<Longrightarrow> length (list_slice xs k ! m) = k
 2. \<lbrakk>m < length xs div k; \<not> length xs < k\<rbrakk> \<Longrightarrow> length (list_slice xs k ! m) = k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; \<not> length xs < k\<rbrakk> \<Longrightarrow> length (list_slice xs k ! m) = k
[PROOF STEP]
apply (simp add: list_slice_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; \<not> length xs < k\<rbrakk> \<Longrightarrow> min (length xs - m * k) k = k
[PROOF STEP]
thm less_div_imp_mult_add_divisor_le
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < length xs div k; \<not> length xs < k\<rbrakk> \<Longrightarrow> min (length xs - m * k) k = k
[PROOF STEP]
apply (drule less_div_imp_mult_add_divisor_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> length xs < k; m * k + k \<le> length xs\<rbrakk> \<Longrightarrow> min (length xs - m * k) k = k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_slice_nth_eq_sublist_list: "
  m < length xs div k \<Longrightarrow> list_slice xs k ! m = sublist_list xs [m * k..<m * k + k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> list_slice xs k ! m = sublist_list xs [m * k..<m * k + k]
[PROOF STEP]
apply (simp add: list_slice_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> xs \<up> (m * k) \<down> k = sublist_list xs [m * k..<m * k + k]
[PROOF STEP]
apply (rule take_drop_eq_sublist_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < length xs div k \<Longrightarrow> m * k + k \<le> length xs
[PROOF STEP]
apply (rule less_div_imp_mult_add_divisor_le, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done