[STATEMENT]
lemma web_flow_iff: "web_flow \<Gamma> f \<longleftrightarrow> current \<Gamma> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. web_flow \<Gamma> f = current \<Gamma> f
[PROOF STEP]
using bipartite_V
[PROOF STATE]
proof (prove)
using this:
\<^bold>V \<subseteq> A \<Gamma> \<union> B \<Gamma>

goal (1 subgoal):
 1. web_flow \<Gamma> f = current \<Gamma> f
[PROOF STEP]
by(auto simp add: web_flow.simps)


[STATEMENT]
lemma countable_bipartite_web_minus_web:
  assumes f: "current \<Gamma> f"
  shows "countable_bipartite_web (\<Gamma> \<ominus> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f)
[PROOF STEP]
using bipartite_V A_vertex bipartite_E disjoint currentD_finite_OUT[OF f] currentD_weight_OUT[OF f] currentD_weight_IN[OF f] currentD_outside_OUT[OF f] currentD_outside_IN[OF f]
[PROOF STATE]
proof (prove)
using this:
\<^bold>V \<subseteq> A \<Gamma> \<union> B \<Gamma>
A \<Gamma> \<subseteq> \<^bold>V
edge \<Gamma> ?x ?y \<Longrightarrow> ?x \<in> A \<Gamma> \<and> ?y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
d_OUT f ?x \<noteq> \<top>
d_OUT f ?x \<le> weight \<Gamma> ?x
d_IN f ?x \<le> weight \<Gamma> ?x
?x \<notin> \<^bold>V \<Longrightarrow> d_OUT f ?x = 0
?x \<notin> \<^bold>V \<Longrightarrow> d_IN f ?x = 0

goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f)
[PROOF STEP]
by unfold_locales (auto simp add:  weight_outside)


[STATEMENT]
lemma current_plus_current_minus:
  assumes f: "current \<Gamma> f"
  and g: "current (\<Gamma> \<ominus> f) g"
  shows "current \<Gamma> (plus_current f g)" (is "current _ ?fg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. d_OUT (plus_current f g) x \<le> weight \<Gamma> x
 2. \<And>x. d_IN (plus_current f g) x \<le> weight \<Gamma> x
 3. \<And>e. e \<notin> \<^bold>E \<Longrightarrow> plus_current f g e = 0
[PROOF STEP]
interpret \<Gamma>: countable_bipartite_web "\<Gamma> \<ominus> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f

goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f)
[PROOF STEP]
by(rule countable_bipartite_web_minus_web)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. d_OUT (plus_current f g) x \<le> weight \<Gamma> x
 2. \<And>x. d_IN (plus_current f g) x \<le> weight \<Gamma> x
 3. \<And>e. e \<notin> \<^bold>E \<Longrightarrow> plus_current f g e = 0
[PROOF STEP]
show "d_OUT ?fg x \<le> weight \<Gamma> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (plus_current f g) x \<le> weight \<Gamma> x
[PROOF STEP]
using currentD_weight_OUT[OF g, of x] currentD_OUT[OF g, of x] currentD_finite_OUT[OF f, of x] currentD_OUT[OF f, of x] currentD_outside_IN[OF f, of x] currentD_outside_OUT[OF f, of x] currentD_weight_OUT[OF f, of x]
[PROOF STATE]
proof (prove)
using this:
d_OUT g x \<le> weight (\<Gamma> \<ominus> f) x
x \<in> B (\<Gamma> \<ominus> f) \<Longrightarrow> d_OUT g x = 0
d_OUT f x \<noteq> \<top>
x \<in> B \<Gamma> \<Longrightarrow> d_OUT f x = 0
x \<notin> \<^bold>V \<Longrightarrow> d_IN f x = 0
x \<notin> \<^bold>V \<Longrightarrow> d_OUT f x = 0
d_OUT f x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. d_OUT (plus_current f g) x \<le> weight \<Gamma> x
[PROOF STEP]
by(cases "x \<in> A \<Gamma> \<or> x \<in> B \<Gamma>")(auto simp add: add.commute d_OUT_def nn_integral_add not_vertex ennreal_le_minus_iff split: if_split_asm)
[PROOF STATE]
proof (state)
this:
d_OUT (plus_current f g) ?x \<le> weight \<Gamma> ?x

goal (2 subgoals):
 1. \<And>x. d_IN (plus_current f g) x \<le> weight \<Gamma> x
 2. \<And>e. e \<notin> \<^bold>E \<Longrightarrow> plus_current f g e = 0
[PROOF STEP]
show "d_IN ?fg x \<le> weight \<Gamma> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (plus_current f g) x \<le> weight \<Gamma> x
[PROOF STEP]
using currentD_weight_IN[OF g, of x] currentD_IN[OF g, of x] currentD_finite_IN[OF f, of x] currentD_OUT[OF f, of x] currentD_outside_IN[OF f, of x] currentD_outside_OUT[OF f, of x] currentD_weight_IN[OF f, of x]
[PROOF STATE]
proof (prove)
using this:
d_IN g x \<le> weight (\<Gamma> \<ominus> f) x
x \<in> A (\<Gamma> \<ominus> f) \<Longrightarrow> d_IN g x = 0
d_IN f x \<noteq> \<top>
x \<in> B \<Gamma> \<Longrightarrow> d_OUT f x = 0
x \<notin> \<^bold>V \<Longrightarrow> d_IN f x = 0
x \<notin> \<^bold>V \<Longrightarrow> d_OUT f x = 0
d_IN f x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. d_IN (plus_current f g) x \<le> weight \<Gamma> x
[PROOF STEP]
by(cases "x \<in> A \<Gamma> \<or> x \<in> B \<Gamma>")(auto simp add: add.commute  d_IN_def nn_integral_add not_vertex ennreal_le_minus_iff split: if_split_asm)
[PROOF STATE]
proof (state)
this:
d_IN (plus_current f g) ?x \<le> weight \<Gamma> ?x

goal (1 subgoal):
 1. \<And>e. e \<notin> \<^bold>E \<Longrightarrow> plus_current f g e = 0
[PROOF STEP]
show "?fg e = 0" if "e \<notin> \<^bold>E" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plus_current f g e = 0
[PROOF STEP]
using that currentD_outside'[OF f, of e] currentD_outside'[OF g, of e]
[PROOF STATE]
proof (prove)
using this:
e \<notin> \<^bold>E
e \<notin> \<^bold>E \<Longrightarrow> f e = 0
e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> f\<^esub> \<Longrightarrow> g e = 0

goal (1 subgoal):
 1. plus_current f g e = 0
[PROOF STEP]
by(cases e) simp
[PROOF STATE]
proof (state)
this:
?e \<notin> \<^bold>E \<Longrightarrow> plus_current f g ?e = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wave_plus_current_minus:
  assumes f: "current \<Gamma> f"
  and w: "wave \<Gamma> f"
  and g: "current (\<Gamma> \<ominus> f) g"
  and w': "wave (\<Gamma> \<ominus> f) g"
  shows "wave \<Gamma> (plus_current f g)" (is "wave _ ?fg")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave \<Gamma> (plus_current f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. separating \<Gamma> (TER (plus_current f g))
 2. current \<Gamma> (plus_current f g)
[PROOF STEP]
show fg: "current \<Gamma> ?fg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
using f g
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
current (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
by(rule current_plus_current_minus)
[PROOF STATE]
proof (state)
this:
current \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. separating \<Gamma> (TER (plus_current f g))
[PROOF STEP]
show sep: "separating \<Gamma> (TER ?fg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separating \<Gamma> (TER (plus_current f g))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y p. \<lbrakk>x \<in> A \<Gamma>; y \<in> B \<Gamma>; path \<Gamma> x p y\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
fix x p y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y p. \<lbrakk>x \<in> A \<Gamma>; y \<in> B \<Gamma>; path \<Gamma> x p y\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
assume x: "x \<in> A \<Gamma>" and p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
[PROOF STATE]
proof (state)
this:
x \<in> A \<Gamma>
path \<Gamma> x p y
y \<in> B \<Gamma>

goal (1 subgoal):
 1. \<And>x y p. \<lbrakk>x \<in> A \<Gamma>; y \<in> B \<Gamma>; path \<Gamma> x p y\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
from p x y disjoint
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p y
x \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
[PROOF STEP]
have py: "p = [y]"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p y
x \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}

goal (1 subgoal):
 1. p = [y]
[PROOF STEP]
by(cases)(auto 4 3 elim: rtrancl_path.cases dest: bipartite_E)
[PROOF STATE]
proof (state)
this:
p = [y]

goal (1 subgoal):
 1. \<And>x y p. \<lbrakk>x \<in> A \<Gamma>; y \<in> B \<Gamma>; path \<Gamma> x p y\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
with waveD_separating[THEN separatingD, OF w p x y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p. z \<in> TER f) \<or> x \<in> TER f
p = [y]
[PROOF STEP]
have "x \<in> TER f \<or> y \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p. z \<in> TER f) \<or> x \<in> TER f
p = [y]

goal (1 subgoal):
 1. x \<in> TER f \<or> y \<in> TER f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> TER f \<or> y \<in> TER f

goal (1 subgoal):
 1. \<And>x y p. \<lbrakk>x \<in> A \<Gamma>; y \<in> B \<Gamma>; path \<Gamma> x p y\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
thus "(\<exists>z\<in>set p. z \<in> TER ?fg) \<or> x \<in> TER ?fg"
[PROOF STATE]
proof (prove)
using this:
x \<in> TER f \<or> y \<in> TER f

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
case right
[PROOF STATE]
proof (state)
this:
y \<in> TER f

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
with y disjoint
[PROOF STATE]
proof (chain)
picking this:
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
y \<in> TER f
[PROOF STEP]
have "y \<in> TER ?fg"
[PROOF STATE]
proof (prove)
using this:
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
y \<in> TER f

goal (1 subgoal):
 1. y \<in> TER (plus_current f g)
[PROOF STEP]
using currentD_OUT[OF fg y]
[PROOF STATE]
proof (prove)
using this:
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
y \<in> TER f
d_OUT (plus_current f g) y = 0

goal (1 subgoal):
 1. y \<in> TER (plus_current f g)
[PROOF STEP]
by(auto simp add: SAT.simps SINK.simps d_IN_def nn_integral_add not_le add_increasing2)
[PROOF STATE]
proof (state)
this:
y \<in> TER (plus_current f g)

goal (2 subgoals):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> TER (plus_current f g)

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
using py
[PROOF STATE]
proof (prove)
using this:
y \<in> TER (plus_current f g)
p = [y]

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)

goal (1 subgoal):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
case x': left
[PROOF STATE]
proof (state)
this:
x \<in> TER f

goal (1 subgoal):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p y
[PROOF STEP]
have "path (\<Gamma> \<ominus> f) x p y"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p y

goal (1 subgoal):
 1. path (\<Gamma> \<ominus> f) x p y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
path (\<Gamma> \<ominus> f) x p y

goal (1 subgoal):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
from waveD_separating[THEN separatingD, OF w' this] x y py
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<in> A (\<Gamma> \<ominus> f); y \<in> B (\<Gamma> \<ominus> f)\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) \<or> x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
x \<in> A \<Gamma>
y \<in> B \<Gamma>
p = [y]
[PROOF STEP]
have "x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<or> y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> A (\<Gamma> \<ominus> f); y \<in> B (\<Gamma> \<ominus> f)\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) \<or> x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
x \<in> A \<Gamma>
y \<in> B \<Gamma>
p = [y]

goal (1 subgoal):
 1. x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<or> y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<or> y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. x \<in> TER f \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<or> y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
case left
[PROOF STATE]
proof (state)
this:
x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (2 subgoals):
 1. x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
hence "x \<in> TER ?fg"
[PROOF STATE]
proof (prove)
using this:
x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. x \<in> TER (plus_current f g)
[PROOF STEP]
using x x'
[PROOF STATE]
proof (prove)
using this:
x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
x \<in> A \<Gamma>
x \<in> TER f

goal (1 subgoal):
 1. x \<in> TER (plus_current f g)
[PROOF STEP]
by(auto simp add: SAT.simps SINK.simps d_OUT_def nn_integral_add)
[PROOF STATE]
proof (state)
this:
x \<in> TER (plus_current f g)

goal (2 subgoals):
 1. x \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
 2. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> TER (plus_current f g)

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)

goal (1 subgoal):
 1. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
case right
[PROOF STATE]
proof (state)
this:
y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
hence "y \<in> TER ?fg"
[PROOF STATE]
proof (prove)
using this:
y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. y \<in> TER (plus_current f g)
[PROOF STEP]
using disjoint y currentD_OUT[OF fg y] currentD_OUT[OF f y] currentD_finite_IN[OF f, of y]
[PROOF STATE]
proof (prove)
using this:
y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
A \<Gamma> \<inter> B \<Gamma> = {}
y \<in> B \<Gamma>
d_OUT (plus_current f g) y = 0
d_OUT f y = 0
d_IN f y \<noteq> \<top>

goal (1 subgoal):
 1. y \<in> TER (plus_current f g)
[PROOF STEP]
by(auto simp add: add.commute SINK.simps SAT.simps d_IN_def nn_integral_add ennreal_minus_le_iff split: if_split_asm)
[PROOF STATE]
proof (state)
this:
y \<in> TER (plus_current f g)

goal (1 subgoal):
 1. y \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g \<Longrightarrow> (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
with py
[PROOF STATE]
proof (chain)
picking this:
p = [y]
y \<in> TER (plus_current f g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = [y]
y \<in> TER (plus_current f g)

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> TER (plus_current f g)) \<or> x \<in> TER (plus_current f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
separating \<Gamma> (TER (plus_current f g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minus_plus_current:
  assumes f: "current \<Gamma> f"
  and g: "current (\<Gamma> \<ominus> f) g"
  shows "\<Gamma> \<ominus> plus_current f g = \<Gamma> \<ominus> f \<ominus> g" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<ominus> plus_current f g = \<Gamma> \<ominus> f \<ominus> g
[PROOF STEP]
proof(rule web.equality)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. edge (\<Gamma> \<ominus> plus_current f g) = edge (\<Gamma> \<ominus> f \<ominus> g)
 2. weight (\<Gamma> \<ominus> plus_current f g) = weight (\<Gamma> \<ominus> f \<ominus> g)
 3. A (\<Gamma> \<ominus> plus_current f g) = A (\<Gamma> \<ominus> f \<ominus> g)
 4. B (\<Gamma> \<ominus> plus_current f g) = B (\<Gamma> \<ominus> f \<ominus> g)
 5. web.more (\<Gamma> \<ominus> plus_current f g) = web.more (\<Gamma> \<ominus> f \<ominus> g)
[PROOF STEP]
have "weight ?lhs x = weight ?rhs x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> plus_current f g) x = weight (\<Gamma> \<ominus> f \<ominus> g) x
[PROOF STEP]
using currentD_weight_IN[OF f, of x] currentD_weight_IN[OF g, of x]
[PROOF STATE]
proof (prove)
using this:
d_IN f x \<le> weight \<Gamma> x
d_IN g x \<le> weight (\<Gamma> \<ominus> f) x

goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> plus_current f g) x = weight (\<Gamma> \<ominus> f \<ominus> g) x
[PROOF STEP]
by (auto simp add: d_IN_def d_OUT_def nn_integral_add diff_add_eq_diff_diff_swap_ennreal add_increasing2 diff_add_assoc2_ennreal add.assoc)
[PROOF STATE]
proof (state)
this:
weight (\<Gamma> \<ominus> plus_current f g) ?x = weight (\<Gamma> \<ominus> f \<ominus> g) ?x

goal (5 subgoals):
 1. edge (\<Gamma> \<ominus> plus_current f g) = edge (\<Gamma> \<ominus> f \<ominus> g)
 2. weight (\<Gamma> \<ominus> plus_current f g) = weight (\<Gamma> \<ominus> f \<ominus> g)
 3. A (\<Gamma> \<ominus> plus_current f g) = A (\<Gamma> \<ominus> f \<ominus> g)
 4. B (\<Gamma> \<ominus> plus_current f g) = B (\<Gamma> \<ominus> f \<ominus> g)
 5. web.more (\<Gamma> \<ominus> plus_current f g) = web.more (\<Gamma> \<ominus> f \<ominus> g)
[PROOF STEP]
thus "weight ?lhs = weight ?rhs"
[PROOF STATE]
proof (prove)
using this:
weight (\<Gamma> \<ominus> plus_current f g) ?x = weight (\<Gamma> \<ominus> f \<ominus> g) ?x

goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> plus_current f g) = weight (\<Gamma> \<ominus> f \<ominus> g)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
weight (\<Gamma> \<ominus> plus_current f g) = weight (\<Gamma> \<ominus> f \<ominus> g)

goal (4 subgoals):
 1. edge (\<Gamma> \<ominus> plus_current f g) = edge (\<Gamma> \<ominus> f \<ominus> g)
 2. A (\<Gamma> \<ominus> plus_current f g) = A (\<Gamma> \<ominus> f \<ominus> g)
 3. B (\<Gamma> \<ominus> plus_current f g) = B (\<Gamma> \<ominus> f \<ominus> g)
 4. web.more (\<Gamma> \<ominus> plus_current f g) = web.more (\<Gamma> \<ominus> f \<ominus> g)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma unhindered_minus_web:
  assumes unhindered: "\<not> hindered \<Gamma>"
  and f: "current \<Gamma> f"
  and w: "wave \<Gamma> f"
  shows "\<not> hindered (\<Gamma> \<ominus> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindered (\<Gamma> \<ominus> f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
assume "hindered (\<Gamma> \<ominus> f)"
[PROOF STATE]
proof (state)
this:
hindered (\<Gamma> \<ominus> f)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hindered (\<Gamma> \<ominus> f)
[PROOF STEP]
obtain g where g: "current (\<Gamma> \<ominus> f) g"
    and w': "wave (\<Gamma> \<ominus> f) g"
    and hind: "hindrance (\<Gamma> \<ominus> f) g"
[PROOF STATE]
proof (prove)
using this:
hindered (\<Gamma> \<ominus> f)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>current (\<Gamma> \<ominus> f) g; wave (\<Gamma> \<ominus> f) g; hindrance (\<Gamma> \<ominus> f) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
current (\<Gamma> \<ominus> f) g
wave (\<Gamma> \<ominus> f) g
hindrance (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
let ?fg = "plus_current f g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
have fg: "current \<Gamma> ?fg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
using f g
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
current (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
by(rule current_plus_current_minus)
[PROOF STATE]
proof (state)
this:
current \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
current \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
have "wave \<Gamma> ?fg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave \<Gamma> (plus_current f g)
[PROOF STEP]
using f w g w'
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
wave \<Gamma> f
current (\<Gamma> \<ominus> f) g
wave (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. wave \<Gamma> (plus_current f g)
[PROOF STEP]
by(rule wave_plus_current_minus)
[PROOF STATE]
proof (state)
this:
wave \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wave \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
from hind
[PROOF STATE]
proof (chain)
picking this:
hindrance (\<Gamma> \<ominus> f) g
[PROOF STEP]
obtain a where a: "a \<in> A \<Gamma>" and n\<E>: "a \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)"
    and wa: "d_OUT g a < weight (\<Gamma> \<ominus> f) a"
[PROOF STATE]
proof (prove)
using this:
hindrance (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A \<Gamma>; a \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g); d_OUT g a < weight (\<Gamma> \<ominus> f) a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
a \<in> A \<Gamma>
a \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)
d_OUT g a < weight (\<Gamma> \<ominus> f) a

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a \<in> A \<Gamma>
[PROOF STEP]
have "hindrance \<Gamma> ?fg"
[PROOF STATE]
proof (prove)
using this:
a \<in> A \<Gamma>

goal (1 subgoal):
 1. hindrance \<Gamma> (plus_current f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<notin> \<E> (TER (plus_current f g))
 2. d_OUT (plus_current f g) a < weight \<Gamma> a
[PROOF STEP]
show "a \<notin> \<E> (TER ?fg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> \<E> (TER (plus_current f g))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
assume \<E>: "a \<in> \<E> (TER ?fg)"
[PROOF STATE]
proof (state)
this:
a \<in> \<E> (TER (plus_current f g))

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<E> (TER (plus_current f g))
[PROOF STEP]
obtain p y where p: "path \<Gamma> a p y" and y: "y \<in> B \<Gamma>"
        and bypass: "\<And>z. z \<in> set p \<Longrightarrow> z \<notin> RF (TER ?fg)"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<E> (TER (plus_current f g))

goal (1 subgoal):
 1. (\<And>p y. \<lbrakk>path \<Gamma> a p y; y \<in> B \<Gamma>; \<And>z. z \<in> set p \<Longrightarrow> z \<notin> RF (TER (plus_current f g))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<E>_E_RF) blast
[PROOF STATE]
proof (state)
this:
path \<Gamma> a p y
y \<in> B \<Gamma>
?z \<in> set p \<Longrightarrow> ?z \<notin> RF (TER (plus_current f g))

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
from p a y disjoint
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> a p y
a \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
[PROOF STEP]
have py: "p = [y]"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> a p y
a \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}

goal (1 subgoal):
 1. p = [y]
[PROOF STEP]
by(cases)(auto 4 3 elim: rtrancl_path.cases dest: bipartite_E)
[PROOF STATE]
proof (state)
this:
p = [y]

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
from bypass[of y] py
[PROOF STATE]
proof (chain)
picking this:
y \<in> set p \<Longrightarrow> y \<notin> RF (TER (plus_current f g))
p = [y]
[PROOF STEP]
have "y \<notin> TER ?fg"
[PROOF STATE]
proof (prove)
using this:
y \<in> set p \<Longrightarrow> y \<notin> RF (TER (plus_current f g))
p = [y]

goal (1 subgoal):
 1. y \<notin> TER (plus_current f g)
[PROOF STEP]
by(auto intro: roofed_greaterI)
[PROOF STATE]
proof (state)
this:
y \<notin> TER (plus_current f g)

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
with currentD_OUT[OF fg y]
[PROOF STATE]
proof (chain)
picking this:
d_OUT (plus_current f g) y = 0
y \<notin> TER (plus_current f g)
[PROOF STEP]
have "y \<notin> SAT \<Gamma> ?fg"
[PROOF STATE]
proof (prove)
using this:
d_OUT (plus_current f g) y = 0
y \<notin> TER (plus_current f g)

goal (1 subgoal):
 1. y \<notin> SAT \<Gamma> (plus_current f g)
[PROOF STEP]
by(auto simp add: SINK.simps)
[PROOF STATE]
proof (state)
this:
y \<notin> SAT \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
hence "y \<notin> SAT (\<Gamma> \<ominus> f) g"
[PROOF STATE]
proof (prove)
using this:
y \<notin> SAT \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. y \<notin> SAT (\<Gamma> \<ominus> f) g
[PROOF STEP]
using y currentD_OUT[OF f y] currentD_finite_IN[OF f, of y]
[PROOF STATE]
proof (prove)
using this:
y \<notin> SAT \<Gamma> (plus_current f g)
y \<in> B \<Gamma>
d_OUT f y = 0
d_IN f y \<noteq> \<top>

goal (1 subgoal):
 1. y \<notin> SAT (\<Gamma> \<ominus> f) g
[PROOF STEP]
by(auto simp add: SAT.simps d_IN_def nn_integral_add ennreal_minus_le_iff add.commute)
[PROOF STATE]
proof (state)
this:
y \<notin> SAT (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
hence "essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a"
[PROOF STATE]
proof (prove)
using this:
y \<notin> SAT (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a
[PROOF STEP]
using p py y
[PROOF STATE]
proof (prove)
using this:
y \<notin> SAT (\<Gamma> \<ominus> f) g
path \<Gamma> a p y
p = [y]
y \<in> B \<Gamma>

goal (1 subgoal):
 1. essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a
[PROOF STEP]
by(auto intro!: essentialI)
[PROOF STATE]
proof (state)
this:
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
from \<E> a
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<E> (TER (plus_current f g))
a \<in> A \<Gamma>
[PROOF STEP]
have "a \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<E> (TER (plus_current f g))
a \<in> A \<Gamma>

goal (1 subgoal):
 1. a \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
[PROOF STEP]
by(auto simp add: SAT.A SINK_plus_current)
[PROOF STATE]
proof (state)
this:
a \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a
a \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g
[PROOF STEP]
have "a \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)"
[PROOF STATE]
proof (prove)
using this:
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g) a
a \<in> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g

goal (1 subgoal):
 1. a \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)

goal (1 subgoal):
 1. a \<in> \<E> (TER (plus_current f g)) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
a \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)

goal (1 subgoal):
 1. False
[PROOF STEP]
using n\<E>
[PROOF STATE]
proof (prove)
using this:
a \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)
a \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> g)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<notin> \<E> (TER (plus_current f g))

goal (1 subgoal):
 1. d_OUT (plus_current f g) a < weight \<Gamma> a
[PROOF STEP]
show "d_OUT ?fg a < weight \<Gamma> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (plus_current f g) a < weight \<Gamma> a
[PROOF STEP]
using a wa currentD_finite_OUT[OF f, of a]
[PROOF STATE]
proof (prove)
using this:
a \<in> A \<Gamma>
d_OUT g a < weight (\<Gamma> \<ominus> f) a
d_OUT f a \<noteq> \<top>

goal (1 subgoal):
 1. d_OUT (plus_current f g) a < weight \<Gamma> a
[PROOF STEP]
by(simp add: d_OUT_def less_diff_eq_ennreal less_top add.commute nn_integral_add)
[PROOF STATE]
proof (state)
this:
d_OUT (plus_current f g) a < weight \<Gamma> a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hindrance \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
current \<Gamma> (plus_current f g)
wave \<Gamma> (plus_current f g)
hindrance \<Gamma> (plus_current f g)
[PROOF STEP]
have "hindered \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (plus_current f g)
wave \<Gamma> (plus_current f g)
hindrance \<Gamma> (plus_current f g)

goal (1 subgoal):
 1. hindered \<Gamma>
[PROOF STEP]
by(blast intro: hindered.intros)
[PROOF STATE]
proof (state)
this:
hindered \<Gamma>

goal (1 subgoal):
 1. hindered (\<Gamma> \<ominus> f) \<Longrightarrow> False
[PROOF STEP]
with unhindered
[PROOF STATE]
proof (chain)
picking this:
\<not> hindered \<Gamma>
hindered \<Gamma>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> hindered \<Gamma>
hindered \<Gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loose_minus_web:
  assumes unhindered: "\<not> hindered \<Gamma>"
  and f: "current \<Gamma> f"
  and w: "wave \<Gamma> f"
  and maximal: "\<And>w. \<lbrakk> current \<Gamma> w; wave \<Gamma> w; f \<le> w \<rbrakk> \<Longrightarrow> f = w"
  shows "loose (\<Gamma> \<ominus> f)" (is "loose ?\<Gamma>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loose (\<Gamma> \<ominus> f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
assume g: "current ?\<Gamma> g" and w': "wave ?\<Gamma> g"
[PROOF STATE]
proof (state)
this:
current (\<Gamma> \<ominus> f) g
wave (\<Gamma> \<ominus> f) g

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
let ?g = "plus_current f g"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
from f g
[PROOF STATE]
proof (chain)
picking this:
current \<Gamma> f
current (\<Gamma> \<ominus> f) g
[PROOF STEP]
have "current \<Gamma> ?g"
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
current (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. current \<Gamma> (plus_current f g)
[PROOF STEP]
by(rule current_plus_current_minus)
[PROOF STATE]
proof (state)
this:
current \<Gamma> (plus_current f g)

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
current \<Gamma> (plus_current f g)

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
from f w g w'
[PROOF STATE]
proof (chain)
picking this:
current \<Gamma> f
wave \<Gamma> f
current (\<Gamma> \<ominus> f) g
wave (\<Gamma> \<ominus> f) g
[PROOF STEP]
have "wave \<Gamma> ?g"
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> f
wave \<Gamma> f
current (\<Gamma> \<ominus> f) g
wave (\<Gamma> \<ominus> f) g

goal (1 subgoal):
 1. wave \<Gamma> (plus_current f g)
[PROOF STEP]
by(rule wave_plus_current_minus)
[PROOF STATE]
proof (state)
this:
wave \<Gamma> (plus_current f g)

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wave \<Gamma> (plus_current f g)

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
have "f \<le> ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<le> plus_current f g
[PROOF STEP]
by(clarsimp simp add: le_fun_def)
[PROOF STATE]
proof (state)
this:
f \<le> plus_current f g

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
current \<Gamma> (plus_current f g)
wave \<Gamma> (plus_current f g)
f \<le> plus_current f g
[PROOF STEP]
have eq: "f = ?g"
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (plus_current f g)
wave \<Gamma> (plus_current f g)
f \<le> plus_current f g

goal (1 subgoal):
 1. f = plus_current f g
[PROOF STEP]
by(rule maximal)
[PROOF STATE]
proof (state)
this:
f = plus_current f g

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
have "g e = 0" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g e = 0
[PROOF STEP]
proof(cases e)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
case (Pair x y)
[PROOF STATE]
proof (state)
this:
e = (x, y)

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
have "f e \<le> d_OUT f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e \<le> d_OUT f x
[PROOF STEP]
unfolding d_OUT_def Pair
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (x, y) \<le> (\<Sum>\<^sup>+ y. f (x, y))
[PROOF STEP]
by(rule nn_integral_ge_point) simp
[PROOF STATE]
proof (state)
this:
f e \<le> d_OUT f x

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f e \<le> d_OUT f x

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
have "\<dots> \<le> weight \<Gamma> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT f x \<le> weight \<Gamma> x
[PROOF STEP]
by(rule currentD_weight_OUT[OF f])
[PROOF STATE]
proof (state)
this:
d_OUT f x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_OUT f x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
have "\<dots> < \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight \<Gamma> x < \<top>
[PROOF STEP]
by(simp add: less_top[symmetric])
[PROOF STATE]
proof (state)
this:
weight \<Gamma> x < \<top>

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> g e = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f e < \<top>
[PROOF STEP]
show "g e = 0"
[PROOF STATE]
proof (prove)
using this:
f e < \<top>

goal (1 subgoal):
 1. g e = 0
[PROOF STEP]
using Pair eq[THEN fun_cong, of e]
[PROOF STATE]
proof (prove)
using this:
f e < \<top>
e = (x, y)
f e = plus_current f g e

goal (1 subgoal):
 1. g e = 0
[PROOF STEP]
by(cases "f e" "g e" rule: ennreal2_cases)(simp_all add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
g e = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g ?e = 0

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>current (\<Gamma> \<ominus> f) fa; wave (\<Gamma> \<ominus> f) fa\<rbrakk> \<Longrightarrow> fa = (\<lambda>_. 0)
 2. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
thus "g = (\<lambda>_. 0)"
[PROOF STATE]
proof (prove)
using this:
g ?e = 0

goal (1 subgoal):
 1. g = (\<lambda>_. 0)
[PROOF STEP]
by(simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
g = (\<lambda>_. 0)

goal (1 subgoal):
 1. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
show "\<not> hindrance ?\<Gamma> zero_current"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
using unhindered
[PROOF STATE]
proof (prove)
using this:
\<not> hindered \<Gamma>

goal (1 subgoal):
 1. \<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
proof(rule contrapos_nn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0) \<Longrightarrow> hindered \<Gamma>
[PROOF STEP]
assume "hindrance ?\<Gamma> zero_current"
[PROOF STATE]
proof (state)
this:
hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)

goal (1 subgoal):
 1. hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0) \<Longrightarrow> hindered \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)
[PROOF STEP]
obtain x where a: "x \<in> A ?\<Gamma>" and \<E>: "x \<notin> \<E>\<^bsub>?\<Gamma>\<^esub> (TER\<^bsub>?\<Gamma>\<^esub> zero_current)"
      and weight: "d_OUT zero_current x < weight ?\<Gamma> x"
[PROOF STATE]
proof (prove)
using this:
hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A (\<Gamma> \<ominus> f); x \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)); d_OUT (\<lambda>_. 0) x < weight (\<Gamma> \<ominus> f) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
x \<in> A (\<Gamma> \<ominus> f)
x \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))
d_OUT (\<lambda>_. 0) x < weight (\<Gamma> \<ominus> f) x

goal (1 subgoal):
 1. hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0) \<Longrightarrow> hindered \<Gamma>
[PROOF STEP]
have "hindrance \<Gamma> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hindrance \<Gamma> f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a \<in> A \<Gamma>
 2. ?a \<notin> \<E> (TER f)
 3. d_OUT f ?a < weight \<Gamma> ?a
[PROOF STEP]
show a': "x \<in> A \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Gamma>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
x \<in> A (\<Gamma> \<ominus> f)

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

goal (2 subgoals):
 1. x \<notin> \<E> (TER f)
 2. d_OUT f x < weight \<Gamma> x
[PROOF STEP]
with weight
[PROOF STATE]
proof (chain)
picking this:
d_OUT (\<lambda>_. 0) x < weight (\<Gamma> \<ominus> f) x
x \<in> A \<Gamma>
[PROOF STEP]
show "d_OUT f x < weight \<Gamma> x"
[PROOF STATE]
proof (prove)
using this:
d_OUT (\<lambda>_. 0) x < weight (\<Gamma> \<ominus> f) x
x \<in> A \<Gamma>

goal (1 subgoal):
 1. d_OUT f x < weight \<Gamma> x
[PROOF STEP]
by(simp add: less_diff_eq_ennreal less_top[symmetric] currentD_finite_OUT[OF f])
[PROOF STATE]
proof (state)
this:
d_OUT f x < weight \<Gamma> x

goal (1 subgoal):
 1. x \<notin> \<E> (TER f)
[PROOF STEP]
show "x \<notin> \<E> (TER f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> \<E> (TER f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
assume "x \<in> \<E> (TER f)"
[PROOF STATE]
proof (state)
this:
x \<in> \<E> (TER f)

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> (TER f)
[PROOF STEP]
obtain p y where p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
          and bypass: "\<And>z. z \<in> set p \<Longrightarrow> z \<notin> RF (TER f)"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> (TER f)

goal (1 subgoal):
 1. (\<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>; \<And>z. z \<in> set p \<Longrightarrow> z \<notin> RF (TER f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<E>_E_RF) auto
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>
?z \<in> set p \<Longrightarrow> ?z \<notin> RF (TER f)

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
from p a' y disjoint
[PROOF STATE]
proof (chain)
picking this:
path \<Gamma> x p y
x \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
[PROOF STEP]
have py: "p = [y]"
[PROOF STATE]
proof (prove)
using this:
path \<Gamma> x p y
x \<in> A \<Gamma>
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}

goal (1 subgoal):
 1. p = [y]
[PROOF STEP]
by(cases)(auto 4 3 elim: rtrancl_path.cases dest: bipartite_E)
[PROOF STATE]
proof (state)
this:
p = [y]

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
hence "y \<notin> (TER f)"
[PROOF STATE]
proof (prove)
using this:
p = [y]

goal (1 subgoal):
 1. y \<notin> TER f
[PROOF STEP]
using bypass[of y]
[PROOF STATE]
proof (prove)
using this:
p = [y]
y \<in> set p \<Longrightarrow> y \<notin> RF (TER f)

goal (1 subgoal):
 1. y \<notin> TER f
[PROOF STEP]
by(auto intro: roofed_greaterI)
[PROOF STATE]
proof (state)
this:
y \<notin> TER f

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
hence "weight ?\<Gamma> y > 0"
[PROOF STATE]
proof (prove)
using this:
y \<notin> TER f

goal (1 subgoal):
 1. 0 < weight (\<Gamma> \<ominus> f) y
[PROOF STEP]
using currentD_OUT[OF f y] disjoint y
[PROOF STATE]
proof (prove)
using this:
y \<notin> TER f
d_OUT f y = 0
A \<Gamma> \<inter> B \<Gamma> = {}
y \<in> B \<Gamma>

goal (1 subgoal):
 1. 0 < weight (\<Gamma> \<ominus> f) y
[PROOF STEP]
by(auto simp add: SINK.simps SAT.simps diff_gr0_ennreal)
[PROOF STATE]
proof (state)
this:
0 < weight (\<Gamma> \<ominus> f) y

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
hence "y \<notin> TER\<^bsub>?\<Gamma>\<^esub> zero_current"
[PROOF STATE]
proof (prove)
using this:
0 < weight (\<Gamma> \<ominus> f) y

goal (1 subgoal):
 1. y \<notin> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)
[PROOF STEP]
using y disjoint
[PROOF STATE]
proof (prove)
using this:
0 < weight (\<Gamma> \<ominus> f) y
y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}

goal (1 subgoal):
 1. y \<notin> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
y \<notin> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
hence "essential ?\<Gamma> (B ?\<Gamma>) (TER\<^bsub>?\<Gamma>\<^esub> zero_current) x"
[PROOF STATE]
proof (prove)
using this:
y \<notin> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)

goal (1 subgoal):
 1. essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)) x
[PROOF STEP]
using p y py
[PROOF STATE]
proof (prove)
using this:
y \<notin> TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)
path \<Gamma> x p y
y \<in> B \<Gamma>
p = [y]

goal (1 subgoal):
 1. essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)) x
[PROOF STEP]
by(auto intro!: essentialI)
[PROOF STATE]
proof (state)
this:
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)) x

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
x \<in> A (\<Gamma> \<ominus> f)
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)) x
[PROOF STEP]
have "x \<in> \<E>\<^bsub>?\<Gamma>\<^esub> (TER\<^bsub>?\<Gamma>\<^esub> zero_current)"
[PROOF STATE]
proof (prove)
using this:
x \<in> A (\<Gamma> \<ominus> f)
essential (\<Gamma> \<ominus> f) (B (\<Gamma> \<ominus> f)) (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0)) x

goal (1 subgoal):
 1. x \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))

goal (1 subgoal):
 1. x \<in> \<E> (TER f) \<Longrightarrow> False
[PROOF STEP]
with \<E>
[PROOF STATE]
proof (chain)
picking this:
x \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))
x \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<notin> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))
x \<in> \<E>\<^bsub>\<Gamma> \<ominus> f\<^esub> (TER\<^bsub>\<Gamma> \<ominus> f\<^esub> (\<lambda>_. 0))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<notin> \<E> (TER f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hindrance \<Gamma> f

goal (1 subgoal):
 1. hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0) \<Longrightarrow> hindered \<Gamma>
[PROOF STEP]
thus "hindered \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
hindrance \<Gamma> f

goal (1 subgoal):
 1. hindered \<Gamma>
[PROOF STEP]
using f w
[PROOF STATE]
proof (prove)
using this:
hindrance \<Gamma> f
current \<Gamma> f
wave \<Gamma> f

goal (1 subgoal):
 1. hindered \<Gamma>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
hindered \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> hindrance (\<Gamma> \<ominus> f) (\<lambda>_. 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weight_minus_web:
  assumes f: "current \<Gamma> f"
  shows "weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
proof(cases "x \<in> B \<Gamma>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
 2. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> B \<Gamma>

goal (2 subgoals):
 1. x \<in> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
 2. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
with currentD_OUT[OF f True] disjoint
[PROOF STATE]
proof (chain)
picking this:
d_OUT f x = 0
A \<Gamma> \<inter> B \<Gamma> = {}
x \<in> B \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d_OUT f x = 0
A \<Gamma> \<inter> B \<Gamma> = {}
x \<in> B \<Gamma>

goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)

goal (1 subgoal):
 1. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> B \<Gamma>

goal (1 subgoal):
 1. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
hence "d_IN f x = 0" "d_OUT f x = 0" if "x \<notin> A \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
x \<notin> B \<Gamma>

goal (1 subgoal):
 1. d_IN f x = 0 &&& d_OUT f x = 0
[PROOF STEP]
using currentD_outside_OUT[OF f, of x] currentD_outside_IN[OF f, of x] bipartite_V that
[PROOF STATE]
proof (prove)
using this:
x \<notin> B \<Gamma>
x \<notin> \<^bold>V \<Longrightarrow> d_OUT f x = 0
x \<notin> \<^bold>V \<Longrightarrow> d_IN f x = 0
\<^bold>V \<subseteq> A \<Gamma> \<union> B \<Gamma>
x \<notin> A \<Gamma>

goal (1 subgoal):
 1. d_IN f x = 0 &&& d_OUT f x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> A \<Gamma> \<Longrightarrow> d_IN f x = 0
x \<notin> A \<Gamma> \<Longrightarrow> d_OUT f x = 0

goal (1 subgoal):
 1. x \<notin> B \<Gamma> \<Longrightarrow> weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A \<Gamma> \<Longrightarrow> d_IN f x = 0
x \<notin> A \<Gamma> \<Longrightarrow> d_OUT f x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> A \<Gamma> \<Longrightarrow> d_IN f x = 0
x \<notin> A \<Gamma> \<Longrightarrow> d_OUT f x = 0

goal (1 subgoal):
 1. weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weight (\<Gamma> \<ominus> f) x = (if x \<in> A \<Gamma> then weight \<Gamma> x - d_OUT f x else weight \<Gamma> x - d_IN f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in -) separating_minus_web [simp]: "separating_gen (G \<ominus> f) = separating_gen G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separating_gen (G \<ominus> f) = separating_gen G
[PROOF STEP]
by(simp add: separating_gen.simps fun_eq_iff)


[STATEMENT]
lemma current_minus:
  assumes f: "current \<Gamma> f"
  and g: "current \<Gamma> g"
  and le: "\<And>e. g e \<le> f e"
  shows "current (\<Gamma> \<ominus> g) (f - g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current (\<Gamma> \<ominus> g) (f - g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. current (\<Gamma> \<ominus> g) (f - g)
[PROOF STEP]
interpret \<Gamma>: countable_bipartite_web "\<Gamma> \<ominus> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> g)
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> g

goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> g)
[PROOF STEP]
by(rule countable_bipartite_web_minus_web)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. current (\<Gamma> \<ominus> g) (f - g)
[PROOF STEP]
note [simp del] = minus_web_sel(2)
    and [simp] = weight_minus_web[OF g]
[PROOF STATE]
proof (state)
this:
weight (?\<Gamma> \<ominus> ?f) ?x = (if ?x \<in> A ?\<Gamma> then weight ?\<Gamma> ?x - d_OUT ?f ?x else weight ?\<Gamma> ?x + d_OUT ?f ?x - d_IN ?f ?x)
weight (\<Gamma> \<ominus> g) ?x = (if ?x \<in> A \<Gamma> then weight \<Gamma> ?x - d_OUT g ?x else weight \<Gamma> ?x - d_IN g ?x)

goal (1 subgoal):
 1. current (\<Gamma> \<ominus> g) (f - g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current (\<Gamma> \<ominus> g) (f - g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. d_OUT (f - g) x \<le> weight (\<Gamma> \<ominus> g) x
 2. \<And>x. d_IN (f - g) x \<le> weight (\<Gamma> \<ominus> g) x
 3. \<And>e. e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub> \<Longrightarrow> (f - g) e = 0
[PROOF STEP]
show "d_OUT (f - g) x \<le> weight (\<Gamma> \<ominus> g) x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f - g) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
unfolding fun_diff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (\<lambda>x. f x - g x) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
using currentD_weight_OUT[OF f, of x] currentD_weight_IN[OF g, of x]
[PROOF STATE]
proof (prove)
using this:
d_OUT f x \<le> weight \<Gamma> x
d_IN g x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. d_OUT (\<lambda>x. f x - g x) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
by(subst d_OUT_diff)(simp_all add: le currentD_finite_OUT[OF g] currentD_OUT'[OF f] currentD_OUT'[OF g] ennreal_minus_mono)
[PROOF STATE]
proof (state)
this:
d_OUT (f - g) ?x \<le> weight (\<Gamma> \<ominus> g) ?x

goal (2 subgoals):
 1. \<And>x. d_IN (f - g) x \<le> weight (\<Gamma> \<ominus> g) x
 2. \<And>e. e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub> \<Longrightarrow> (f - g) e = 0
[PROOF STEP]
show "d_IN (f - g) x \<le> weight (\<Gamma> \<ominus> g) x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (f - g) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
unfolding fun_diff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (\<lambda>x. f x - g x) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
using currentD_weight_IN[OF f, of x] currentD_weight_OUT[OF g, of x]
[PROOF STATE]
proof (prove)
using this:
d_IN f x \<le> weight \<Gamma> x
d_OUT g x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. d_IN (\<lambda>x. f x - g x) x \<le> weight (\<Gamma> \<ominus> g) x
[PROOF STEP]
by(subst d_IN_diff)(simp_all add: le currentD_finite_IN[OF g] currentD_IN[OF f] currentD_IN[OF g] ennreal_minus_mono)
[PROOF STATE]
proof (state)
this:
d_IN (f - g) ?x \<le> weight (\<Gamma> \<ominus> g) ?x

goal (1 subgoal):
 1. \<And>e. e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub> \<Longrightarrow> (f - g) e = 0
[PROOF STEP]
show "(f - g) e = 0" if "e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub>" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f - g) e = 0
[PROOF STEP]
using that currentD_outside'[OF f] currentD_outside'[OF g]
[PROOF STATE]
proof (prove)
using this:
e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub>
?e \<notin> \<^bold>E \<Longrightarrow> f ?e = 0
?e \<notin> \<^bold>E \<Longrightarrow> g ?e = 0

goal (1 subgoal):
 1. (f - g) e = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?e \<notin> \<^bold>E\<^bsub>\<Gamma> \<ominus> g\<^esub> \<Longrightarrow> (f - g) ?e = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
current (\<Gamma> \<ominus> g) (f - g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in -) essential_minus_web [simp]: "essential (\<Gamma> \<ominus> f) = essential \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. essential (\<Gamma> \<ominus> f) = essential \<Gamma>
[PROOF STEP]
by(simp add: essential_def fun_eq_iff)


[STATEMENT]
lemma (in -) RF_in_essential: fixes B shows "essential \<Gamma> B S x \<Longrightarrow> x \<in> roofed_gen \<Gamma> B S \<longleftrightarrow> x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. essential \<Gamma> B S x \<Longrightarrow> (x \<in> roofed_gen \<Gamma> B S) = (x \<in> S)
[PROOF STEP]
by(auto intro: roofed_greaterI elim!: essentialE_RF dest: roofedD)


[STATEMENT]
lemma (in -) d_OUT_fun_upd:
  assumes "f (x, y) \<noteq> \<top>" "f (x, y) \<ge> 0" "k \<noteq> \<top>" "k \<ge> 0"
  shows "d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
proof(cases "x = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = x'

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
have "?lhs = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<Sum>\<^sup>+ y'. f (x, y') * indicator {y} y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f((x, y) := k)) x' = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV)
[PROOF STEP]
unfolding d_OUT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ ya. (f((x, y) := k)) (x', ya)) = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV)
[PROOF STEP]
using assms True
[PROOF STATE]
proof (prove)
using this:
f (x, y) \<noteq> \<top>
0 \<le> f (x, y)
k \<noteq> \<top>
0 \<le> k
x = x'

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ ya. (f((x, y) := k)) (x', ya)) = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_diff[symmetric])
      (auto intro!: nn_integral_cong simp add: AE_count_space split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_OUT (f((x, y) := k)) x' = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV)

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_OUT (f((x, y) := k)) x' = (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV)

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
have "(\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = d_OUT f x + (\<Sum>\<^sup>+ y'. k * indicator {y} y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV)
[PROOF STEP]
unfolding d_OUT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = (\<Sum>\<^sup>+ y. f (x, y)) + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f (x, y) \<noteq> \<top>
0 \<le> f (x, y)
k \<noteq> \<top>
0 \<le> k

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = (\<Sum>\<^sup>+ y. f (x, y)) + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_add[symmetric])
      (auto intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV)

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y'. f (x, y') + k * indicator {y} y') = d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV)

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
have "\<dots> - (\<Sum>\<^sup>+ y'. f (x, y') * indicator {y} y') = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV) - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV) = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
x = x'
f (x, y) \<noteq> \<top>
0 \<le> f (x, y)
k \<noteq> \<top>
0 \<le> k

goal (1 subgoal):
 1. d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV) - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV) = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
by(subst diff_add_assoc2_ennreal[symmetric])(auto simp add: d_OUT_def intro!: nn_integral_ge_point)
[PROOF STATE]
proof (state)
this:
d_OUT f x + (\<integral>\<^sup>+y'\<in>{y}. k\<partial>count_space UNIV) - (\<integral>\<^sup>+y'\<in>{y}. f (x, y')\<partial>count_space UNIV) = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')

goal (2 subgoals):
 1. x = x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
 2. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')

goal (1 subgoal):
 1. d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')

goal (1 subgoal):
 1. x \<noteq> x' \<Longrightarrow> d_OUT (f((x, y) := k)) x' = (if x = x' then d_OUT f x - f (x, y) + k else d_OUT f x')
[PROOF STEP]
qed(simp add: d_OUT_def)