[STATEMENT]
lemma (in valid_unMultigraph) rem_UnPath_parity_v':
  assumes "finite E"  "is_trail v ps v'"
  shows "v\<noteq>v' \<longleftrightarrow> (odd (degree v' (rem_unPath ps G)) = even(degree v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite E
is_trail v ps v'

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G))
[PROOF STEP]
proof (induct ps arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; is_trail v [] v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath [] G)) = even (degree v' G))
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
finite E
is_trail v [] v'

goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; is_trail v [] v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath [] G)) = even (degree v' G))
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite E
is_trail v [] v'

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath [] G)) = even (degree v' G))
[PROOF STEP]
by (metis is_trail.simps(1) rem_unPath.simps(1))
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath [] G)) = even (degree v' G))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite E; is_trail ?v xs v'\<rbrakk> \<Longrightarrow> (?v \<noteq> v') = (odd (degree v' (rem_unPath xs G)) = even (degree v' G))
finite E
is_trail v (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
print_cases
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite E; is_trail ?v xs v'\<rbrakk> \<Longrightarrow> (?v \<noteq> v') = (odd (degree v' (rem_unPath xs G)) = even (degree v' G))
finite E
is_trail v (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
hence rem_x:"odd (degree v' (rem_unPath (x#xs) G)) = odd(degree v' (del_unEdge
            x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
by (metis  rem_unPath.simps(2) rem_unPath_com)
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
have "x3=v' \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x3 = v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
proof (cases "v=v'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x3 = v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = v'

goal (2 subgoals):
 1. \<lbrakk>x3 = v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
assume "x3=v'"
[PROOF STATE]
proof (state)
this:
x3 = v'

goal (2 subgoals):
 1. \<lbrakk>x3 = v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "x1=v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = v'
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. x1 = v'
[PROOF STEP]
by (metis Cons.prems(2) True is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
x1 = v'

goal (2 subgoals):
 1. \<lbrakk>x3 = v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x1 = v'

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
using \<open>x3=v'\<close>
[PROOF STATE]
proof (prove)
using this:
x1 = v'
x3 = v'

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) no_id x)
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
assume "x3=v'"
[PROOF STATE]
proof (state)
this:
x3 = v'

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
using rem_x
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=odd(degree v' (rem_unPath xs G) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x1,x2,x3) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x3,x2,x1) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
by (metis \<open>x3 = v'\<close> del_edge_undirected_degree_minus delete_edge_sym  x)
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=even(degree v' (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
have "(x1,x2,x3)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> E
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
hence "(x3,x2,x1)\<in>edges (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. (x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) corres distinct_elim_rev x)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
hence "(x3,x2,x1)\<in>{e \<in> edges (rem_unPath xs G). fst e = v'}"
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. (x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
using \<open>x3=v'\<close>
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)
x3 = v'

goal (1 subgoal):
 1. (x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
by (metis (mono_tags) fst_conv mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
have "finite {e \<in> edges (rem_unPath xs G). fst e = v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
finite E

goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
have "degree v' (rem_unPath xs G)\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. degree v' (rem_unPath xs G) \<noteq> 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. card {e \<in> edges (rem_unPath xs G). fst e = v'} \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree v' (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree v' (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=even (degree v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree v' (rem_unPath xs G)) = even (degree v' G)
[PROOF STEP]
using \<open>x3 = v'\<close> assms
[PROOF STATE]
proof (prove)
using this:
x3 = v'
finite E
is_trail v ps v'

goal (1 subgoal):
 1. even (degree v' (rem_unPath xs G)) = even (degree v' G)
[PROOF STEP]
by (metis (mono_tags) Cons.hyps Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
even (degree v' (rem_unPath xs G)) = even (degree v' G)

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)"
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. \<lbrakk>x3 = v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
by (metis False)
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x3 = v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x3 = v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
have "x3\<noteq>v'\<Longrightarrow>?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x3 \<noteq> v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
proof (cases "v=v'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = v'

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
assume "x3\<noteq>v'"
[PROOF STATE]
proof (state)
this:
x3 \<noteq> v'

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
using rem_x
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=odd(degree v' (rem_unPath xs G) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x1,x2,x3) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x3,x2,x1) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
using True x
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)
v = v'
x = (x1, x2, x3)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)
[PROOF STEP]
by (metis Cons.prems(2) del_edge_undirected_degree_minus is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G) - 1)

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=even(degree v' (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
have "(x1,x2,x3)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> E
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
hence "(x1,x2,x3)\<in>edges (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) distinct_elim x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
hence "(x1,x2,x3)\<in>{e \<in> edges (rem_unPath xs G). fst e = v'}"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. (x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
using \<open>v=v'\<close> x  Cons
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)
v = v'
x = (x1, x2, x3)
\<lbrakk>finite E; is_trail ?v xs v'\<rbrakk> \<Longrightarrow> (?v \<noteq> v') = (odd (degree v' (rem_unPath xs G)) = even (degree v' G))
finite E
is_trail v (x # xs) v'

goal (1 subgoal):
 1. (x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
by (metis (lifting, mono_tags) fst_conv is_trail.simps(2) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
have "finite {e \<in> edges (rem_unPath xs G). fst e = v'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
finite E

goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}
[PROOF STEP]
have "degree v' (rem_unPath xs G)\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. degree v' (rem_unPath xs G) \<noteq> 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> {e \<in> edges (rem_unPath xs G). fst e = v'}
finite {e \<in> edges (rem_unPath xs G). fst e = v'}

goal (1 subgoal):
 1. card {e \<in> edges (rem_unPath xs G). fst e = v'} \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree v' (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree v' (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G) - 1) = even (degree v' (rem_unPath xs G))

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...\<noteq>even (degree v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree v' (rem_unPath xs G)) \<noteq> even (degree v' G)
[PROOF STEP]
using \<open>x3 \<noteq> v'\<close> assms
[PROOF STATE]
proof (prove)
using this:
x3 \<noteq> v'
finite E
is_trail v ps v'

goal (1 subgoal):
 1. even (degree v' (rem_unPath xs G)) \<noteq> even (degree v' G)
[PROOF STEP]
by (metis Cons.hyps Cons.prems(2)is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
even (degree v' (rem_unPath xs G)) \<noteq> even (degree v' G)

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
odd (degree v' (rem_unPath (x # xs) G)) \<noteq> even (degree v' G)
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G))\<noteq>even (degree v' G)"
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) \<noteq> even (degree v' G)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) \<noteq> even (degree v' G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) \<noteq> even (degree v' G)

goal (2 subgoals):
 1. \<lbrakk>x3 \<noteq> v'; v = v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
 2. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) \<noteq> even (degree v' G)

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
by (metis True)
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
assume "x3\<noteq>v'"
[PROOF STATE]
proof (state)
this:
x3 \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
using rem_x
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=odd(degree v' (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
have "v=x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = x1
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
v = x1

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
hence "v'\<notin>{x1,x3}"
[PROOF STATE]
proof (prove)
using this:
v = x1

goal (1 subgoal):
 1. v' \<notin> {x1, x3}
[PROOF STEP]
by (metis (mono_tags) False \<open>x3 \<noteq> v'\<close> empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
v' \<notin> {x1, x3}

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v' \<notin> {x1, x3}

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
have "valid_unMultigraph (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
have "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v' \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))
[PROOF STEP]
have "degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))
                            =degree v' (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
using this:
v' \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree v' (rem_unPath xs G)
[PROOF STEP]
using degree_frame
[PROOF STATE]
proof (prove)
using this:
v' \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))
\<lbrakk>finite E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G

goal (1 subgoal):
 1. degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree v' (rem_unPath xs G)
[PROOF STEP]
by (metis valid_unMultigraph.degree_frame)
[PROOF STATE]
proof (state)
this:
degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree v' (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree v' (rem_unPath xs G)

goal (1 subgoal):
 1. odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))) = odd (degree v' (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
have "...=even (degree v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G)) = even (degree v' G)
[PROOF STEP]
using assms x \<open>x3 \<noteq> v'\<close>
[PROOF STATE]
proof (prove)
using this:
finite E
is_trail v ps v'
x = (x1, x2, x3)
x3 \<noteq> v'

goal (1 subgoal):
 1. odd (degree v' (rem_unPath xs G)) = even (degree v' G)
[PROOF STEP]
by (metis Cons.hyps Cons.prems(2)  is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath xs G)) = even (degree v' G)

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)
[PROOF STEP]
have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)"
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. \<lbrakk>x3 \<noteq> v'; v \<noteq> v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G)

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
by (metis False)
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x3 \<noteq> v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath ps G)) = even (degree v' G)); finite E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (a # ps) G)) = even (degree v' G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x3 = v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
x3 \<noteq> v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x3 = v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
x3 \<noteq> v' \<Longrightarrow> (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v \<noteq> v') = (odd (degree v' (rem_unPath (x # xs) G)) = even (degree v' G))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) rem_UnPath_parity_v:
  assumes "finite E"  "is_trail v ps v'"
  shows "v\<noteq>v' \<longleftrightarrow> (odd (degree v (rem_unPath ps G)) = even(degree v G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<noteq> v') = (odd (degree v (rem_unPath ps G)) = even (degree v G))
[PROOF STEP]
by (metis assms is_trail_rev rem_UnPath_parity_v' rem_unPath_graph)


[STATEMENT]
lemma (in valid_unMultigraph) rem_UnPath_parity_others:
  assumes "finite E"  "is_trail v ps v'" "n\<notin>{v,v'}"
  shows " even (degree n (rem_unPath ps G)) = even(degree n G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (rem_unPath ps G)) = even (degree n G)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite E
is_trail v ps v'
n \<notin> {v, v'}

goal (1 subgoal):
 1. even (degree n (rem_unPath ps G)) = even (degree n G)
[PROOF STEP]
proof (induct ps arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; is_trail v [] v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath [] G)) = even (degree n G)
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
finite E
is_trail v [] v'
n \<notin> {v, v'}

goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; is_trail v [] v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath [] G)) = even (degree n G)
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite E
is_trail v [] v'
n \<notin> {v, v'}

goal (1 subgoal):
 1. even (degree n (rem_unPath [] G)) = even (degree n G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath [] G)) = even (degree n G)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite E; is_trail ?v xs v'; n \<notin> {?v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath xs G)) = even (degree n G)
finite E
is_trail v (x # xs) v'
n \<notin> {v, v'}

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
hence "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com)
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
have "n=x3 \<Longrightarrow>?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
assume "n=x3"
[PROOF STATE]
proof (state)
this:
n = x3

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com x)
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "...=even(degree n (rem_unPath xs G) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
have "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x1,x2,x3) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
have "(x3,x2,x1) \<in>edges( rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
using \<open>n = x3\<close> del_edge_undirected_degree_minus'
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath xs G))
(x1, x2, x3) \<in> edges (rem_unPath xs G)
(x3, x2, x1) \<in> edges (rem_unPath xs G)
n = x3
\<lbrakk>finite (edges ?g); (?v, ?e, ?v') \<in> edges ?g; (?v', ?e, ?v) \<in> edges ?g\<rbrakk> \<Longrightarrow> degree ?v' (del_unEdge ?v ?e ?v' ?g) = degree ?v' ?g - 1

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G) - 1)

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "...=odd(degree n (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
have "(x1,x2,x3)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> E
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
hence "(x3,x2,x1)\<in>edges (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> E

goal (1 subgoal):
 1. (x3, x2, x1) \<in> edges (rem_unPath xs G)
[PROOF STEP]
by (metis Cons.prems(2) corres distinct_elim_rev x)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
hence "(x3,x2,x1)\<in>{e \<in> edges (rem_unPath xs G). fst e = n}"
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)

goal (1 subgoal):
 1. (x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}
[PROOF STEP]
using \<open>n=x3\<close>
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> edges (rem_unPath xs G)
n = x3

goal (1 subgoal):
 1. (x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}
[PROOF STEP]
by (metis (mono_tags) fst_conv mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
have "finite {e \<in> edges (rem_unPath xs G). fst e = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = n}
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
finite E

goal (1 subgoal):
 1. finite {e \<in> edges (rem_unPath xs G). fst e = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {e \<in> edges (rem_unPath xs G). fst e = n}

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}
finite {e \<in> edges (rem_unPath xs G). fst e = n}
[PROOF STEP]
have "degree n (rem_unPath xs G)\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}
finite {e \<in> edges (rem_unPath xs G). fst e = n}

goal (1 subgoal):
 1. degree n (rem_unPath xs G) \<noteq> 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> {e \<in> edges (rem_unPath xs G). fst e = n}
finite {e \<in> edges (rem_unPath xs G). fst e = n}

goal (1 subgoal):
 1. card {e \<in> edges (rem_unPath xs G). fst e = n} \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree n (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree n (rem_unPath xs G) \<noteq> 0

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath xs G) - 1) = odd (degree n (rem_unPath xs G))

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "...=even(degree n G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
have "x3\<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x3 \<noteq> v'
[PROOF STEP]
by (metis \<open>n = x3\<close> assms(3) insert_iff)
[PROOF STATE]
proof (state)
this:
x3 \<noteq> v'

goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
hence "odd (degree x3 (rem_unPath xs G)) = even(degree x3 G)"
[PROOF STATE]
proof (prove)
using this:
x3 \<noteq> v'

goal (1 subgoal):
 1. odd (degree x3 (rem_unPath xs G)) = even (degree x3 G)
[PROOF STEP]
using Cons assms
[PROOF STATE]
proof (prove)
using this:
x3 \<noteq> v'
\<lbrakk>finite E; is_trail ?v xs v'; n \<notin> {?v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath xs G)) = even (degree n G)
finite E
is_trail v (x # xs) v'
n \<notin> {v, v'}
finite E
is_trail v ps v'
n \<notin> {v, v'}

goal (1 subgoal):
 1. odd (degree x3 (rem_unPath xs G)) = even (degree x3 G)
[PROOF STEP]
by (metis is_trail.simps(2) rem_UnPath_parity_v x)
[PROOF STATE]
proof (state)
this:
odd (degree x3 (rem_unPath xs G)) = even (degree x3 G)

goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree x3 (rem_unPath xs G)) = even (degree x3 G)

goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
using \<open>n=x3\<close>
[PROOF STATE]
proof (prove)
using this:
odd (degree x3 (rem_unPath xs G)) = even (degree x3 G)
n = x3

goal (1 subgoal):
 1. odd (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree n (rem_unPath xs G)) = even (degree n G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
odd (degree n (rem_unPath xs G)) = even (degree n G)

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)"
[PROOF STATE]
proof (prove)
using this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
have "n\<noteq>x3 \<Longrightarrow>?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
assume "n\<noteq>x3"
[PROOF STATE]
proof (state)
this:
n \<noteq> x3

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com x)
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)))

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "...=even(degree n (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
have "v=x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = x1
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
v = x1

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
hence "n\<notin>{x1,x3}"
[PROOF STATE]
proof (prove)
using this:
v = x1

goal (1 subgoal):
 1. n \<notin> {x1, x3}
[PROOF STEP]
by (metis Cons.prems(3) \<open>n \<noteq> x3\<close> insertE insertI1 singletonE)
[PROOF STATE]
proof (state)
this:
n \<notin> {x1, x3}

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<notin> {x1, x3}

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
have "valid_unMultigraph (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
have "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))
[PROOF STEP]
have "degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))
                            =degree n (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
using this:
n \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree n (rem_unPath xs G)
[PROOF STEP]
using degree_frame
[PROOF STATE]
proof (prove)
using this:
n \<notin> {x1, x3}
valid_unMultigraph (rem_unPath xs G)
finite (edges (rem_unPath xs G))
\<lbrakk>finite E; ?x \<notin> {?v, ?v'}\<rbrakk> \<Longrightarrow> degree ?x (del_unEdge ?v ?w ?v' G) = degree ?x G

goal (1 subgoal):
 1. degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree n (rem_unPath xs G)
[PROOF STEP]
by (metis valid_unMultigraph.degree_frame)
[PROOF STATE]
proof (state)
this:
degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree n (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)) = degree n (rem_unPath xs G)

goal (1 subgoal):
 1. even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
even (degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))) = even (degree n (rem_unPath xs G))

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "...=even(degree n G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
using Cons assms \<open>n \<noteq> x3\<close> x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite E; is_trail ?v xs v'; n \<notin> {?v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath xs G)) = even (degree n G)
finite E
is_trail v (x # xs) v'
n \<notin> {v, v'}
finite E
is_trail v ps v'
n \<notin> {v, v'}
n \<noteq> x3
x = (x1, x2, x3)

goal (1 subgoal):
 1. even (degree n (rem_unPath xs G)) = even (degree n G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath xs G)) = even (degree n G)

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)"
[PROOF STATE]
proof (prove)
using this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; is_trail v ps v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath ps G)) = even (degree n G); finite E; is_trail v (a # ps) v'; n \<notin> {v, v'}\<rbrakk> \<Longrightarrow> even (degree n (rem_unPath (a # ps) G)) = even (degree n G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
n \<noteq> x3 \<Longrightarrow> even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal (1 subgoal):
 1. even (degree n (rem_unPath (x # xs) G)) = even (degree n G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (degree n (rem_unPath (x # xs) G)) = even (degree n G)

goal:
No subgoals!
[PROOF STEP]
qed