[STATEMENT]
lemma del_UnEdge_even_even:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')\<in>edges G"
    assumes parity_assms: "even (degree v G)" "even (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
interpret G:valid_unMultigraph
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have  "v\<in>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have  "v'\<in>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
[PROOF STATE]
proof (state)
this:
v' \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> odd_nodes_set (del_unEdge v w v' G)
v' \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
have extra_odd_nodes:"{v,v'} \<subseteq> odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
v \<in> odd_nodes_set (del_unEdge v w v' G)
v' \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
v' \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}

goal (1 subgoal):
 1. {v, v'} \<subseteq> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "v \<notin>odd_nodes_set G" and "v'\<notin>odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> odd_nodes_set G &&& v' \<notin> odd_nodes_set G
[PROOF STEP]
using parity_assms
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
even (degree v' G)

goal (1 subgoal):
 1. v \<notin> odd_nodes_set G &&& v' \<notin> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
even (degree v' G)

goal (1 subgoal):
 1. v \<notin> {v \<in> G.V. odd (degree v G)} &&& v' \<notin> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<notin> odd_nodes_set G
v' \<notin> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
hence vv'_odd_disjoint: "{v,v'} \<inter> odd_nodes_set G = {}"
[PROOF STATE]
proof (prove)
using this:
v \<notin> odd_nodes_set G
v' \<notin> odd_nodes_set G

goal (1 subgoal):
 1. {v, v'} \<inter> odd_nodes_set G = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v, v'} \<inter> odd_nodes_set G = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v'} \<inter> odd_nodes_set G = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "odd_nodes_set(del_unEdge v w v' G) -{v,v'}\<subseteq>odd_nodes_set G "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<subseteq> odd_nodes_set G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
assume x_odd_set: "x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'}"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
hence "degree x (del_unEdge v w v' G) = degree x G"
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'}

goal (1 subgoal):
 1. degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
by (metis Diff_iff G.degree_frame assms(2))
[PROOF STATE]
proof (state)
this:
degree x (del_unEdge v w v' G) = degree x G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
hence "odd(degree x G)"
[PROOF STATE]
proof (prove)
using this:
degree x (del_unEdge v w v' G) = degree x G

goal (1 subgoal):
 1. odd (degree x G)
[PROOF STEP]
using x_odd_set
[PROOF STATE]
proof (prove)
using this:
degree x (del_unEdge v w v' G) = degree x G
x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'}

goal (1 subgoal):
 1. odd (degree x G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
degree x (del_unEdge v w v' G) = degree x G
x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))} - {v, v'}

goal (1 subgoal):
 1. odd (degree x G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree x G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (degree x G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
have "x \<in> nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> G.V
[PROOF STEP]
using x_odd_set
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'}

goal (1 subgoal):
 1. x \<in> G.V
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))} - {v, v'}

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

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd (degree x G)
x \<in> G.V
[PROOF STEP]
show "x \<in> odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
odd (degree x G)
x \<in> G.V

goal (1 subgoal):
 1. x \<in> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
odd (degree x G)
x \<in> G.V

goal (1 subgoal):
 1. x \<in> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "odd_nodes_set G \<subseteq> odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set G \<subseteq> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
assume x_odd_set:  "x \<in> odd_nodes_set G"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> odd(degree x (del_unEdge v w v' G))"
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set G

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> odd (degree x (del_unEdge v w v' G))
[PROOF STEP]
by (metis (lifting) G.degree_frame assms(2) mem_Collect_eq odd_nodes_set_def)
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x (del_unEdge v w v' G))

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> x\<in>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x (del_unEdge v w v' G))

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
using x_odd_set del_UnEdge_node
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x (del_unEdge v w v' G))
x \<in> odd_nodes_set G
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x (del_unEdge v w v' G))
x \<in> {v \<in> G.V. odd (degree v G)}
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
have "x\<in>{v,v'} \<Longrightarrow> x\<in>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
using extra_odd_nodes
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
show "x \<in> odd_nodes_set (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
{v, v'} \<inter> odd_nodes_set G = {}
odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<subseteq> odd_nodes_set G
odd_nodes_set G \<subseteq> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
have "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G \<union> {v,v'}"
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
{v, v'} \<inter> odd_nodes_set G = {}
odd_nodes_set (del_unEdge v w v' G) - {v, v'} \<subseteq> odd_nodes_set G
odd_nodes_set G \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
thus "num_of_odd_nodes(del_unEdge v w v' G) = num_of_odd_nodes G + 2"
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
assume "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G \<union> {v,v'}"
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "v\<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
using G.no_id \<open>(v,w,v')\<in>edges G\<close>
[PROOF STATE]
proof (prove)
using this:
(?v, ?w, ?v) \<notin> G.E
(v, w, v') \<in> G.E

goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
hence "card{v,v'}=2"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'

goal (1 subgoal):
 1. card {v, v'} = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {v, v'} = 2

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {v, v'} = 2

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have " odd_nodes_set G \<inter> {v,v'} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set G \<inter> {v, v'} = {}
[PROOF STEP]
using vv'_odd_disjoint
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<inter> odd_nodes_set G = {}

goal (1 subgoal):
 1. odd_nodes_set G \<inter> {v, v'} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<inter> {v, v'} = {}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<inter> {v, v'} = {}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "finite(odd_nodes_set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
by (metis (lifting) assms(3) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI)
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set G)

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set G)

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
have "finite {v,v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v, v'}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}
card {v, v'} = 2
odd_nodes_set G \<inter> {v, v'} = {}
finite (odd_nodes_set G)
finite {v, v'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}
card {v, v'} = 2
odd_nodes_set G \<inter> {v, v'} = {}
finite (odd_nodes_set G)
finite {v, v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}
card {v, v'} = 2
odd_nodes_set G \<inter> {v, v'} = {}
finite (odd_nodes_set G)
finite {v, v'}

goal (1 subgoal):
 1. card (odd_nodes_set (del_unEdge v w v' G)) = card (odd_nodes_set G) + 2
[PROOF STEP]
using card_Un_disjoint
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) = odd_nodes_set G \<union> {v, v'}
card {v, v'} = 2
odd_nodes_set G \<inter> {v, v'} = {}
finite (odd_nodes_set G)
finite {v, v'}
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> card (?A \<union> ?B) = card ?A + card ?B

goal (1 subgoal):
 1. card (odd_nodes_set (del_unEdge v w v' G)) = card (odd_nodes_set G) + 2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G + 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_UnEdge_even_odd:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')\<in>edges G"
    assumes parity_assms: "even (degree v G)" "odd (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
interpret G : valid_unMultigraph
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have odd_v:"v\<in>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have  not_odd_v':"v'\<notin>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<notin> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
[PROOF STATE]
proof (state)
this:
v' \<notin> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have "odd_nodes_set(del_unEdge v w v' G) \<union> {v'} \<subseteq>odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<subseteq> odd_nodes_set G \<union> {v}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
assume x_prems:" x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
have "x=v' \<Longrightarrow>x\<in>odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
using parity_assms
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
odd (degree v' G)

goal (1 subgoal):
 1. x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
by (metis (lifting) G.E_validD(2) Un_def assms(4) mem_Collect_eq odd_nodes_set_def )
[PROOF STATE]
proof (state)
this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
have "x=v \<Longrightarrow> x\<in>odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
by (metis insertI1 insert_is_Un sup_commute)
[PROOF STATE]
proof (state)
this:
x = v \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = v \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
have "x\<notin>{v,v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
using x_prems
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> x \<in> odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
using G.degree_frame \<open>finite (edges G)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
\<lbrakk>finite G.E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G
finite G.E

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> x\<in>odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
x = v \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
show "x \<in> odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
using this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
x = v \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set G \<union> {v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<subseteq> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<subseteq> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have "odd_nodes_set G \<union> {v} \<subseteq> odd_nodes_set(del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set G \<union> {v} \<subseteq> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
assume x_prems: "x \<in> odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
have "x=v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
by (metis UnI1 odd_v)
[PROOF STATE]
proof (state)
this:
x = v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
have "x=v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
have "x\<notin>{v,v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
using x_prems
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow>  x\<in>odd_nodes_set (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> {v \<in> G.V. odd (degree v G)} \<union> {v}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
using G.degree_frame \<open>finite (edges G)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> {v \<in> G.V. odd (degree v G)} \<union> {v}
\<lbrakk>finite G.E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G
finite G.E

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G \<union> {v} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
x = v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
show "x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}"
[PROOF STATE]
proof (prove)
using this:
x = v \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
x = v' \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<union> {v} \<subseteq> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<subseteq> odd_nodes_set G \<union> {v}
odd_nodes_set G \<union> {v} \<subseteq> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}
[PROOF STEP]
have "odd_nodes_set(del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}"
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} \<subseteq> odd_nodes_set G \<union> {v}
odd_nodes_set G \<union> {v} \<subseteq> odd_nodes_set (del_unEdge v w v' G) \<union> {v'}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have " odd_nodes_set G \<inter> {v} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set G \<inter> {v} = {}
[PROOF STEP]
using parity_assms
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
odd (degree v' G)

goal (1 subgoal):
 1. odd_nodes_set G \<inter> {v} = {}
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
odd (degree v' G)

goal (1 subgoal):
 1. {v \<in> G.V. odd (degree v G)} \<inter> {v} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<inter> {v} = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set G \<inter> {v} = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have " odd_nodes_set(del_unEdge v w v' G) \<inter> {v'}={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}
[PROOF STEP]
by (metis Int_insert_left_if0 inf_bot_left inf_commute not_odd_v')
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have "finite (odd_nodes_set(del_unEdge v w v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (odd_nodes_set (del_unEdge v w v' G))
[PROOF STEP]
using \<open>finite (nodes G)\<close>
[PROOF STATE]
proof (prove)
using this:
finite G.V

goal (1 subgoal):
 1. finite (odd_nodes_set (del_unEdge v w v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set (del_unEdge v w v' G))

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set (del_unEdge v w v' G))

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
have "finite (odd_nodes_set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
using \<open>finite (nodes G)\<close>
[PROOF STATE]
proof (prove)
using this:
finite G.V

goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set G)

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}
odd_nodes_set G \<inter> {v} = {}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite (odd_nodes_set G)
[PROOF STEP]
have "card(odd_nodes_set G) + card {v} =
                   card(odd_nodes_set(del_unEdge v w v' G)) + card {v'}"
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}
odd_nodes_set G \<inter> {v} = {}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite (odd_nodes_set G)

goal (1 subgoal):
 1. card (odd_nodes_set G) + card {v} = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}
[PROOF STEP]
using card_Un_disjoint[of "odd_nodes_set (del_unEdge v w v' G)" "{v'}"]
      card_Un_disjoint[of "odd_nodes_set G" "{v}"]
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set (del_unEdge v w v' G) \<union> {v'} = odd_nodes_set G \<union> {v}
odd_nodes_set G \<inter> {v} = {}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite (odd_nodes_set G)
\<lbrakk>finite (odd_nodes_set (del_unEdge v w v' G)); finite {v'}; odd_nodes_set (del_unEdge v w v' G) \<inter> {v'} = {}\<rbrakk> \<Longrightarrow> card (odd_nodes_set (del_unEdge v w v' G) \<union> {v'}) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}
\<lbrakk>finite (odd_nodes_set G); finite {v}; odd_nodes_set G \<inter> {v} = {}\<rbrakk> \<Longrightarrow> card (odd_nodes_set G \<union> {v}) = card (odd_nodes_set G) + card {v}

goal (1 subgoal):
 1. card (odd_nodes_set G) + card {v} = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (odd_nodes_set G) + card {v} = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card (odd_nodes_set G) + card {v} = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
card (odd_nodes_set G) + card {v} = card (odd_nodes_set (del_unEdge v w v' G)) + card {v'}

goal (1 subgoal):
 1. card (odd_nodes_set (del_unEdge v w v' G)) = card (odd_nodes_set G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_UnEdge_odd_even:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')\<in>edges G"
    assumes parity_assms: "odd (degree v G)" "even (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v w v' G) = num_of_odd_nodes G
[PROOF STEP]
by (metis assms del_UnEdge_even_odd delete_edge_sym parity_assms valid_unMultigraph.corres)


[STATEMENT]
lemma del_UnEdge_odd_odd:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')\<in>edges G"
    assumes parity_assms: "odd (degree v G)" "odd (degree v' G)"
    shows "num_of_odd_nodes G=num_of_odd_nodes(del_unEdge v w v' G)+2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
interpret G:valid_unMultigraph
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have  "v\<notin>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
[PROOF STATE]
proof (state)
this:
v \<notin> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<notin> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have  "v'\<notin>odd_nodes_set(del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<notin> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
[PROOF STATE]
proof (state)
this:
v' \<notin> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<notin> odd_nodes_set (del_unEdge v w v' G)
v' \<notin> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
have vv'_disjoint: "{v,v'} \<inter> odd_nodes_set(del_unEdge v w v' G) = {}"
[PROOF STATE]
proof (prove)
using this:
v \<notin> odd_nodes_set (del_unEdge v w v' G)
v' \<notin> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. {v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}
[PROOF STEP]
by (metis (full_types) Int_insert_left_if0 inf_bot_left)
[PROOF STATE]
proof (state)
this:
{v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have extra_odd_nodes:"{v,v'} \<subseteq> odd_nodes_set( G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v, v'} \<subseteq> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v, v'} \<subseteq> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
using \<open>(v,w,v')\<in>edges G\<close>
[PROOF STATE]
proof (prove)
using this:
(v, w, v') \<in> G.E

goal (1 subgoal):
 1. {v, v'} \<subseteq> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
by (metis (lifting) G.E_validD empty_subsetI insert_subset mem_Collect_eq parity_assms)
[PROOF STATE]
proof (state)
this:
{v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have "odd_nodes_set G -{v,v'}\<subseteq>odd_nodes_set (del_unEdge v w v' G) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set G - {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
assume x_odd_set: "x \<in> odd_nodes_set G - {v, v'}"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set G - {v, v'}

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
hence "degree x G = degree x (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set G - {v, v'}

goal (1 subgoal):
 1. degree x G = degree x (del_unEdge v w v' G)
[PROOF STEP]
by (metis Diff_iff G.degree_frame assms(2))
[PROOF STATE]
proof (state)
this:
degree x G = degree x (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
hence "odd(degree x (del_unEdge v w v' G))"
[PROOF STATE]
proof (prove)
using this:
degree x G = degree x (del_unEdge v w v' G)

goal (1 subgoal):
 1. odd (degree x (del_unEdge v w v' G))
[PROOF STEP]
using x_odd_set
[PROOF STATE]
proof (prove)
using this:
degree x G = degree x (del_unEdge v w v' G)
x \<in> odd_nodes_set G - {v, v'}

goal (1 subgoal):
 1. odd (degree x (del_unEdge v w v' G))
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
degree x G = degree x (del_unEdge v w v' G)
x \<in> {v \<in> G.V. odd (degree v G)} - {v, v'}

goal (1 subgoal):
 1. odd (degree x (del_unEdge v w v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree x (del_unEdge v w v' G))

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (degree x (del_unEdge v w v' G))

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
have "x \<in> nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
using x_odd_set
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set G - {v, v'}

goal (1 subgoal):
 1. x \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {v \<in> G.V. odd (degree v G)} - {v, v'}

goal (1 subgoal):
 1. x \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set G - {v, v'} \<Longrightarrow> x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd (degree x (del_unEdge v w v' G))
x \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
show "x \<in> odd_nodes_set (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
using this:
odd (degree x (del_unEdge v w v' G))
x \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<in> odd_nodes_set (del_unEdge v w v' G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
odd (degree x (del_unEdge v w v' G))
x \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set G - {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set G - {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have "odd_nodes_set (del_unEdge v w v' G) \<subseteq> odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<subseteq> odd_nodes_set G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
assume x_odd_set:  "x \<in> odd_nodes_set (del_unEdge v w v' G)"
[PROOF STATE]
proof (state)
this:
x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> odd(degree x G)"
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set (del_unEdge v w v' G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)
[PROOF STEP]
using assms G.degree_frame
[PROOF STATE]
proof (prove)
using this:
x \<in> odd_nodes_set (del_unEdge v w v' G)
valid_unMultigraph G
finite G.E
finite G.V
(v, w, v') \<in> G.E
odd (degree v G)
odd (degree v' G)
\<lbrakk>finite G.E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
valid_unMultigraph G
finite G.E
finite G.V
(v, w, v') \<in> G.E
odd (degree v G)
odd (degree v' G)
\<lbrakk>finite G.E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
hence "x\<notin>{v,v'} \<Longrightarrow> x\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
using x_odd_set del_UnEdge_node
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)
x \<in> odd_nodes_set (del_unEdge v w v' G)
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> odd (degree x G)
x \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> x \<in> {v \<in> G.V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
have "x\<in>{v,v'} \<Longrightarrow> x\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
using extra_odd_nodes
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<And>x. x \<in> odd_nodes_set (del_unEdge v w v' G) \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
[PROOF STEP]
show "x \<in> odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G
x \<in> {v, v'} \<Longrightarrow> x \<in> odd_nodes_set G

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}
{v, v'} \<subseteq> odd_nodes_set G
odd_nodes_set G - {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
odd_nodes_set (del_unEdge v w v' G) \<subseteq> odd_nodes_set G
[PROOF STEP]
have "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) \<union> {v,v'}"
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}
{v, v'} \<subseteq> odd_nodes_set G
odd_nodes_set G - {v, v'} \<subseteq> odd_nodes_set (del_unEdge v w v' G)
odd_nodes_set (del_unEdge v w v' G) \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
assume "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) \<union> {v,v'}"
[PROOF STATE]
proof (state)
this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have " odd_nodes_set (del_unEdge v w v' G) \<inter> {v,v'} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
[PROOF STEP]
using vv'_disjoint
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<inter> odd_nodes_set (del_unEdge v w v' G) = {}

goal (1 subgoal):
 1. odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have "finite(odd_nodes_set (del_unEdge v w v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (odd_nodes_set (del_unEdge v w v' G))
[PROOF STEP]
using assms del_UnEdge_node finite_subset
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G
finite G.E
finite G.V
(v, w, v') \<in> G.E
odd (degree v G)
odd (degree v' G)
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (odd_nodes_set (del_unEdge v w v' G))
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G
finite G.E
finite G.V
(v, w, v') \<in> G.E
odd (degree v G)
odd (degree v' G)
(?v \<in> nodes (del_unEdge ?u ?e ?u' ?G)) = (?v \<in> nodes ?G)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set (del_unEdge v w v' G))

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set (del_unEdge v w v' G))

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have "finite {v,v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v, v'}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite {v, v'}
[PROOF STEP]
have "card(odd_nodes_set G)
                       = card(odd_nodes_set  (del_unEdge v w v' G)) + card{v,v'}"
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite {v, v'}

goal (1 subgoal):
 1. card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite {v, v'}

goal (1 subgoal):
 1. card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
[PROOF STEP]
using card_Un_disjoint
[PROOF STATE]
proof (prove)
using this:
odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'}
odd_nodes_set (del_unEdge v w v' G) \<inter> {v, v'} = {}
finite (odd_nodes_set (del_unEdge v w v' G))
finite {v, v'}
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> card (?A \<union> ?B) = card ?A + card ?B

goal (1 subgoal):
 1. card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
have "v\<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
using G.no_id \<open>(v,w,v')\<in>edges G\<close>
[PROOF STATE]
proof (prove)
using this:
(?v, ?w, ?v) \<notin> G.E
(v, w, v') \<in> G.E

goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
hence "card{v,v'}=2"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> v'

goal (1 subgoal):
 1. card {v, v'} = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {v, v'} = 2

goal (1 subgoal):
 1. odd_nodes_set G = odd_nodes_set (del_unEdge v w v' G) \<union> {v, v'} \<Longrightarrow> num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
card {v, v'} = 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
card {v, v'} = 2

goal (1 subgoal):
 1. num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + card {v, v'}
card {v, v'} = 2

goal (1 subgoal):
 1. card (odd_nodes_set G) = card (odd_nodes_set (del_unEdge v w v' G)) + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes G = num_of_odd_nodes (del_unEdge v w v' G) + 2

goal:
No subgoals!
[PROOF STEP]
qed