[STATEMENT]
lemma maintained_standard_noconstants:
  assumes mnt:"maintainedA (standard_rules C L) G'"
  and gr:"graph (G'::('V Standard_Constant, 'V') labeled_graph)"
         "fst ` edges G' \<subseteq> L" (* Graph on labels L *)
  and cf:"getRel S_Bot G' = {}" (* Conflict free *)
shows "\<exists> f g (G::('V, 'V') std_graph). G = map_graph_fn G (f o g) \<and> G = map_graph_fn G' f
              \<and> subgraph (map_graph_fn G g) G'
              \<and> standard' C G
              \<and> (\<forall> r. maintained r G' \<longrightarrow> maintained r G)
              \<and> (\<forall> x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow>
                          (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x,y) \<in> :G':\<lbrakk>e\<rbrakk>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
note mnt = mnt[unfolded standard_rules_def]
[PROOF STATE]
proof (state)
this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from mnt
[PROOF STATE]
proof (chain)
picking this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
[PROOF STEP]
have "maintainedA (identity_rules L) G'"
[PROOF STATE]
proof (prove)
using this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. maintainedA (identity_rules L) G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintainedA (identity_rules L) G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from identity_rules[OF gr(1) this gr(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G' f) \<and> subgraph (map_graph_fn G' f) G' \<and> (\<forall>l x y. ((l, x, y) \<in> edges G') = ((l, f x, f y) \<in> edges G'))
[PROOF STEP]
obtain h where
    h:"h \<circ> h = h" "ident_rel S_Idt (map_graph_fn G' h)" "subgraph (map_graph_fn G' h) G'"
      "((l, x, y) \<in> edges G') = ((l, h x, h y) \<in> edges G')" for l x y
[PROOF STATE]
proof (prove)
using this:
\<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G' f) \<and> subgraph (map_graph_fn G' f) G' \<and> (\<forall>l x y. ((l, x, y) \<in> edges G') = ((l, f x, f y) \<in> edges G'))

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<circ> h = h; ident_rel S_Idt (map_graph_fn G' h); subgraph (map_graph_fn G' h) G'; \<And>l x y. ((l, x, y) \<in> edges G') = ((l, h x, h y) \<in> edges G')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h \<circ> h = h
ident_rel S_Idt (map_graph_fn G' h)
subgraph (map_graph_fn G' h) G'
((?l, ?x, ?y) \<in> edges G') = ((?l, h ?x, h ?y) \<in> edges G')

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have mg:"\<And> r. maintained r G' \<Longrightarrow> maintained r (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. maintained r G' \<Longrightarrow> maintained r (map_graph_fn G' h)
[PROOF STEP]
using idemp_embedding_maintained_preserved[OF h(3)] h(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> vertices G' \<Longrightarrow> (h \<circ> h) x = h x; maintained ?r G'\<rbrakk> \<Longrightarrow> maintained ?r (map_graph_fn G' h)
h \<circ> h = h

goal (1 subgoal):
 1. \<And>r. maintained r G' \<Longrightarrow> maintained r (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintained ?r G' \<Longrightarrow> maintained ?r (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from mnt
[PROOF STATE]
proof (chain)
picking this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
[PROOF STEP]
have tr:"maintained (top_rule S_Top) G'" and ne:"maintained nonempty_rule G'"
[PROOF STATE]
proof (prove)
using this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. maintained (top_rule S_Top) G' &&& maintained nonempty_rule G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintained (top_rule S_Top) G'
maintained nonempty_rule G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from nonempty_rule[OF gr(1)] ne
[PROOF STATE]
proof (chain)
picking this:
maintained nonempty_rule G' = (vertices G' \<noteq> {})
maintained nonempty_rule G'
[PROOF STEP]
obtain x where x:"x \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
maintained nonempty_rule G' = (vertices G' \<noteq> {})
maintained nonempty_rule G'

goal (1 subgoal):
 1. (\<And>x. x \<in> vertices G' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> vertices G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from tr[unfolded top_rule[OF gr(1)]] x
[PROOF STATE]
proof (chain)
picking this:
vertices G' \<times> vertices G' = getRel S_Top G'
x \<in> vertices G'
[PROOF STEP]
have top_nonempty:"(x, x) \<in> getRel S_Top G'"
[PROOF STATE]
proof (prove)
using this:
vertices G' \<times> vertices G' = getRel S_Top G'
x \<in> vertices G'

goal (1 subgoal):
 1. (x, x) \<in> getRel S_Top G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel S_Top G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have "\<And> c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
proof(goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
case (1 c)
[PROOF STATE]
proof (state)
this:
c \<in> C

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
with mnt
[PROOF STATE]
proof (chain)
picking this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
c \<in> C
[PROOF STEP]
have cr5: "maintained (const_exists c) G'"
              and cr7: "maintained (const_prop c) G'"
[PROOF STATE]
proof (prove)
using this:
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
c \<in> C

goal (1 subgoal):
 1. maintained (const_exists c) G' &&& maintained (const_prop c) G'
[PROOF STEP]
unfolding constant_rules_def
[PROOF STATE]
proof (prove)
using this:
maintainedA (const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<noteq> c\<^sub>2} \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
c \<in> C

goal (1 subgoal):
 1. maintained (const_exists c) G' &&& maintained (const_prop c) G'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
maintained (const_exists c) G'
maintained (const_prop c) G'

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
from top_nonempty cr5[unfolded maintained_holds_subset_iff[OF gr(1)] const_exists_def]
[PROOF STATE]
proof (chain)
picking this:
(x, x) \<in> getRel S_Top G'
:G':\<lbrakk>\<top>\<rbrakk> \<subseteq> :G':\<lbrakk>A_Cmp (A_Cmp \<top> (A_Lbl (S_Const c))) \<top>\<rbrakk>
[PROOF STEP]
obtain y z where yz:"(y,z) \<in> getRel (S_Const c) G'"
[PROOF STATE]
proof (prove)
using this:
(x, x) \<in> getRel S_Top G'
:G':\<lbrakk>\<top>\<rbrakk> \<subseteq> :G':\<lbrakk>A_Cmp (A_Cmp \<top> (A_Lbl (S_Const c))) \<top>\<rbrakk>

goal (1 subgoal):
 1. (\<And>y z. (y, z) \<in> getRel (S_Const c) G' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, z) \<in> getRel (S_Const c) G'

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
from this gr(1)
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> getRel (S_Const c) G'
graph G'
[PROOF STEP]
have yzv:"y \<in> vertices G'" "z \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> getRel (S_Const c) G'
graph G'

goal (1 subgoal):
 1. y \<in> vertices G' &&& z \<in> vertices G'
[PROOF STEP]
by (auto simp:getRel_def)
[PROOF STATE]
proof (state)
this:
y \<in> vertices G'
z \<in> vertices G'

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
from getRel_hom[OF yz yzv]
[PROOF STATE]
proof (chain)
picking this:
(?f y, ?f z) \<in> getRel (S_Const c) (map_graph_fn G' ?f)
[PROOF STEP]
have hi:"(h y,h z) \<in> getRel (S_Const c) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
(?f y, ?f z) \<in> getRel (S_Const c) (map_graph_fn G' ?f)

goal (1 subgoal):
 1. (h y, h z) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(h y, h z) \<in> getRel (S_Const c) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
with h(2) cr7[THEN mg,unfolded maintained_holds_subset_iff[OF map_graph_fn_graphI] const_prop_def]
[PROOF STATE]
proof (chain)
picking this:
ident_rel S_Idt (map_graph_fn G' h)
:map_graph_fn G' h:\<lbrakk>A_Lbl (S_Const c)\<rbrakk> \<subseteq> :map_graph_fn G' h:\<lbrakk>\<one>\<rbrakk>
(h y, h z) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
have "h y = h z"
[PROOF STATE]
proof (prove)
using this:
ident_rel S_Idt (map_graph_fn G' h)
:map_graph_fn G' h:\<lbrakk>A_Lbl (S_Const c)\<rbrakk> \<subseteq> :map_graph_fn G' h:\<lbrakk>\<one>\<rbrakk>
(h y, h z) \<in> getRel (S_Const c) (map_graph_fn G' h)

goal (1 subgoal):
 1. h y = h z
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
h y = h z

goal (1 subgoal):
 1. \<And>c. c \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
thus "\<exists> v. (v,v) \<in> getRel (S_Const c) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
h y = h z

goal (1 subgoal):
 1. \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
using hi
[PROOF STATE]
proof (prove)
using this:
h y = h z
(h y, h z) \<in> getRel (S_Const c) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v. (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?c1 \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const ?c1) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence "\<forall> c. \<exists> v. c \<in> C \<longrightarrow> (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
?c1 \<in> C \<Longrightarrow> \<exists>v. (v, v) \<in> getRel (S_Const ?c1) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<forall>c. \<exists>v. c \<in> C \<longrightarrow> (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>c. \<exists>v. c \<in> C \<longrightarrow> (v, v) \<in> getRel (S_Const c) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x. x \<in> C \<longrightarrow> (f x, f x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
obtain m
    where m:"\<And> x. x \<in> C \<Longrightarrow> (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x. x \<in> C \<longrightarrow> (f x, f x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (\<And>m. (\<And>x. x \<in> C \<Longrightarrow> (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x1 \<in> C \<Longrightarrow> (m ?x1, m ?x1) \<in> getRel (S_Const ?x1) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
let ?m' = "\<lambda> x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
define f where "f \<equiv> ?m' o h"
[PROOF STATE]
proof (state)
this:
f \<equiv> (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have "\<And> x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> m x = m y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
proof(goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
case (1 x y)
[PROOF STATE]
proof (state)
this:
x \<in> C
y \<in> C
m x = m y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> C \<Longrightarrow> (m ?x1, m ?x1) \<in> getRel (S_Const ?x1) (map_graph_fn G' h)
x \<in> C
y \<in> C
m x = m y
[PROOF STEP]
have "(m x,m x) \<in> getRel (S_Const y) (map_graph_fn G' h)"
                "(m x,m x) \<in> getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> C \<Longrightarrow> (m ?x1, m ?x1) \<in> getRel (S_Const ?x1) (map_graph_fn G' h)
x \<in> C
y \<in> C
m x = m y

goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const y) (map_graph_fn G' h) &&& (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
(m x, m x) \<in> getRel (S_Const y) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence mx: "(m x,m x) \<in> getRel (S_Const y) G'"
              "(m x,m x) \<in> getRel (S_Const x) G'"
[PROOF STATE]
proof (prove)
using this:
(m x, m x) \<in> getRel (S_Const y) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const y) G' &&& (m x, m x) \<in> getRel (S_Const x) G'
[PROOF STEP]
using h(3)
[PROOF STATE]
proof (prove)
using this:
(m x, m x) \<in> getRel (S_Const y) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
subgraph (map_graph_fn G' h) G'

goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const y) G' &&& (m x, m x) \<in> getRel (S_Const x) G'
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
(m x, m x) \<in> getRel (S_Const y) G'
(m x, m x) \<in> getRel (S_Const x) G'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from 1(1,2) mnt
[PROOF STATE]
proof (chain)
picking this:
x \<in> C
y \<in> C
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
[PROOF STEP]
have cr8:"x \<noteq> y \<Longrightarrow> maintained (const_disj x y) G'"
[PROOF STATE]
proof (prove)
using this:
x \<in> C
y \<in> C
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> maintained (const_disj x y) G'
[PROOF STEP]
unfolding constant_rules_def
[PROOF STATE]
proof (prove)
using this:
x \<in> C
y \<in> C
maintainedA (const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<noteq> c\<^sub>2} \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> maintained (const_disj x y) G'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<noteq> y \<Longrightarrow> maintained (const_disj x y) G'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from cr8[unfolded maintained_holds_subset_iff[OF gr(1)] const_disj_def] mx
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y \<Longrightarrow> :G':\<lbrakk>A_Cmp (A_Lbl (S_Const x)) (A_Lbl (S_Const y))\<rbrakk> \<subseteq> :G':\<lbrakk>\<bottom>\<rbrakk>
(m x, m x) \<in> getRel (S_Const y) G'
(m x, m x) \<in> getRel (S_Const x) G'
[PROOF STEP]
have "x\<noteq>y\<Longrightarrow>(m x,m x) \<in> :G':\<lbrakk>\<bottom>\<rbrakk>"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y \<Longrightarrow> :G':\<lbrakk>A_Cmp (A_Lbl (S_Const x)) (A_Lbl (S_Const y))\<rbrakk> \<subseteq> :G':\<lbrakk>\<bottom>\<rbrakk>
(m x, m x) \<in> getRel (S_Const y) G'
(m x, m x) \<in> getRel (S_Const x) G'

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> (m x, m x) \<in> :G':\<lbrakk>\<bottom>\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y \<Longrightarrow> (m x, m x) \<in> :G':\<lbrakk>\<bottom>\<rbrakk>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> C; y \<in> C; m x = m y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y \<Longrightarrow> (m x, m x) \<in> :G':\<lbrakk>\<bottom>\<rbrakk>

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using cf
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y \<Longrightarrow> (m x, m x) \<in> :G':\<lbrakk>\<bottom>\<rbrakk>
getRel S_Bot G' = {}

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x1 \<in> C; ?y1 \<in> C; m ?x1 = m ?y1\<rbrakk> \<Longrightarrow> ?x1 = ?y1

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence "univalent (converse (BNF_Def.Gr C m))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x1 \<in> C; ?y1 \<in> C; m ?x1 = m ?y1\<rbrakk> \<Longrightarrow> ?x1 = ?y1

goal (1 subgoal):
 1. univalent ((BNF_Def.Gr C m)\<inverse>)
[PROOF STEP]
unfolding univalent_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x1 \<in> C; ?y1 \<in> C; m ?x1 = m ?y1\<rbrakk> \<Longrightarrow> ?x1 = ?y1

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> (BNF_Def.Gr C m)\<inverse> \<and> (x, z) \<in> (BNF_Def.Gr C m)\<inverse> \<longrightarrow> z = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
univalent ((BNF_Def.Gr C m)\<inverse>)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence inj_m:"inj_on m C"
[PROOF STATE]
proof (prove)
using this:
univalent ((BNF_Def.Gr C m)\<inverse>)

goal (1 subgoal):
 1. inj_on m C
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
univalent ((BNF_Def.Gr C m)\<inverse>)

goal (1 subgoal):
 1. \<forall>x\<in>C. \<forall>y\<in>C. m x = m y \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on m C

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from inj_on_the_inv_into[OF inj_m]
[PROOF STATE]
proof (chain)
picking this:
inj_on (the_inv_into C m) (m ` C)
[PROOF STEP]
have inj_m':"inj ?m'"
[PROOF STATE]
proof (prove)
using this:
inj_on (the_inv_into C m) (m ` C)

goal (1 subgoal):
 1. inj (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>m ` C. \<forall>y\<in>m ` C. the_inv_into C m x = the_inv_into C m y \<longrightarrow> x = y

goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. (if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) = (if y \<in> m ` C then Inl (the_inv_into C m y) else Inr y) \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
define G where "G = map_graph_fn G' f"
[PROOF STATE]
proof (state)
this:
G = map_graph_fn G' f

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence G:"graph G" "f x \<in> vertices G" "getRel S_Bot G = {}"
[PROOF STATE]
proof (prove)
using this:
G = map_graph_fn G' f

goal (1 subgoal):
 1. graph G &&& f x \<in> vertices G &&& getRel S_Bot G = {}
[PROOF STEP]
using x cf
[PROOF STATE]
proof (prove)
using this:
G = map_graph_fn G' f
x \<in> vertices G'
getRel S_Bot G' = {}

goal (1 subgoal):
 1. graph G &&& f x \<in> vertices G &&& getRel S_Bot G = {}
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
G = map_graph_fn G' f
x \<in> vertices G'
{(x, y). (S_Bot, x, y) \<in> edges G'} = {}

goal (1 subgoal):
 1. graph G &&& f x \<in> vertices G &&& {(x, y). (S_Bot, x, y) \<in> edges G} = {}
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
graph G
f x \<in> vertices G
getRel S_Bot G = {}

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from comp_inj_on[OF inj_on_the_inv_into[OF inj_m] inj_Inl, unfolded o_def] inj_Inr
[PROOF STATE]
proof (chain)
picking this:
inj_on (\<lambda>x. Inl (the_inv_into C m x)) (m ` C)
inj_on Inr ?A
[PROOF STEP]
have inj_m':"inj_on ?m' (vertices G')"
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>x. Inl (the_inv_into C m x)) (m ` C)
inj_on Inr ?A

goal (1 subgoal):
 1. inj_on (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) (vertices G')
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>m ` C. \<forall>y\<in>m ` C. Inl (the_inv_into C m x) = Inl (the_inv_into C m y) \<longrightarrow> x = y
\<forall>x\<in>?A. \<forall>y\<in>?A. Inr x = Inr y \<longrightarrow> x = y

goal (1 subgoal):
 1. \<forall>x\<in>vertices G'. \<forall>y\<in>vertices G'. (if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) = (if y \<in> m ` C then Inl (the_inv_into C m y) else Inr y) \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) (vertices G')

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
define g where "g = the_inv_into (vertices G') ?m'"
[PROOF STATE]
proof (state)
this:
g = the_inv_into (vertices G') (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have gf_h:"\<And> x. x \<in> vertices G' \<Longrightarrow> (g o f) x = h x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> (g \<circ> f) x = h x
[PROOF STEP]
unfolding g_def f_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> the_inv_into (vertices G') (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) (if h x \<in> m ` C then Inl (the_inv_into C m (h x)) else Inr (h x)) = h x
[PROOF STEP]
apply(rule the_inv_into_f_f[OF inj_m'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
h \<circ> h = h
ident_rel S_Idt (map_graph_fn G' h)
subgraph (map_graph_fn G' h) G'
((?l, ?x, ?y) \<in> edges G') = ((?l, h ?x, h ?y) \<in> edges G')

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
unfolding subgraph_def graph_union_iff
[PROOF STATE]
proof (prove)
using this:
h \<circ> h = h
ident_rel S_Idt (map_graph_fn G' h)
graph (map_graph_fn G' h) \<and> graph G' \<and> edges (map_graph_fn G' h) \<subseteq> edges G' \<and> vertices (map_graph_fn G' h) \<subseteq> vertices G'
((?l, ?x, ?y) \<in> edges G') = ((?l, h ?x, h ?y) \<in> edges G')

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> vertices G' \<Longrightarrow> (g \<circ> f) ?x1 = h ?x1

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have mg_eq:"map_graph_fn G' (g \<circ> f) = map_graph_fn G' h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_graph_fn G' (g \<circ> f) = map_graph_fn G' h
[PROOF STEP]
by (rule map_graph_fn_eqI[OF gf_h])
[PROOF STATE]
proof (state)
this:
map_graph_fn G' (g \<circ> f) = map_graph_fn G' h

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have "\<And> x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
using h(3)
[PROOF STATE]
proof (prove)
using this:
subgraph (map_graph_fn G' h) G'

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
unfolding subgraph_def graph_union_iff
[PROOF STATE]
proof (prove)
using this:
graph (map_graph_fn G' h) \<and> graph G' \<and> edges (map_graph_fn G' h) \<subseteq> edges G' \<and> vertices (map_graph_fn G' h) \<subseteq> vertices G'

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> h x \<in> vertices G'
[PROOF STEP]
by(cases G',auto)
[PROOF STATE]
proof (state)
this:
?x1 \<in> vertices G' \<Longrightarrow> h ?x1 \<in> vertices G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence gf_id:"\<And> x. x \<in> vertices G' \<Longrightarrow> (g o f) (h x) = (h x)"
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> vertices G' \<Longrightarrow> h ?x1 \<in> vertices G'

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> (g \<circ> f) (h x) = h x
[PROOF STEP]
using h(1) gf_h
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> vertices G' \<Longrightarrow> h ?x1 \<in> vertices G'
h \<circ> h = h
?x1 \<in> vertices G' \<Longrightarrow> (g \<circ> f) ?x1 = h ?x1

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> (g \<circ> f) (h x) = h x
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> vertices G' \<Longrightarrow> h ?x1 \<in> vertices G'
(\<lambda>x. h (h x)) = h
?x1 \<in> vertices G' \<Longrightarrow> g (f ?x1) = h ?x1

goal (1 subgoal):
 1. \<And>x. x \<in> vertices G' \<Longrightarrow> g (f (h x)) = h x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x1 \<in> vertices G' \<Longrightarrow> (g \<circ> f) (h ?x1) = h ?x1

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x1 \<in> vertices G' \<Longrightarrow> (g \<circ> f) (h ?x1) = h ?x1

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
assume "x \<in> vertices G"
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vertices G
[PROOF STEP]
obtain y where y:"f y = x" "y \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>f y = x; y \<in> vertices G'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph_fn G' f)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>f y = x; y \<in> vertices G'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f y = x
y \<in> vertices G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from gf_h[OF y(2)]
[PROOF STATE]
proof (chain)
picking this:
(g \<circ> f) y = h y
[PROOF STEP]
have "(f o g) (f y) = f (h y)"
[PROOF STATE]
proof (prove)
using this:
(g \<circ> f) y = h y

goal (1 subgoal):
 1. (f \<circ> g) (f y) = f (h y)
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
g (f y) = h y

goal (1 subgoal):
 1. f (g (f y)) = f (h y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<circ> g) (f y) = f (h y)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<circ> g) (f y) = f (h y)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have "\<dots> = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (h y) = f y
[PROOF STEP]
using h(1)
[PROOF STATE]
proof (prove)
using this:
h \<circ> h = h

goal (1 subgoal):
 1. f (h y) = f y
[PROOF STEP]
unfolding f_def o_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. h (h x)) = h

goal (1 subgoal):
 1. (if h (h y) \<in> m ` C then Inl (the_inv_into C m (h (h y))) else Inr (h (h y))) = (if h y \<in> m ` C then Inl (the_inv_into C m (h y)) else Inr (h y))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f (h y) = f y

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<circ> g) (f y) = f y
[PROOF STEP]
have "(f o g) x = x"
[PROOF STATE]
proof (prove)
using this:
(f \<circ> g) (f y) = f y

goal (1 subgoal):
 1. (f \<circ> g) x = x
[PROOF STEP]
unfolding y
[PROOF STATE]
proof (prove)
using this:
(f \<circ> g) x = x

goal (1 subgoal):
 1. (f \<circ> g) x = x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f \<circ> g) x = x

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?xa3 \<in> vertices G \<Longrightarrow> (f \<circ> g) ?xa3 = ?xa3

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
note fg_id = this
[PROOF STATE]
proof (state)
this:
?xa3 \<in> vertices G \<Longrightarrow> (f \<circ> g) ?xa3 = ?xa3

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have fg_inv:"map_graph_fn G (f o g) = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_graph_fn G (f \<circ> g) = G
[PROOF STEP]
using h(1) G_def f_def mg_eq map_graph_fn_comp
[PROOF STATE]
proof (prove)
using this:
h \<circ> h = h
G = map_graph_fn G' f
f \<equiv> (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h
map_graph_fn G' (g \<circ> f) = map_graph_fn G' h
map_graph_fn ?G (?f \<circ> ?g) = map_graph_fn (map_graph_fn ?G ?g) ?f

goal (1 subgoal):
 1. map_graph_fn G (f \<circ> g) = G
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
map_graph_fn G (f \<circ> g) = G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have ir:"ident_rel S_Idt G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ident_rel S_Idt G
[PROOF STEP]
unfolding set_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x \<in> getRel S_Idt G) = (x \<in> (\<lambda>x. (x, x)) ` vertices G)
[PROOF STEP]
proof(standard,standard,goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> getRel S_Idt G

goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
from this[unfolded G_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> getRel S_Idt (map_graph_fn G' f)
[PROOF STEP]
obtain v1 v2 where v:"(v1,v2) \<in> getRel S_Idt G'" "x = (f v1,f v2)"
[PROOF STATE]
proof (prove)
using this:
x \<in> getRel S_Idt (map_graph_fn G' f)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>(v1, v2) \<in> getRel S_Idt G'; x = (f v1, f v2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding getRel_def map_graph_def on_triple_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {(x, y). (S_Idt, x, y) \<in> edges (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' f \<and> (t, t') \<in> on_graph G' f} `` edges G') (on_graph G' f `` vertices G'))}

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>(v1, v2) \<in> {(x, y). (S_Idt, x, y) \<in> edges G'}; x = (f v1, f v2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> getRel S_Idt G'
x = (f v1, f v2)

goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence vv:"v1 \<in> vertices G'" "v2 \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> getRel S_Idt G'
x = (f v1, f v2)

goal (1 subgoal):
 1. v1 \<in> vertices G' &&& v2 \<in> vertices G'
[PROOF STEP]
using gr
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> getRel S_Idt G'
x = (f v1, f v2)
graph G'
fst ` edges G' \<subseteq> L

goal (1 subgoal):
 1. v1 \<in> vertices G' &&& v2 \<in> vertices G'
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> {(x, y). (S_Idt, x, y) \<in> edges G'}
x = (f v1, f v2)
graph G'
fst ` edges G' \<subseteq> L

goal (1 subgoal):
 1. v1 \<in> vertices G' &&& v2 \<in> vertices G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v1 \<in> vertices G'
v2 \<in> vertices G'

goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
with h(2) v(1)
[PROOF STATE]
proof (chain)
picking this:
ident_rel S_Idt (map_graph_fn G' h)
(v1, v2) \<in> getRel S_Idt G'
v1 \<in> vertices G'
v2 \<in> vertices G'
[PROOF STEP]
have "h v1 = h v2"
[PROOF STATE]
proof (prove)
using this:
ident_rel S_Idt (map_graph_fn G' h)
(v1, v2) \<in> getRel S_Idt G'
v1 \<in> vertices G'
v2 \<in> vertices G'

goal (1 subgoal):
 1. h v1 = h v2
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt (map_graph_fn G' h) = {y. \<exists>x\<in>vertices (map_graph_fn G' h). y = (x, x)}
(v1, v2) \<in> getRel S_Idt G'
v1 \<in> vertices G'
v2 \<in> vertices G'

goal (1 subgoal):
 1. h v1 = h v2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h v1 = h v2

goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence x:"x = (f v1,f v1)"
[PROOF STATE]
proof (prove)
using this:
h v1 = h v2

goal (1 subgoal):
 1. x = (f v1, f v1)
[PROOF STEP]
unfolding f_def v
[PROOF STATE]
proof (prove)
using this:
h v1 = h v2

goal (1 subgoal):
 1. (((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v1, ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v2) = (((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v1, ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (f v1, f v1)

goal (2 subgoals):
 1. \<And>x. x \<in> getRel S_Idt G \<Longrightarrow> x \<in> (\<lambda>x. (x, x)) ` vertices G
 2. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
from vv(1)
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> vertices G'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vertices G'

goal (1 subgoal):
 1. x \<in> (\<lambda>x. (x, x)) ` vertices G
[PROOF STEP]
unfolding x G_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vertices G'

goal (1 subgoal):
 1. (f v1, f v1) \<in> (\<lambda>x. (x, x)) ` vertices (map_graph_fn G' f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. (x, x)) ` vertices G

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. (x, x)) ` vertices G

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence x:"fst x = snd x" "fst x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. (x, x)) ` vertices G

goal (1 subgoal):
 1. fst x = snd x &&& fst x \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x = snd x
fst x \<in> vertices G

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence "(fst x) \<in> f ` vertices G'"
[PROOF STATE]
proof (prove)
using this:
fst x = snd x
fst x \<in> vertices G

goal (1 subgoal):
 1. fst x \<in> f ` vertices G'
[PROOF STEP]
unfolding G_def o_def
[PROOF STATE]
proof (prove)
using this:
fst x = snd x
fst x \<in> vertices (map_graph_fn G' f)

goal (1 subgoal):
 1. fst x \<in> f ` vertices G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x \<in> f ` vertices G'

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x \<in> f ` vertices G'
[PROOF STEP]
obtain v where v:"v \<in> vertices G'" "f v = fst x"
[PROOF STATE]
proof (prove)
using this:
fst x \<in> f ` vertices G'

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> vertices G'; f v = fst x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> vertices G'
f v = fst x

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence hv:"h v \<in> vertices (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices G'
f v = fst x

goal (1 subgoal):
 1. h v \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h v \<in> vertices (map_graph_fn G' h)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence "(h v,h v) \<in> getRel S_Idt (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
h v \<in> vertices (map_graph_fn G' h)

goal (1 subgoal):
 1. (h v, h v) \<in> getRel S_Idt (map_graph_fn G' h)
[PROOF STEP]
unfolding h(2)
[PROOF STATE]
proof (prove)
using this:
h v \<in> vertices (map_graph_fn G' h)

goal (1 subgoal):
 1. (h v, h v) \<in> (\<lambda>x. (x, x)) ` vertices (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(h v, h v) \<in> getRel S_Idt (map_graph_fn G' h)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
from getRel_hom[OF this hv hv]
[PROOF STATE]
proof (chain)
picking this:
(?f (h v), ?f (h v)) \<in> getRel S_Idt (map_graph_fn (map_graph_fn G' h) ?f)
[PROOF STEP]
have "(?m' (h v),?m' (h v)) \<in> getRel S_Idt (map_graph_fn G' (?m' o h))"
[PROOF STATE]
proof (prove)
using this:
(?f (h v), ?f (h v)) \<in> getRel S_Idt (map_graph_fn (map_graph_fn G' h) ?f)

goal (1 subgoal):
 1. (if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v), if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v)) \<in> getRel S_Idt (map_graph_fn G' ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h))
[PROOF STEP]
unfolding map_graph_fn_comp
[PROOF STATE]
proof (prove)
using this:
(?f (h v), ?f (h v)) \<in> getRel S_Idt (map_graph_fn (map_graph_fn G' h) ?f)

goal (1 subgoal):
 1. (if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v), if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v)) \<in> getRel S_Idt (map_graph_fn (map_graph_fn G' h) (\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v), if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v)) \<in> getRel S_Idt (map_graph_fn G' ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence "(f v,f v) \<in> getRel S_Idt (map_graph_fn G' f)"
[PROOF STATE]
proof (prove)
using this:
(if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v), if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v)) \<in> getRel S_Idt (map_graph_fn G' ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h))

goal (1 subgoal):
 1. (f v, f v) \<in> getRel S_Idt (map_graph_fn G' f)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
(if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v), if h v \<in> m ` C then Inl (the_inv_into C m (h v)) else Inr (h v)) \<in> getRel S_Idt (map_graph_fn G' ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h))

goal (1 subgoal):
 1. (((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v, ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) v) \<in> getRel S_Idt (map_graph_fn G' ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f v, f v) \<in> getRel S_Idt (map_graph_fn G' f)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
hence "(fst x,snd x) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
using this:
(f v, f v) \<in> getRel S_Idt (map_graph_fn G' f)

goal (1 subgoal):
 1. (fst x, snd x) \<in> getRel S_Idt G
[PROOF STEP]
unfolding x v G_def
[PROOF STATE]
proof (prove)
using this:
(snd x, snd x) \<in> getRel S_Idt (map_graph_fn G' f)

goal (1 subgoal):
 1. (snd x, snd x) \<in> getRel S_Idt (map_graph_fn G' f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(fst x, snd x) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x, x)) ` vertices G \<Longrightarrow> x \<in> getRel S_Idt G
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(fst x, snd x) \<in> getRel S_Idt G

goal (1 subgoal):
 1. x \<in> getRel S_Idt G
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
(fst x, snd x) \<in> getRel S_Idt (map_graph_fn G' f)

goal (1 subgoal):
 1. x \<in> getRel S_Idt (map_graph_fn G' f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> getRel S_Idt G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ident_rel S_Idt G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from tr[unfolded top_rule[OF gr(1)]]
[PROOF STATE]
proof (chain)
picking this:
vertices G' \<times> vertices G' = getRel S_Top G'
[PROOF STEP]
have tr0:"getRel S_Top (map_graph_fn G' h)
          = {(x,y). x \<in> vertices (map_graph_fn G' h) \<and> y \<in> vertices (map_graph_fn G' h)}"
    and tr:"getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G}"
[PROOF STATE]
proof (prove)
using this:
vertices G' \<times> vertices G' = getRel S_Top G'

goal (1 subgoal):
 1. getRel S_Top (map_graph_fn G' h) = {(x, y). x \<in> vertices (map_graph_fn G' h) \<and> y \<in> vertices (map_graph_fn G' h)} &&& getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G}
[PROOF STEP]
unfolding G_def getRel_def on_triple_def map_graph_def
[PROOF STATE]
proof (prove)
using this:
vertices G' \<times> vertices G' = {(x, y). (S_Top, x, y) \<in> edges G'}

goal (1 subgoal):
 1. {(x, y). (S_Top, x, y) \<in> edges (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' h \<and> (t, t') \<in> on_graph G' h} `` edges G') (on_graph G' h `` vertices G'))} = {(x, y). x \<in> vertices (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' h \<and> (t, t') \<in> on_graph G' h} `` edges G') (on_graph G' h `` vertices G')) \<and> y \<in> vertices (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' h \<and> (t, t') \<in> on_graph G' h} `` edges G') (on_graph G' h `` vertices G'))} &&& {(x, y). (S_Top, x, y) \<in> edges (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' f \<and> (t, t') \<in> on_graph G' f} `` edges G') (on_graph G' f `` vertices G'))} = {(x, y). x \<in> vertices (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' f \<and> (t, t') \<in> on_graph G' f} `` edges G') (on_graph G' f `` vertices G')) \<and> y \<in> vertices (LG ({((l, s, t), l', s', t'). l = l' \<and> (s, s') \<in> on_graph G' f \<and> (t, t') \<in> on_graph G' f} `` edges G') (on_graph G' f `` vertices G'))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel S_Top (map_graph_fn G' h) = {(x, y). x \<in> vertices (map_graph_fn G' h) \<and> y \<in> vertices (map_graph_fn G' h)}
getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G}

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have m:"\<And> x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
assume x:"x \<in> C"
[PROOF STATE]
proof (state)
this:
x \<in> C

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> C

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
fix y z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
assume a:"(y,z) \<in> getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
let ?t = "getRel S_Top (map_graph_fn G' h)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
let ?r = "getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
have mx:"(m x,m x) \<in> getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
using m x
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> C \<Longrightarrow> (m ?x1, m ?x1) \<in> getRel (S_Const ?x1) (map_graph_fn G' h)
x \<in> C

goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
have v:"y \<in> vertices (map_graph_fn G' h)"
                    "z \<in> vertices (map_graph_fn G' h)"
                    "m x \<in> vertices (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. y \<in> vertices (map_graph_fn G' h) &&& z \<in> vertices (map_graph_fn G' h) &&& m x \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> {(x, y). (S_Const x, x, y) \<in> edges (map_graph_fn G' h)}
(m x, m x) \<in> {(x, y). (S_Const x, x, y) \<in> edges (map_graph_fn G' h)}

goal (1 subgoal):
 1. y \<in> vertices (map_graph_fn G' h) &&& z \<in> vertices (map_graph_fn G' h) &&& m x \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
y \<in> vertices (map_graph_fn G' h)
z \<in> vertices (map_graph_fn G' h)
m x \<in> vertices (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
with tr0
[PROOF STATE]
proof (chain)
picking this:
getRel S_Top (map_graph_fn G' h) = {(x, y). x \<in> vertices (map_graph_fn G' h) \<and> y \<in> vertices (map_graph_fn G' h)}
y \<in> vertices (map_graph_fn G' h)
z \<in> vertices (map_graph_fn G' h)
m x \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
have "(m x,y) \<in> ?t" "(z,m x) \<in> ?t"
[PROOF STATE]
proof (prove)
using this:
getRel S_Top (map_graph_fn G' h) = {(x, y). x \<in> vertices (map_graph_fn G' h) \<and> y \<in> vertices (map_graph_fn G' h)}
y \<in> vertices (map_graph_fn G' h)
z \<in> vertices (map_graph_fn G' h)
m x \<in> vertices (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, y) \<in> getRel S_Top (map_graph_fn G' h) &&& (z, m x) \<in> getRel S_Top (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m x, y) \<in> getRel S_Top (map_graph_fn G' h)
(z, m x) \<in> getRel S_Top (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
with a mx
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, y) \<in> getRel S_Top (map_graph_fn G' h)
(z, m x) \<in> getRel S_Top (map_graph_fn G' h)
[PROOF STEP]
have lhs:"(m x,z) \<in> ?r O ?t O ?r" "(y,m x) \<in> ?r O ?t O ?r"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
(m x, y) \<in> getRel S_Top (map_graph_fn G' h)
(z, m x) \<in> getRel S_Top (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, z) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h) &&& (y, m x) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m x, z) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)
(y, m x) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
from x mnt
[PROOF STATE]
proof (chain)
picking this:
x \<in> C
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'
[PROOF STEP]
have "maintained (const_exists_rev x) G'"
                  and "maintained (const_prop x) G'"
[PROOF STATE]
proof (prove)
using this:
x \<in> C
maintainedA (constant_rules C \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. maintained (const_exists_rev x) G' &&& maintained (const_prop x) G'
[PROOF STEP]
unfolding constant_rules_def
[PROOF STATE]
proof (prove)
using this:
x \<in> C
maintainedA (const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<noteq> c\<^sub>2} \<union> identity_rules L \<union> {top_rule S_Top, nonempty_rule}) G'

goal (1 subgoal):
 1. maintained (const_exists_rev x) G' &&& maintained (const_prop x) G'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
maintained (const_exists_rev x) G'
maintained (const_prop x) G'

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
hence cr6:"maintained (const_exists_rev x) (map_graph_fn G' h)"
        and cr7:"maintained (const_prop x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
maintained (const_exists_rev x) G'
maintained (const_prop x) G'

goal (1 subgoal):
 1. maintained (const_exists_rev x) (map_graph_fn G' h) &&& maintained (const_prop x) (map_graph_fn G' h)
[PROOF STEP]
by (intro mg, force)+
[PROOF STATE]
proof (state)
this:
maintained (const_exists_rev x) (map_graph_fn G' h)
maintained (const_prop x) (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
hence "(m x,z) \<in> getRel S_Idt (map_graph_fn G' h)"
            "(y,m x) \<in> getRel S_Idt (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
maintained (const_exists_rev x) (map_graph_fn G' h)
maintained (const_prop x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, z) \<in> getRel S_Idt (map_graph_fn G' h) &&& (y, m x) \<in> getRel S_Idt (map_graph_fn G' h)
[PROOF STEP]
using lhs
[PROOF STATE]
proof (prove)
using this:
maintained (const_exists_rev x) (map_graph_fn G' h)
maintained (const_prop x) (map_graph_fn G' h)
(m x, z) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)
(y, m x) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, z) \<in> getRel S_Idt (map_graph_fn G' h) &&& (y, m x) \<in> getRel S_Idt (map_graph_fn G' h)
[PROOF STEP]
unfolding maintained_holds_subset_iff[OF map_graph_fn_graphI]
                  const_exists_rev_def const_prop_def
[PROOF STATE]
proof (prove)
using this:
:map_graph_fn G' h:\<lbrakk>A_Cmp (A_Cmp (A_Lbl (S_Const x)) \<top>) (A_Lbl (S_Const x))\<rbrakk> \<subseteq> :map_graph_fn G' h:\<lbrakk>A_Lbl (S_Const x)\<rbrakk>
:map_graph_fn G' h:\<lbrakk>A_Lbl (S_Const x)\<rbrakk> \<subseteq> :map_graph_fn G' h:\<lbrakk>\<one>\<rbrakk>
(m x, z) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)
(y, m x) \<in> getRel (S_Const x) (map_graph_fn G' h) O getRel S_Top (map_graph_fn G' h) O getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, z) \<in> getRel S_Idt (map_graph_fn G' h) &&& (y, m x) \<in> getRel S_Idt (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m x, z) \<in> getRel S_Idt (map_graph_fn G' h)
(y, m x) \<in> getRel S_Idt (map_graph_fn G' h)

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
hence "y = m x" "z = m x"
[PROOF STATE]
proof (prove)
using this:
(m x, z) \<in> getRel S_Idt (map_graph_fn G' h)
(y, m x) \<in> getRel S_Idt (map_graph_fn G' h)

goal (1 subgoal):
 1. y = m x &&& z = m x
[PROOF STEP]
using h(2)
[PROOF STATE]
proof (prove)
using this:
(m x, z) \<in> getRel S_Idt (map_graph_fn G' h)
(y, m x) \<in> getRel S_Idt (map_graph_fn G' h)
ident_rel S_Idt (map_graph_fn G' h)

goal (1 subgoal):
 1. y = m x &&& z = m x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = m x
z = m x

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?y3, ?z3) \<in> getRel (S_Const x) (map_graph_fn G' h) \<Longrightarrow> ?y3 = m x
(?y3, ?z3) \<in> getRel (S_Const x) (map_graph_fn G' h) \<Longrightarrow> ?z3 = m x

goal (2 subgoals):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
 2. \<And>x. x \<in> C \<Longrightarrow> getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
thus "getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}"
[PROOF STATE]
proof (prove)
using this:
(?y3, ?z3) \<in> getRel (S_Const x) (map_graph_fn G' h) \<Longrightarrow> ?y3 = m x
(?y3, ?z3) \<in> getRel (S_Const x) (map_graph_fn G' h) \<Longrightarrow> ?z3 = m x

goal (1 subgoal):
 1. getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel (S_Const x) (map_graph_fn G' h) \<subseteq> {(m x, m x)}

goal (1 subgoal):
 1. \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} \<subseteq> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
qed (insert m,auto)
[PROOF STATE]
proof (state)
this:
?x1 \<in> C \<Longrightarrow> {(m ?x1, m ?x1)} = getRel (S_Const ?x1) (map_graph_fn G' h)

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
from mg_eq
[PROOF STATE]
proof (chain)
picking this:
map_graph_fn G' (g \<circ> f) = map_graph_fn G' h
[PROOF STEP]
have mg_eq:"map_graph_fn G g = map_graph_fn G' h"
[PROOF STATE]
proof (prove)
using this:
map_graph_fn G' (g \<circ> f) = map_graph_fn G' h

goal (1 subgoal):
 1. map_graph_fn G g = map_graph_fn G' h
[PROOF STEP]
unfolding G_def map_graph_fn_comp
[PROOF STATE]
proof (prove)
using this:
map_graph_fn (map_graph_fn G' f) g = map_graph_fn G' h

goal (1 subgoal):
 1. map_graph_fn (map_graph_fn G' f) g = map_graph_fn G' h
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map_graph_fn G g = map_graph_fn G' h

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
map_graph_fn G g = map_graph_fn G' h

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
fix v::"'V + 'V'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
assume a:"(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C"
[PROOF STATE]
proof (state)
this:
(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence "getRel l G = {(v, v)}"
[PROOF STATE]
proof (prove)
using this:
(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C

goal (1 subgoal):
 1. getRel l G = {(v, v)}
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C
?x1 \<in> C \<Longrightarrow> {(m ?x1, m ?x1)} = getRel (S_Const ?x1) (map_graph_fn G' h)

goal (1 subgoal):
 1. getRel l G = {(v, v)}
[PROOF STEP]
proof(cases l)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
case (S_Const x)
[PROOF STATE]
proof (state)
this:
l = S_Const x

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence x:"l = S_Const x" "v = Inl x" "x \<in> C"
[PROOF STATE]
proof (prove)
using this:
l = S_Const x

goal (1 subgoal):
 1. l = S_Const x &&& v = Inl x &&& x \<in> C
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
l = S_Const x
(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C

goal (1 subgoal):
 1. l = S_Const x &&& v = Inl x &&& x \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = S_Const x
v = Inl x
x \<in> C

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence mx:"m x \<in> m ` C"
[PROOF STATE]
proof (prove)
using this:
l = S_Const x
v = Inl x
x \<in> C

goal (1 subgoal):
 1. m x \<in> m ` C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m x \<in> m ` C

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
from m[OF x(3)]
[PROOF STATE]
proof (chain)
picking this:
{(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
have "(m x,m x) \<in> getRel (S_Const x) (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
{(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence "(S_Const x,m x,m x) \<in> edges (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
(m x, m x) \<in> getRel (S_Const x) (map_graph_fn G' h)

goal (1 subgoal):
 1. (S_Const x, m x, m x) \<in> edges (map_graph_fn G' h)
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(m x, m x) \<in> {(x, y). (S_Const x, x, y) \<in> edges (map_graph_fn G' h)}

goal (1 subgoal):
 1. (S_Const x, m x, m x) \<in> edges (map_graph_fn G' h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(S_Const x, m x, m x) \<in> edges (map_graph_fn G' h)

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence "m x \<in> vertices (map_graph_fn G' h)"
[PROOF STATE]
proof (prove)
using this:
(S_Const x, m x, m x) \<in> edges (map_graph_fn G' h)

goal (1 subgoal):
 1. m x \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
unfolding map_graph_def Image_def
[PROOF STATE]
proof (prove)
using this:
(S_Const x, m x, m x) \<in> edges (LG {y. \<exists>x\<in>edges G'. (x, y) \<in> on_triple (on_graph G' h)} {y. \<exists>x\<in>vertices G'. (x, y) \<in> on_graph G' h})

goal (1 subgoal):
 1. m x \<in> vertices (LG {y. \<exists>x\<in>edges G'. (x, y) \<in> on_triple (on_graph G' h)} {y. \<exists>x\<in>vertices G'. (x, y) \<in> on_graph G' h})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m x \<in> vertices (map_graph_fn G' h)

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x \<in> vertices (map_graph_fn G' h)
[PROOF STEP]
obtain x' where x':"m x = h x'" "x' \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
m x \<in> vertices (map_graph_fn G' h)

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>m x = h x'; x' \<in> vertices G'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m x = h x'
x' \<in> vertices G'

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
from h(1)
[PROOF STATE]
proof (chain)
picking this:
h \<circ> h = h
[PROOF STEP]
have hmx[simp]:"h (m x) = m x"
[PROOF STATE]
proof (prove)
using this:
h \<circ> h = h

goal (1 subgoal):
 1. h (m x) = m x
[PROOF STEP]
unfolding x' o_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. h (h x)) = h

goal (1 subgoal):
 1. h (h x') = h x'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
h (m x) = m x

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence fmx:"f (m x) = v"
[PROOF STATE]
proof (prove)
using this:
h (m x) = m x

goal (1 subgoal):
 1. f (m x) = v
[PROOF STEP]
unfolding x f_def
[PROOF STATE]
proof (prove)
using this:
h (m x) = m x

goal (1 subgoal):
 1. ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) (m x) = Inl x
[PROOF STEP]
using the_inv_into_f_f[OF inj_m] inj_m[unfolded inj_on_def,rule_format,OF x(3)] mx
[PROOF STATE]
proof (prove)
using this:
h (m x) = m x
?x \<in> C \<Longrightarrow> the_inv_into C m (m ?x) = ?x
\<lbrakk>?y \<in> C; m x = m ?y\<rbrakk> \<Longrightarrow> x = ?y
m x \<in> m ` C

goal (1 subgoal):
 1. ((\<lambda>x. if x \<in> m ` C then Inl (the_inv_into C m x) else Inr x) \<circ> h) (m x) = Inl x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (m x) = v

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
have "{(f (m x), f (m x))} = getRel l (map_graph_fn G (f \<circ> g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(f (m x), f (m x))} = getRel l (map_graph_fn G (f \<circ> g))
[PROOF STEP]
unfolding map_graph_fn_comp getRel_hom_map[OF map_graph_fn_graphI]
                  m[OF x(3),folded mg_eq x(1),symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(f (m x), f (m x))} = map_prod f f ` {(m x, m x)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(f (m x), f (m x))} = getRel l (map_graph_fn G (f \<circ> g))

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
hence gr:"getRel l G = {(f (m x), f (m x))}"
[PROOF STATE]
proof (prove)
using this:
{(f (m x), f (m x))} = getRel l (map_graph_fn G (f \<circ> g))

goal (1 subgoal):
 1. getRel l G = {(f (m x), f (m x))}
[PROOF STEP]
unfolding fg_inv
[PROOF STATE]
proof (prove)
using this:
{(f (m x), f (m x))} = getRel l G

goal (1 subgoal):
 1. getRel l G = {(f (m x), f (m x))}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
getRel l G = {(f (m x), f (m x))}

goal (4 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 4. \<And>x4. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Const x4\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getRel l G = {(v, v)}
[PROOF STEP]
unfolding gr fmx
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(v, v)} = {(v, v)}
[PROOF STEP]
by (fact refl)
[PROOF STATE]
proof (state)
this:
getRel l G = {(v, v)}

goal (3 subgoals):
 1. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Top\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 2. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Bot\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
 3. \<lbrakk>(l, v) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C; \<And>x. x \<in> C \<Longrightarrow> {(m x, m x)} = getRel (S_Const x) (map_graph_fn G' h); l = S_Idt\<rbrakk> \<Longrightarrow> getRel l G = {(v, v)}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
getRel l G = {(v, v)}

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?l3, ?v3) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C \<Longrightarrow> getRel ?l3 G = {(?v3, ?v3)}

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
note cr = this
[PROOF STATE]
proof (state)
this:
(?l3, ?v3) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C \<Longrightarrow> getRel ?l3 G = {(?v3, ?v3)}

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have sg:"subgraph (map_graph_fn G g) G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (map_graph_fn G g) G'
[PROOF STEP]
unfolding mg_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (map_graph_fn G' h) G'
[PROOF STEP]
using h(3)
[PROOF STATE]
proof (prove)
using this:
subgraph (map_graph_fn G' h) G'

goal (1 subgoal):
 1. subgraph (map_graph_fn G' h) G'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subgraph (map_graph_fn G g) G'

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have std:"standard' C G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. standard' C G
[PROOF STEP]
unfolding standard_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
[PROOF STEP]
using G ir tr cr
[PROOF STATE]
proof (prove)
using this:
graph G
f x \<in> vertices G
getRel S_Bot G = {}
ident_rel S_Idt G
getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G}
(?l3, ?v3) \<in> (\<lambda>c. (S_Const c, Inl c)) ` C \<Longrightarrow> getRel ?l3 G = {(?v3, ?v3)}

goal (1 subgoal):
 1. graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
standard' C G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
have mtd:"\<And>r. maintained r G' \<Longrightarrow> maintained r G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. maintained r G' \<Longrightarrow> maintained r G
[PROOF STEP]
proof(goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. maintained r G' \<Longrightarrow> maintained r G
[PROOF STEP]
case (1 r)
[PROOF STATE]
proof (state)
this:
maintained r G'

goal (1 subgoal):
 1. \<And>r. maintained r G' \<Longrightarrow> maintained r G
[PROOF STEP]
from mg[OF 1,folded mg_eq] maintained_preserved_by_isomorphism[OF fg_id G(1)]
[PROOF STATE]
proof (chain)
picking this:
maintained r (map_graph_fn G g)
\<lbrakk>\<And>x. x \<in> vertices G \<Longrightarrow> x \<in> vertices G; maintained ?r (map_graph_fn G g)\<rbrakk> \<Longrightarrow> maintained ?r G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
maintained r (map_graph_fn G g)
\<lbrakk>\<And>x. x \<in> vertices G \<Longrightarrow> x \<in> vertices G; maintained ?r (map_graph_fn G g)\<rbrakk> \<Longrightarrow> maintained ?r G

goal (1 subgoal):
 1. maintained r G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
maintained r G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
maintained ?r1 G' \<Longrightarrow> maintained ?r1 G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
maintained ?r1 G' \<Longrightarrow> maintained ?r1 G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
fix x y e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
assume "x \<in> vertices G'" "y \<in> vertices G'"
           "(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>"
[PROOF STATE]
proof (state)
this:
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence "(x,y) \<in> :G':\<lbrakk>e\<rbrakk>"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>

goal (1 subgoal):
 1. (x, y) \<in> :G':\<lbrakk>e\<rbrakk>
[PROOF STEP]
proof(induct e arbitrary: x y)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
case (A_Cmp e1 e2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e1\<rbrakk>
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e2\<rbrakk>
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>

goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e1\<rbrakk>
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e2\<rbrakk>
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>
[PROOF STEP]
obtain z where z:"(g (f x), z) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>"
                              "(z, g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e1\<rbrakk>
\<lbrakk>?x2 \<in> vertices G'; ?y2 \<in> vertices G'; (g (f ?x2), g (f ?y2)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> :G':\<lbrakk>e2\<rbrakk>
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(g (f x), z) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>; (z, g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(g (f x), z) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>
(z, g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>

goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
hence "z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)"
[PROOF STATE]
proof (prove)
using this:
(g (f x), z) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>
(z, g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>

goal (1 subgoal):
 1. z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)
[PROOF STEP]
using semantics_in_vertices(1)[OF map_graph_fn_graphI]
[PROOF STATE]
proof (prove)
using this:
(g (f x), z) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>
(z, g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>
(?a, ?b) \<in> :map_graph_fn ?G1 ?f1:\<lbrakk>?e\<rbrakk> \<Longrightarrow> ?a \<in> vertices (map_graph_fn ?G1 ?f1)

goal (1 subgoal):
 1. z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)

goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)
[PROOF STEP]
obtain z' where z':"z = g (f z')" "z' \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
z \<in> vertices (map_graph_fn (map_graph_fn G' f) g)

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z = g (f z'); z' \<in> vertices G'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = g (f z')
z' \<in> vertices G'

goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
with A_Cmp(1)[OF A_Cmp(3) z'(2) z(1)[unfolded z']]
             A_Cmp(2)[OF z'(2) A_Cmp(4) z(2)[unfolded z']]
[PROOF STATE]
proof (chain)
picking this:
(x, z') \<in> :G':\<lbrakk>e1\<rbrakk>
(z', y) \<in> :G':\<lbrakk>e2\<rbrakk>
z = g (f z')
z' \<in> vertices G'
[PROOF STEP]
have "(x, y) \<in> (:G':\<lbrakk>e1\<rbrakk>) O (:G':\<lbrakk>e2\<rbrakk>)"
[PROOF STATE]
proof (prove)
using this:
(x, z') \<in> :G':\<lbrakk>e1\<rbrakk>
(z', y) \<in> :G':\<lbrakk>e2\<rbrakk>
z = g (f z')
z' \<in> vertices G'

goal (1 subgoal):
 1. (x, y) \<in> (:G':\<lbrakk>e1\<rbrakk>) O (:G':\<lbrakk>e2\<rbrakk>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (:G':\<lbrakk>e1\<rbrakk>) O (:G':\<lbrakk>e2\<rbrakk>)

goal (4 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cmp e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
 3. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 4. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> (:G':\<lbrakk>e1\<rbrakk>) O (:G':\<lbrakk>e2\<rbrakk>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (:G':\<lbrakk>e1\<rbrakk>) O (:G':\<lbrakk>e2\<rbrakk>)

goal (1 subgoal):
 1. (x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> :G':\<lbrakk>A_Cmp e1 e2\<rbrakk>

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
case (A_Lbl l)
[PROOF STATE]
proof (state)
this:
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl l\<rbrakk>

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
hence "(l, g (f x), g (f y)) \<in> edges (map_graph_fn G g)"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G'
y \<in> vertices G'
(g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl l\<rbrakk>

goal (1 subgoal):
 1. (l, g (f x), g (f y)) \<in> edges (map_graph_fn G g)
[PROOF STEP]
by (auto simp:getRel_def G_def)
[PROOF STATE]
proof (state)
this:
(l, g (f x), g (f y)) \<in> edges (map_graph_fn G g)

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l, g (f x), g (f y)) \<in> edges (map_graph_fn G g)
[PROOF STEP]
obtain x' y'
          where "(l, x', y') \<in> edges G" "g (f x) = g x'" "g (f y) = g y'"
[PROOF STATE]
proof (prove)
using this:
(l, g (f x), g (f y)) \<in> edges (map_graph_fn G g)

goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>(l, x', y') \<in> edges G; g (f x) = g x'; g (f y) = g y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, x', y') \<in> edges G
g (f x) = g x'
g (f y) = g y'

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l, x', y') \<in> edges G
g (f x) = g x'
g (f y) = g y'
[PROOF STEP]
obtain x' y'
          where xy:"(l, x', y') \<in> edges G'" "g (f x) = g (f x')" "g (f y) = g (f y')"
[PROOF STATE]
proof (prove)
using this:
(l, x', y') \<in> edges G
g (f x) = g x'
g (f y) = g y'

goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>(l, x', y') \<in> edges G'; g (f x) = g (f x'); g (f y) = g (f y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
(l, x', y') \<in> edges (map_graph_fn G' f)
g (f x) = g x'
g (f y) = g y'

goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>(l, x', y') \<in> edges G'; g (f x) = g (f x'); g (f y) = g (f y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, x', y') \<in> edges G'
g (f x) = g (f x')
g (f y) = g (f y')

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
hence "x' \<in> vertices G'" "y' \<in> vertices G'"
[PROOF STATE]
proof (prove)
using this:
(l, x', y') \<in> edges G'
g (f x) = g (f x')
g (f y) = g (f y')

goal (1 subgoal):
 1. x' \<in> vertices G' &&& y' \<in> vertices G'
[PROOF STEP]
using gr(1)
[PROOF STATE]
proof (prove)
using this:
(l, x', y') \<in> edges G'
g (f x) = g (f x')
g (f y) = g (f y')
graph G'

goal (1 subgoal):
 1. x' \<in> vertices G' &&& y' \<in> vertices G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<in> vertices G'
y' \<in> vertices G'

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
from this[THEN gf_h,unfolded o_def] A_Lbl(1,2)[THEN gf_h,unfolded o_def]
[PROOF STATE]
proof (chain)
picking this:
g (f x') = h x'
g (f y') = h y'
g (f x) = h x
g (f y) = h y
[PROOF STEP]
have "h x = h x'" "h y = h y'"
[PROOF STATE]
proof (prove)
using this:
g (f x') = h x'
g (f y') = h y'
g (f x) = h x
g (f y) = h y

goal (1 subgoal):
 1. h x = h x' &&& h y = h y'
[PROOF STEP]
using xy(2,3)
[PROOF STATE]
proof (prove)
using this:
g (f x') = h x'
g (f y') = h y'
g (f x) = h x
g (f y) = h y
g (f x) = g (f x')
g (f y) = g (f y')

goal (1 subgoal):
 1. h x = h x' &&& h y = h y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h x = h x'
h y = h y'

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
hence "(l, x, y) \<in> edges G'"
[PROOF STATE]
proof (prove)
using this:
h x = h x'
h y = h y'

goal (1 subgoal):
 1. (l, x, y) \<in> edges G'
[PROOF STEP]
using h(4)[of l x y] h(4)[of l x' y'] xy(1)
[PROOF STATE]
proof (prove)
using this:
h x = h x'
h y = h y'
((l, x, y) \<in> edges G') = ((l, h x, h y) \<in> edges G')
((l, x', y') \<in> edges G') = ((l, h x', h y') \<in> edges G')
(l, x', y') \<in> edges G'

goal (1 subgoal):
 1. (l, x, y) \<in> edges G'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, x, y) \<in> edges G'

goal (3 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
 3. \<And>x xa y. \<lbrakk>xa \<in> vertices G'; y \<in> vertices G'; (g (f xa), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Lbl x\<rbrakk>\<rbrakk> \<Longrightarrow> (xa, y) \<in> :G':\<lbrakk>A_Lbl x\<rbrakk>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l, x, y) \<in> edges G'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G'

goal (1 subgoal):
 1. (x, y) \<in> :G':\<lbrakk>A_Lbl l\<rbrakk>
[PROOF STEP]
by (simp add:getRel_def)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> :G':\<lbrakk>A_Lbl l\<rbrakk>

goal (2 subgoals):
 1. \<And>e1 e2 x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e1\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e1\<rbrakk>; \<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e2\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Int e1 e2\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Int e1 e2\<rbrakk>
 2. \<And>e x y. \<lbrakk>\<And>x y. \<lbrakk>x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>; x \<in> vertices G'; y \<in> vertices G'; (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>A_Cnv e\<rbrakk>\<rbrakk> \<Longrightarrow> (x, y) \<in> :G':\<lbrakk>A_Cnv e\<rbrakk>
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> :G':\<lbrakk>e\<rbrakk>

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?xa4 \<in> vertices G'; ?y4 \<in> vertices G'; (g (f ?xa4), g (f ?y4)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>?e4\<rbrakk>\<rbrakk> \<Longrightarrow> (?xa4, ?y4) \<in> :G':\<lbrakk>?e4\<rbrakk>

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
hence cons:"(\<forall> x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x,y) \<in> :G':\<lbrakk>e\<rbrakk>)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xa4 \<in> vertices G'; ?y4 \<in> vertices G'; (g (f ?xa4), g (f ?y4)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>?e4\<rbrakk>\<rbrakk> \<Longrightarrow> (?xa4, ?y4) \<in> :G':\<lbrakk>?e4\<rbrakk>

goal (1 subgoal):
 1. \<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xa4 \<in> vertices G'; ?y4 \<in> vertices G'; (g (f ?xa4), g (f ?y4)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>?e4\<rbrakk>\<rbrakk> \<Longrightarrow> (?xa4, ?y4) \<in> :G':\<lbrakk>?e4\<rbrakk>

goal (1 subgoal):
 1. \<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn (map_graph_fn G' f) g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
using cons G_def fg_inv[symmetric] sg std mtd
[PROOF STATE]
proof (prove)
using this:
\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>
G = map_graph_fn G' f
G = map_graph_fn G (f \<circ> g)
subgraph (map_graph_fn G g) G'
standard' C G
maintained ?r1 G' \<Longrightarrow> maintained ?r1 G

goal (1 subgoal):
 1. \<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f g G. G = map_graph_fn G (f \<circ> g) \<and> G = map_graph_fn G' f \<and> subgraph (map_graph_fn G g) G' \<and> standard' C G \<and> (\<forall>r. maintained r G' \<longrightarrow> maintained r G) \<and> (\<forall>x y e. x \<in> vertices G' \<longrightarrow> y \<in> vertices G' \<longrightarrow> (g (f x), g (f y)) \<in> :map_graph_fn G g:\<lbrakk>e\<rbrakk> \<longrightarrow> (x, y) \<in> :G':\<lbrakk>e\<rbrakk>)

goal:
No subgoals!
[PROOF STEP]
qed