[STATEMENT]
lemma complement_succ_1_refine: "(complement_succ_1, complement_succ) \<in>
    Id \<rightarrow> Id \<rightarrow> cs_rel \<rightarrow> \<langle>cs_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_succ_1, complement_succ) \<in> Id \<rightarrow> Id \<rightarrow> cs_rel \<rightarrow> \<langle>cs_rel\<rangle>set_rel
[PROOF STEP]
proof (clarsimp simp: br_set_rel_alt in_br_conv)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' a'a ab. complement_succ a' a'a (cs_abs ab) = cs_abs ` complement_succ_1 a' a'a ab
[PROOF STEP]
fix A :: "('a, 'b) nba"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' a'a ab. complement_succ a' a'a (cs_abs ab) = cs_abs ` complement_succ_1 a' a'a ab
[PROOF STEP]
fix a f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' a'a ab. complement_succ a' a'a (cs_abs ab) = cs_abs ` complement_succ_1 a' a'a ab
[PROOF STEP]
show "complement_succ A a (cs_abs f) = cs_abs ` complement_succ_1 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complement_succ A a (cs_abs f) = cs_abs ` complement_succ_1 A a f
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa b. (aa, b) \<in> complement_succ A a (cs_abs f) \<Longrightarrow> (aa, b) \<in> cs_abs ` complement_succ_1 A a f
 2. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
fix g Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa b. (aa, b) \<in> complement_succ A a (cs_abs f) \<Longrightarrow> (aa, b) \<in> cs_abs ` complement_succ_1 A a f
 2. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
assume 1: "(g, Q) \<in> complement_succ A a (cs_abs f)"
[PROOF STATE]
proof (state)
this:
(g, Q) \<in> complement_succ A a (cs_abs f)

goal (2 subgoals):
 1. \<And>aa b. (aa, b) \<in> complement_succ A a (cs_abs f) \<Longrightarrow> (aa, b) \<in> cs_abs ` complement_succ_1 A a f
 2. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
have 2: "Q \<subseteq> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<subseteq> dom g
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> complement_succ A a (cs_abs f)

goal (1 subgoal):
 1. Q \<subseteq> dom g
[PROOF STEP]
unfolding complement_succ_def lr_succ_def st_succ_def
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> (case cs_abs f of (f, P) \<Rightarrow> {(g, {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}) |g. g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p)) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (the (g q)))}})

goal (1 subgoal):
 1. Q \<subseteq> dom g
[PROOF STEP]
by (auto) (metis IntE cs_abs_rep cs_lr_dom cs_rep_st)
[PROOF STATE]
proof (state)
this:
Q \<subseteq> dom g

goal (2 subgoals):
 1. \<And>aa b. (aa, b) \<in> complement_succ A a (cs_abs f) \<Longrightarrow> (aa, b) \<in> cs_abs ` complement_succ_1 A a f
 2. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
have 3: "cs_st f \<subseteq> dom (cs_lr f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st f \<subseteq> dom (cs_lr f)
[PROOF STEP]
unfolding cs_st_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` Some ` snd -` {True} \<subseteq> dom (cs_lr f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs_st f \<subseteq> dom (cs_lr f)

goal (2 subgoals):
 1. \<And>aa b. (aa, b) \<in> complement_succ A a (cs_abs f) \<Longrightarrow> (aa, b) \<in> cs_abs ` complement_succ_1 A a f
 2. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
show "(g, Q) \<in> cs_abs ` complement_succ_1 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g, Q) \<in> cs_abs ` complement_succ_1 A a f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (g, Q) = cs_abs ?x
 2. ?x \<in> complement_succ_1 A a f
[PROOF STEP]
show "(g, Q) = cs_abs (cs_rep (g, Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g, Q) = cs_abs (cs_rep (g, Q))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
Q \<subseteq> dom g

goal (1 subgoal):
 1. (g, Q) = cs_abs (cs_rep (g, Q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(g, Q) = cs_abs (cs_rep (g, Q))

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
have "cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (cs_abs f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (cs_abs f))
[PROOF STEP]
using complement_succ_1_rep 3 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P \<subseteq> dom ?f; (?g, ?Q) \<in> complement_succ ?A ?a (?f, ?P)\<rbrakk> \<Longrightarrow> cs_rep (?g, ?Q) \<in> complement_succ_1 ?A ?a (cs_rep (?f, ?P))
cs_st f \<subseteq> dom (cs_lr f)
(g, Q) \<in> complement_succ A a (cs_abs f)

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (cs_abs f))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (cs_abs f))

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (cs_abs f))

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
have "cs_rep (cs_abs f) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (cs_abs f) = f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs_rep (cs_abs f) = f

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
show "cs_rep (g, Q) \<in> complement_succ_1 A a f"
[PROOF STATE]
proof (prove)
using this:
cs_rep (g, Q) \<in> complement_succ_1 A a f

goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a f
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_rep (g, Q) \<in> complement_succ_1 A a f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(g, Q) \<in> cs_abs ` complement_succ_1 A a f

goal (1 subgoal):
 1. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
assume 1: "g \<in> complement_succ_1 A a f"
[PROOF STATE]
proof (state)
this:
g \<in> complement_succ_1 A a f

goal (1 subgoal):
 1. \<And>aa b fa. fa \<in> complement_succ_1 A a f \<Longrightarrow> cs_abs fa \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
show "cs_abs g \<in> complement_succ A a (cs_abs f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_abs g \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
using complement_succ_1_abs 1
[PROOF STATE]
proof (prove)
using this:
?g \<in> complement_succ_1 ?A ?a ?f \<Longrightarrow> cs_abs ?g \<in> complement_succ ?A ?a (cs_abs ?f)
g \<in> complement_succ_1 A a f

goal (1 subgoal):
 1. cs_abs g \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_abs g \<in> complement_succ A a (cs_abs f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
complement_succ A a (cs_abs f) = cs_abs ` complement_succ_1 A a f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ranks_2_refine: "ranks_2 = ranks_1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranks_2 = ranks_1
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. ranks_2 x xa xb = ranks_1 x xa xb
[PROOF STEP]
fix A :: "('a, 'b) nba" and a f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. ranks_2 x xa xb = ranks_1 x xa xb
[PROOF STEP]
show "ranks_2 A a f = ranks_1 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranks_2 A a f = ranks_1 A a f
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
assume 1: "g \<in> ranks_2 A a f"
[PROOF STATE]
proof (state)
this:
g \<in> ranks_2 A a f

goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 2: "dom g = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_2 A a f

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
unfolding ranks_2_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))}

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 3: "g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)" for q l d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_2 A a f

goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
unfolding ranks_2_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))}

goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g ?q = Some (?l, ?d) \<Longrightarrow> ?l \<le> \<Sqinter> (fst ` Some -` f ` pred A a ?q)

goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 4: "g q = Some (l, d) \<Longrightarrow> d \<longleftrightarrow> \<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l" for q l d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_2 A a f

goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
unfolding ranks_2_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))}

goal (1 subgoal):
 1. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g ?q = Some (?l, ?d) \<Longrightarrow> ?d = (\<Squnion> (snd ` Some -` f ` pred A a ?q) \<and> even ?l)

goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 5: "g q = Some (l, d) \<Longrightarrow> accepting A q \<Longrightarrow> even l" for q l d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_2 A a f

goal (1 subgoal):
 1. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
unfolding ranks_2_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))}

goal (1 subgoal):
 1. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>g ?q = Some (?l, ?d); accepting A ?q\<rbrakk> \<Longrightarrow> even ?l

goal (2 subgoals):
 1. \<And>x. x \<in> ranks_2 A a f \<Longrightarrow> x \<in> ranks_1 A a f
 2. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
show "g \<in> ranks_1 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> ranks_1 A a f
[PROOF STEP]
unfolding ranks_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}
[PROOF STEP]
proof (intro CollectI conjI ballI impI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. dom g = \<Union> (transition A a ` dom f)
 2. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 3. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 4. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
show "dom g = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
assume 10: "p \<in> dom f" "q \<in> transition A a p"
[PROOF STATE]
proof (state)
this:
p \<in> dom f
q \<in> transition A a p

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
obtain k c where 11: "f p = Some (k, c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k c. f p = Some (k, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 10(1)
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f

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

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
have 12: "q \<in> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> dom g
[PROOF STEP]
using 10 2
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f
q \<in> transition A a p
dom g = \<Union> (transition A a ` dom f)

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

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
obtain l d where 13: "g q = Some (l, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l d. g q = Some (l, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 12
[PROOF STATE]
proof (prove)
using this:
q \<in> dom g

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

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
have "fst (the (g q)) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (g q)) = l
[PROOF STEP]
unfolding 13
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (Some (l, d))) = l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (the (g q)) = l

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst (the (g q)) = l

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
have "\<dots> \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
using 3 13
[PROOF STATE]
proof (prove)
using this:
g ?q = Some (?l, ?d) \<Longrightarrow> ?l \<le> \<Sqinter> (fst ` Some -` f ` pred A a ?q)
g q = Some (l, d)

goal (1 subgoal):
 1. l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
have "\<dots> \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (fst ` Some -` f ` pred A a q) \<le> k
[PROOF STEP]
proof (rule cInf_lower)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> fst ` Some -` f ` pred A a q
 2. bdd_below (fst ` Some -` f ` pred A a q)
[PROOF STEP]
show "k \<in> fst ` Some -` f ` pred A a q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> fst ` Some -` f ` pred A a q
[PROOF STEP]
using 11 10(2)
[PROOF STATE]
proof (prove)
using this:
f p = Some (k, c)
q \<in> transition A a p

goal (1 subgoal):
 1. k \<in> fst ` Some -` f ` pred A a q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
k \<in> fst ` Some -` f ` pred A a q

goal (1 subgoal):
 1. bdd_below (fst ` Some -` f ` pred A a q)
[PROOF STEP]
show "bdd_below (fst ` Some -` f ` pred A a q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below (fst ` Some -` f ` pred A a q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bdd_below (fst ` Some -` f ` pred A a q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sqinter> (fst ` Some -` f ` pred A a q) \<le> k

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sqinter> (fst ` Some -` f ` pred A a q) \<le> k

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
have "\<dots> = fst (the (f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = fst (the (f p))
[PROOF STEP]
unfolding 11
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = fst (the (Some (k, c)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = fst (the (f p))

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
 2. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 3. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fst (the (g q)) \<le> fst (the (f p))
[PROOF STEP]
show "fst (the (g q)) \<le> fst (the (f p))"
[PROOF STATE]
proof (prove)
using this:
fst (the (g q)) \<le> fst (the (f p))

goal (1 subgoal):
 1. fst (the (g q)) \<le> fst (the (f p))
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
fst (the (g q)) \<le> fst (the (f p))

goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 2. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 2. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 2. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
assume 10: "q \<in> dom g" "accepting A q"
[PROOF STATE]
proof (state)
this:
q \<in> dom g
accepting A q

goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
 2. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
show "even (fst (the (g q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (fst (the (g q)))
[PROOF STEP]
using 10 5
[PROOF STATE]
proof (prove)
using this:
q \<in> dom g
accepting A q
\<lbrakk>g ?q = Some (?l, ?d); accepting A ?q\<rbrakk> \<Longrightarrow> even ?l

goal (1 subgoal):
 1. even (fst (the (g q)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (fst (the (g q)))

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
show "cs_st g = {q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs_st g \<subseteq> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
 2. {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} \<subseteq> cs_st g
[PROOF STEP]
show "cs_st g \<subseteq> {q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g \<subseteq> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
g ?q = Some (?l, ?d) \<Longrightarrow> ?d = (\<Squnion> (snd ` Some -` f ` pred A a ?q) \<and> even ?l)

goal (1 subgoal):
 1. cs_st g \<subseteq> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
unfolding cs_st_def image_def vimage_def
[PROOF STATE]
proof (prove)
using this:
g ?q = Some (?l, ?d) \<Longrightarrow> ?d = (\<Squnion> {y. \<exists>x\<in>{x. Some x \<in> {y. \<exists>x\<in>pred A a ?q. y = f x}}. y = snd x} \<and> even ?l)

goal (1 subgoal):
 1. {x. g x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}} \<subseteq> {q \<in> \<Union> {y. \<exists>x\<in>{x. f x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}}. y = transition A a x}. even (fst (the (g q)))}
[PROOF STEP]
by auto metis+
[PROOF STATE]
proof (state)
this:
cs_st g \<subseteq> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} \<subseteq> cs_st g
[PROOF STEP]
show "{q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))} \<subseteq> cs_st g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} \<subseteq> cs_st g
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>even (fst (the (g x))); xa \<in> cs_st f; x \<in> transition A a xa\<rbrakk> \<Longrightarrow> x \<in> cs_st g
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>even (fst (the (g x))); xa \<in> cs_st f; x \<in> transition A a xa\<rbrakk> \<Longrightarrow> x \<in> cs_st g
[PROOF STEP]
assume 10: "even (fst (the (g q)))" "p \<in> cs_st f" "q \<in> transition A a p"
[PROOF STATE]
proof (state)
this:
even (fst (the (g q)))
p \<in> cs_st f
q \<in> transition A a p

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>even (fst (the (g x))); xa \<in> cs_st f; x \<in> transition A a xa\<rbrakk> \<Longrightarrow> x \<in> cs_st g
[PROOF STEP]
have 12: "q \<in> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> dom g
[PROOF STEP]
using 10 2
[PROOF STATE]
proof (prove)
using this:
even (fst (the (g q)))
p \<in> cs_st f
q \<in> transition A a p
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. q \<in> dom g
[PROOF STEP]
unfolding cs_st_def
[PROOF STATE]
proof (prove)
using this:
even (fst (the (g q)))
p \<in> f -` Some ` snd -` {True}
q \<in> transition A a p
dom g = \<Union> (transition A a ` dom f)

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

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>even (fst (the (g x))); xa \<in> cs_st f; x \<in> transition A a xa\<rbrakk> \<Longrightarrow> x \<in> cs_st g
[PROOF STEP]
show "q \<in> cs_st g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> cs_st g
[PROOF STEP]
using 10 4 12
[PROOF STATE]
proof (prove)
using this:
even (fst (the (g q)))
p \<in> cs_st f
q \<in> transition A a p
g ?q = Some (?l, ?d) \<Longrightarrow> ?d = (\<Squnion> (snd ` Some -` f ` pred A a ?q) \<and> even ?l)
q \<in> dom g

goal (1 subgoal):
 1. q \<in> cs_st g
[PROOF STEP]
unfolding cs_st_def image_def
[PROOF STATE]
proof (prove)
using this:
even (fst (the (g q)))
p \<in> f -` {y. \<exists>x\<in>snd -` {True}. y = Some x}
q \<in> transition A a p
g ?q = Some (?l, ?d) \<Longrightarrow> ?d = (\<Squnion> {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a ?q. y = f x}. y = snd x} \<and> even ?l)
q \<in> dom g

goal (1 subgoal):
 1. q \<in> g -` {y. \<exists>x\<in>snd -` {True}. y = Some x}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
q \<in> cs_st g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} \<subseteq> cs_st g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
assume 1: "g \<in> ranks_1 A a f"
[PROOF STATE]
proof (state)
this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 2: "dom g = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
unfolding ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 3: "\<And> p q. p \<in> dom f \<Longrightarrow> q \<in> transition A a p \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
[PROOF STEP]
unfolding ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> dom f; q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (g q)) \<le> fst (the (f p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p \<in> dom f; ?q \<in> transition A a ?p\<rbrakk> \<Longrightarrow> fst (the (g ?q)) \<le> fst (the (f ?p))

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 4: "\<And> q. q \<in> dom g \<Longrightarrow> accepting A q \<Longrightarrow> even (fst (the (g q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
[PROOF STEP]
unfolding ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom g; accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (g q)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> dom g; accepting A ?q\<rbrakk> \<Longrightarrow> even (fst (the (g ?q)))

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
have 5: "cs_st g = {q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
g \<in> ranks_1 A a f

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
unfolding ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal (1 subgoal):
 1. \<And>x. x \<in> ranks_1 A a f \<Longrightarrow> x \<in> ranks_2 A a f
[PROOF STEP]
show "g \<in> ranks_2 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> ranks_2 A a f
[PROOF STEP]
unfolding ranks_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))}
[PROOF STEP]
proof (intro CollectI conjI allI impI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. dom g = \<Union> (transition A a ` dom f)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 3. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 4. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
show "dom g = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (3 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 3. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 3. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
fix q l d
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 3. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
assume 10: "g q = Some (l, d)"
[PROOF STATE]
proof (state)
this:
g q = Some (l, d)

goal (3 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 3. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
have 11: "q \<in> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> dom g
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
g q = Some (l, d)

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

goal (3 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
 2. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 3. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
show "l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)
[PROOF STEP]
proof (rule cInf_greatest)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst ` Some -` f ` pred A a q \<noteq> {}
 2. \<And>x. x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> x
[PROOF STEP]
show "fst ` Some -` f ` pred A a q \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` f ` pred A a q \<noteq> {}
[PROOF STEP]
using 11
[PROOF STATE]
proof (prove)
using this:
q \<in> dom g

goal (1 subgoal):
 1. fst ` Some -` f ` pred A a q \<noteq> {}
[PROOF STEP]
unfolding 2 image_def vimage_def
[PROOF STATE]
proof (prove)
using this:
q \<in> \<Union> {y. \<exists>x\<in>dom f. y = transition A a x}

goal (1 subgoal):
 1. {y. \<exists>x\<in>{x. Some x \<in> {y. \<exists>x\<in>pred A a q. y = f x}}. y = fst x} \<noteq> {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` pred A a q \<noteq> {}

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> x
[PROOF STEP]
show "\<And> x. x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> x
[PROOF STEP]
using 3 10
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<in> dom f; ?q \<in> transition A a ?p\<rbrakk> \<Longrightarrow> fst (the (g ?q)) \<le> fst (the (f ?p))
g q = Some (l, d)

goal (1 subgoal):
 1. \<And>x. x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> x
[PROOF STEP]
by (auto) (metis domI fst_conv option.sel)
[PROOF STATE]
proof (state)
this:
?x \<in> fst ` Some -` f ` pred A a q \<Longrightarrow> l \<le> ?x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
have "d \<longleftrightarrow> q \<in> cs_st g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d = (q \<in> cs_st g)
[PROOF STEP]
unfolding cs_st_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d = (q \<in> g -` Some ` snd -` {True})
[PROOF STEP]
by (force simp: 10)
[PROOF STATE]
proof (state)
this:
d = (q \<in> cs_st g)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d = (q \<in> cs_st g)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
have "cs_st g = {q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
have "q \<in> \<dots> \<longleftrightarrow> (\<exists> x \<in> cs_st f. q \<in> transition A a x) \<and> even l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}) = ((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l)
[PROOF STEP]
unfolding mem_Collect_eq 10
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> \<Union> (transition A a ` cs_st f) \<and> even (fst (the (Some (l, d))))) = ((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(q \<in> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}) = ((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(q \<in> {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}) = ((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
have "\<dots> \<longleftrightarrow> \<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l) = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
unfolding cs_st_def image_def vimage_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>x\<in>{x. f x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}}. q \<in> transition A a x) \<and> even l) = (\<Squnion> {y. \<exists>x\<in>{x. Some x \<in> {y. \<exists>x\<in>pred A a q. y = f x}}. y = snd x} \<and> even l)
[PROOF STEP]
by auto metis+
[PROOF STATE]
proof (state)
this:
((\<exists>x\<in>cs_st f. q \<in> transition A a x) \<and> even l) = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)

goal (2 subgoals):
 1. \<And>q l d. g q = Some (l, d) \<Longrightarrow> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
 2. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
show "d \<longleftrightarrow> \<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l"
[PROOF STATE]
proof (prove)
using this:
d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)

goal (1 subgoal):
 1. d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l)

goal (1 subgoal):
 1. \<And>q l d. \<lbrakk>g q = Some (l, d); accepting A q\<rbrakk> \<Longrightarrow> even l
[PROOF STEP]
show "accepting A q \<Longrightarrow> even l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accepting A q \<Longrightarrow> even l
[PROOF STEP]
using 4 10 11
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> dom g; accepting A ?q\<rbrakk> \<Longrightarrow> even (fst (the (g ?q)))
g q = Some (l, d)
q \<in> dom g

goal (1 subgoal):
 1. accepting A q \<Longrightarrow> even l
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
accepting A q \<Longrightarrow> even l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<in> ranks_2 A a f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ranks_2 A a f = ranks_1 A a f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_2_refine: "(complement_2, complement_1) \<in> \<langle>Id, Id\<rangle> nba_rel \<rightarrow> \<langle>Id, Id\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_2, complement_1) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
unfolding complement_2_def complement_1_def complement_succ_2_def complement_succ_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. nba (alphabet A) {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} (\<lambda>a. ranks_2 A a \<circ> refresh_1) (\<lambda>f. True \<notin> snd ` ran f), \<lambda>A. nba (alphabet A) {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} (\<lambda>a. ranks_1 A a \<circ> refresh_1) (\<lambda>f. cs_st f = {})) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
unfolding ranks_2_refine cs_st_def image_def vimage_def ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. nba (alphabet A) {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} (\<lambda>a. ranks_1 A a \<circ> refresh_1) (\<lambda>f. True \<notin> {y. \<exists>x\<in>{b. \<exists>a. f a = Some b}. y = snd x}), \<lambda>A. nba (alphabet A) {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} (\<lambda>a. ranks_1 A a \<circ> refresh_1) (\<lambda>f. {x. f x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}} = {})) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma bounds_3_dom[simp]: "dom (bounds_3 A a f) = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (bounds_3 A a f) = \<Union> (transition A a ` dom f)
[PROOF STEP]
unfolding bounds_3_def Let_def dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {aa. (if Some -` f ` pred A a aa = {} then None else Some (\<Sqinter> (fst ` Some -` f ` pred A a aa), \<Squnion> (snd ` Some -` f ` pred A a aa))) \<noteq> None} = \<Union> (transition A a ` {a. f a \<noteq> None})
[PROOF STEP]
by (force split: if_splits)


[STATEMENT]
lemma items_3_nonempty[intro!, simp]: "items_3 A p s \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. items_3 A p s \<noteq> {}
[PROOF STEP]
unfolding items_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case s of (k, c) \<Rightarrow> {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A p \<longrightarrow> even l)}) \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma items_3_finite[intro!, simp]: "finite (items_3 A p s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (items_3 A p s)
[PROOF STEP]
unfolding items_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (case s of (k, c) \<Rightarrow> {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A p \<longrightarrow> even l)})
[PROOF STEP]
by (auto split: prod.splits)


[STATEMENT]
lemma get_3_dom[simp]: "dom (get_3 A f) = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (get_3 A f) = dom f
[PROOF STEP]
unfolding get_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>p. map_option (items_3 A p) (f p)) = dom f
[PROOF STEP]
by (auto split: bind_splits)


[STATEMENT]
lemma get_3_finite[intro, simp]: "S \<in> ran (get_3 A f) \<Longrightarrow> finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<in> ran (get_3 A f) \<Longrightarrow> finite S
[PROOF STEP]
unfolding get_3_def ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<in> {b. \<exists>a. map_option (items_3 A a) (f a) = Some b} \<Longrightarrow> finite S
[PROOF STEP]
by auto


[STATEMENT]
lemma get_3_update[simp]: "get_3 A (f (p \<mapsto> s)) = (get_3 A f) (p \<mapsto> items_3 A p s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_3 A (f(p \<mapsto> s)) = get_3 A f(p \<mapsto> items_3 A p s)
[PROOF STEP]
unfolding get_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>pa. map_option (items_3 A pa) ((f(p \<mapsto> s)) pa)) = (\<lambda>p. map_option (items_3 A p) (f p))(p \<mapsto> items_3 A p s)
[PROOF STEP]
by auto


[STATEMENT]
lemma expand_map_get_bounds_3: "expand_map \<circ> get_3 A \<circ> bounds_3 A a = ranks_2 A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((expand_map \<circ>\<circ> get_3) A \<circ>\<circ>\<circ> bounds_3) A a = ranks_2 A a
[PROOF STEP]
proof (intro ext set_eqI, unfold comp_apply)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. (xa \<in> expand_map (get_3 A (bounds_3 A a x))) = (xa \<in> ranks_2 A a x)
[PROOF STEP]
fix f g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. (xa \<in> expand_map (get_3 A (bounds_3 A a x))) = (xa \<in> ranks_2 A a x)
[PROOF STEP]
have 1: "(\<forall> x S y. get_3 A (bounds_3 A a f) x = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S) \<longleftrightarrow>
      (\<forall> q S l d. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x S y. get_3 A (bounds_3 A a f) x = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S) = (\<forall>q S l d. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>x S y. get_3 A (bounds_3 A a f) x = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S) = (\<forall>q S l d. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S)

goal (1 subgoal):
 1. \<And>x xa. (xa \<in> expand_map (get_3 A (bounds_3 A a x))) = (xa \<in> ranks_2 A a x)
[PROOF STEP]
have 2: "(\<forall> S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) \<longleftrightarrow>
      (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter>(fst ` (Some -` f ` pred A a q)) \<and>
      (d \<longleftrightarrow> \<Squnion>(snd ` (Some -` f ` pred A a q)) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))"
      if 3: "dom g = \<Union>((transition A a) ` (dom f))" for q l d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
have 4: "q \<notin> dom g" if "Some -` f ` pred A a q = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<notin> dom g
[PROOF STEP]
unfolding 3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<notin> \<Union> (transition A a ` dom f)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Some -` f ` pred A a q = {}

goal (1 subgoal):
 1. q \<notin> \<Union> (transition A a ` dom f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Some -` f ` pred A a q = {} \<Longrightarrow> q \<notin> dom g

goal (1 subgoal):
 1. (\<forall>S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
unfolding get_3_def items_3_def bounds_3_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>S. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A q \<longrightarrow> even l)}) (if Some -` f ` pred A a q = {} then None else Some (\<Sqinter> (fst ` Some -` f ` pred A a q), \<Squnion> (snd ` Some -` f ` pred A a q))) = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
Some -` f ` pred A a q = {} \<Longrightarrow> q \<notin> dom g

goal (1 subgoal):
 1. (\<forall>S. map_option (\<lambda>(k, c). {(l, c \<and> even l) |l. l \<le> k \<and> (accepting A q \<longrightarrow> even l)}) (if Some -` f ` pred A a q = {} then None else Some (\<Sqinter> (fst ` Some -` f ` pred A a q), \<Squnion> (snd ` Some -` f ` pred A a q))) = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>S. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S) = (g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f) \<Longrightarrow> (\<forall>S. get_3 A (bounds_3 A a f) ?q = Some S \<longrightarrow> g ?q = Some (?l, ?d) \<longrightarrow> (?l, ?d) \<in> S) = (g ?q = Some (?l, ?d) \<longrightarrow> ?l \<le> \<Sqinter> (fst ` Some -` f ` pred A a ?q) \<and> ?d = (\<Squnion> (snd ` Some -` f ` pred A a ?q) \<and> even ?l) \<and> (accepting A ?q \<longrightarrow> even ?l))

goal (1 subgoal):
 1. \<And>x xa. (xa \<in> expand_map (get_3 A (bounds_3 A a x))) = (xa \<in> ranks_2 A a x)
[PROOF STEP]
show "g \<in> expand_map (get_3 A (bounds_3 A a f)) \<longleftrightarrow> g \<in> ranks_2 A a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<in> expand_map (get_3 A (bounds_3 A a f))) = (g \<in> ranks_2 A a f)
[PROOF STEP]
unfolding expand_map_alt_def ranks_2_def mem_Collect_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dom g = dom (get_3 A (bounds_3 A a f)) \<and> (\<forall>x S y. get_3 A (bounds_3 A a f) x = Some S \<longrightarrow> g x = Some y \<longrightarrow> y \<in> S)) = (dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l)))
[PROOF STEP]
unfolding get_3_dom bounds_3_dom 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q S l d. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S)) = (dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f) \<Longrightarrow> (\<forall>S. get_3 A (bounds_3 A a f) ?q = Some S \<longrightarrow> g ?q = Some (?l, ?d) \<longrightarrow> (?l, ?d) \<in> S) = (g ?q = Some (?l, ?d) \<longrightarrow> ?l \<le> \<Sqinter> (fst ` Some -` f ` pred A a ?q) \<and> ?d = (\<Squnion> (snd ` Some -` f ` pred A a ?q) \<and> even ?l) \<and> (accepting A ?q \<longrightarrow> even ?l))

goal (1 subgoal):
 1. (dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q S l d. get_3 A (bounds_3 A a f) q = Some S \<longrightarrow> g q = Some (l, d) \<longrightarrow> (l, d) \<in> S)) = (dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>q l d. g q = Some (l, d) \<longrightarrow> l \<le> \<Sqinter> (fst ` Some -` f ` pred A a q) \<and> d = (\<Squnion> (snd ` Some -` f ` pred A a q) \<and> even l) \<and> (accepting A q \<longrightarrow> even l)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(g \<in> expand_map (get_3 A (bounds_3 A a f))) = (g \<in> ranks_2 A a f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_succ_3_refine: "complement_succ_3 = complement_succ_2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complement_succ_3 = complement_succ_2
[PROOF STEP]
unfolding complement_succ_3_def complement_succ_2_def expand_map_get_bounds_3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A a. ranks_2 A a \<circ> refresh_1) = (\<lambda>A a. ranks_2 A a \<circ> refresh_1)
[PROOF STEP]
by rule


[STATEMENT]
lemma complement_initial_3_refine: "{const (Some (2 * card (nodes A), False)) |` initial A} =
    {(Some \<circ> (const (2 * card (nodes A), False))) |` initial A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} = {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A}
[PROOF STEP]
unfolding comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} = {(\<lambda>x. Some (2 * card (nodes A), False)) |` initial A}
[PROOF STEP]
by rule


[STATEMENT]
lemma complement_accepting_3_refine: "True \<notin> snd ` ran f \<longleftrightarrow> (\<forall> (p, k, c) \<in> map_to_set f. \<not> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True \<notin> snd ` ran f) = (\<forall>(p, k, c)\<in>map_to_set f. \<not> c)
[PROOF STEP]
unfolding map_to_set_def ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True \<notin> snd ` {b. \<exists>a. f a = Some b}) = (\<forall>(p, k, c)\<in>{(k, v). f k = Some v}. \<not> c)
[PROOF STEP]
by auto


[STATEMENT]
lemma complement_3_refine: "(complement_3, complement_2) \<in> \<langle>Id, Id\<rangle> nba_rel \<rightarrow> \<langle>Id, Id\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (complement_3, complement_2) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
unfolding complement_3_def complement_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. 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), \<lambda>A. nba (alphabet A) {(\<lambda>_. Some (2 * card (nodes A), False)) |` initial A} (complement_succ_2 A) (\<lambda>f. True \<notin> snd ` ran f)) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
unfolding complement_succ_3_refine complement_initial_3_refine complement_accepting_3_refine
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_2 A) (\<lambda>f. \<forall>(p, k, c)\<in>map_to_set f. \<not> c), \<lambda>A. nba (alphabet A) {(Some \<circ> (\<lambda>_. (2 * card (nodes A), False))) |` initial A} (complement_succ_2 A) (\<lambda>f. \<forall>(p, k, y)\<in>map_to_set f. \<not> y)) \<in> \<langle>Id, Id\<rangle>nba_rel \<rightarrow> \<langle>Id, Id\<rangle>nba_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma get_4_dom[simp]: "dom (get_4 A f) = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (get_4 A f) = dom f
[PROOF STEP]
unfolding get_4_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>p. map_option (items_4 A p) (f p)) = dom f
[PROOF STEP]
by (auto split: bind_splits)


[STATEMENT]
lemma bounds_R:
    assumes "(f, g) \<in> R"
    assumes "bounds_3 A a (refresh_1 f) p = Some (n, e)"
    assumes "bounds_3 A a (refresh_1 g) p = Some (k, c)"
    shows "n \<le> k" "e \<longleftrightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> k &&& e = c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have 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)) \<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 assms(1)
[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 (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "n = \<Sqinter>(fst ` (Some -` refresh_1 f ` pred A a p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = \<Sqinter> (fst ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 f) p = Some (n, e)

goal (1 subgoal):
 1. n = \<Sqinter> (fst ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
unfolding bounds_3_def
[PROOF STATE]
proof (prove)
using this:
(let S = Some -` refresh_1 f ` pred A a p in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (n, e)

goal (1 subgoal):
 1. n = \<Sqinter> (fst ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
by (auto simp: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
n = \<Sqinter> (fst ` Some -` refresh_1 f ` pred A a p)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n = \<Sqinter> (fst ` Some -` refresh_1 f ` pred A a p)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "fst ` Some -` refresh_1 f ` pred A a p = fst ` Some -` f ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` refresh_1 f ` pred A a p = fst ` Some -` f ` pred A a p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst ` Some -` refresh_1 f ` pred A a p \<subseteq> fst ` Some -` f ` pred A a p
 2. fst ` Some -` f ` pred A a p \<subseteq> fst ` Some -` refresh_1 f ` pred A a p
[PROOF STEP]
show " fst ` Some -` refresh_1 f ` pred A a p \<subseteq> fst ` Some -` f ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` refresh_1 f ` pred A a p \<subseteq> fst ` Some -` f ` pred A a p
[PROOF STEP]
unfolding refresh_1_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = (if True \<in> {y. \<exists>x\<in>ran f. y = snd x} then f else map_option (apsnd \<top>) \<circ> f) x}. y = fst x} \<subseteq> {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = f x}. y = fst x}
[PROOF STEP]
by (auto simp: map_option_case split: option.split) (force)
[PROOF STATE]
proof (state)
this:
fst ` Some -` refresh_1 f ` pred A a p \<subseteq> fst ` Some -` f ` pred A a p

goal (1 subgoal):
 1. fst ` Some -` f ` pred A a p \<subseteq> fst ` Some -` refresh_1 f ` pred A a p
[PROOF STEP]
show "fst ` Some -` f ` pred A a p \<subseteq> fst ` Some -` refresh_1 f ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` f ` pred A a p \<subseteq> fst ` Some -` refresh_1 f ` pred A a p
[PROOF STEP]
unfolding refresh_1_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = f x}. y = fst x} \<subseteq> {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = (if True \<in> {y. \<exists>x\<in>ran f. y = snd x} then f else map_option (apsnd \<top>) \<circ> f) x}. y = fst x}
[PROOF STEP]
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` pred A a p \<subseteq> fst ` Some -` refresh_1 f ` pred A a p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst ` Some -` refresh_1 f ` pred A a p = fst ` Some -` f ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` Some -` refresh_1 f ` pred A a p = fst ` Some -` f ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = fst ` Some -` f ` (pred A a p \<inter> dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` f ` pred A a p = fst ` Some -` f ` (pred A a p \<inter> dom f)
[PROOF STEP]
unfolding dom_def image_def Int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = f x}. y = fst x} = {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>{x \<in> pred A a p. x \<in> {a. f a \<noteq> None}}. y = f x}. y = fst x}
[PROOF STEP]
by auto metis
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` pred A a p = fst ` Some -` f ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` pred A a p = fst ` Some -` f ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = fst ` the ` f ` (pred A a p \<inter> dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` f ` (pred A a p \<inter> dom f) = fst ` the ` f ` (pred A a p \<inter> dom f)
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` f ` (pred A a p \<inter> {a. f a \<noteq> None}) = fst ` the ` f ` (pred A a p \<inter> {a. f a \<noteq> None})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` (pred A a p \<inter> dom f) = fst ` the ` f ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` Some -` f ` (pred A a p \<inter> dom f) = fst ` the ` f ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = (fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` the ` f ` (pred A a p \<inter> dom f) = (fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` the ` f ` (pred A a p \<inter> dom f) = (fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` the ` f ` (pred A a p \<inter> dom f) = (fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<Sqinter>((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)) \<le>
      \<Sqinter>((fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)) \<le> \<Sqinter> ((fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g))
[PROOF STEP]
proof (rule cINF_mono)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pred A a p \<inter> dom g \<noteq> {}
 2. bdd_below ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f))
 3. \<And>m. m \<in> pred A a p \<inter> dom g \<Longrightarrow> \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m
[PROOF STEP]
show "pred A a p \<inter> dom g \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred A a p \<inter> dom g \<noteq> {}
[PROOF STEP]
using assms(2) 1(1)
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 f) p = Some (n, e)
dom f = dom g

goal (1 subgoal):
 1. pred A a p \<inter> dom g \<noteq> {}
[PROOF STEP]
unfolding bounds_3_def refresh_1_def
[PROOF STATE]
proof (prove)
using this:
(let S = Some -` (if True \<in> snd ` ran f then f else map_option (apsnd \<top>) \<circ> f) ` pred A a p in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (n, e)
dom f = dom g

goal (1 subgoal):
 1. pred A a p \<inter> dom g \<noteq> {}
[PROOF STEP]
by (auto simp: Let_def split: if_splits) (force+)
[PROOF STATE]
proof (state)
this:
pred A a p \<inter> dom g \<noteq> {}

goal (2 subgoals):
 1. bdd_below ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f))
 2. \<And>m. m \<in> pred A a p \<inter> dom g \<Longrightarrow> \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m
[PROOF STEP]
show "bdd_below ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_below ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
bdd_below ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f))

goal (1 subgoal):
 1. \<And>m. m \<in> pred A a p \<inter> dom g \<Longrightarrow> \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m
[PROOF STEP]
show "\<exists> n \<in> pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m"
        if "m \<in> pred A a p \<inter> dom g" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m
[PROOF STEP]
using 1 that
[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))
m \<in> pred A a p \<inter> dom g

goal (1 subgoal):
 1. \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?m \<in> pred A a p \<inter> dom g \<Longrightarrow> \<exists>n\<in>pred A a p \<inter> dom f. (fst \<circ> the \<circ> f) n \<le> (fst \<circ> the \<circ> g) ?m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sqinter> ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)) \<le> \<Sqinter> ((fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g))

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sqinter> ((fst \<circ> the \<circ> f) ` (pred A a p \<inter> dom f)) \<le> \<Sqinter> ((fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g))

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "(fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g) = fst ` the ` g ` (pred A a p \<inter> dom g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g) = fst ` the ` g ` (pred A a p \<inter> dom g)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g) = fst ` the ` g ` (pred A a p \<inter> dom g)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(fst \<circ> the \<circ> g) ` (pred A a p \<inter> dom g) = fst ` the ` g ` (pred A a p \<inter> dom g)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = fst ` Some -` g ` (pred A a p \<inter> dom g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` the ` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` (pred A a p \<inter> dom g)
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` the ` g ` (pred A a p \<inter> {a. g a \<noteq> None}) = fst ` Some -` g ` (pred A a p \<inter> {a. g a \<noteq> None})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` the ` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` (pred A a p \<inter> dom g)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` the ` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` (pred A a p \<inter> dom g)

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = fst ` Some -` g ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` pred A a p
[PROOF STEP]
unfolding dom_def image_def Int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>{x \<in> pred A a p. x \<in> {a. g a \<noteq> None}}. y = g x}. y = fst x} = {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = g x}. y = fst x}
[PROOF STEP]
by auto metis
[PROOF STATE]
proof (state)
this:
fst ` Some -` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` Some -` g ` (pred A a p \<inter> dom g) = fst ` Some -` g ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<dots> = fst ` Some -` refresh_1 g ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` g ` pred A a p = fst ` Some -` refresh_1 g ` pred A a p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst ` Some -` g ` pred A a p \<subseteq> fst ` Some -` refresh_1 g ` pred A a p
 2. fst ` Some -` refresh_1 g ` pred A a p \<subseteq> fst ` Some -` g ` pred A a p
[PROOF STEP]
show "fst ` Some -` g ` pred A a p \<subseteq> fst ` Some -` refresh_1 g ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` g ` pred A a p \<subseteq> fst ` Some -` refresh_1 g ` pred A a p
[PROOF STEP]
unfolding refresh_1_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = g x}. y = fst x} \<subseteq> {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = (if True \<in> {y. \<exists>x\<in>ran g. y = snd x} then g else map_option (apsnd \<top>) \<circ> g) x}. y = fst x}
[PROOF STEP]
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
[PROOF STATE]
proof (state)
this:
fst ` Some -` g ` pred A a p \<subseteq> fst ` Some -` refresh_1 g ` pred A a p

goal (1 subgoal):
 1. fst ` Some -` refresh_1 g ` pred A a p \<subseteq> fst ` Some -` g ` pred A a p
[PROOF STEP]
show "fst ` Some -` refresh_1 g ` pred A a p \<subseteq> fst ` Some -` g ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` Some -` refresh_1 g ` pred A a p \<subseteq> fst ` Some -` g ` pred A a p
[PROOF STEP]
unfolding refresh_1_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = (if True \<in> {y. \<exists>x\<in>ran g. y = snd x} then g else map_option (apsnd \<top>) \<circ> g) x}. y = fst x} \<subseteq> {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = g x}. y = fst x}
[PROOF STEP]
by (auto simp: map_option_case split: option.split) (force)
[PROOF STATE]
proof (state)
this:
fst ` Some -` refresh_1 g ` pred A a p \<subseteq> fst ` Some -` g ` pred A a p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst ` Some -` g ` pred A a p = fst ` Some -` refresh_1 g ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` Some -` g ` pred A a p = fst ` Some -` refresh_1 g ` pred A a p

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
have "\<Sqinter>(fst ` (Some -` refresh_1 g ` pred A a p)) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (fst ` Some -` refresh_1 g ` pred A a p) = k
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. \<Sqinter> (fst ` Some -` refresh_1 g ` pred A a p) = k
[PROOF STEP]
unfolding bounds_3_def
[PROOF STATE]
proof (prove)
using this:
(let S = Some -` refresh_1 g ` pred A a p in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (k, c)

goal (1 subgoal):
 1. \<Sqinter> (fst ` Some -` refresh_1 g ` pred A a p) = k
[PROOF STEP]
by (auto simp: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
\<Sqinter> (fst ` Some -` refresh_1 g ` pred A a p) = k

goal (2 subgoals):
 1. n \<le> k
 2. e = c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n \<le> k
[PROOF STEP]
show "n \<le> k"
[PROOF STATE]
proof (prove)
using this:
n \<le> k

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

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "e \<longleftrightarrow> \<Squnion>(snd ` (Some -` refresh_1 f ` pred A a p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = \<Squnion> (snd ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 f) p = Some (n, e)

goal (1 subgoal):
 1. e = \<Squnion> (snd ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
unfolding bounds_3_def
[PROOF STATE]
proof (prove)
using this:
(let S = Some -` refresh_1 f ` pred A a p in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (n, e)

goal (1 subgoal):
 1. e = \<Squnion> (snd ` Some -` refresh_1 f ` pred A a p)
[PROOF STEP]
by (auto simp: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
e = \<Squnion> (snd ` Some -` refresh_1 f ` pred A a p)

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
e = \<Squnion> (snd ` Some -` refresh_1 f ` pred A a p)

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "snd ` Some -` refresh_1 f ` pred A a p = snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` Some -` refresh_1 f ` pred A a p = snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))
[PROOF STEP]
unfolding dom_def image_def Int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = refresh_1 f x}. y = snd x} = {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>{x \<in> pred A a p. x \<in> {a. refresh_1 f a \<noteq> None}}. y = refresh_1 f x}. y = snd x}
[PROOF STEP]
by auto metis
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 f ` pred A a p = snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 f ` pred A a p = snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` Some -` refresh_1 f ` (pred A a p \<inter> {a. refresh_1 f a \<noteq> None}) = snd ` the ` refresh_1 f ` (pred A a p \<inter> {a. refresh_1 f a \<noteq> None})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = (snd \<circ> the \<circ> refresh_1 f) ` (pred A a p \<inter> dom (refresh_1 f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` the ` refresh_1 f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = (snd \<circ> the \<circ> refresh_1 g) ` (pred A a p \<inter> dom (refresh_1 g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g))
[PROOF STEP]
proof (rule image_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pred A a p \<inter> dom (refresh_1 f) = pred A a p \<inter> dom (refresh_1 g)
 2. \<And>x. x \<in> pred A a p \<inter> dom (refresh_1 g) \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f x = (snd \<circ> the \<circ>\<circ> refresh_1) g x
[PROOF STEP]
show "pred A a p \<inter> dom (refresh_1 f) = pred A a p \<inter> dom (refresh_1 g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred A a p \<inter> dom (refresh_1 f) = pred A a p \<inter> dom (refresh_1 g)
[PROOF STEP]
unfolding refresh_1_dom 1(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred A a p \<inter> dom g = pred A a p \<inter> dom g
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
pred A a p \<inter> dom (refresh_1 f) = pred A a p \<inter> dom (refresh_1 g)

goal (1 subgoal):
 1. \<And>x. x \<in> pred A a p \<inter> dom (refresh_1 g) \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f x = (snd \<circ> the \<circ>\<circ> refresh_1) g x
[PROOF STEP]
show "(snd \<circ> the \<circ> refresh_1 f) q \<longleftrightarrow> (snd \<circ> the \<circ> refresh_1 g) q"
        if 2: "q \<in> pred A a p \<inter> dom (refresh_1 g)" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q = (snd \<circ> the \<circ>\<circ> refresh_1) g q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
 2. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
have 3: "\<forall> x \<in> ran f. \<not> snd x \<Longrightarrow> (n, True) \<in> ran g \<Longrightarrow> g q = Some (k, c) \<Longrightarrow> c" for n k c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran f. \<not> snd x; (n, True) \<in> ran g; g q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
using 1(1, 3)
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran f. \<not> snd x; (n, True) \<in> ran g; g q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
unfolding dom_def ran_def
[PROOF STATE]
proof (prove)
using this:
{a. f a \<noteq> None} = {a. g a \<noteq> None}
\<forall>p\<in>{a. f a \<noteq> None}. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>{b. \<exists>a. f a = Some b}. \<not> snd x; (n, True) \<in> {b. \<exists>a. g a = Some b}; g q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>ran f. \<not> snd x; (?n, True) \<in> ran g; g q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c

goal (2 subgoals):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
 2. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
have 4: "g q = Some (n, True) \<Longrightarrow> f q = Some (k, c) \<Longrightarrow> c" for n k c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g q = Some (n, True); f q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
using 1(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>g q = Some (n, True); f q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>{a. f a \<noteq> None}. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>g q = Some (n, True); f q = Some (k, c)\<rbrakk> \<Longrightarrow> c
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>g q = Some (?n, True); f q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c

goal (2 subgoals):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
 2. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
have 5: "\<forall> x \<in> ran g. \<not> snd x \<Longrightarrow> (k, True) \<in> ran f \<Longrightarrow> False" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran g. \<not> snd x; (k, True) \<in> ran f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using 1(1, 3)
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran g. \<not> snd x; (k, True) \<in> ran f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding dom_def ran_def
[PROOF STATE]
proof (prove)
using this:
{a. f a \<noteq> None} = {a. g a \<noteq> None}
\<forall>p\<in>{a. f a \<noteq> None}. snd (the (f p)) = snd (the (g p))

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>{b. \<exists>a. g a = Some b}. \<not> snd x; (k, True) \<in> {b. \<exists>a. f a = Some b}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>ran g. \<not> snd x; (?k, True) \<in> ran f\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
 2. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
show "(snd \<circ> the \<circ> refresh_1 f) q \<Longrightarrow> (snd \<circ> the \<circ> refresh_1 g) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
[PROOF STEP]
using 1(1, 3) 2 3
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
q \<in> pred A a p \<inter> dom (refresh_1 g)
\<lbrakk>\<forall>x\<in>ran f. \<not> snd x; (?n, True) \<in> ran g; g q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c

goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q
[PROOF STEP]
unfolding refresh_1_def
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
q \<in> pred A a p \<inter> dom (if True \<in> snd ` ran g then g else map_option (apsnd \<top>) \<circ> g)
\<lbrakk>\<forall>x\<in>ran f. \<not> snd x; (?n, True) \<in> ran g; g q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c

goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ>\<circ> If (True \<in> snd ` ran f)) f (map_option (apsnd \<top>) \<circ> f) q \<Longrightarrow> (snd \<circ> the \<circ>\<circ>\<circ> If (True \<in> snd ` ran g)) g (map_option (apsnd \<top>) \<circ> g) q
[PROOF STEP]
by (force split: if_splits)
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) f q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) g q

goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
show "(snd \<circ> the \<circ> refresh_1 g) q \<Longrightarrow> (snd \<circ> the \<circ> refresh_1 f) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
using 1(1, 3) 2 4 5
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
q \<in> pred A a p \<inter> dom (refresh_1 g)
\<lbrakk>g q = Some (?n, True); f q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c
\<lbrakk>\<forall>x\<in>ran g. \<not> snd x; (?k, True) \<in> ran f\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q
[PROOF STEP]
unfolding refresh_1_def
[PROOF STATE]
proof (prove)
using this:
dom f = dom g
\<forall>p\<in>dom f. snd (the (f p)) = snd (the (g p))
q \<in> pred A a p \<inter> dom (if True \<in> snd ` ran g then g else map_option (apsnd \<top>) \<circ> g)
\<lbrakk>g q = Some (?n, True); f q = Some (?k, ?c)\<rbrakk> \<Longrightarrow> ?c
\<lbrakk>\<forall>x\<in>ran g. \<not> snd x; (?k, True) \<in> ran f\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ>\<circ> If (True \<in> snd ` ran g)) g (map_option (apsnd \<top>) \<circ> g) q \<Longrightarrow> (snd \<circ> the \<circ>\<circ>\<circ> If (True \<in> snd ` ran f)) f (map_option (apsnd \<top>) \<circ> f) q
[PROOF STEP]
by (auto simp: map_option_case split: option.splits if_splits) (force+)
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) g q \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q \<in> pred A a p \<inter> dom (refresh_1 g) \<Longrightarrow> (snd \<circ> the \<circ>\<circ> refresh_1) f ?q = (snd \<circ> the \<circ>\<circ> refresh_1) g ?q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) f ` (pred A a p \<inter> dom (refresh_1 f)) = (snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(snd \<circ> the \<circ>\<circ> refresh_1) g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` the ` refresh_1 g ` (pred A a p \<inter> {a. refresh_1 g a \<noteq> None}) = snd ` Some -` refresh_1 g ` (pred A a p \<inter> {a. refresh_1 g a \<noteq> None})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` the ` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g))

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<dots> = snd ` Some -` refresh_1 g ` pred A a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` pred A a p
[PROOF STEP]
unfolding dom_def image_def Int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>{x \<in> pred A a p. x \<in> {a. refresh_1 g a \<noteq> None}}. y = refresh_1 g x}. y = snd x} = {y. \<exists>x\<in>Some -` {y. \<exists>x\<in>pred A a p. y = refresh_1 g x}. y = snd x}
[PROOF STEP]
by auto metis
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` pred A a p

goal (1 subgoal):
 1. e = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` Some -` refresh_1 g ` (pred A a p \<inter> dom (refresh_1 g)) = snd ` Some -` refresh_1 g ` pred A a p

goal (1 subgoal):
 1. e = c
[PROOF STEP]
have "\<Squnion>(snd ` (Some -` refresh_1 g ` pred A a p)) \<longleftrightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (snd ` Some -` refresh_1 g ` pred A a p) = c
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
bounds_3 A a (refresh_1 g) p = Some (k, c)

goal (1 subgoal):
 1. \<Squnion> (snd ` Some -` refresh_1 g ` pred A a p) = c
[PROOF STEP]
unfolding bounds_3_def
[PROOF STATE]
proof (prove)
using this:
(let S = Some -` refresh_1 g ` pred A a p in if S = {} then None else Some (\<Sqinter> (fst ` S), \<Squnion> (snd ` S))) = Some (k, c)

goal (1 subgoal):
 1. \<Squnion> (snd ` Some -` refresh_1 g ` pred A a p) = c
[PROOF STEP]
by (auto simp: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
\<Squnion> (snd ` Some -` refresh_1 g ` pred A a p) = c

goal (1 subgoal):
 1. e = c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
e = c
[PROOF STEP]
show "e \<longleftrightarrow> c"
[PROOF STATE]
proof (prove)
using this:
e = c

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

goal:
No subgoals!
[PROOF STEP]
qed