[STATEMENT]
lemma augment_edge_preflow_preserve: "\<lbrakk>0\<le>\<Delta>; \<Delta> \<le> cf (u,v); \<Delta> \<le> excess f u\<rbrakk>
  \<Longrightarrow> Preflow c s t (augment_edge f (u,v) \<Delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> Preflow c s t (augment_edge f (u, v) \<Delta>)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>e. (0::'capacity) \<le> augment_edge f (u, v) \<Delta> e \<and> augment_edge f (u, v) \<Delta> e \<le> c e
 2. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>va\<in>V - {s, t}. sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>e. (0::'capacity) \<le> augment_edge f (u, v) \<Delta> e \<and> augment_edge f (u, v) \<Delta> e \<le> c e
[PROOF STEP]
unfolding residualGraph_def augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> (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::'capacity)); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>e. (0::'capacity) \<le> (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> e \<and> (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> e \<le> c e
[PROOF STEP]
using capacity_const
[PROOF STATE]
proof (prove)
using this:
\<forall>e. (0::'capacity) \<le> f e \<and> f e \<le> c e

goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> (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::'capacity)); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>e. (0::'capacity) \<le> (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> e \<and> (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> e \<le> c e
[PROOF STEP]
by (fastforce split!: if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>va\<in>V - {s, t}. sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u\<rbrakk> \<Longrightarrow> \<forall>va\<in>V - {s, t}. sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
proof (intro ballI; clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>va. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u; va \<in> V; va \<noteq> s; va \<noteq> t\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
assume "0\<le>\<Delta>" "\<Delta> \<le> cf (u,v)" "\<Delta> \<le> excess f u"
[PROOF STATE]
proof (state)
this:
(0::'capacity) \<le> \<Delta>
\<Delta> \<le> cf (u, v)
\<Delta> \<le> excess f u

goal (1 subgoal):
 1. \<And>va. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u; va \<in> V; va \<noteq> s; va \<noteq> t\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
fix v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>va. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u; va \<in> V; va \<noteq> s; va \<noteq> t\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
assume V': "v'\<in>V" "v'\<noteq>s" "v'\<noteq>t"
[PROOF STATE]
proof (state)
this:
v' \<in> V
v' \<noteq> s
v' \<noteq> t

goal (1 subgoal):
 1. \<And>va. \<lbrakk>(0::'capacity) \<le> \<Delta>; \<Delta> \<le> cf (u, v); \<Delta> \<le> excess f u; va \<in> V; va \<noteq> s; va \<noteq> t\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing va) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming va)
[PROOF STEP]
show "sum (augment_edge f (u, v) \<Delta>) (outgoing v')
            \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume "\<Delta> = 0"
[PROOF STATE]
proof (state)
this:
\<Delta> = (0::'capacity)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
with no_deficient_nodes
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
\<Delta> = (0::'capacity)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
\<Delta> = (0::'capacity)

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
using V'
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
\<Delta> = (0::'capacity)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

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

goal (1 subgoal):
 1. \<Delta> \<noteq> (0::'capacity) \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta> \<noteq> (0::'capacity) \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume "\<Delta> \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<Delta> \<noteq> (0::'capacity)

goal (1 subgoal):
 1. \<Delta> \<noteq> (0::'capacity) \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
with \<open>0\<le>\<Delta>\<close>
[PROOF STATE]
proof (chain)
picking this:
(0::'capacity) \<le> \<Delta>
\<Delta> \<noteq> (0::'capacity)
[PROOF STEP]
have "0<\<Delta>"
[PROOF STATE]
proof (prove)
using this:
(0::'capacity) \<le> \<Delta>
\<Delta> \<noteq> (0::'capacity)

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

goal (1 subgoal):
 1. \<Delta> \<noteq> (0::'capacity) \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
with \<open>\<Delta> \<le> cf (u,v)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Delta> \<le> cf (u, v)
(0::'capacity) < \<Delta>
[PROOF STEP]
have "(u,v)\<in>cf.E"
[PROOF STATE]
proof (prove)
using this:
\<Delta> \<le> cf (u, v)
(0::'capacity) < \<Delta>

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

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

goal (1 subgoal):
 1. \<Delta> \<noteq> (0::'capacity) \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: "(u,v)\<in>E"
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
hence AE: "augment_edge f (u,v) \<Delta> = f ( (u,v) := f (u,v) + \<Delta> )"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E

goal (1 subgoal):
 1. augment_edge f (u, v) \<Delta> = f((u, v) := f (u, v) + \<Delta>)
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E

goal (1 subgoal):
 1. (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> = f((u, v) := f (u, v) + \<Delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
augment_edge f (u, v) \<Delta> = f((u, v) := f (u, v) + \<Delta>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have 1: "\<forall>e\<in>outgoing v'. augment_edge f (u,v) \<Delta> e = f e" if "v'\<noteq>u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u

goal (1 subgoal):
 1. \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
unfolding outgoing_def AE
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u

goal (1 subgoal):
 1. \<forall>e\<in>{(v', u) |u. (v', u) \<in> E}. (f((u, v) := f (u, v) + \<Delta>)) e = f e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have 2: "\<forall>e\<in>incoming v'. augment_edge f (u,v) \<Delta> e = f e" if "v'\<noteq>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v

goal (1 subgoal):
 1. \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
unfolding incoming_def AE
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v

goal (1 subgoal):
 1. \<forall>e\<in>{(u, v') |u. (u, v') \<in> E}. (f((u, v) := f (u, v) + \<Delta>)) e = f e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
from \<open>(u,v)\<in>E\<close> no_self_loop
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> E
\<forall>u. (u, u) \<notin> E
[PROOF STEP]
have "u\<noteq>v"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E
\<forall>u. (u, u) \<notin> E

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume "v' \<noteq> u" "v' \<noteq> v"
[PROOF STATE]
proof (state)
this:
v' \<noteq> u
v' \<noteq> v

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
with 1 2 V' no_deficient_nodes
[PROOF STATE]
proof (chain)
picking this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
v' \<in> V
v' \<noteq> s
v' \<noteq> t
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<noteq> u
v' \<noteq> v
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
v' \<in> V
v' \<noteq> s
v' \<noteq> t
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<noteq> u
v' \<noteq> v

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: "v'=v"
[PROOF STATE]
proof (state)
this:
v' = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "sum (augment_edge f (u, v) \<Delta>) (outgoing v')
              = sum f (outgoing v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing v)
[PROOF STEP]
using 1 \<open>u\<noteq>v\<close> V'
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
u \<noteq> v
v' \<in> V
v' \<noteq> s
v' \<noteq> t

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing v)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "\<dots> \<le> sum f (incoming v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (outgoing v) \<le> sum f (incoming v)
[PROOF STEP]
using V' no_deficient_nodes
[PROOF STATE]
proof (prove)
using this:
v' \<in> V
v' \<noteq> s
v' \<noteq> t
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)

goal (1 subgoal):
 1. sum f (outgoing v) \<le> sum f (incoming v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f (outgoing v) \<le> sum f (incoming v)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f (outgoing v) \<le> sum f (incoming v)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "\<dots> \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (incoming v) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v)
[PROOF STEP]
apply (rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> incoming v \<Longrightarrow> f i \<le> augment_edge f (u, v) \<Delta> i
[PROOF STEP]
using \<open>0\<le>\<Delta>\<close>
[PROOF STATE]
proof (prove)
using this:
(0::'capacity) \<le> \<Delta>

goal (1 subgoal):
 1. \<And>i. i \<in> incoming v \<Longrightarrow> f i \<le> augment_edge f (u, v) \<Delta> i
[PROOF STEP]
by (auto simp: incoming_def augment_edge_def split!: if_split)
[PROOF STATE]
proof (state)
this:
sum f (incoming v) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v)

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: "v'=u"
[PROOF STATE]
proof (state)
this:
v' = u

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have A1: "sum (augment_edge f (u,v) \<Delta>) (incoming v')
                  = sum f (incoming u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (incoming v') = sum f (incoming u)
[PROOF STEP]
using 2 \<open>u\<noteq>v\<close>
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
u \<noteq> v

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "(u,v) \<in> outgoing u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> outgoing u
[PROOF STEP]
using \<open>(u,v)\<in>E\<close>
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E

goal (1 subgoal):
 1. (u, v) \<in> outgoing u
[PROOF STEP]
by (auto simp: outgoing_def)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> outgoing u

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
note AUX = sum.remove[OF _ this, simplified]
[PROOF STATE]
proof (state)
this:
sum ?g (outgoing u) = ?g (u, v) + sum ?g (outgoing u - {(u, v)})

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have A2: "sum (augment_edge f (u,v) \<Delta>) (outgoing u)
                  = sum f (outgoing u) + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing u) = sum f (outgoing u) + \<Delta>
[PROOF STEP]
using AUX[of "augment_edge f (u,v) \<Delta>"] AUX[of "f"]
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (outgoing u) = augment_edge f (u, v) \<Delta> (u, v) + sum (augment_edge f (u, v) \<Delta>) (outgoing u - {(u, v)})
sum f (outgoing u) = f (u, v) + sum f (outgoing u - {(u, v)})

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
from A1 A2 \<open>\<Delta> \<le> excess f u\<close> no_deficient_nodes V'
[PROOF STATE]
proof (chain)
picking this:
sum (augment_edge f (u, v) \<Delta>) (incoming v') = sum f (incoming u)
sum (augment_edge f (u, v) \<Delta>) (outgoing u) = sum f (outgoing u) + \<Delta>
\<Delta> \<le> excess f u
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (incoming v') = sum f (incoming u)
sum (augment_edge f (u, v) \<Delta>) (outgoing u) = sum f (outgoing u) + \<Delta>
\<Delta> \<le> excess f u
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
unfolding excess_def
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (incoming v') = sum f (incoming u)
sum (augment_edge f (u, v) \<Delta>) (outgoing u) = sum f (outgoing u) + \<Delta>
\<Delta> \<le> sum f (incoming u) - sum f (outgoing u)
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (2 subgoals):
 1. ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
 2. \<not> ?P \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: \<open>(u,v)\<notin>E\<close>
[PROOF STATE]
proof (state)
this:
(u, v) \<notin> E

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
hence [simp]: "(v,u)\<in>E"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<notin> E

goal (1 subgoal):
 1. (v, u) \<in> E
[PROOF STEP]
using cfE_ss_invE \<open>(u,v)\<in>cf.E\<close>
[PROOF STATE]
proof (prove)
using this:
(u, v) \<notin> E
cf.E \<subseteq> E \<union> E\<inverse>
(u, v) \<in> cf.E

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
from \<open>(u,v)\<notin>E\<close> \<open>(v,u)\<in>E\<close>
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<notin> E
(v, u) \<in> E
[PROOF STEP]
have "u\<noteq>v"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<notin> E
(v, u) \<in> E

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have AE: "augment_edge f (u,v) \<Delta> = f ( (v,u) := f (v,u) - \<Delta> )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. augment_edge f (u, v) \<Delta> = f((v, u) := f (v, u) - \<Delta>)
[PROOF STEP]
unfolding augment_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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> = f((v, u) := f (v, u) - \<Delta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
augment_edge f (u, v) \<Delta> = f((v, u) := f (v, u) - \<Delta>)

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have 1: "\<forall>e\<in>outgoing v'. augment_edge f (u,v) \<Delta> e = f e" if "v'\<noteq>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v

goal (1 subgoal):
 1. \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
unfolding outgoing_def AE
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v

goal (1 subgoal):
 1. \<forall>e\<in>{(v', u) |u. (v', u) \<in> E}. (f((v, u) := f (v, u) - \<Delta>)) e = f e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have 2: "\<forall>e\<in>incoming v'. augment_edge f (u,v) \<Delta> e = f e" if "v'\<noteq>u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u

goal (1 subgoal):
 1. \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
[PROOF STEP]
unfolding incoming_def AE
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u

goal (1 subgoal):
 1. \<forall>e\<in>{(u, v') |u. (u, v') \<in> E}. (f((v, u) := f (v, u) - \<Delta>)) e = f e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume "v' \<noteq> u" "v' \<noteq> v"
[PROOF STATE]
proof (state)
this:
v' \<noteq> u
v' \<noteq> v

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
with 1 2 V' no_deficient_nodes
[PROOF STATE]
proof (chain)
picking this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
v' \<in> V
v' \<noteq> s
v' \<noteq> t
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<noteq> u
v' \<noteq> v
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
v' \<in> V
v' \<noteq> s
v' \<noteq> t
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<noteq> u
v' \<noteq> v

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>v' \<noteq> u; v' \<noteq> v\<rbrakk> \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: "v'=u"
[PROOF STATE]
proof (state)
this:
v' = u

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have A1: "sum (augment_edge f (u, v) \<Delta>) (outgoing v')
                  = sum f (outgoing u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing u)
[PROOF STEP]
using 1 \<open>u\<noteq>v\<close> V'
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> v \<Longrightarrow> \<forall>e\<in>outgoing v'. augment_edge f (u, v) \<Delta> e = f e
u \<noteq> v
v' \<in> V
v' \<noteq> s
v' \<noteq> t

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "(v,u) \<in> incoming u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, u) \<in> incoming u
[PROOF STEP]
using \<open>(v,u)\<in>E\<close>
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> E

goal (1 subgoal):
 1. (v, u) \<in> incoming u
[PROOF STEP]
by (auto simp: incoming_def)
[PROOF STATE]
proof (state)
this:
(v, u) \<in> incoming u

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
note AUX = sum.remove[OF _ this, simplified]
[PROOF STATE]
proof (state)
this:
sum ?g (incoming u) = ?g (v, u) + sum ?g (incoming u - {(v, u)})

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have A2: "sum (augment_edge f (u,v) \<Delta>) (incoming u)
                  = sum f (incoming u) - \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (incoming u) = sum f (incoming u) - \<Delta>
[PROOF STEP]
using AUX[of "augment_edge f (u,v) \<Delta>"] AUX[of "f"]
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (incoming u) = augment_edge f (u, v) \<Delta> (v, u) + sum (augment_edge f (u, v) \<Delta>) (incoming u - {(v, u)})
sum f (incoming u) = f (v, u) + sum f (incoming u - {(v, u)})

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
from A1 A2 \<open>\<Delta> \<le> excess f u\<close> no_deficient_nodes V'
[PROOF STATE]
proof (chain)
picking this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing u)
sum (augment_edge f (u, v) \<Delta>) (incoming u) = sum f (incoming u) - \<Delta>
\<Delta> \<le> excess f u
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing u)
sum (augment_edge f (u, v) \<Delta>) (incoming u) = sum f (incoming u) - \<Delta>
\<Delta> \<le> excess f u
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
unfolding excess_def
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') = sum f (outgoing u)
sum (augment_edge f (u, v) \<Delta>) (incoming u) = sum f (incoming u) - \<Delta>
\<Delta> \<le> sum f (incoming u) - sum f (outgoing u)
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v' = u \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
assume [simp]: "v'=v"
[PROOF STATE]
proof (state)
this:
v' = v

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "sum (augment_edge f (u,v) \<Delta>) (outgoing v')
              \<le> sum f (outgoing v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum f (outgoing v')
[PROOF STEP]
apply (rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> outgoing v' \<Longrightarrow> augment_edge f (u, v) \<Delta> i \<le> f i
[PROOF STEP]
using \<open>0<\<Delta>\<close>
[PROOF STATE]
proof (prove)
using this:
(0::'capacity) < \<Delta>

goal (1 subgoal):
 1. \<And>i. i \<in> outgoing v' \<Longrightarrow> augment_edge f (u, v) \<Delta> i \<le> f i
[PROOF STEP]
by (auto simp: augment_edge_def)
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum f (outgoing v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum f (outgoing v')

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "\<dots> \<le> sum f (incoming v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (outgoing v') \<le> sum f (incoming v)
[PROOF STEP]
using no_deficient_nodes V'
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V - {s, t}. sum f (outgoing v) \<le> sum f (incoming v)
v' \<in> V
v' \<noteq> s
v' \<noteq> t

goal (1 subgoal):
 1. sum f (outgoing v') \<le> sum f (incoming v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f (outgoing v') \<le> sum f (incoming v)

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f (outgoing v') \<le> sum f (incoming v)

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have "\<dots> \<le> sum (augment_edge f (u,v) \<Delta>) (incoming v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (incoming v) \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
using 2 \<open>u\<noteq>v\<close>
[PROOF STATE]
proof (prove)
using this:
v' \<noteq> u \<Longrightarrow> \<forall>e\<in>incoming v'. augment_edge f (u, v) \<Delta> e = f e
u \<noteq> v

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

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

goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v' = v \<Longrightarrow> sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

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

goal (1 subgoal):
 1. sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (augment_edge f (u, v) \<Delta>) (outgoing v') \<le> sum (augment_edge f (u, v) \<Delta>) (incoming v')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma push_precondI[intro?]:
  "\<lbrakk>excess f u > 0; (u,v)\<in>cfE_of f; l u = l v + 1\<rbrakk> \<Longrightarrow> push_precond f l (u,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) < excess f u; (u, v) \<in> cfE_of f; l u = l v + 1\<rbrakk> \<Longrightarrow> push_precond f l (u, v)
[PROOF STEP]
unfolding push_precond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'capacity) < excess f u; (u, v) \<in> cfE_of f; l u = l v + 1\<rbrakk> \<Longrightarrow> case (u, v) of (u, v) \<Rightarrow> (0::'capacity) < excess f u \<and> (u, v) \<in> cfE_of f \<and> l u = l v + 1
[PROOF STEP]
by auto


[STATEMENT]
lemma pp_init_invar: "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]
apply (unfold_locales;
      ((auto simp: pp_init_f_def pp_init_l_def cap_non_negative; fail)
        | (intro ballI)?))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
assume "v\<in>V - {s,t}"
[PROOF STATE]
proof (state)
this:
v \<in> V - {s, t}

goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
hence "\<forall>e\<in>outgoing v. pp_init_f e = 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> V - {s, t}

goal (1 subgoal):
 1. \<forall>e\<in>outgoing v. pp_init_f e = (0::'capacity)
[PROOF STEP]
by (auto simp: outgoing_def pp_init_f_def)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>outgoing v. pp_init_f e = (0::'capacity)

goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
hence [simp]: "sum pp_init_f (outgoing v) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>outgoing v. pp_init_f e = (0::'capacity)

goal (1 subgoal):
 1. sum pp_init_f (outgoing v) = (0::'capacity)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum pp_init_f (outgoing v) = (0::'capacity)

goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
have "0 \<le> pp_init_f e" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'capacity) \<le> pp_init_f e
[PROOF STEP]
by (auto simp: pp_init_f_def cap_non_negative split: prod.split)
[PROOF STATE]
proof (state)
this:
(0::'capacity) \<le> pp_init_f ?e

goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
from sum_bounded_below[of "incoming v" 0 pp_init_f, OF this]
[PROOF STATE]
proof (chain)
picking this:
of_nat (card (incoming v)) * (0::'capacity) \<le> sum pp_init_f (incoming v)
[PROOF STEP]
have "0 \<le> sum pp_init_f (incoming v)"
[PROOF STATE]
proof (prove)
using this:
of_nat (card (incoming v)) * (0::'capacity) \<le> sum pp_init_f (incoming v)

goal (1 subgoal):
 1. (0::'capacity) \<le> sum pp_init_f (incoming v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'capacity) \<le> sum pp_init_f (incoming v)

goal (2 subgoals):
 1. \<And>v. v \<in> V - {s, t} \<Longrightarrow> sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
 2. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
thus "sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)"
[PROOF STATE]
proof (prove)
using this:
(0::'capacity) \<le> sum pp_init_f (incoming v)

goal (1 subgoal):
 1. sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum pp_init_f (outgoing v) \<le> sum pp_init_f (incoming v)

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
assume "(u, v) \<in> Graph.E (residualGraph c pp_init_f)"
[PROOF STATE]
proof (state)
this:
(u, v) \<in> cfE_of pp_init_f

goal (1 subgoal):
 1. \<And>u v. (u, v) \<in> cfE_of pp_init_f \<Longrightarrow> pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
thus "pp_init_l u \<le> pp_init_l v + 1"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cfE_of pp_init_f

goal (1 subgoal):
 1. pp_init_l u \<le> pp_init_l v + 1
[PROOF STEP]
unfolding pp_init_l_def Graph.E_def pp_init_f_def residualGraph_def
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> {(u, v). (case (u, v) of (u, v) \<Rightarrow> if (u, v) \<in> {(u, v). c (u, v) \<noteq> (0::'capacity)} then c (u, v) - (case (u, v) of (u, v) \<Rightarrow> if u = s then c (u, v) else (0::'capacity)) else if (v, u) \<in> {(u, v). c (u, v) \<noteq> (0::'capacity)} then case (v, u) of (u, v) \<Rightarrow> if u = s then c (u, v) else (0::'capacity) else (0::'capacity)) \<noteq> (0::'capacity)}

goal (1 subgoal):
 1. ((\<lambda>x. 0)(s := card V)) u \<le> ((\<lambda>x. 0)(s := card V)) v + 1
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
pp_init_l u \<le> pp_init_l v + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_init_f_preflow: "NPreflow c s t pp_init_f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NPreflow c s t pp_init_f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NPreflow c s t pp_init_f
[PROOF STEP]
from pp_init_invar
[PROOF STATE]
proof (chain)
picking this:
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)
using this:
Labeling c s t pp_init_f pp_init_l

goal (1 subgoal):
 1. Labeling c s t pp_init_f pp_init_l
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NPreflow c s t pp_init_f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NPreflow c s t pp_init_f
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
NPreflow c s t pp_init_f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem push_pres_Labeling:
  assumes "push_precond f l e"
  shows "Labeling c s t (push_effect f e) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t (push_effect f e) l
[PROOF STEP]
unfolding push_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t (case e of (u, v) \<Rightarrow> augment_edge f (u, v) (min (excess f u) (cf (u, v)))) l
[PROOF STEP]
proof (cases e; clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
assume [simp]: "e=(u,v)"
[PROOF STATE]
proof (state)
this:
e = (u, v)

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
let ?f' = "(augment_edge f (u, v) (min (excess f u) (cf (u, v))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
push_precond f l e
[PROOF STEP]
have
    ACTIVE: "excess f u > 0"
    and EDGE: "(u,v)\<in>cf.E"
    and ADM: "l u = l v + 1"
[PROOF STATE]
proof (prove)
using this:
push_precond f l e

goal (1 subgoal):
 1. (0::'a) < excess f u &&& (u, v) \<in> cf.E &&& l u = l v + 1
[PROOF STEP]
unfolding push_precond_def
[PROOF STATE]
proof (prove)
using this:
case e of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1

goal (1 subgoal):
 1. (0::'a) < excess f u &&& (u, v) \<in> cf.E &&& l u = l v + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) < excess f u
(u, v) \<in> cf.E
l u = l v + 1

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
interpret cf': Preflow c s t ?f'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Preflow c s t (augment_edge f (u, v) (min (excess f u) (cf (u, v))))
[PROOF STEP]
apply (rule augment_edge_preflow_preserve)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (0::'a) \<le> min (excess f u) (cf (u, v))
 2. min (excess f u) (cf (u, v)) \<le> cf (u, v)
 3. min (excess f u) (cf (u, v)) \<le> excess f u
[PROOF STEP]
using ACTIVE resE_nonNegative
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u
(0::'a) \<le> cf ?e

goal (3 subgoals):
 1. (0::'a) \<le> min (excess f u) (cf (u, v))
 2. min (excess f u) (cf (u, v)) \<le> cf (u, v)
 3. min (excess f u) (cf (u, v)) \<le> excess f u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> Labeling c s t (augment_edge f (a, b) (min (excess f a) (cf (a, b)))) l
[PROOF STEP]
show "Labeling c s t ?f' l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labeling c s t (augment_edge f (u, v) (min (excess f u) (cf (u, v)))) l
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ua va. (ua, va) \<in> cfE_of (augment_edge f (u, v) (min (excess f u) (cf (u, v)))) \<Longrightarrow> l ua \<le> l va + 1
 2. l s = card V
 3. l t = 0
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1

goal (3 subgoals):
 1. \<And>ua va. (ua, va) \<in> cfE_of (augment_edge f (u, v) (min (excess f u) (cf (u, v)))) \<Longrightarrow> l ua \<le> l va + 1
 2. l s = card V
 3. l t = 0
[PROOF STEP]
using cfE_augment_ss[OF EDGE] ADM
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1
cfE_of (augment_edge f (u, v) ?\<Delta>) \<subseteq> insert (v, u) cf.E
l u = l v + 1

goal (3 subgoals):
 1. \<And>ua va. (ua, va) \<in> cfE_of (augment_edge f (u, v) (min (excess f u) (cf (u, v)))) \<Longrightarrow> l ua \<le> l va + 1
 2. l s = card V
 3. l t = 0
[PROOF STEP]
apply (fastforce)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l s = card V
 2. l t = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Labeling c s t (augment_edge f (u, v) (min (excess f u) (cf (u, v)))) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_min_cf_outgoing[simp, intro!]: "finite {l v |v. (u, v) \<in> cf.E}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
have "{l v |v. (u, v) \<in> cf.E} = l`snd`cf.outgoing u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l v |v. (u, v) \<in> cf.E} = l ` snd ` cf.outgoing u
[PROOF STEP]
by (auto simp: cf.outgoing_def)
[PROOF STATE]
proof (state)
this:
{l v |v. (u, v) \<in> cf.E} = l ` snd ` cf.outgoing u

goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{l v |v. (u, v) \<in> cf.E} = l ` snd ` cf.outgoing u

goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
have "finite (l`snd`cf.outgoing u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (l ` snd ` cf.outgoing u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (l ` snd ` cf.outgoing u)

goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{l v |v. (u, v) \<in> cf.E} = l ` snd ` cf.outgoing u
finite (l ` snd ` cf.outgoing u)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{l v |v. (u, v) \<in> cf.E} = l ` snd ` cf.outgoing u
finite (l ` snd ` cf.outgoing u)

goal (1 subgoal):
 1. finite {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {l v |v. (u, v) \<in> cf.E}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem
  assumes PRE: "relabel_precond f l u"
  shows relabel_increase_u: "relabel_effect f l u u > l u" (is ?G1)
    and relabel_pres_Labeling: "Labeling c s t f (relabel_effect f l u)" (is ?G2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l u < relabel_effect f l u u &&& Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from PRE
[PROOF STATE]
proof (chain)
picking this:
relabel_precond f l u
[PROOF STEP]
have
        NOT_SINK: "u\<noteq>t"
    and ACTIVE: "excess f u > 0"
    and NO_ADM: "\<And>v. (u,v)\<in>cf.E \<Longrightarrow> l u \<noteq> l v + 1"
[PROOF STATE]
proof (prove)
using this:
relabel_precond f l u

goal (1 subgoal):
 1. u \<noteq> t &&& (0::'a) < excess f u &&& (\<And>v. (u, v) \<in> cf.E \<Longrightarrow> l u \<noteq> l v + 1)
[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. u \<noteq> t &&& (0::'a) < excess f u &&& (\<And>v. (u, v) \<in> cf.E \<Longrightarrow> l u \<noteq> l v + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> t
(0::'a) < excess f u
(u, ?v) \<in> cf.E \<Longrightarrow> l u \<noteq> l ?v + 1

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from ACTIVE
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < excess f u
[PROOF STEP]
have [simp]: "s\<noteq>u"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u

goal (1 subgoal):
 1. s \<noteq> u
[PROOF STEP]
using excess_s_non_pos
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u
excess f s \<le> (0::'a)

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

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from active_has_cf_outgoing[OF ACTIVE]
[PROOF STATE]
proof (chain)
picking this:
cf.outgoing u \<noteq> {}
[PROOF STEP]
have [simp]: "\<exists>v. (u, v) \<in> cf.E"
[PROOF STATE]
proof (prove)
using this:
cf.outgoing u \<noteq> {}

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

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
from NO_ADM valid
[PROOF STATE]
proof (chain)
picking this:
(u, ?v) \<in> cf.E \<Longrightarrow> l u \<noteq> l ?v + 1
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1
[PROOF STEP]
have "l u < l v + 1" if "(u,v)\<in>cf.E" for v
[PROOF STATE]
proof (prove)
using this:
(u, ?v) \<in> cf.E \<Longrightarrow> l u \<noteq> l ?v + 1
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1

goal (1 subgoal):
 1. l u < l v + 1
[PROOF STEP]
by (simp add: nat_less_le that)
[PROOF STATE]
proof (state)
this:
(u, ?v) \<in> cf.E \<Longrightarrow> l u < l ?v + 1

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
hence LU_INCR: "l u \<le> Min { l v | v. (u,v)\<in>cf.E }"
[PROOF STATE]
proof (prove)
using this:
(u, ?v) \<in> cf.E \<Longrightarrow> l u < l ?v + 1

goal (1 subgoal):
 1. l u \<le> Min {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
by (auto simp: less_Suc_eq_le)
[PROOF STATE]
proof (state)
this:
l u \<le> Min {l v |v. (u, v) \<in> cf.E}

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
with valid
[PROOF STATE]
proof (chain)
picking this:
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1
l u \<le> Min {l v |v. (u, v) \<in> cf.E}
[PROOF STEP]
have "\<forall>u'. (u',u)\<in>cf.E \<longrightarrow> l u' \<le> Min { l v | v. (u,v)\<in>cf.E } + 1"
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1
l u \<le> Min {l v |v. (u, v) \<in> cf.E}

goal (1 subgoal):
 1. \<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1
[PROOF STEP]
by (smt ab_semigroup_add_class.add.commute add_le_cancel_left le_trans)
[PROOF STATE]
proof (state)
this:
\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
have "\<forall>v. (u,v)\<in>cf.E \<longrightarrow> Min { l v | v. (u,v)\<in>cf.E } + 1 \<le> l v + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1
[PROOF STEP]
using Min_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> Min ?A \<le> ?x

goal (1 subgoal):
 1. \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1

goal (2 subgoals):
 1. l u < relabel_effect f l u u
 2. Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1
\<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1
[PROOF STEP]
show ?G1 ?G2
[PROOF STATE]
proof (prove)
using this:
\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1
\<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1

goal (1 subgoal):
 1. l u < relabel_effect f l u u &&& Labeling c s t f (relabel_effect f l u)
[PROOF STEP]
unfolding relabel_effect_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Min {l v |v. (u, v) \<in> cf.E} + 1
\<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} + 1 \<le> l v + 1

goal (1 subgoal):
 1. l u < (l(u := Min {l v |v. (u, v) \<in> cf.E} + 1)) u &&& Labeling c s t f (l(u := Min {l v |v. (u, v) \<in> cf.E} + 1))
[PROOF STEP]
apply (clarsimp_all simp: PRE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> l u < Suc (Min {l v |v. (u, v) \<in> cf.E})
 2. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> Labeling c s t f (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E})))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> l u < Suc (Min {l v |v. (u, v) \<in> cf.E})
[PROOF STEP]
using LU_INCR
[PROOF STATE]
proof (prove)
using this:
l u \<le> Min {l v |v. (u, v) \<in> cf.E}

goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> l u < Suc (Min {l v |v. (u, v) \<in> cf.E})
[PROOF STEP]
by (simp add: less_Suc_eq_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> Labeling c s t f (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E})))
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ua v. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v; (ua, v) \<in> cf.E\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) ua \<le> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) v + 1
 2. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) s = card V
 3. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) t = 0
[PROOF STEP]
subgoal for u' v'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v; (u', v') \<in> cf.E\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) u' \<le> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) v' + 1
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> cf.E \<Longrightarrow> l ?u \<le> l ?v + 1

goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v; (u', v') \<in> cf.E\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) u' \<le> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) v' + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) s = card V
 2. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) t = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) s = card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) t = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) t = 0
[PROOF STEP]
using NOT_SINK
[PROOF STATE]
proof (prove)
using this:
u \<noteq> t

goal (1 subgoal):
 1. \<lbrakk>\<forall>u'. (u', u) \<in> cf.E \<longrightarrow> l u' \<le> Suc (Min {l v |v. (u, v) \<in> cf.E}); \<forall>v. (u, v) \<in> cf.E \<longrightarrow> Min {l v |v. (u, v) \<in> cf.E} \<le> l v\<rbrakk> \<Longrightarrow> (l(u := Suc (Min {l v |v. (u, v) \<in> cf.E}))) t = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
l u < relabel_effect f l u u
Labeling c s t f (relabel_effect f l u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma relabel_preserve_other: "u\<noteq>v \<Longrightarrow> relabel_effect f l u v = l v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> relabel_effect f l u v = l v
[PROOF STEP]
unfolding relabel_effect_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (l(u := Min {l v |v. (u, v) \<in> cf.E} + 1)) v = l v
[PROOF STEP]
by auto


[STATEMENT]
theorem push_relabel_term_imp_maxflow:
  assumes no_push: "\<forall>(u,v)\<in>cf.E. \<not>push_precond f l (u,v)"
  assumes no_relabel: "\<forall>u. \<not>relabel_precond f l u"
  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:
\<forall>(u, v)\<in>cf.E. \<not> push_precond f l (u, v)
\<forall>u. \<not> relabel_precond f l u
[PROOF STEP]
have "\<forall>u\<in>V-{t}. excess f u \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cf.E. \<not> push_precond f l (u, v)
\<forall>u. \<not> relabel_precond f l u

goal (1 subgoal):
 1. \<forall>u\<in>V - {t}. excess f u \<le> (0::'a)
[PROOF STEP]
unfolding push_precond_def relabel_precond_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cf.E. \<not> (case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1)
\<forall>u. \<not> (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. \<forall>u\<in>V - {t}. excess f u \<le> (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>V - {t}. excess f u \<le> (0::'a)

goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
with excess_non_negative
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>V - {s, t}. (0::'a) \<le> excess f v
\<forall>u\<in>V - {t}. excess f u \<le> (0::'a)
[PROOF STEP]
have "\<forall>u\<in>V-{s,t}. excess f u = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V - {s, t}. (0::'a) \<le> excess f v
\<forall>u\<in>V - {t}. excess f u \<le> (0::'a)

goal (1 subgoal):
 1. \<forall>u\<in>V - {s, t}. excess f u = (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>V - {s, t}. excess f u = (0::'a)

goal (1 subgoal):
 1. isMaxFlow f
[PROOF STEP]
with no_excess_imp_maxflow
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>V - {s, t}. excess f u = (0::'a) \<Longrightarrow> isMaxFlow f
\<forall>u\<in>V - {s, t}. excess f u = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>V - {s, t}. excess f u = (0::'a) \<Longrightarrow> isMaxFlow f
\<forall>u\<in>V - {s, t}. excess f u = (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uv_cf_edge[simp, intro!]: "(u,v)\<in>cf.E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> cf.E
[PROOF STEP]
using PRE
[PROOF STATE]
proof (prove)
using this:
push_precond f l (u, v)

goal (1 subgoal):
 1. (u, v) \<in> cf.E
[PROOF STEP]
unfolding push_precond_def
[PROOF STATE]
proof (prove)
using this:
case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1

goal (1 subgoal):
 1. (u, v) \<in> cf.E
[PROOF STEP]
by auto


[STATEMENT]
lemma excess_u_pos: "excess f u > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < excess f u
[PROOF STEP]
using PRE
[PROOF STATE]
proof (prove)
using this:
push_precond f l (u, v)

goal (1 subgoal):
 1. (0::'a) < excess f u
[PROOF STEP]
unfolding push_precond_def
[PROOF STATE]
proof (prove)
using this:
case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1

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


[STATEMENT]
lemma l_u_eq[simp]: "l u = l v + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l u = l v + 1
[PROOF STEP]
using PRE
[PROOF STATE]
proof (prove)
using this:
push_precond f l (u, v)

goal (1 subgoal):
 1. l u = l v + 1
[PROOF STEP]
unfolding push_precond_def
[PROOF STATE]
proof (prove)
using this:
case (u, v) of (u, v) \<Rightarrow> (0::'a) < excess f u \<and> (u, v) \<in> cf.E \<and> l u = l v + 1

goal (1 subgoal):
 1. l u = l v + 1
[PROOF STEP]
by auto


[STATEMENT]
lemma uv_edge_cases:
    obtains (par) "(u,v)\<in>E" "(v,u)\<notin>E"
          | (rev) "(v,u)\<in>E" "(u,v)\<notin>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using uv_cf_edge cfE_ss_invE no_parallel_edge
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> cf.E
cf.E \<subseteq> E \<union> E\<inverse>
\<forall>u v. (u, v) \<in> E \<longrightarrow> (v, u) \<notin> E

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma uv_not_eq[simp]: "u\<noteq>v" "v\<noteq>u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v &&& v \<noteq> u
[PROOF STEP]
using E_ss_VxV cfE_ss_invE[THEN subsetD, OF uv_cf_edge] no_parallel_edge
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> V \<times> V
(u, v) \<in> E \<union> E\<inverse>
\<forall>u v. (u, v) \<in> E \<longrightarrow> (v, u) \<notin> E

goal (1 subgoal):
 1. u \<noteq> v &&& v \<noteq> u
[PROOF STEP]
by auto


[STATEMENT]
lemma \<Delta>_positive: "\<Delta> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < \<Delta>
[PROOF STEP]
unfolding \<Delta>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < min (excess f u) (cf (u, v))
[PROOF STEP]
using excess_u_pos uv_cf_edge[unfolded cf.E_def] resE_positive
[PROOF STATE]
proof (prove)
using this:
(0::'a) < excess f u
(u, v) \<in> {(u, v). cf (u, v) \<noteq> (0::'a)}
?e \<in> cf.E \<Longrightarrow> (0::'a) < cf ?e

goal (1 subgoal):
 1. (0::'a) < min (excess f u) (cf (u, v))
[PROOF STEP]
by auto


[STATEMENT]
lemma f'_alt: "f' = augment_edge f (u,v) \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' = augment_edge f (u, v) \<Delta>
[PROOF STEP]
unfolding push_effect_def \<Delta>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (u, v) of (u, v) \<Rightarrow> augment_edge f (u, v) (min (excess f u) (cf (u, v)))) = augment_edge f (u, v) (min (excess f u) (cf (u, v)))
[PROOF STEP]
by auto


[STATEMENT]
lemma cf'_alt: "l'.cf = augment_edge_cf cf (u,v) \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'.cf = augment_edge_cf cf (u, v) \<Delta>
[PROOF STEP]
unfolding push_effect_def \<Delta>_def augment_edge_cf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_of (case (u, v) of (u, v) \<Rightarrow> augment_edge f (u, v) (min (excess f u) (cf (u, v)))) = (case (u, v) of (u, v) \<Rightarrow> \<lambda>\<Delta>. cf((u, v) := cf (u, v) - \<Delta>, (v, u) := cf (v, u) + \<Delta>)) (min (excess f u) (cf (u, v)))
[PROOF STEP]
by (auto simp: augment_edge_cf')


[STATEMENT]
lemma excess'_u[simp]: "excess f' u = excess f u - \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. excess f' u = excess f u - \<Delta>
[PROOF STEP]
unfolding excess_def[where f=f']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
show "sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<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 u) - sum f' (outgoing u) = excess f u - \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<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 u) - sum f' (outgoing u) = excess f u - \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
hence UV_ONI:"(u,v)\<in>outgoing u - incoming u"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E
(v, u) \<notin> E

goal (1 subgoal):
 1. (u, v) \<in> outgoing u - incoming u
[PROOF STEP]
by (auto simp: incoming_def outgoing_def no_self_loop)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> outgoing u - incoming u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> incoming u \<Longrightarrow> augment_edge f (u, v) \<Delta> x = f x
[PROOF STEP]
apply (subst augment_edge_other)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> incoming u; (u, v) \<in> outgoing u - incoming u\<rbrakk> \<Longrightarrow> (u, v) \<in> E
 2. \<And>x. \<lbrakk>x \<in> incoming u; (u, v) \<in> outgoing u - incoming u\<rbrakk> \<Longrightarrow> x \<noteq> (u, v)
 3. \<And>x. \<lbrakk>x \<in> incoming u; (u, v) \<in> outgoing u - incoming u\<rbrakk> \<Longrightarrow> f x = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f' (incoming u) = sum f (incoming u)

goal (2 subgoals):
 1. \<lbrakk>(u, v) \<in> E; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
have "sum f' (outgoing u)
        = sum f (outgoing u) + (\<Sum>x\<in>outgoing u. if x = (u, v) then \<Delta> else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f' (outgoing u) = sum f (outgoing u) + (\<Sum>x\<in>outgoing u. 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>) (outgoing u) = (\<Sum>x\<in>outgoing u. f x + (if x = (u, v) then \<Delta> else (0::'a)))
[PROOF STEP]
by (rule sum.cong) auto
[PROOF STATE]
proof (state)
this:
sum f' (outgoing u) = sum f (outgoing u) + (\<Sum>x\<in>outgoing u. 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 u) - sum f' (outgoing u) = excess f u - \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f' (outgoing u) = sum f (outgoing u) + (\<Sum>x\<in>outgoing u. 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 u) - sum f' (outgoing u) = excess f u - \<Delta>
 2. \<lbrakk>(v, u) \<in> E; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> sum f' (incoming u) - sum f' (outgoing u) = excess f u - \<Delta>
[PROOF STEP]
have "\<dots> = sum f (outgoing u) + \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (outgoing u) + (\<Sum>x\<in>outgoing u. if x = (u, v) then \<Delta> else (0::'a)) = sum f (outgoing u) + \<Delta>
[PROOF STEP]
using UV_ONI
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> outgoing u - incoming u

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> outgoing u \<Longrightarrow> augment_edge f (u, v) \<Delta> x = f x
[PROOF STEP]
apply (subst augment_edge_rev_other)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> outgoing u; (v, u) \<in> incoming u - outgoing u\<rbrakk> \<Longrightarrow> (u, v) \<notin> E
 2. \<And>x. \<lbrakk>x \<in> outgoing u; (v, u) \<in> incoming u - outgoing u\<rbrakk> \<Longrightarrow> x \<noteq> (v, u)
 3. \<And>x. \<lbrakk>x \<in> outgoing u; (v, u) \<in> incoming u - outgoing u\<rbrakk> \<Longrightarrow> f x = f x
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
sum f' (outgoing u) = sum f (outgoing u)

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed