[STATEMENT]
lemma excess'_v[simp]: "excess f' v = excess f v + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. excess f' v = excess f v + \<Delta>
[PROOF STEP]
unfolding excess_def[where f=f']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
show "sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
proof (cases rule: uv_edge_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
case [simp]: par
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E
(v, u) \<notin> E

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have UV_INO: "(u,v)\<in>incoming v - outgoing v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> incoming v - outgoing v
[PROOF STEP]
unfolding incoming_def outgoing_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> {(u, v) |u. (u, v) \<in> E} - {(v, u) |u. (v, u) \<in> E}
[PROOF STEP]
by (auto simp: no_self_loop)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> incoming v - outgoing v

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have 1: "sum f' (outgoing v) = sum f (outgoing v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (outgoing v) = sum f (outgoing v)
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> incoming v - outgoing v

goal (1 subgoal):
 1. sum f' (outgoing v) = sum f (outgoing v)
[PROOF STEP]
unfolding f'_alt
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> incoming v - outgoing v

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v) = sum f (outgoing v)
[PROOF STEP]
by (auto simp: augment_edge_def intro: sum.cong)
[PROOF STATE]
proof (state)
this:
sum f' (outgoing v) = sum f (outgoing v)

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have "sum f' (incoming v)
        = sum f (incoming v) + (\<Sum>x\<in>incoming v. if x=(u,v) then \<Delta> else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming v) = sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a))
[PROOF STEP]
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta>) (incoming v) = (\<Sum>x\<in>incoming v. f x + (if x = (u, v) then \<Delta> else (0::'a)))
[PROOF STEP]
apply (rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. incoming v = incoming v
 2. \<And>x. x \<in> incoming v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (u, v) then \<Delta> else (0::'a))
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> incoming v - outgoing v

goal (2 subgoals):
 1. incoming v = incoming v
 2. \<And>x. x \<in> incoming v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (u, v) then \<Delta> else (0::'a))
[PROOF STEP]
unfolding f'_alt
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> incoming v - outgoing v

goal (2 subgoals):
 1. incoming v = incoming v
 2. \<And>x. x \<in> incoming v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (u, v) then \<Delta> else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) = sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a))

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) = sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a))

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have "\<dots> = sum f (incoming v) + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a)) = sum f (incoming v) + \<Delta>
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> incoming v - outgoing v

goal (1 subgoal):
 1. sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a)) = sum f (incoming v) + \<Delta>
[PROOF STEP]
by (auto simp: sum.delta)
[PROOF STATE]
proof (state)
this:
sum f (incoming v) + (\<Sum>x\<in>incoming v. if x = (u, v) then \<Delta> else (0::'a)) = sum f (incoming v) + \<Delta>

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f' (incoming v) = sum f (incoming v) + \<Delta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f' (incoming v) = sum f (incoming v) + \<Delta>

goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
sum f' (incoming v) = sum f (incoming v) + \<Delta>
sum f' (outgoing v) = sum f (outgoing v)

goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
by (auto simp: excess_def)
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
case [simp]: rev
[PROOF STATE]
proof (state)
this:
(v, u) \<in> E
(u, v) \<notin> E

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have UV_INO:"(v,u)\<in>outgoing v - incoming v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, u) \<in> outgoing v - incoming v
[PROOF STEP]
by (auto simp: incoming_def outgoing_def no_self_loop)
[PROOF STATE]
proof (state)
this:
(v, u) \<in> outgoing v - incoming v

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have 1: "sum f' (incoming v) = sum f (incoming v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming v) = sum f (incoming v)
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> outgoing v - incoming v

goal (1 subgoal):
 1. sum f' (incoming v) = sum f (incoming v)
[PROOF STEP]
unfolding f'_alt
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> outgoing v - incoming v

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (incoming v) = sum f (incoming v)
[PROOF STEP]
by (auto simp: augment_edge_def intro: sum.cong)
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) = sum f (incoming v)

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have "sum f' (outgoing v)
        = sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x=(v,u) then - \<Delta> else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (outgoing v) = sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a))
[PROOF STEP]
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta>) (outgoing v) = (\<Sum>x\<in>outgoing v. f x + (if x = (v, u) then - \<Delta> else (0::'a)))
[PROOF STEP]
apply (rule sum.cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. outgoing v = outgoing v
 2. \<And>x. x \<in> outgoing v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (v, u) then - \<Delta> else (0::'a))
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> outgoing v - incoming v

goal (2 subgoals):
 1. outgoing v = outgoing v
 2. \<And>x. x \<in> outgoing v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (v, u) then - \<Delta> else (0::'a))
[PROOF STEP]
unfolding f'_alt
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> outgoing v - incoming v

goal (2 subgoals):
 1. outgoing v = outgoing v
 2. \<And>x. x \<in> outgoing v \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. if (u, v) \<in> E then f((u, v) := f (u, v) + \<Delta>) else if (v, u) \<in> E then f((v, u) := f (v, u) - \<Delta>) else f) \<Delta> x = f x + (if x = (v, u) then - \<Delta> else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f' (outgoing v) = sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a))

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f' (outgoing v) = sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a))

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
have "\<dots> = sum f (outgoing v) - \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a)) = sum f (outgoing v) - \<Delta>
[PROOF STEP]
using UV_INO
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> outgoing v - incoming v

goal (1 subgoal):
 1. sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a)) = sum f (outgoing v) - \<Delta>
[PROOF STEP]
by (auto simp: sum.delta)
[PROOF STATE]
proof (state)
this:
sum f (outgoing v) + (\<Sum>x\<in>outgoing v. if x = (v, u) then - \<Delta> else (0::'a)) = sum f (outgoing v) - \<Delta>

goal (1 subgoal):
 1. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f' (outgoing v) = sum f (outgoing v) - \<Delta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f' (outgoing v) = sum f (outgoing v) - \<Delta>

goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
sum f' (outgoing v) = sum f (outgoing v) - \<Delta>
sum f' (incoming v) = sum f (incoming v)

goal (1 subgoal):
 1. sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>
[PROOF STEP]
by (auto simp: excess_def)
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum f' (incoming v) - sum f' (outgoing v) = excess f v + \<Delta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma excess'_other[simp]:
    assumes "x \<noteq> u" "x \<noteq> v"
    shows "excess f' x = excess f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. excess f' x = excess f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. excess f' x = excess f x
[PROOF STEP]
have NE: "(u,v)\<notin>incoming x" "(u,v)\<notin>outgoing x"
          "(v,u)\<notin>incoming x" "(v,u)\<notin>outgoing x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((u, v) \<notin> incoming x &&& (u, v) \<notin> outgoing x) &&& (v, u) \<notin> incoming x &&& (v, u) \<notin> outgoing x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
x \<noteq> v

goal (1 subgoal):
 1. ((u, v) \<notin> incoming x &&& (u, v) \<notin> outgoing x) &&& (v, u) \<notin> incoming x &&& (v, u) \<notin> outgoing x
[PROOF STEP]
unfolding incoming_def outgoing_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
x \<noteq> v

goal (1 subgoal):
 1. ((u, v) \<notin> {(u, x) |u. (u, x) \<in> E} &&& (u, v) \<notin> {(x, u) |u. (x, u) \<in> E}) &&& (v, u) \<notin> {(u, x) |u. (u, x) \<in> E} &&& (v, u) \<notin> {(x, u) |u. (x, u) \<in> E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<notin> incoming x
(u, v) \<notin> outgoing x
(v, u) \<notin> incoming x
(v, u) \<notin> outgoing x

goal (1 subgoal):
 1. excess f' x = excess f x
[PROOF STEP]
have
      "sum f' (outgoing x) = sum f (outgoing x)"
      "sum f' (incoming x) = sum f (incoming x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (outgoing x) = sum f (outgoing x) &&& sum f' (incoming x) = sum f (incoming x)
[PROOF STEP]
by (auto
            simp: augment_edge_def f'_alt NE
            split!: if_split
            intro: sum.cong)
[PROOF STATE]
proof (state)
this:
sum f' (outgoing x) = sum f (outgoing x)
sum f' (incoming x) = sum f (incoming x)

goal (1 subgoal):
 1. excess f' x = excess f x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f' (outgoing x) = sum f (outgoing x)
sum f' (incoming x) = sum f (incoming x)

goal (1 subgoal):
 1. excess f' x = excess f x
[PROOF STEP]
unfolding excess_def
[PROOF STATE]
proof (prove)
using this:
sum f' (outgoing x) = sum f (outgoing x)
sum f' (incoming x) = sum f (incoming x)

goal (1 subgoal):
 1. sum f' (incoming x) - sum f' (outgoing x) = sum f (incoming x) - sum f (outgoing x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
excess f' x = excess f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma excess'_if:
    "excess f' x = (
           if x=u then excess f u - \<Delta>
      else if x=v then excess f v + \<Delta>
         else excess f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. excess f' x = (if x = u then excess f u - \<Delta> else if x = v then excess f v + \<Delta> else excess f x)
[PROOF STEP]
by simp


[STATEMENT]
lemma cardE_nz_aux[simp, intro!]:
  "card E \<noteq> 0" "card E \<ge> Suc 0" "card E > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card E \<noteq> 0 &&& Suc 0 \<le> card E &&& 0 < card E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. card E \<noteq> 0
 2. Suc 0 \<le> card E
 3. 0 < card E
[PROOF STEP]
show "card E \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card E \<noteq> 0
[PROOF STEP]
by (simp add: E_not_empty)
[PROOF STATE]
proof (state)
this:
card E \<noteq> 0

goal (2 subgoals):
 1. Suc 0 \<le> card E
 2. 0 < card E
[PROOF STEP]
thus "card E \<ge> Suc 0"
[PROOF STATE]
proof (prove)
using this:
card E \<noteq> 0

goal (1 subgoal):
 1. Suc 0 \<le> card E
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Suc 0 \<le> card E

goal (1 subgoal):
 1. 0 < card E
[PROOF STEP]
thus "card E > 0"
[PROOF STATE]
proof (prove)
using this:
Suc 0 \<le> card E

goal (1 subgoal):
 1. 0 < card E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < card E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_V_est_E: "card V \<le> 2 * card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
have "card V \<le> card (fst`E) + card (snd`E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card V \<le> card (fst ` E) + card (snd ` E)
[PROOF STEP]
by (auto simp: card_Un_le V_alt)
[PROOF STATE]
proof (state)
this:
card V \<le> card (fst ` E) + card (snd ` E)

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card V \<le> card (fst ` E) + card (snd ` E)

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
note card_image_le[OF finite_E]
[PROOF STATE]
proof (state)
this:
card (?f ` E) \<le> card E

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (?f ` E) \<le> card E

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
note card_image_le[OF finite_E]
[PROOF STATE]
proof (state)
this:
card (?f ` E) \<le> card E

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> card (fst ` E) + x \<le> card (fst ` E) + y; \<And>x y. x \<le> y \<Longrightarrow> x + card E \<le> y + card E\<rbrakk> \<Longrightarrow> card V \<le> card E + card E
[PROOF STEP]
show "card V \<le> 2 * card E"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> card (fst ` E) + x \<le> card (fst ` E) + y; \<And>x y. x \<le> y \<Longrightarrow> x + card E \<le> y + card E\<rbrakk> \<Longrightarrow> card V \<le> card E + card E

goal (1 subgoal):
 1. card V \<le> 2 * card E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card V \<le> 2 * card E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma height_bound': "u\<in>V \<Longrightarrow> l u \<le> 2*card V - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> V \<Longrightarrow> l u \<le> 2 * card V - 1
[PROOF STEP]
using height_bound
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>V. l u \<le> 2 * card V - 1

goal (1 subgoal):
 1. u \<in> V \<Longrightarrow> l u \<le> 2 * card V - 1
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Network) pp_init_height_bound:
  "Height_Bounded_Labeling c s t pp_init_f pp_init_l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
interpret Labeling c s t pp_init_f pp_init_l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
by (rule pp_init_invar)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
by unfold_locales (auto simp: pp_init_l_def)
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t pp_init_f pp_init_l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma push_pres_height_bound:
  assumes "push_precond f l e"
  shows "Height_Bounded_Labeling c s t (push_effect f e) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t (push_effect f e) l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t (push_effect f e) l
[PROOF STEP]
from push_pres_Labeling[OF assms]
[PROOF STATE]
proof (chain)
picking this:
Labeling c s t (push_effect f e) l
[PROOF STEP]
interpret l': Labeling c s t "push_effect f e" l
[PROOF STATE]
proof (prove)
using this:
Labeling c s t (push_effect f e) l

goal (1 subgoal):
 1. Labeling c s t (push_effect f e) l
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t (push_effect f e) l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t (push_effect f e) l
[PROOF STEP]
using height_bound
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>V. l u \<le> 2 * card V - 1

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t (push_effect f e) l
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t (push_effect f e) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Labeling) excess_imp_source_path:
  assumes "excess f u > 0"
  obtains p where "cf.isSimplePath u p s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain U where U_def: "U = {v|p v. cf.isSimplePath u p v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U. U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}

goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have fct1: "U \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<subseteq> V
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> x \<in> V
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> x \<in> V
[PROOF STEP]
assume "v \<in> U"
[PROOF STATE]
proof (state)
this:
v \<in> U

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> x \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> U
[PROOF STEP]
have "(u, v) \<in> cf.E\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
v \<in> U

goal (1 subgoal):
 1. (u, v) \<in> cf.E\<^sup>*
[PROOF STEP]
using U_def cf.isSimplePath_def cf.isPath_rtc
[PROOF STATE]
proof (prove)
using this:
v \<in> U
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}
cf.isSimplePath ?u ?p ?v \<equiv> cf.isPath ?u ?p ?v \<and> distinct (cf.pathVertices ?u ?p)
cf.isPath ?u ?p ?v \<Longrightarrow> (?u, ?v) \<in> cf.E\<^sup>*

goal (1 subgoal):
 1. (u, v) \<in> cf.E\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cf.E\<^sup>*

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> x \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> cf.E\<^sup>*
[PROOF STEP]
obtain u' where "u = v \<or> ((u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E)"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cf.E\<^sup>*

goal (1 subgoal):
 1. (\<And>u'. u = v \<or> (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson rtranclE)
[PROOF STATE]
proof (state)
this:
u = v \<or> (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> x \<in> V
[PROOF STEP]
thus "v \<in> V"
[PROOF STATE]
proof (prove)
using this:
u = v \<or> (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E

goal (1 subgoal):
 1. v \<in> V
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> v \<in> V
 2. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
assume "u = v"
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> v \<in> V
 2. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. v \<in> V
[PROOF STEP]
using excess_nodes_only[OF assms]
[PROOF STATE]
proof (prove)
using this:
u = v
u \<in> V

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

goal (1 subgoal):
 1. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
assume "(u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E"
[PROOF STATE]
proof (state)
this:
(u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E

goal (1 subgoal):
 1. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E
[PROOF STEP]
have "v \<in> cf.V"
[PROOF STATE]
proof (prove)
using this:
(u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E

goal (1 subgoal):
 1. v \<in> cf.V
[PROOF STEP]
unfolding cf.V_def
[PROOF STATE]
proof (prove)
using this:
(u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E

goal (1 subgoal):
 1. v \<in> {u. \<exists>v. (u, v) \<in> cf.E \<or> (v, u) \<in> cf.E}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> cf.V

goal (1 subgoal):
 1. (u, u') \<in> cf.E\<^sup>* \<and> (u', v) \<in> cf.E \<Longrightarrow> v \<in> V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> cf.V

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U \<subseteq> V

goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "s \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> U
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
assume "s \<notin> U"
[PROOF STATE]
proof (state)
this:
s \<notin> U

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
obtain U' where U'_def: "U' = V - U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U'. U' = V - U \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U' = V - U

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
have "(\<Sum>u\<in>U. excess f u)
        = (\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (v, u))) - (\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (u, v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "(\<Sum>u\<in>U. excess f u)
          = (\<Sum>u\<in>U. (\<Sum>v\<in>incoming u. f v)) - (\<Sum>u\<in>U.(\<Sum>v\<in>outgoing u. f v))"
        (is "_ = ?R1 - ?R2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. sum f (incoming u)) - (\<Sum>u\<in>U. sum f (outgoing u))
[PROOF STEP]
unfolding excess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. sum f (incoming u) - sum f (outgoing u)) = (\<Sum>u\<in>U. sum f (incoming u)) - (\<Sum>u\<in>U. sum f (outgoing u))
[PROOF STEP]
by (simp add: sum_subtractf)
[PROOF STATE]
proof (state)
this:
sum (excess f) U = (\<Sum>u\<in>U. sum f (incoming u)) - (\<Sum>u\<in>U. sum f (outgoing u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (excess f) U = (\<Sum>u\<in>U. sum f (incoming u)) - (\<Sum>u\<in>U. sum f (outgoing u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "?R1 = (\<Sum>u\<in>U. (\<Sum>v\<in>V. f (v, u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. sum f (incoming u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u))
[PROOF STEP]
using sum_incoming_alt_flow fct1
[PROOF STATE]
proof (prove)
using this:
?u \<in> V \<Longrightarrow> sum f (incoming ?u) = (\<Sum>v\<in>V. f (v, ?u))
U \<subseteq> V

goal (1 subgoal):
 1. (\<Sum>u\<in>U. sum f (incoming u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u))
[PROOF STEP]
by (meson subsetCE sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. sum f (incoming u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. sum f (incoming u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "\<dots> = (\<Sum>u\<in>U. (\<Sum>v\<in>U. f (v, u))) + (\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (v, u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
have "(\<Sum>v\<in>V. f (v, u)) = (\<Sum>v\<in>U. f (v, u)) + (\<Sum>v\<in>U'. f (v, u))" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. f (v, u)) = (\<Sum>v\<in>U. f (v, u)) + (\<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
using U'_def fct1 finite_V
[PROOF STATE]
proof (prove)
using this:
U' = V - U
U \<subseteq> V
finite V

goal (1 subgoal):
 1. (\<Sum>v\<in>V. f (v, u)) = (\<Sum>v\<in>U. f (v, u)) + (\<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
by (metis ab_semigroup_add_class.add.commute sum.subset_diff)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. f (v, ?u)) = (\<Sum>v\<in>U. f (v, ?u)) + (\<Sum>v\<in>U'. f (v, ?u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>v\<in>V. f (v, ?u)) = (\<Sum>v\<in>U. f (v, ?u)) + (\<Sum>v\<in>U'. f (v, ?u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (v, u)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "?R2 = (\<Sum>u\<in>U. (\<Sum>v\<in>V. f (u, v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. sum f (outgoing u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v))
[PROOF STEP]
using sum_outgoing_alt_flow fct1
[PROOF STATE]
proof (prove)
using this:
?u \<in> V \<Longrightarrow> sum f (outgoing ?u) = (\<Sum>v\<in>V. f (?u, v))
U \<subseteq> V

goal (1 subgoal):
 1. (\<Sum>u\<in>U. sum f (outgoing u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v))
[PROOF STEP]
by (meson subsetCE sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. sum f (outgoing u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. sum f (outgoing u)) = (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "\<dots> = (\<Sum>u\<in>U. (\<Sum>v\<in>U. f (u, v))) + (\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (u, v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "(\<Sum>v\<in>V. f (u, v)) = (\<Sum>v\<in>U. f (u, v)) + (\<Sum>v\<in>U'. f (u, v))" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. f (u, v)) = (\<Sum>v\<in>U. f (u, v)) + (\<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
using U'_def fct1 finite_V
[PROOF STATE]
proof (prove)
using this:
U' = V - U
U \<subseteq> V
finite V

goal (1 subgoal):
 1. (\<Sum>v\<in>V. f (u, v)) = (\<Sum>v\<in>U. f (u, v)) + (\<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
by (metis ab_semigroup_add_class.add.commute sum.subset_diff)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. f (?u, v)) = (\<Sum>v\<in>U. f (?u, v)) + (\<Sum>v\<in>U'. f (?u, v))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>v\<in>V. f (?u, v)) = (\<Sum>v\<in>U. f (?u, v)) + (\<Sum>v\<in>U'. f (?u, v))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>V. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
have "(\<Sum>u\<in>U. (\<Sum>v\<in>U. f (u, v))) = (\<Sum>u\<in>U. (\<Sum>v\<in>U. f (v, u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
fix A :: "nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
assume "finite A"
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
have "(\<Sum>u\<in>A. (\<Sum>v\<in>A. f (u, v))) = (\<Sum>u\<in>A. (\<Sum>v\<in>A. f (v, u)))"
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
proof (induction "card A" arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = card A
finite A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>0 = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
 2. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = card A
finite A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = card A
finite A

goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = card ?A; finite ?A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (u, v)) = (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (v, u))
Suc x = card A
finite A

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = card ?A; finite ?A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (u, v)) = (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (v, u))
Suc x = card A
finite A
[PROOF STEP]
obtain A' a
              where o1:"A = insert a A'" and o2:"x = card A'" and o3:"finite A'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = card ?A; finite ?A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (u, v)) = (\<Sum>u\<in>?A. \<Sum>v\<in>?A. f (v, u))
Suc x = card A
finite A

goal (1 subgoal):
 1. (\<And>a A'. \<lbrakk>A = insert a A'; x = card A'; finite A'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis card_insert_disjoint card_le_Suc_iff le_refl nat.inject)
[PROOF STATE]
proof (state)
this:
A = insert a A'
x = card A'
finite A'

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = insert a A'
x = card A'
finite A'
[PROOF STEP]
have lm:"(\<Sum>e\<in>A. g e) = (\<Sum>e\<in>A'. g e) + g a"
              for g :: "nat \<Rightarrow> 'a"
[PROOF STATE]
proof (prove)
using this:
A = insert a A'
x = card A'
finite A'

goal (1 subgoal):
 1. sum g A = sum g A' + g a
[PROOF STEP]
using Suc.hyps(2)
[PROOF STATE]
proof (prove)
using this:
A = insert a A'
x = card A'
finite A'
Suc x = card A

goal (1 subgoal):
 1. sum g A = sum g A' + g a
[PROOF STEP]
by (metis card_insert_if n_not_Suc_n
                        semiring_normalization_rules(24) sum.insert)
[PROOF STATE]
proof (state)
this:
sum ?g A = sum ?g A' + ?g a

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
have "(\<Sum>u\<in>A. (\<Sum>v\<in>A. f (u, v)))
              = (\<Sum>u\<in>A'. (\<Sum>v\<in>A. f (u, v))) + (\<Sum>v\<in>A. f (a, v))"
              (is "_ = ?R1 + ?R2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) + (\<Sum>v\<in>A. f (a, v))
[PROOF STEP]
using lm
[PROOF STATE]
proof (prove)
using this:
sum ?g A = sum ?g A' + ?g a

goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) + (\<Sum>v\<in>A. f (a, v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) + (\<Sum>v\<in>A. f (a, v))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) + (\<Sum>v\<in>A. f (a, v))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
have "?R1 = (\<Sum>u\<in>A'. (\<Sum>v\<in>A'. f (u, v))) + (\<Sum>u\<in>A'. f(u, a))"
              (is "_ = ?R1_1 + ?R1_2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) + (\<Sum>u\<in>A'. f (u, a))
[PROOF STEP]
using lm sum.distrib
[PROOF STATE]
proof (prove)
using this:
sum ?g A = sum ?g A' + ?g a
(\<Sum>x\<in>?A. ?g x + ?h x) = sum ?g ?A + sum ?h ?A

goal (1 subgoal):
 1. (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) + (\<Sum>u\<in>A'. f (u, a))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) + (\<Sum>u\<in>A'. f (u, a))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) + (\<Sum>u\<in>A'. f (u, a))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
note add.assoc
[PROOF STATE]
proof (state)
this:
?a + ?b + ?c = ?a + (?b + ?c)

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?a + ?b + ?c = ?a + (?b + ?c)

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
have "?R1_2 + ?R2 = (\<Sum>u\<in>A'. f(a, u)) + (\<Sum>v\<in>A. f(v, a))"
              (is "_ = ?R1_2' + ?R2'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>A'. f (u, a)) + (\<Sum>v\<in>A. f (a, v)) = (\<Sum>u\<in>A'. f (a, u)) + (\<Sum>v\<in>A. f (v, a))
[PROOF STEP]
using lm
[PROOF STATE]
proof (prove)
using this:
sum ?g A = sum ?g A' + ?g a

goal (1 subgoal):
 1. (\<Sum>u\<in>A'. f (u, a)) + (\<Sum>v\<in>A. f (a, v)) = (\<Sum>u\<in>A'. f (a, u)) + (\<Sum>v\<in>A. f (v, a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. f (u, a)) + (\<Sum>v\<in>A. f (a, v)) = (\<Sum>u\<in>A'. f (a, u)) + (\<Sum>v\<in>A. f (v, a))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. f (u, a)) + (\<Sum>v\<in>A. f (a, v)) = (\<Sum>u\<in>A'. f (a, u)) + (\<Sum>v\<in>A. f (v, a))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
have "?R1_1 = (\<Sum>u\<in>A'. (\<Sum>v\<in>A'. f (v, u)))"
              (is "_ = ?R1_1'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u))
[PROOF STEP]
using Suc.hyps(1)[of A'] o2 o3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = card A'; finite A'\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u))
x = card A'
finite A'

goal (1 subgoal):
 1. (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
note add.assoc[symmetric]
[PROOF STATE]
proof (state)
this:
?a + (?b + ?c) = ?a + ?b + ?c

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?a + (?b + ?c) = ?a + ?b + ?c

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
have "?R1_1' + ?R1_2' = (\<Sum>u\<in>A'. (\<Sum>v\<in>A. f (v, u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u)) + (\<Sum>u\<in>A'. f (a, u)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
by (metis (no_types, lifting) lm sum.cong sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A'. \<Sum>v\<in>A'. f (v, u)) + (\<Sum>u\<in>A'. f (a, u)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (v, u))

goal (1 subgoal):
 1. \<And>x A. \<lbrakk>\<And>A. \<lbrakk>x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u)); Suc x = card A; finite A\<rbrakk> \<Longrightarrow> (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (v, u)) + (\<Sum>v\<in>A. f (v, a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (v, u)) + (\<Sum>v\<in>A. f (v, a))

goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
using lm[symmetric]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A'. \<Sum>v\<in>A. f (v, u)) + (\<Sum>v\<in>A. f (v, a))
sum ?g A' + ?g a = sum ?g A

goal (1 subgoal):
 1. (\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>A. \<Sum>v\<in>A. f (u, v)) = (\<Sum>u\<in>A. \<Sum>v\<in>A. f (v, u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
finite ?A2 \<Longrightarrow> (\<Sum>u\<in>?A2. \<Sum>v\<in>?A2. f (u, v)) = (\<Sum>u\<in>?A2. \<Sum>v\<in>?A2. f (v, u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
note this[of U]
[PROOF STATE]
proof (state)
this:
finite U \<Longrightarrow> (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite U \<Longrightarrow> (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
using fct1 finite_V finite_subset
[PROOF STATE]
proof (prove)
using this:
finite U \<Longrightarrow> (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
U \<subseteq> V
finite V
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. (\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>U. \<Sum>v\<in>U. f (u, v)) = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - ((\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - ((\<Sum>u\<in>U. \<Sum>v\<in>U. f (v, u)) + (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v)))

goal (1 subgoal):
 1. sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
have "(\<Sum>u\<in>U. excess f u) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
have "u \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> U
[PROOF STEP]
using U_def
[PROOF STATE]
proof (prove)
using this:
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}

goal (1 subgoal):
 1. u \<in> U
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> U

goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> U

goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
have "u \<in> U \<Longrightarrow> excess f u \<ge> 0" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> U \<Longrightarrow> (0::'a) \<le> excess f u
[PROOF STEP]
using fct1 excess_non_negative' \<open>s \<notin> U\<close>
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> V
\<forall>v\<in>V - {s}. (0::'a) \<le> excess f v
s \<notin> U

goal (1 subgoal):
 1. u \<in> U \<Longrightarrow> (0::'a) \<le> excess f u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?u \<in> U \<Longrightarrow> (0::'a) \<le> excess f ?u

goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> U
?u \<in> U \<Longrightarrow> (0::'a) \<le> excess f ?u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> U
?u \<in> U \<Longrightarrow> (0::'a) \<le> excess f ?u

goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
using assms fct1 finite_V
[PROOF STATE]
proof (prove)
using this:
u \<in> U
?u \<in> U \<Longrightarrow> (0::'a) \<le> excess f ?u
(0::'a) < excess f u
U \<subseteq> V
finite V

goal (1 subgoal):
 1. (0::'a) < sum (excess f) U
[PROOF STEP]
by (metis Diff_cancel Diff_eq_empty_iff
                  Diff_infinite_finite finite_Diff sum_pos2)
[PROOF STATE]
proof (state)
this:
(0::'a) < sum (excess f) U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(0::'a) < sum (excess f) U

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
(0::'a) < sum (excess f) U
[PROOF STEP]
have
      fct2: "(\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (v, u))) - (\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (u, v))) > 0"
[PROOF STATE]
proof (prove)
using this:
sum (excess f) U = (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
(0::'a) < sum (excess f) U

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
have fct3: "(\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (v, u))) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
have "(\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (v, u))) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
using capacity_const
[PROOF STATE]
proof (prove)
using this:
\<forall>e. (0::'a) \<le> f e \<and> f e \<le> c e

goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
by (simp add: sum_nonneg)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
have "(\<Sum>u\<in>U. (\<Sum>v\<in>U'. f (u, v))) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
using capacity_const
[PROOF STATE]
proof (prove)
using this:
\<forall>e. (0::'a) \<le> f e \<and> f e \<le> c e

goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
by (simp add: sum_nonneg)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
using fct2
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
(0::'a) \<le> (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))
(0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u)) - (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (u, v))

goal (1 subgoal):
 1. (0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
have "\<exists>u' v'. (u' \<in> U \<and> v' \<in> U' \<and> f (v', u') > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u') \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> f (v', u') > 0)"
[PROOF STATE]
proof (state)
this:
\<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')

goal (1 subgoal):
 1. \<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u') \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')
[PROOF STEP]
have "(\<forall>u' v'. (u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = 0))"
[PROOF STATE]
proof (prove)
using this:
\<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')

goal (1 subgoal):
 1. \<forall>u' v'. u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = (0::'a)
[PROOF STEP]
using capacity_const
[PROOF STATE]
proof (prove)
using this:
\<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')
\<forall>e. (0::'a) \<le> f e \<and> f e \<le> c e

goal (1 subgoal):
 1. \<forall>u' v'. u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = (0::'a)
[PROOF STEP]
by (metis le_neq_trans)
[PROOF STATE]
proof (state)
this:
\<forall>u' v'. u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = (0::'a)

goal (1 subgoal):
 1. \<nexists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u') \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<forall>u' v'. u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using fct3
[PROOF STATE]
proof (prove)
using this:
\<forall>u' v'. u' \<in> U \<and> v' \<in> U' \<longrightarrow> f (v', u') = (0::'a)
(0::'a) < (\<Sum>u\<in>U. \<Sum>v\<in>U'. f (v, u))

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')
[PROOF STEP]
obtain u' v' where "u' \<in> U" and "v' \<in> U'" and "f (v', u') > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>u' v'. u' \<in> U \<and> v' \<in> U' \<and> (0::'a) < f (v', u')

goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>u' \<in> U; v' \<in> U'; (0::'a) < f (v', u')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u' \<in> U
v' \<in> U'
(0::'a) < f (v', u')

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
obtain p1 where "cf.isSimplePath u p1 u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1. cf.isSimplePath u p1 u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using U_def \<open>u' \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}
u' \<in> U

goal (1 subgoal):
 1. (\<And>p1. cf.isSimplePath u p1 u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cf.isSimplePath u p1 u'

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cf.isSimplePath u p1 u'

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
have "(u', v') \<in> cf.E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u', v') \<in> cf.E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u', v') \<in> cf.E
[PROOF STEP]
have "(v', u') \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v', u') \<in> E
[PROOF STEP]
using capacity_const \<open>f (v', u') > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>e. (0::'a) \<le> f e \<and> f e \<le> c e
(0::'a) < f (v', u')

goal (1 subgoal):
 1. (v', u') \<in> E
[PROOF STEP]
by (metis not_less zero_flow_simp)
[PROOF STATE]
proof (state)
this:
(v', u') \<in> E

goal (1 subgoal):
 1. (u', v') \<in> cf.E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v', u') \<in> E
[PROOF STEP]
have "cf (u', v') > 0"
[PROOF STATE]
proof (prove)
using this:
(v', u') \<in> E

goal (1 subgoal):
 1. (0::'a) < cf (u', v')
[PROOF STEP]
unfolding cf_def
[PROOF STATE]
proof (prove)
using this:
(v', u') \<in> E

goal (1 subgoal):
 1. (0::'a) < (case (u', v') of (u, v) \<Rightarrow> if (u, v) \<in> E then c (u, v) - f (u, v) else if (v, u) \<in> E then f (v, u) else (0::'a))
[PROOF STEP]
using no_parallel_edge \<open>f (v', u') > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(v', u') \<in> E
\<forall>u v. (u, v) \<in> E \<longrightarrow> (v, u) \<notin> E
(0::'a) < f (v', u')

goal (1 subgoal):
 1. (0::'a) < (case (u', v') of (u, v) \<Rightarrow> if (u, v) \<in> E then c (u, v) - f (u, v) else if (v, u) \<in> E then f (v, u) else (0::'a))
[PROOF STEP]
by (auto split: if_split)
[PROOF STATE]
proof (state)
this:
(0::'a) < cf (u', v')

goal (1 subgoal):
 1. (u', v') \<in> cf.E
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) < cf (u', v')

goal (1 subgoal):
 1. (u', v') \<in> cf.E
[PROOF STEP]
unfolding cf.E_def
[PROOF STATE]
proof (prove)
using this:
(0::'a) < cf (u', v')

goal (1 subgoal):
 1. (u', v') \<in> {(u, v). cf (u, v) \<noteq> (0::'a)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(u', v') \<in> cf.E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u', v') \<in> cf.E

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cf.isSimplePath u p1 u'
(u', v') \<in> cf.E
[PROOF STEP]
have "cf.isPath u (p1 @ [(u', v')]) v'"
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p1 u'
(u', v') \<in> cf.E

goal (1 subgoal):
 1. cf.isPath u (p1 @ [(u', v')]) v'
[PROOF STEP]
using Graph.isPath_append_edge Graph.isSimplePath_def
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p1 u'
(u', v') \<in> cf.E
\<lbrakk>Graph.isPath ?c ?v ?p ?v'; (?v', ?v'') \<in> Graph.E ?c\<rbrakk> \<Longrightarrow> Graph.isPath ?c ?v (?p @ [(?v', ?v'')]) ?v''
Graph.isSimplePath ?c ?u ?p ?v \<equiv> Graph.isPath ?c ?u ?p ?v \<and> distinct (cf.pathVertices ?u ?p)

goal (1 subgoal):
 1. cf.isPath u (p1 @ [(u', v')]) v'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cf.isPath u (p1 @ [(u', v')]) v'

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cf.isPath u (p1 @ [(u', v')]) v'
[PROOF STEP]
obtain p2 where "cf.isSimplePath u p2 v'"
[PROOF STATE]
proof (prove)
using this:
cf.isPath u (p1 @ [(u', v')]) v'

goal (1 subgoal):
 1. (\<And>p2. cf.isSimplePath u p2 v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cf.isSPath_pathLE
[PROOF STATE]
proof (prove)
using this:
cf.isPath u (p1 @ [(u', v')]) v'
cf.isPath ?s ?p ?t \<Longrightarrow> \<exists>p'. cf.isSimplePath ?s p' ?t

goal (1 subgoal):
 1. (\<And>p2. cf.isSimplePath u p2 v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cf.isSimplePath u p2 v'

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cf.isSimplePath u p2 v'
[PROOF STEP]
have "v' \<in> U"
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p2 v'

goal (1 subgoal):
 1. v' \<in> U
[PROOF STEP]
using U_def
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p2 v'
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}

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

goal (1 subgoal):
 1. s \<notin> U \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v' \<in> U

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>v' \<in> U'\<close> and U'_def
[PROOF STATE]
proof (prove)
using this:
v' \<in> U
v' \<in> U'
U' = V - U

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s \<in> U

goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> U
[PROOF STEP]
obtain p' where "cf.isSimplePath u p' s"
[PROOF STATE]
proof (prove)
using this:
s \<in> U

goal (1 subgoal):
 1. (\<And>p'. cf.isSimplePath u p' s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using U_def
[PROOF STATE]
proof (prove)
using this:
s \<in> U
U = {uu_. \<exists>p v. uu_ = v \<and> cf.isSimplePath u p v}

goal (1 subgoal):
 1. (\<And>p'. cf.isSimplePath u p' s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cf.isSimplePath u p' s

goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p' s

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relabel_pres_height_bound:
  assumes "relabel_precond f l u"
  shows "Height_Bounded_Labeling c s t f (relabel_effect f l u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
let ?l' = "relabel_effect f l u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from relabel_pres_Labeling[OF assms]
[PROOF STATE]
proof (chain)
picking this:
Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
interpret l': Labeling c s t f ?l'
[PROOF STATE]
proof (prove)
using this:
Labeling c s t f (relabel_effect f l u)

goal (1 subgoal):
 1. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
relabel_precond f l u
[PROOF STEP]
have "excess f u > 0"
[PROOF STATE]
proof (prove)
using this:
relabel_precond f l u

goal (1 subgoal):
 1. (0::'a) < excess f u
[PROOF STEP]
unfolding relabel_precond_def
[PROOF STATE]
proof (prove)
using this:
u \<noteq> t \<and> (0::'a) < excess f u \<and> (\<forall>v. (u, v) \<in> cf.E \<longrightarrow> l u \<noteq> l v + 1)

goal (1 subgoal):
 1. (0::'a) < excess f u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) < excess f u

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
with l'.excess_imp_source_path
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(0::'a) < excess f ?u; \<And>p. cf.isSimplePath ?u p s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
(0::'a) < excess f u
[PROOF STEP]
obtain p where p_obt: "cf.isSimplePath u p s"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) < excess f ?u; \<And>p. cf.isSimplePath ?u p s \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
(0::'a) < excess f u

goal (1 subgoal):
 1. (\<And>p. cf.isSimplePath u p s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cf.isSimplePath u p s

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
have "u \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> V
[PROOF STEP]
using excess_nodes_only \<open>excess f u > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f ?v \<Longrightarrow> ?v \<in> V
(0::'a) < excess f u

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

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
[PROOF STEP]
have "length p < card V"
[PROOF STATE]
proof (prove)
using this:
u \<in> V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
using cf.simplePath_length_less_V[of u p] p_obt
[PROOF STATE]
proof (prove)
using this:
u \<in> V
\<lbrakk>u \<in> cf.V; cf.isSimplePath u p ?v\<rbrakk> \<Longrightarrow> length p < card cf.V
cf.isSimplePath u p s

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p < card V

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length p < card V

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
have "?l' u \<le> ?l' s + length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relabel_effect f l u u \<le> relabel_effect f l u s + length p
[PROOF STEP]
using p_obt l'.gen_valid[of u p s] p_obt
[PROOF STATE]
proof (prove)
using this:
cf.isSimplePath u p s
cf.isPath u p s \<Longrightarrow> relabel_effect f l u u \<le> relabel_effect f l u s + length p
cf.isSimplePath u p s

goal (1 subgoal):
 1. relabel_effect f l u u \<le> relabel_effect f l u s + length p
[PROOF STEP]
unfolding cf.isSimplePath_def
[PROOF STATE]
proof (prove)
using this:
cf.isPath u p s \<and> distinct (cf.pathVertices u p)
cf.isPath u p s \<Longrightarrow> relabel_effect f l u u \<le> relabel_effect f l u s + length p
cf.isPath u p s \<and> distinct (cf.pathVertices u p)

goal (1 subgoal):
 1. relabel_effect f l u u \<le> relabel_effect f l u s + length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
relabel_effect f l u u \<le> relabel_effect f l u s + length p

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
relabel_effect f l u u \<le> relabel_effect f l u s + length p

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
have "?l' s = card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relabel_effect f l u s = card V
[PROOF STEP]
using l'.Labeling_axioms Labeling_def Labeling_axioms_def
[PROOF STATE]
proof (prove)
using this:
Labeling c s t f (relabel_effect f l u)
Labeling ?c ?s ?t ?f ?l \<equiv> NPreflow ?c ?s ?t ?f \<and> Labeling_axioms ?c ?s ?t ?f ?l
Labeling_axioms ?c ?s ?t ?f ?l \<equiv> (\<forall>u v. (u, v) \<in> Graph.E (residualGraph ?c ?f) \<longrightarrow> ?l u \<le> ?l v + 1) \<and> ?l ?s = card (Graph.V ?c) \<and> ?l ?t = 0

goal (1 subgoal):
 1. relabel_effect f l u s = card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
relabel_effect f l u s = card V

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length p < card V
relabel_effect f l u u \<le> relabel_effect f l u s + length p
relabel_effect f l u s = card V
[PROOF STEP]
have "?l' u \<le> 2*card V - 1"
[PROOF STATE]
proof (prove)
using this:
length p < card V
relabel_effect f l u u \<le> relabel_effect f l u s + length p
relabel_effect f l u s = card V

goal (1 subgoal):
 1. relabel_effect f l u u \<le> 2 * card V - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
relabel_effect f l u u \<le> 2 * card V - 1

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
thus "Height_Bounded_Labeling c s t f ?l'"
[PROOF STATE]
proof (prove)
using this:
relabel_effect f l u u \<le> 2 * card V - 1

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relabel_effect f l u u \<le> 2 * card V - 1 \<Longrightarrow> \<forall>ua\<in>V. relabel_effect f l u ua \<le> 2 * card V - 1
[PROOF STEP]
using height_bound relabel_preserve_other
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>V. l u \<le> 2 * card V - 1
?u \<noteq> ?v \<Longrightarrow> relabel_effect f l ?u ?v = l ?v

goal (1 subgoal):
 1. relabel_effect f l u u \<le> 2 * card V - 1 \<Longrightarrow> \<forall>ua\<in>V. relabel_effect f l u ua \<le> 2 * card V - 1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Height_Bounded_Labeling c s t f (relabel_effect f l u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Network) sum_height_measure_is_OV2:
  "sum_heights_measure l \<le> 2*(card V)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_heights_measure l \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
unfolding  sum_heights_measure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "2 * card V - l v \<le> 2 * card V" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * card V - l v \<le> 2 * card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * card V - l ?v \<le> 2 * card V

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * card V - l ?v \<le> 2 * card V
[PROOF STEP]
have "(\<Sum>v\<in>V. 2 * card V - l v) \<le> (\<Sum>v\<in>V. 2 * card V)"
[PROOF STATE]
proof (prove)
using this:
2 * card V - l ?v \<le> 2 * card V

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> (\<Sum>v\<in>V. 2 * card V)
[PROOF STEP]
by (meson sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V - l v) \<le> (\<Sum>v\<in>V. 2 * card V)

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V - l v) \<le> (\<Sum>v\<in>V. 2 * card V)

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
have "(\<Sum>v\<in>V. 2 * card V) = card V * (2 * card V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V) = card V * (2 * card V)
[PROOF STEP]
using finite_V
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V) = card V * (2 * card V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V) = card V * (2 * card V)

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>v\<in>V. 2 * card V - l v) \<le> card V * (2 * card V)
[PROOF STEP]
show "(\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)^2"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>v\<in>V. 2 * card V - l v) \<le> card V * (2 * card V)

goal (1 subgoal):
 1. (\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>V. 2 * card V - l v) \<le> 2 * (card V)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Height_Bounded_Labeling) pr_algo_maintains_hb_labeling:
  assumes "((f,l),a,(f',l')) \<in> pr_algo_lts"
  shows "Height_Bounded_Labeling c s t f' l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f' l'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((f, l), a, f', l') \<in> pr_algo_lts

goal (1 subgoal):
 1. Height_Bounded_Labeling c s t f' l'
[PROOF STEP]
by cases (simp_all add: push_pres_height_bound relabel_pres_height_bound)


[STATEMENT]
lemma (in Height_Bounded_Labeling) pr_algo_term_maxflow:
  assumes "(f,l)\<notin>Domain pr_algo_lts"
  shows "isMaxFlow f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(f, l) \<notin> Domain pr_algo_lts
[PROOF STEP]
have "\<nexists>e. push_precond f l e" and "\<nexists>u. relabel_precond f l u"
[PROOF STATE]
proof (prove)
using this:
(f, l) \<notin> Domain pr_algo_lts

goal (1 subgoal):
 1. \<nexists>e. push_precond f l e &&& \<nexists>u. relabel_precond f l u
[PROOF STEP]
by (auto simp: Domain_iff dest: pr_algo_lts.intros)
[PROOF STATE]
proof (state)
this:
\<nexists>e. push_precond f l e
\<nexists>u. relabel_precond f l u

goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
with push_relabel_term_imp_maxflow
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>(u, v)\<in>cf.E. \<not> push_precond f l (u, v); \<forall>u. \<not> relabel_precond f l u\<rbrakk> \<Longrightarrow> isMaxFlow f
\<nexists>e. push_precond f l e
\<nexists>u. relabel_precond f l u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>(u, v)\<in>cf.E. \<not> push_precond f l (u, v); \<forall>u. \<not> relabel_precond f l u\<rbrakk> \<Longrightarrow> isMaxFlow f
\<nexists>e. push_precond f l e
\<nexists>u. relabel_precond f l u

goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isMaxFlow f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma push_precond_eq_sat_or_nonsat:
  "push_precond f l e \<longleftrightarrow> sat_push_precond f l e \<or> nonsat_push_precond f l e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. push_precond f l e = (sat_push_precond f l e \<or> nonsat_push_precond f l e)
[PROOF STEP]
unfolding push_precond_def sat_push_precond_def nonsat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1) = ((case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> cf_of f (u, v) \<le> excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1) \<or> (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> excess f u < cf_of f (u, v) \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1))
[PROOF STEP]
by auto


[STATEMENT]
lemma sat_nonsat_push_disj:
  "sat_push_precond f l e \<Longrightarrow> \<not>nonsat_push_precond f l e"
  "nonsat_push_precond f l e \<Longrightarrow> \<not>sat_push_precond f l e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sat_push_precond f l e \<Longrightarrow> \<not> nonsat_push_precond f l e) &&& (nonsat_push_precond f l e \<Longrightarrow> \<not> sat_push_precond f l e)
[PROOF STEP]
unfolding sat_push_precond_def nonsat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> cf_of f (u, v) \<le> excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1 \<Longrightarrow> \<not> (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> excess f u < cf_of f (u, v) \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1)) &&& (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> excess f u < cf_of f (u, v) \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1 \<Longrightarrow> \<not> (case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> cf_of f (u, v) \<le> excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1))
[PROOF STEP]
by auto


[STATEMENT]
lemma sat_push_alt: "sat_push_precond f l e
  \<Longrightarrow> push_effect f e = augment_edge f e (cf_of f e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sat_push_precond f l e \<Longrightarrow> push_effect f e = augment_edge f e (cf_of f e)
[PROOF STEP]
unfolding push_effect_def push_precond_eq_sat_or_nonsat sat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case e of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> cf_of f (u, v) \<le> excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1 \<Longrightarrow> (case e of (u, v) \<Rightarrow> augment_edge f (u, v) (min (excess f u) (cf_of f (u, v)))) = augment_edge f e (cf_of f e)
[PROOF STEP]
by (auto simp: min_absorb2)


[STATEMENT]
lemma nonsat_push_alt: "nonsat_push_precond f l (u,v)
  \<Longrightarrow> push_effect f (u,v) = augment_edge f (u,v) (excess f u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_push_precond f l (u, v) \<Longrightarrow> push_effect f (u, v) = augment_edge f (u, v) (excess f u)
[PROOF STEP]
unfolding push_effect_def push_precond_eq_sat_or_nonsat nonsat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (u, v) of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> excess f u < cf_of f (u, v) \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1 \<Longrightarrow> (case (u, v) of (u, v) \<Rightarrow> augment_edge f (u, v) (min (excess f u) (cf_of f (u, v)))) = augment_edge f (u, v) (excess f u)
[PROOF STEP]
by (auto simp: min_absorb1)


[STATEMENT]
lemma nonsat_push_\<Delta>: "nonsat_push_precond f l (u,v) \<Longrightarrow> \<Delta> = excess f u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nonsat_push_precond f l (u, v) \<Longrightarrow> \<Delta> = excess f u
[PROOF STEP]
unfolding \<Delta>_def nonsat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> excess f u < cf (u, v) \<and> (u, v) \<in> cf.E \<and> l u = l v + 1 \<Longrightarrow> min (excess f u) (cf (u, v)) = excess f u
[PROOF STEP]
by auto


[STATEMENT]
lemma sat_push_\<Delta>: "sat_push_precond f l (u,v) \<Longrightarrow> \<Delta> = cf (u,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sat_push_precond f l (u, v) \<Longrightarrow> \<Delta> = cf (u, v)
[PROOF STEP]
unfolding \<Delta>_def sat_push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> cf (u, v) \<le> excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1 \<Longrightarrow> min (excess f u) (cf (u, v)) = cf (u, v)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_RELABEL_project_conv[simp]:
  "is_RELABEL \<circ> project_operation = is_RELABEL'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_RELABEL \<circ> project_operation = is_RELABEL'
[PROOF STEP]
apply (clarsimp intro!: ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. is_RELABEL (project_operation x) = is_RELABEL' x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_RELABEL (project_operation x) = is_RELABEL' x
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_PUSH_project_conv[simp]:
  "is_PUSH \<circ> project_operation = (\<lambda>x. is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_PUSH \<circ> project_operation = (\<lambda>x. is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x)
[PROOF STEP]
apply (clarsimp intro!: ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. is_PUSH (project_operation x) = (is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_PUSH (project_operation x) = (is_SAT_PUSH' x \<or> is_NONSAT_PUSH' x)
[PROOF STEP]
by (cases x) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done