[STATEMENT]
lemma rel_pmf_measureI_aux:
  assumes ex_flow: "\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S"
    and le: "\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}"
  shows "rel_pmf R p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
from ex_flow
[PROOF STATE]
proof (chain)
picking this:
\<exists>f S. flow \<Delta> f \<and> MFMC_Network.cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
obtain f S
    where f: "flow \<Delta> f" and cut: "cut \<Delta> S" and ortho: "orthogonal \<Delta> f S"
[PROOF STATE]
proof (prove)
using this:
\<exists>f S. flow \<Delta> f \<and> MFMC_Network.cut \<Delta> S \<and> orthogonal \<Delta> f S

goal (1 subgoal):
 1. (\<And>f S. \<lbrakk>flow \<Delta> f; MFMC_Network.cut \<Delta> S; orthogonal \<Delta> f S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
flow \<Delta> f
MFMC_Network.cut \<Delta> S
orthogonal \<Delta> f S

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
from cut
[PROOF STATE]
proof (chain)
picking this:
MFMC_Network.cut \<Delta> S
[PROOF STEP]
obtain Source: "Source \<in> S" and Sink: "Sink \<notin> S"
[PROOF STATE]
proof (prove)
using this:
MFMC_Network.cut \<Delta> S

goal (1 subgoal):
 1. (\<lbrakk>Source \<in> S; Sink \<notin> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases simp
[PROOF STATE]
proof (state)
this:
Source \<in> S
Sink \<notin> S

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have f_finite [simp]: "f e < top" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e < \<top>
[PROOF STEP]
using network.flowD_finite[OF f, of e]
[PROOF STATE]
proof (prove)
using this:
f e \<noteq> \<top>

goal (1 subgoal):
 1. f e < \<top>
[PROOF STEP]
by (simp_all add: less_top)
[PROOF STATE]
proof (state)
this:
f ?e < \<top>

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have IN_f_Left: "d_IN f (Left x) = f (Source, Left x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f (vertex.Left x) = f (Source, vertex.Left x)
[PROOF STEP]
by(subst d_IN_alt_def[of _ \<Delta>])(simp_all add: nn_integral_count_space_indicator max_def network.flowD_outside[OF f])
[PROOF STATE]
proof (state)
this:
d_IN f (vertex.Left ?x) = f (Source, vertex.Left ?x)

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have OUT_f_Right: "d_OUT f (Right y) = f (Right y, Sink)" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT f (vertex.Right y) = f (vertex.Right y, Sink)
[PROOF STEP]
by(subst d_OUT_alt_def[of _ \<Delta>])(simp_all add: nn_integral_count_space_indicator max_def network.flowD_outside[OF f])
[PROOF STATE]
proof (state)
this:
d_OUT f (vertex.Right ?y) = f (vertex.Right ?y, Sink)

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have "value_flow \<Delta> f \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_flow \<Delta> f \<le> 1
[PROOF STEP]
using flowD_capacity_OUT[OF f, of Source]
[PROOF STATE]
proof (prove)
using this:
d_OUT f Source \<le> d_OUT (capacity \<Delta>) Source

goal (1 subgoal):
 1. value_flow \<Delta> f \<le> 1
[PROOF STEP]
by(simp add: OUT_cap_Source)
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f \<le> 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f \<le> 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have "1 \<le> value_flow \<Delta> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
let ?L = "Left -` S \<inter> set_pmf p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
let ?R' = "{y|y x. x \<in> set_pmf p \<and> Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> Right y \<in> S}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
let ?R'' = "{y|y x. x \<in> set_pmf p \<and> Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> \<not> Right y \<in> S}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "value_flow \<Delta> f = (\<Sum>\<^sup>+ x\<in>range Left. f (Source, x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_flow \<Delta> f = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))
[PROOF STEP]
unfolding d_OUT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. f (source \<Delta>, y)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))
[PROOF STEP]
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. f (Source, Left x) * indicator ?L x) + (\<Sum>\<^sup>+ x. f (Source, Left x) * indicator (- ?L) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x)) = (\<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x)) = (\<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x)) = (\<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "(\<Sum>\<^sup>+ x. f (Source, Left x) * indicator (- ?L) x) = (\<Sum>\<^sup>+ x\<in>- ?L. cap (Source, Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x))
[PROOF STEP]
using orthogonalD_out[OF ortho _ Source]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>edge \<Delta> Source ?y; ?y \<notin> S\<rbrakk> \<Longrightarrow> f (Source, ?y) = capacity \<Delta> (Source, ?y)

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x))
[PROOF STEP]
apply(auto simp add: set_pmf_iff network.flowD_outside[OF f] nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>edge' Source y; y \<notin> S\<rbrakk> \<Longrightarrow> f (Source, y) = cap (Source, y); vertex.Left x \<notin> S\<rbrakk> \<Longrightarrow> f (Source, vertex.Left x) = ennreal (pmf p x)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. \<lbrakk>edge' Source y; y \<notin> S\<rbrakk> \<Longrightarrow> f (Source, y) = cap (Source, y); vertex.Left x \<notin> S\<rbrakk> \<Longrightarrow> f (Source, vertex.Left x) = ennreal (pmf p x)
[PROOF STEP]
by(cases "x \<in> set_pmf p")(auto simp add: set_pmf_iff network.flowD_outside[OF f])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- (vertex.Left -` S \<inter> set_pmf p). f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x\<in>- ?L. pmf p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). cap (Source, vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = emeasure p (- ?L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x)) = emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p))
[PROOF STEP]
by(simp add: nn_integral_pmf)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x)) = emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>- (vertex.Left -` S \<inter> set_pmf p). ennreal (pmf p x)) = emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "(\<Sum>\<^sup>+ x. f (Source, Left x) * indicator ?L x) = (\<Sum>\<^sup>+ x\<in>?L. d_IN f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x))
[PROOF STEP]
by(subst d_IN_alt_def[of _ \<Delta>])(auto simp add: network.flowD_outside[OF f] nn_integral_count_space_indicator intro!: nn_integral_cong)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (Source, vertex.Left x)\<partial>count_space UNIV = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x\<in>?L. d_OUT f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x))
[PROOF STEP]
by(rule nn_integral_cong flowD_KIR[OF f, symmetric])+ simp_all
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (Left x, y) * indicator (range Right) y * indicator ?L x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x)
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>vertex.Left -` S \<inter> set_pmf p. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>range Right. \<Sum>\<^sup>+ x. f (Left x, y) * indicator ?L x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_fst_count_space[where f="case_prod _", simplified])
        (simp add: nn_integral_snd_count_space[where f="case_prod _", simplified] nn_integral_count_space_indicator nn_integral_cmult[symmetric] mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y) * indicator (range vertex.Right) y * indicator (vertex.Left -` S \<inter> set_pmf p) x) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV)
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Right. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x * indicator ?R' y) +
      (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x * indicator ?R'' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) + (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
by(subst nn_integral_add[symmetric]; simp)
        (subst nn_integral_add[symmetric]; auto intro!: nn_integral_cong split: split_indicator intro!: network.flowD_outside[OF f])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) + (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<integral>\<^sup>+x\<in>vertex.Left -` S \<inter> set_pmf p. f (vertex.Left x, vertex.Right y)\<partial>count_space UNIV) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) + (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x * indicator ?R' y) =
       (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?R' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)
[PROOF STEP]
apply(clarsimp simp add: network.flowD_outside[OF f] intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>vertex.Left xa \<in> S \<longrightarrow> xa \<notin> set_pmf p; xb \<in> set_pmf p; vertex.Left xb \<in> S; R xb x; x \<in> set_pmf q; vertex.Right x \<in> S\<rbrakk> \<Longrightarrow> f (vertex.Left xa, vertex.Right x) = 0
[PROOF STEP]
subgoal for y x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vertex.Left x \<in> S \<longrightarrow> x \<notin> set_pmf p; xb_ \<in> set_pmf p; vertex.Left xb_ \<in> S; R xb_ y; y \<in> set_pmf q; vertex.Right y \<in> S\<rbrakk> \<Longrightarrow> f (vertex.Left x, vertex.Right y) = 0
[PROOF STEP]
by(cases "edge \<Delta> (Left x) (Right y)")(auto intro: orthogonalD_in[OF ortho] network.flowD_outside[OF f])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range Left. f (x, Right y) * indicator ?R' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R'. d_IN f (Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y))
[PROOF STEP]
by(subst d_IN_alt_def[of _ \<Delta>])(auto simp add: network.flowD_outside[OF f] nn_integral_count_space_indicator incoming_def intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y) * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} y) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R'. d_OUT f (Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y))
[PROOF STEP]
using flowD_KIR[OF f]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> source \<Delta>; ?x \<noteq> sink \<Delta>\<rbrakk> \<Longrightarrow> KIR f ?x

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R'. d_OUT cap (Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y))
[PROOF STEP]
by(auto 4 3 intro!: nn_integral_cong simp add: d_OUT_def network.flowD_outside[OF f] Sink dest: intro: orthogonalD_out[OF ortho, of "Right _" Sink, simplified])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>?R'. pmf q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y)) = (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x))
[PROOF STEP]
by(simp add: OUT_cap_Right)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y)) = (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. d_OUT cap (vertex.Right y)) = (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> = emeasure q ?R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x)) = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}
[PROOF STEP]
by(simp add: nn_integral_pmf)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x)) = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}. ennreal (pmf q x)) = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S}

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y) * indicator ?L x * indicator ?R'' y) \<ge> emeasure q ?R''" (is "?lhs \<ge> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
have "?lhs = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. (if R x y then pmf q y else 0) * indicator ?L x * indicator ?R'' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))
[PROOF STEP]
by(rule nn_integral_cong)+(auto split: split_indicator simp add: network.flowD_outside[OF f] simp add: orthogonalD_out[OF ortho, of "Left _" "Right _", simplified])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
have "\<dots> \<ge> (\<Sum>\<^sup>+ y. pmf q y * indicator ?R'' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} x)) \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))
[PROOF STEP]
by(rule nn_integral_mono)(auto split: split_indicator intro: order_trans[OF _ nn_integral_ge_point])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} x)) \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} x)) \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. ennreal ((if R x y then pmf q y else 0) * indicat_real (vertex.Left -` S \<inter> set_pmf p) x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y))

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
have "(\<Sum>\<^sup>+ y. pmf q y * indicator ?R'' y) = (\<Sum>\<^sup>+ y\<in>?R''. pmf q y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} x)) = (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S}. ennreal (pmf q x))
[PROOF STEP]
by(auto simp add: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} x)) = (\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S}. ennreal (pmf q x))

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S}. ennreal (pmf q x)) \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sup>+ x\<in>{uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S}. ennreal (pmf q x)) \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
by(simp add: nn_integral_pmf)
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
value_flow \<Delta> f = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p))
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)
[PROOF STEP]
have "value_flow \<Delta> f \<ge> emeasure q ?R' + emeasure q ?R'' + emeasure p (- ?L)"
[PROOF STATE]
proof (prove)
using this:
value_flow \<Delta> f = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p))
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} \<le> (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y) * indicator (vertex.Left -` S \<inter> set_pmf p) x * indicator {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} y)

goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f
[PROOF STEP]
by(simp add: add_right_mono)
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "emeasure q ?R' + emeasure q ?R'' = emeasure q {y|y x. x \<in> set_pmf p \<and> Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}
[PROOF STEP]
by(subst plus_emeasure)(auto intro!: arg_cong2[where f=emeasure])
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<in> S} + emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q \<and> vertex.Right y \<notin> S} = emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "\<dots> \<ge> emeasure p ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) \<le> emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}
[PROOF STEP]
using le[of ?L]
[PROOF STATE]
proof (prove)
using this:
measure_pmf.prob p (vertex.Left -` S \<inter> set_pmf p) \<le> measure_pmf.prob q {y. \<exists>x\<in>vertex.Left -` S \<inter> set_pmf p. R x y}

goal (1 subgoal):
 1. emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) \<le> emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}
[PROOF STEP]
by(auto elim!: order_trans simp add: measure_pmf.emeasure_eq_measure AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE)
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) \<le> emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q} + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) \<le> emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}
[PROOF STEP]
have "value_flow \<Delta> f \<ge> emeasure (measure_pmf p) ?L + emeasure (measure_pmf p) (- ?L)"
[PROOF STATE]
proof (prove)
using this:
emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q} + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) \<le> emeasure (measure_pmf q) {uu_. \<exists>y x. uu_ = y \<and> x \<in> set_pmf p \<and> vertex.Left x \<in> S \<and> R x y \<and> y \<in> set_pmf q}

goal (1 subgoal):
 1. emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f
[PROOF STEP]
by (smt (verit, best) add_right_mono inf.absorb_iff2 le_inf_iff)
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "emeasure (measure_pmf p) ?L + emeasure (measure_pmf p) (- ?L) = emeasure (measure_pmf p) (?L \<union> - ?L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) = emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p \<union> - (vertex.Left -` S \<inter> set_pmf p))
[PROOF STEP]
by(subst plus_emeasure) auto
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) = emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p \<union> - (vertex.Left -` S \<inter> set_pmf p))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p) + emeasure (measure_pmf p) (- (vertex.Left -` S \<inter> set_pmf p)) = emeasure (measure_pmf p) (vertex.Left -` S \<inter> set_pmf p \<union> - (vertex.Left -` S \<inter> set_pmf p))

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
have "?L \<union> -?L = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex.Left -` S \<inter> set_pmf p \<union> - (vertex.Left -` S \<inter> set_pmf p) = UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex.Left -` S \<inter> set_pmf p \<union> - (vertex.Left -` S \<inter> set_pmf p) = UNIV

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (measure_pmf p) UNIV \<le> value_flow \<Delta> f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
emeasure (measure_pmf p) UNIV \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. 1 \<le> value_flow \<Delta> f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> value_flow \<Delta> f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
value_flow \<Delta> f \<le> 1
1 \<le> value_flow \<Delta> f
[PROOF STEP]
have val: "value_flow \<Delta> f = 1"
[PROOF STATE]
proof (prove)
using this:
value_flow \<Delta> f \<le> 1
1 \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. value_flow \<Delta> f = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f = 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have SAT_p: "f (Source, Left x) = pmf p x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Source, vertex.Left x) = ennreal (pmf p x)
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (Source, vertex.Left x) \<le> ennreal (pmf p x)
 2. ennreal (pmf p x) \<le> f (Source, vertex.Left x)
[PROOF STEP]
show "f (Source, Left x) \<le> pmf p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Source, vertex.Left x) \<le> ennreal (pmf p x)
[PROOF STEP]
using flowD_capacity[OF f, of "(Source, Left x)"]
[PROOF STATE]
proof (prove)
using this:
f (Source, vertex.Left x) \<le> capacity \<Delta> (Source, vertex.Left x)

goal (1 subgoal):
 1. f (Source, vertex.Left x) \<le> ennreal (pmf p x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Source, vertex.Left x) \<le> ennreal (pmf p x)

goal (1 subgoal):
 1. ennreal (pmf p x) \<le> f (Source, vertex.Left x)
[PROOF STEP]
show "pmf p x \<le> f (Source, Left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf p x) \<le> f (Source, vertex.Left x)
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
assume *: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x)

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have finite: "(\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
have "(\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) \<le> (\<Sum>\<^sup>+ y\<in>range Left. f (Source, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))
[PROOF STEP]
by(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_mono split: split_indicator)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))

goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))

goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
have "\<dots> = value_flow \<Delta> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y)) = value_flow \<Delta> f
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y)) = value_flow \<Delta> f

goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> value_flow \<Delta> f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> value_flow \<Delta> f

goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
using val
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<le> value_flow \<Delta> f
value_flow \<Delta> f = 1

goal (1 subgoal):
 1. \<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
by (auto simp: top_unique)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "value_flow \<Delta> f = (\<Sum>\<^sup>+ y\<in>range Left. f (Source, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_flow \<Delta> f = (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f = (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
value_flow \<Delta> f = (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) + (\<Sum>\<^sup>+ y. f (Source, Left y) * indicator {x} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y)) = (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y)) = (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Left. f (Source, y)) = (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV)

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < (\<Sum>\<^sup>+ y. f (Source, Left y) * indicator (- {x}) y) + (\<Sum>\<^sup>+ y. pmf p y * indicator {x} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV) < (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))
[PROOF STEP]
using * finite
[PROOF STATE]
proof (prove)
using this:
\<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x)
\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV \<noteq> \<infinity>

goal (1 subgoal):
 1. (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV) < (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))
[PROOF STEP]
by(auto simp add:)
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV) < (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<integral>\<^sup>+y\<in>{x}. f (Source, vertex.Left y)\<partial>count_space UNIV) < (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> (\<Sum>\<^sup>+ y. pmf p y * indicator (- {x}) y) + (\<Sum>\<^sup>+ y. pmf p y * indicator {x} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) \<le> (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))
[PROOF STEP]
using flowD_capacity[OF f, of "(Source, Left _)"]
[PROOF STATE]
proof (prove)
using this:
f (Source, vertex.Left ?uu3) \<le> capacity \<Delta> (Source, vertex.Left ?uu3)

goal (1 subgoal):
 1. (\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) \<le> (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))
[PROOF STEP]
by(auto intro!: nn_integral_mono split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) \<le> (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+y\<in>- {x}. f (Source, vertex.Left y)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) \<le> (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. pmf p y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real (- {x}) xa)) + (\<Sum>\<^sup>+ xa. ennreal (pmf p xa * indicat_real {x} xa)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1
[PROOF STEP]
unfolding nn_integral_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf p) UNIV = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1

goal (1 subgoal):
 1. \<not> ennreal (pmf p x) \<le> f (Source, vertex.Left x) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
value_flow \<Delta> f < 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
value_flow \<Delta> f < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using val
[PROOF STATE]
proof (prove)
using this:
value_flow \<Delta> f < 1
value_flow \<Delta> f = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (pmf p x) \<le> f (Source, vertex.Left x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (Source, vertex.Left ?x) = ennreal (pmf p ?x)

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have IN_Sink: "d_IN f Sink = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range Right. f (x, Sink))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))
[PROOF STEP]
unfolding d_IN_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. f (x, Sink)) = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))
[PROOF STEP]
by(auto intro!: nn_integral_cong network.flowD_outside[OF f] simp add: nn_integral_count_space_indicator split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. d_OUT f (Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex OUT_f_Right)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. d_IN f (Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y. d_IN f (vertex.Right y))
[PROOF STEP]
by(simp add: flowD_KIR[OF f])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y. d_IN f (vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. d_OUT f (vertex.Right y)) = (\<Sum>\<^sup>+ y. d_IN f (vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. (\<Sum>\<^sup>+ x\<in>range Left. f (x, Right y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))
[PROOF STEP]
by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. d_IN f (vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (Left x, Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (Left x, Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y))
[PROOF STEP]
by(subst nn_integral_fst_count_space[where f="case_prod _", simplified])(simp add: nn_integral_snd_count_space[where f="case_prod _", simplified])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y. \<Sum>\<^sup>+ x. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. (\<Sum>\<^sup>+ y\<in>range Right. f (Left x, y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, vertex.Right y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. d_OUT f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))
[PROOF STEP]
unfolding d_OUT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. f (vertex.Left x, y))
[PROOF STEP]
by(auto intro!: nn_integral_cong network.flowD_outside[OF f] simp add: nn_integral_count_space_indicator split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. d_IN f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))
[PROOF STEP]
by(simp add: flowD_KIR[OF f])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. pmf p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))
[PROOF STEP]
by(simp add: IN_f_Left SAT_p)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x. ennreal (pmf p x))

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1
[PROOF STEP]
unfolding nn_integral_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf p) UNIV = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf p x)) = 1

goal (1 subgoal):
 1. d_IN f Sink = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_IN f Sink = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d_IN f Sink = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d_IN f Sink = 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have SAT_q: "f (Right y, Sink) = pmf q y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (vertex.Right y, Sink) = ennreal (pmf q y)
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (vertex.Right y, Sink) \<le> ennreal (pmf q y)
 2. ennreal (pmf q y) \<le> f (vertex.Right y, Sink)
[PROOF STEP]
show "f (Right y, Sink) \<le> pmf q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (vertex.Right y, Sink) \<le> ennreal (pmf q y)
[PROOF STEP]
using flowD_capacity[OF f, of "(Right y, Sink)"]
[PROOF STATE]
proof (prove)
using this:
f (vertex.Right y, Sink) \<le> capacity \<Delta> (vertex.Right y, Sink)

goal (1 subgoal):
 1. f (vertex.Right y, Sink) \<le> ennreal (pmf q y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (vertex.Right y, Sink) \<le> ennreal (pmf q y)

goal (1 subgoal):
 1. ennreal (pmf q y) \<le> f (vertex.Right y, Sink)
[PROOF STEP]
show "pmf q y \<le> f (Right y, Sink)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf q y) \<le> f (vertex.Right y, Sink)
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
assume *: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink)

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have finite: "(\<Sum>\<^sup>+ x. f (Right x, Sink) * indicator (- {y}) x) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
have "(\<Sum>\<^sup>+ x. f (Right x, Sink) * indicator (- {y}) x) \<le> (\<Sum>\<^sup>+ x\<in>range Right. f (x, Sink))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))
[PROOF STEP]
by(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_mono split: split_indicator)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
have "\<dots> = d_IN f Sink"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = d_IN f Sink
[PROOF STEP]
by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = d_IN f Sink

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> d_IN f Sink
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> d_IN f Sink

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
using IN_Sink
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<le> d_IN f Sink
d_IN f Sink = 1

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>
[PROOF STEP]
by (auto simp: top_unique)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range Right. f (x, Sink))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))
[PROOF STEP]
by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_IN f Sink = (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. f (Right x, Sink) * indicator (- {y}) x) + (\<Sum>\<^sup>+ x. f (Right x, Sink) * indicator {y} x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV)
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV)

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Right. f (x, Sink)) = (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV)

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < (\<Sum>\<^sup>+ x. f (Right x, Sink) * indicator (- {y}) x) + (\<Sum>\<^sup>+ x. pmf q x * indicator {y} x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) < (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))
[PROOF STEP]
using * finite
[PROOF STATE]
proof (prove)
using this:
\<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink)
\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV \<noteq> \<infinity>

goal (1 subgoal):
 1. (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) < (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) < (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>{y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) < (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> (\<Sum>\<^sup>+ x. pmf q x * indicator (- {y}) x) + (\<Sum>\<^sup>+ x. pmf q x * indicator {y} x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) \<le> (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))
[PROOF STEP]
using flowD_capacity[OF f, of "(Right _, Sink)"]
[PROOF STATE]
proof (prove)
using this:
f (vertex.Right ?uu3, Sink) \<le> capacity \<Delta> (vertex.Right ?uu3, Sink)

goal (1 subgoal):
 1. (\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) \<le> (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))
[PROOF STEP]
by(auto intro!: nn_integral_mono split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) \<le> (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<integral>\<^sup>+x\<in>- {y}. f (vertex.Right x, Sink)\<partial>count_space UNIV) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) \<le> (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. pmf q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) = (\<Sum>\<^sup>+ x. ennreal (pmf q x))
[PROOF STEP]
by(subst nn_integral_add[symmetric])(auto intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) = (\<Sum>\<^sup>+ x. ennreal (pmf q x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real (- {y}) x)) + (\<Sum>\<^sup>+ x. ennreal (pmf q x * indicat_real {y} x)) = (\<Sum>\<^sup>+ x. ennreal (pmf q x))

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (pmf q x)) = 1
[PROOF STEP]
unfolding nn_integral_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf q) UNIV = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (pmf q x)) = 1

goal (1 subgoal):
 1. \<not> ennreal (pmf q y) \<le> f (vertex.Right y, Sink) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d_IN f Sink < 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
d_IN f Sink < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using IN_Sink
[PROOF STATE]
proof (prove)
using this:
d_IN f Sink < 1
d_IN f Sink = 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (pmf q y) \<le> f (vertex.Right y, Sink)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (vertex.Right ?y, Sink) = ennreal (pmf q ?y)

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
let ?z = "\<lambda>(x, y). enn2real (f (Left x, Right y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have nonneg: "\<And>xy. 0 \<le> ?z xy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xy. 0 \<le> (case xy of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
0 \<le> (case ?xy of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have prob: "(\<Sum>\<^sup>+ xy. ?z xy) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "(\<Sum>\<^sup>+ xy. ?z xy) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> ?z) (x, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y))
[PROOF STEP]
unfolding nn_integral_fst_count_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = integral\<^sup>N (count_space UNIV) (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y))))
[PROOF STEP]
by(simp add: split_def o_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. (\<Sum>\<^sup>+y\<in>range Right. f (Left x, y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))
[PROOF STEP]
by(auto simp add: nn_integral_count_space_reindex intro!: nn_integral_cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y. (ennreal \<circ> (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))) (x, y)) = (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. d_OUT f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator split: split_indicator intro!: nn_integral_cong network.flowD_outside[OF f])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. \<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x. d_IN f (Left x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))
[PROOF STEP]
using flowD_KIR[OF f]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> source \<Delta>; ?x \<noteq> sink \<Delta>\<rbrakk> \<Longrightarrow> KIR f ?x

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_OUT f (vertex.Left x)) = (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x\<in>range Left. f (Source, x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex IN_f_Left)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. d_IN f (vertex.Left x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
have "\<dots> = value_flow \<Delta> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x)) = value_flow \<Delta> f
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Left. f (Source, x)) = value_flow \<Delta> f

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = value_flow \<Delta> f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = value_flow \<Delta> f

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
using val
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = value_flow \<Delta> f
value_flow \<Delta> f = 1

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
note z = nonneg prob
[PROOF STATE]
proof (state)
this:
0 \<le> (case ?xy of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))
(\<Sum>\<^sup>+ x. ennreal (case x of (x, y) \<Rightarrow> enn2real (f (vertex.Left x, vertex.Right y)))) = 1

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
define z where "z = embed_pmf ?z"
[PROOF STATE]
proof (state)
this:
z = embed_pmf (\<lambda>(x, y). enn2real (f (vertex.Left x, vertex.Right y)))

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
have z_sel [simp]: "pmf z (x, y) = enn2real (f (Left x, Right y))" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf z (x, y) = enn2real (f (vertex.Left x, vertex.Right y))
[PROOF STEP]
by(simp add: z_def pmf_embed_pmf[OF z])
[PROOF STATE]
proof (state)
this:
pmf z (?x, ?y) = enn2real (f (vertex.Left ?x, vertex.Right ?y))

goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf R p q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y
 2. map_pmf fst ?pq = p
 3. map_pmf snd ?pq = q
[PROOF STEP]
show "R x y" if "(x, y) \<in> set_pmf z" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R x y
[PROOF STEP]
using that network.flowD_outside[OF f, of "(Left x, Right y)"]
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> set_pmf z
(vertex.Left x, vertex.Right y) \<notin> \<^bold>E\<^bsub>\<Delta>\<^esub> \<Longrightarrow> f (vertex.Left x, vertex.Right y) = 0

goal (1 subgoal):
 1. R x y
[PROOF STEP]
unfolding set_pmf_iff
[PROOF STATE]
proof (prove)
using this:
pmf z (x, y) \<noteq> 0
(vertex.Left x, vertex.Right y) \<notin> \<^bold>E\<^bsub>\<Delta>\<^esub> \<Longrightarrow> f (vertex.Left x, vertex.Right y) = 0

goal (1 subgoal):
 1. R x y
[PROOF STEP]
by(auto simp add: enn2real_eq_0_iff)
[PROOF STATE]
proof (state)
this:
(?x, ?y) \<in> set_pmf z \<Longrightarrow> R ?x ?y

goal (2 subgoals):
 1. map_pmf fst z = p
 2. map_pmf snd z = q
[PROOF STEP]
show "map_pmf fst z = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst z = p
[PROOF STEP]
proof(rule pmf_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "pmf (map_pmf fst z) x = (\<Sum>\<^sup>+ e\<in>range (Pair x). pmf z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf (map_pmf fst z) x) = (\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x))
[PROOF STEP]
by(auto simp add: ennreal_pmf_map nn_integral_measure_pmf nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
ennreal (pmf (map_pmf fst z) x) = (\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf (map_pmf fst z) x) = (\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ y\<in>range Right. f (Left x, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x)) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x)) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range (Pair x). ennreal (pmf z x)) = (\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "\<dots> = d_OUT f (Left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = d_OUT f (vertex.Left x)
[PROOF STEP]
by(auto simp add: d_OUT_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = d_OUT f (vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ y\<in>range vertex.Right. f (vertex.Left x, y)) = d_OUT f (vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "\<dots> = d_IN f (Left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. KIR f (vertex.Left x)
[PROOF STEP]
by(rule flowD_KIR[OF f]) simp_all
[PROOF STATE]
proof (state)
this:
KIR f (vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
KIR f (vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "\<dots> = f (Source, Left x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f (vertex.Left x) = f (Source, vertex.Left x)
[PROOF STEP]
by(simp add: IN_f_Left)
[PROOF STATE]
proof (state)
this:
d_IN f (vertex.Left x) = f (Source, vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_IN f (vertex.Left x) = f (Source, vertex.Left x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
have "\<dots> = pmf p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Source, vertex.Left x) = ennreal (pmf p x)
[PROOF STEP]
by(simp add: SAT_p)
[PROOF STATE]
proof (state)
this:
f (Source, vertex.Left x) = ennreal (pmf p x)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf fst z) i = pmf p i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (pmf (map_pmf fst z) x) = ennreal (pmf p x)
[PROOF STEP]
show "pmf (map_pmf fst z) x = pmf p x"
[PROOF STATE]
proof (prove)
using this:
ennreal (pmf (map_pmf fst z) x) = ennreal (pmf p x)

goal (1 subgoal):
 1. pmf (map_pmf fst z) x = pmf p x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (map_pmf fst z) x = pmf p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_pmf fst z = p

goal (1 subgoal):
 1. map_pmf snd z = q
[PROOF STEP]
show "map_pmf snd z = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf snd z = q
[PROOF STEP]
proof(rule pmf_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "pmf (map_pmf snd z) y = (\<Sum>\<^sup>+ e\<in>range (\<lambda>x. (x, y)). pmf z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf (map_pmf snd z) y) = (\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x))
[PROOF STEP]
by(auto simp add: ennreal_pmf_map nn_integral_measure_pmf nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
[PROOF STATE]
proof (state)
this:
ennreal (pmf (map_pmf snd z) y) = (\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf (map_pmf snd z) y) = (\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sup>+ x\<in>range Left. f (x, Right y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))
[PROOF STEP]
by(simp add: nn_integral_count_space_reindex)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range (\<lambda>x. (x, y)). ennreal (pmf z x)) = (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y))

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "\<dots> = d_IN f (Right y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = d_IN f (vertex.Right y)
[PROOF STEP]
by(auto simp add: d_IN_def nn_integral_count_space_indicator intro!: nn_integral_cong network.flowD_outside[OF f] split: split_indicator)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = d_IN f (vertex.Right y)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x\<in>range vertex.Left. f (x, vertex.Right y)) = d_IN f (vertex.Right y)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "\<dots> = d_OUT f (Right y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN f (vertex.Right y) = d_OUT f (vertex.Right y)
[PROOF STEP]
by(simp add: flowD_KIR[OF f])
[PROOF STATE]
proof (state)
this:
d_IN f (vertex.Right y) = d_OUT f (vertex.Right y)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_IN f (vertex.Right y) = d_OUT f (vertex.Right y)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "\<dots> = f (Right y, Sink)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT f (vertex.Right y) = f (vertex.Right y, Sink)
[PROOF STEP]
by(simp add: OUT_f_Right)
[PROOF STATE]
proof (state)
this:
d_OUT f (vertex.Right y) = f (vertex.Right y, Sink)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_OUT f (vertex.Right y) = f (vertex.Right y, Sink)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
have "\<dots> = pmf q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (vertex.Right y, Sink) = ennreal (pmf q y)
[PROOF STEP]
by(simp add: SAT_q)
[PROOF STATE]
proof (state)
this:
f (vertex.Right y, Sink) = ennreal (pmf q y)

goal (1 subgoal):
 1. \<And>i. pmf (map_pmf snd z) i = pmf q i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (pmf (map_pmf snd z) y) = ennreal (pmf q y)
[PROOF STEP]
show "pmf (map_pmf snd z) y = pmf q y"
[PROOF STATE]
proof (prove)
using this:
ennreal (pmf (map_pmf snd z) y) = ennreal (pmf q y)

goal (1 subgoal):
 1. pmf (map_pmf snd z) y = pmf q y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (map_pmf snd z) y = pmf q y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_pmf snd z = q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_pmf R p q

goal:
No subgoals!
[PROOF STEP]
qed