[STATEMENT]
lemma (in valid_unMultigraph) rem_UnPath_odd:
  assumes "finite E" "finite V" "is_trail v ps v'"
  assumes parity_assms:  "odd (degree v' G)"
  shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
          + (if odd (degree v G)\<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v ps v'
odd (degree v' G)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof (induct ps arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; finite V; is_trail v [] v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath [] G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
finite E
finite V
is_trail v [] v'
odd (degree v' G)

goal (2 subgoals):
 1. \<And>v. \<lbrakk>finite E; finite V; is_trail v [] v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath [] G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v [] v'
odd (degree v' G)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath [] G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath [] G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[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; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have fin_nodes: "finite (nodes (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (rem_unPath xs G))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have fin_edges: "finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have valid_rem_xs: "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. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have x_in:"(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 (full_types) Cons.prems(3) 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. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "even (degree x1 (rem_unPath xs G))
        \<Longrightarrow> even(degree x3 (rem_unPath xs G)) \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))"
                           "even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (state)
this:
even (degree x1 (rem_unPath xs G))
even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (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:
num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))

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

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "... =num_of_odd_nodes (rem_unPath xs G)+2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) + 2
[PROOF STEP]
using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in del_UnEdge_even_even
[PROOF STATE]
proof (prove)
using this:
even (degree x1 (rem_unPath xs G))
even (degree x3 (rem_unPath xs G))
finite (nodes (rem_unPath xs G))
finite (edges (rem_unPath xs G))
valid_unMultigraph (rem_unPath xs G)
(x1, x2, x3) \<in> edges (rem_unPath xs G)
\<lbrakk>valid_unMultigraph ?G; finite (edges ?G); finite (nodes ?G); (?v, ?w, ?v') \<in> edges ?G; even (degree ?v ?G); even (degree ?v' ?G)\<rbrakk> \<Longrightarrow> num_of_odd_nodes (del_unEdge ?v ?w ?v' ?G) = num_of_odd_nodes ?G + 2

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) + 2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) + 2

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

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree x3 G) \<and> x3\<noteq>v' then - 2 else 0 )+2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G) + 2) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2
[PROOF STEP]
using Cons.hyps[OF \<open>finite E\<close> \<open>finite V\<close>,of x3] \<open>is_trail v (x # xs) v'\<close>
          \<open>odd (degree v' G)\<close> x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_trail x3 xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
is_trail v (x # xs) v'
odd (degree v' G)
x = (x1, x2, x3)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G) + 2) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G) + 2) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G) + 2) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)
[PROOF STEP]
have "odd (degree x3 G) \<and> x3\<noteq>v' \<longleftrightarrow> even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
[PROOF STEP]
using Cons.prems assms
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)
[PROOF STEP]
using parity_x1_x3(2)
[PROOF STATE]
proof (prove)
using this:
(odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) + 2 = int (num_of_odd_nodes G)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof (cases "v\<noteq>v'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "x1\<noteq>x3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> x3
[PROOF STEP]
by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "is_trail x3 xs v' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail x3 xs v'
[PROOF STEP]
by (metis Cons.prems(3) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
is_trail x3 xs v'

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<noteq> x3
is_trail x3 xs v'
[PROOF STEP]
have  "even (degree x1 (rem_unPath xs G))
                          \<longleftrightarrow> even (degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
is_trail x3 xs v'

goal (1 subgoal):
 1. even (degree x1 (rem_unPath xs G)) = even (degree x1 G)
[PROOF STEP]
using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1)
                rem_UnPath_parity_others x
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
is_trail x3 xs v'
v \<noteq> v'
is_trail v (x # xs) v'
finite E
finite V
even (degree x1 (rem_unPath xs G))
\<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)
x = (x1, x2, x3)

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

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "even (degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
even (degree x1 (rem_unPath xs G)) = even (degree x1 G)

goal (1 subgoal):
 1. even (degree x1 G)
[PROOF STEP]
by (metis parity_x1_x3(1))
[PROOF STATE]
proof (state)
this:
even (degree x1 G)

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
even (degree x1 G)

goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by (metis (opaque_lifting, mono_tags) Cons.prems(3)  is_trail.simps(2)
                monoid_add_class.add.right_neutral x)
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> v \<noteq> v'

goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> v \<noteq> v'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> v \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "even (degree x1 (rem_unPath xs G)) \<Longrightarrow>
                    odd(degree x3 (rem_unPath xs G)) \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))"
                           "odd (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (state)
this:
even (degree x1 (rem_unPath xs G))
odd (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (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:
num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))

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

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "... =num_of_odd_nodes (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G)
[PROOF STEP]
using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in
[PROOF STATE]
proof (prove)
using this:
even (degree x1 (rem_unPath xs G))
odd (degree x3 (rem_unPath xs G))
finite (nodes (rem_unPath xs G))
finite (edges (rem_unPath xs G))
valid_unMultigraph (rem_unPath xs G)
(x1, x2, x3) \<in> edges (rem_unPath xs G)

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

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

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree x3 G) \<and> x3\<noteq>v' then - 2 else 0 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
[PROOF STEP]
using  Cons.hyps[OF \<open>finite E\<close> \<open>finite V\<close>, of x3] Cons.prems(3) assms(1) assms(2)
          parity_assms x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_trail x3 xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
is_trail v (x # xs) v'
finite E
finite V
odd (degree v' G)
x = (x1, x2, x3)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)
[PROOF STEP]
have "odd(degree x3 G) \<and> x3\<noteq>v' \<longleftrightarrow> even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
[PROOF STEP]
using Cons.prems assms
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)
[PROOF STEP]
using parity_x1_x3(2)
[PROOF STATE]
proof (prove)
using this:
(odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
odd (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...= num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof (cases "v\<noteq>v'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "x1\<noteq>x3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> x3
[PROOF STEP]
by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "is_trail x3 xs v' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail x3 xs v'
[PROOF STEP]
by (metis Cons.prems(3) is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
is_trail x3 xs v'

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<noteq> x3
is_trail x3 xs v'
[PROOF STEP]
have  "even (degree x1 (rem_unPath xs G))
                          \<longleftrightarrow> even (degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
is_trail x3 xs v'

goal (1 subgoal):
 1. even (degree x1 (rem_unPath xs G)) = even (degree x1 G)
[PROOF STEP]
using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1)
                rem_UnPath_parity_others x
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
is_trail x3 xs v'
v \<noteq> v'
is_trail v (x # xs) v'
finite E
finite V
even (degree x1 (rem_unPath xs G))
\<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)
x = (x1, x2, x3)

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

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "even (degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
even (degree x1 (rem_unPath xs G)) = even (degree x1 G)

goal (1 subgoal):
 1. even (degree x1 G)
[PROOF STEP]
by (metis parity_x1_x3(1))
[PROOF STATE]
proof (state)
this:
even (degree x1 G)

goal (2 subgoals):
 1. v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
 2. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
with Cons.prems(3) x
[PROOF STATE]
proof (chain)
picking this:
is_trail v (x # xs) v'
x = (x1, x2, x3)
even (degree x1 G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_trail v (x # xs) v'
x = (x1, x2, x3)
even (degree x1 G)

goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> v \<noteq> v'

goal (1 subgoal):
 1. \<not> v \<noteq> v' \<Longrightarrow> int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> v \<noteq> v'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> v \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "odd (degree x1 (rem_unPath xs G)) \<Longrightarrow>
                    even(degree x3 (rem_unPath xs G)) \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))"
                           "even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (state)
this:
odd (degree x1 (rem_unPath xs G))
even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (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:
num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))

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

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "... =num_of_odd_nodes (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G)
[PROOF STEP]
using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 (rem_unPath xs G))
even (degree x3 (rem_unPath xs G))
finite (nodes (rem_unPath xs G))
finite (edges (rem_unPath xs G))
valid_unMultigraph (rem_unPath xs G)
(x1, x2, x3) \<in> edges (rem_unPath xs G)

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

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

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree x3 G) \<and> x3\<noteq>v' then -2 else 0 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
[PROOF STEP]
using  Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
is_trail v (x # xs) v'
finite E
finite V
odd (degree v' G)
x = (x1, x2, x3)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G + (- 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2
[PROOF STEP]
have "odd(degree x3 G) \<and> x3\<noteq>v' \<longleftrightarrow> even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
[PROOF STEP]
using Cons.prems assms
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2
[PROOF STEP]
hence "odd(degree x3 G) \<and> x3\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
(odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree x3 G) \<and> x3 \<noteq> v'
[PROOF STEP]
by (metis parity_x1_x3(2))
[PROOF STATE]
proof (state)
this:
odd (degree x3 G) \<and> x3 \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree x3 G) \<and> x3 \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0) = int (num_of_odd_nodes G) + - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "x1\<noteq>x3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> x3
[PROOF STEP]
by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "x1\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3

goal (1 subgoal):
 1. x1 \<noteq> v'
[PROOF STEP]
using Cons assms
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

goal (1 subgoal):
 1. x1 \<noteq> v'
[PROOF STEP]
by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<noteq> x3
x1 \<noteq> v'
[PROOF STEP]
have "x1\<notin>{x3,v'}"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
x1 \<noteq> v'

goal (1 subgoal):
 1. x1 \<notin> {x3, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 \<notin> {x3, v'}

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence  "odd(degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
x1 \<notin> {x3, v'}

goal (1 subgoal):
 1. odd (degree x1 G)
[PROOF STEP]
using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1)
[PROOF STATE]
proof (prove)
using this:
x1 \<notin> {x3, v'}
is_trail v (x # xs) v'
finite E
finite V
odd (degree x1 (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree x1 G)
[PROOF STEP]
by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
[PROOF STATE]
proof (state)
this:
odd (degree x1 G)

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "odd(degree x1 G) \<and> x1\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G)

goal (1 subgoal):
 1. odd (degree x1 G) \<and> x1 \<noteq> v'
[PROOF STEP]
using \<open>x1 \<noteq> v'\<close>
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G)
x1 \<noteq> v'

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "odd(degree v G) \<and> v\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G) \<and> x1 \<noteq> v'

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree v G) \<and> v \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G) + - 2 = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree x1 (rem_unPath xs G)); even (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>finite E; finite V; is_trail v ps v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0); finite E; finite V; is_trail v (a # ps) v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (a # ps) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "odd (degree x1 (rem_unPath xs G)) \<Longrightarrow>
                    odd(degree x3 (rem_unPath xs G)) \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))"
                           "odd (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (state)
this:
odd (degree x1 (rem_unPath xs G))
odd (degree x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (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:
num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (rem_unPath (x # xs) G) = num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "... =num_of_odd_nodes (rem_unPath xs G)-(2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) - 2
[PROOF STEP]
using del_UnEdge_odd_odd
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_unMultigraph ?G; finite (edges ?G); finite (nodes ?G); (?v, ?w, ?v') \<in> edges ?G; odd (degree ?v ?G); odd (degree ?v' ?G)\<rbrakk> \<Longrightarrow> num_of_odd_nodes ?G = num_of_odd_nodes (del_unEdge ?v ?w ?v' ?G) + 2

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) - 2
[PROOF STEP]
by (metis add_implies_diff  fin_edges fin_nodes parity_x1_x3 valid_rem_xs x_in)
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G)) = num_of_odd_nodes (rem_unPath xs G) - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G -(2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2
[PROOF STEP]
have "odd(degree x3 G) \<and> x3\<noteq>v' \<longleftrightarrow> even (degree x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (odd (degree x3 G) \<and> x3 \<noteq> v') = even (degree x3 (rem_unPath xs G))
[PROOF STEP]
using Cons.prems assms
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

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

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

goal (1 subgoal):
 1. \<not> (odd (degree x3 G) \<and> x3 \<noteq> v')
[PROOF STEP]
by (metis parity_x1_x3(2))
[PROOF STATE]
proof (state)
this:
\<not> (odd (degree x3 G) \<and> x3 \<noteq> v')

goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath xs G)=
                  num_of_odd_nodes G+(if odd(degree x3 G) \<and> x3\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
[PROOF STEP]
by (metis Cons.hyps Cons.prems(3) assms(1) assms(2)
                is_trail.simps(2) parity_assms x)
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2
[PROOF STEP]
using \<open>\<not> (odd (degree x3 G) \<and> x3 \<noteq> v')\<close>
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree x3 G) \<and> x3 \<noteq> v' then - 2 else 0)
\<not> (odd (degree x3 G) \<and> x3 \<noteq> v')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (rem_unPath xs G) - 2 = num_of_odd_nodes G - 2

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "...=num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "x1\<noteq>x3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> x3
[PROOF STEP]
by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<noteq> x3

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "x1\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3

goal (1 subgoal):
 1. x1 \<noteq> v'
[PROOF STEP]
using Cons assms
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
\<lbrakk>finite E; finite V; is_trail ?v xs v'; odd (degree v' G)\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath xs G)) = int (num_of_odd_nodes G) + (if odd (degree ?v G) \<and> ?v \<noteq> v' then - 2 else 0)
finite E
finite V
is_trail v (x # xs) v'
odd (degree v' G)
finite E
finite V
is_trail v ps v'
odd (degree v' G)

goal (1 subgoal):
 1. x1 \<noteq> v'
[PROOF STEP]
by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 \<noteq> x3
x1 \<noteq> v'
[PROOF STEP]
have "x1\<notin>{x3,v'}"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> x3
x1 \<noteq> v'

goal (1 subgoal):
 1. x1 \<notin> {x3, v'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 \<notin> {x3, v'}

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence  "odd(degree x1 G)"
[PROOF STATE]
proof (prove)
using this:
x1 \<notin> {x3, v'}

goal (1 subgoal):
 1. odd (degree x1 G)
[PROOF STEP]
using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1)
[PROOF STATE]
proof (prove)
using this:
x1 \<notin> {x3, v'}
is_trail v (x # xs) v'
finite E
finite V
odd (degree x1 (rem_unPath xs G))

goal (1 subgoal):
 1. odd (degree x1 G)
[PROOF STEP]
by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
[PROOF STATE]
proof (state)
this:
odd (degree x1 G)

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "odd(degree x1 G) \<and> x1\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G)

goal (1 subgoal):
 1. odd (degree x1 G) \<and> x1 \<noteq> v'
[PROOF STEP]
using \<open>x1 \<noteq> v'\<close>
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G)
x1 \<noteq> v'

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "odd(degree v G) \<and> v\<noteq>v'"
[PROOF STATE]
proof (prove)
using this:
odd (degree x1 G) \<and> x1 \<noteq> v'

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
hence "v\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
odd (degree v G) \<and> v \<noteq> v'

goal (1 subgoal):
 1. v \<in> odd_nodes_set G
[PROOF STEP]
using Cons.prems(3) E_validD(1)  x
[PROOF STATE]
proof (prove)
using this:
odd (degree v G) \<and> v \<noteq> v'
is_trail v (x # xs) v'
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v \<in> V
x = (x1, x2, x3)

goal (1 subgoal):
 1. v \<in> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
odd (degree v G) \<and> v \<noteq> v'
is_trail v (x # xs) v'
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v \<in> V
x = (x1, x2, x3)

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set G

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "v'\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> odd_nodes_set G
[PROOF STEP]
using  is_path_memb[OF is_trail_intro[OF assms(3)]]  parity_assms
[PROOF STATE]
proof (prove)
using this:
v \<in> V \<and> v' \<in> V
odd (degree v' G)

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

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> odd_nodes_set G
v' \<in> odd_nodes_set G
[PROOF STEP]
have "{v,v'}\<subseteq>odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
v \<in> odd_nodes_set G
v' \<in> odd_nodes_set G

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v'} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "v\<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
by (metis \<open>odd (degree v G) \<and> v \<noteq> v'\<close>)
[PROOF STATE]
proof (state)
this:
v \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[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 auto
[PROOF STATE]
proof (state)
this:
card {v, v'} = 2

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {v, v'} = 2

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[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 V\<close>
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
finite V

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

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{v, v'} \<subseteq> odd_nodes_set G
card {v, v'} = 2
finite (odd_nodes_set G)
[PROOF STEP]
have "num_of_odd_nodes G\<ge>2"
[PROOF STATE]
proof (prove)
using this:
{v, v'} \<subseteq> odd_nodes_set G
card {v, v'} = 2
finite (odd_nodes_set G)

goal (1 subgoal):
 1. 2 \<le> num_of_odd_nodes G
[PROOF STEP]
by (metis card_mono num_of_odd_nodes_def)
[PROOF STATE]
proof (state)
this:
2 \<le> num_of_odd_nodes G

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 \<le> num_of_odd_nodes G

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
using \<open>odd (degree v G) \<and> v \<noteq> v'\<close>
[PROOF STATE]
proof (prove)
using this:
2 \<le> num_of_odd_nodes G
odd (degree v G) \<and> v \<noteq> v'

goal (1 subgoal):
 1. int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes G - 2) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) \<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. \<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree x1 (rem_unPath xs G)); odd (degree x3 (rem_unPath xs G))\<rbrakk> \<Longrightarrow> int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

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

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath (x # xs) G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) rem_UnPath_cycle:
  assumes "finite E" "finite V" "is_trail v ps v'" "v=v'"
  shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G" (is "?L=?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
proof  (cases "even(degree v' G)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. even (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
 2. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
even (degree v' G)

goal (2 subgoals):
 1. even (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
 2. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
hence "?L = num_of_odd_nodes G + (if even (degree v G)\<and> v\<noteq>v' then 2 else 0)"
[PROOF STATE]
proof (prove)
using this:
even (degree v' G)

goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G) \<and> v \<noteq> v' then 2 else 0)
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) rem_UnPath_even)
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G) \<and> v \<noteq> v' then 2 else 0)

goal (2 subgoals):
 1. even (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
 2. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite E
finite V
is_trail v ps v'
v = v'
num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G) \<and> v \<noteq> v' then 2 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite E
finite V
is_trail v ps v'
v = v'
num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G) \<and> v \<noteq> v' then 2 else 0)

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

goal (1 subgoal):
 1. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
odd (degree v' G)

goal (1 subgoal):
 1. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
hence "?L = num_of_odd_nodes G + (if odd (degree v G)\<and> v\<noteq>v' then -2 else 0)"
[PROOF STATE]
proof (prove)
using this:
odd (degree v' G)

goal (1 subgoal):
 1. int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) rem_UnPath_odd)
[PROOF STATE]
proof (state)
this:
int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. odd (degree v' G) \<Longrightarrow> num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)

goal (1 subgoal):
 1. num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
[PROOF STEP]
using \<open>v = v'\<close>
[PROOF STATE]
proof (prove)
using this:
int (num_of_odd_nodes (rem_unPath ps G)) = int (num_of_odd_nodes G) + (if odd (degree v G) \<and> v \<noteq> v' then - 2 else 0)
v = v'

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

goal:
No subgoals!
[PROOF STEP]
qed