[STATEMENT]
theorem unhindered_linkable:
  assumes unhindered: "\<not> hindered \<Gamma>"
  shows "linkable \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
proof(cases "A \<Gamma> = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<Gamma> = {} \<Longrightarrow> linkable \<Gamma>
 2. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<Gamma> = {}

goal (2 subgoals):
 1. A \<Gamma> = {} \<Longrightarrow> linkable \<Gamma>
 2. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<Gamma> = {}

goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
by(auto intro!: exI[where x="zero_current"] linkage.intros simp add: web_flow_iff )
[PROOF STATE]
proof (state)
this:
linkable \<Gamma>

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
case nempty: False
[PROOF STATE]
proof (state)
this:
A \<Gamma> \<noteq> {}

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
let ?P = "\<lambda>f a f'. current (\<Gamma> \<ominus> f) f' \<and> d_OUT f' a = weight (\<Gamma> \<ominus> f) a \<and> \<not> hindered (\<Gamma> \<ominus> f \<ominus> f')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
define enum where "enum = from_nat_into (A \<Gamma>)"
[PROOF STATE]
proof (state)
this:
enum = from_nat_into (A \<Gamma>)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have enum_A: "enum n \<in> A \<Gamma>" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum n \<in> A \<Gamma>
[PROOF STEP]
using from_nat_into[OF nempty, of n]
[PROOF STATE]
proof (prove)
using this:
from_nat_into (A \<Gamma>) n \<in> A \<Gamma>

goal (1 subgoal):
 1. enum n \<in> A \<Gamma>
[PROOF STEP]
by(simp add: enum_def)
[PROOF STATE]
proof (state)
this:
enum ?n \<in> A \<Gamma>

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have vertex_enum [simp]: "vertex \<Gamma> (enum n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex \<Gamma> (enum n)
[PROOF STEP]
using enum_A[of n] A_vertex
[PROOF STATE]
proof (prove)
using this:
enum n \<in> A \<Gamma>
A \<Gamma> \<subseteq> \<^bold>V

goal (1 subgoal):
 1. vertex \<Gamma> (enum n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vertex \<Gamma> (enum ?n)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
define f where "f = rec_nat zero_current (\<lambda>n f. let f' = SOME f'. ?P f (enum n) f' in plus_current f f')"
[PROOF STATE]
proof (state)
this:
f = rec_nat (\<lambda>_. 0) (\<lambda>n f. Let (SOME f'. current (\<Gamma> \<ominus> f) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f \<ominus> f')) (plus_current f))

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have f_0 [simp]: "f 0 = zero_current"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = (\<lambda>_. 0)
[PROOF STEP]
by(simp add: f_def)
[PROOF STATE]
proof (state)
this:
f 0 = (\<lambda>_. 0)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have f_Suc: "f (Suc n) = plus_current (f n) (Eps (?P (f n) (enum n)))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc n) = plus_current (f n) (SOME f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f'))
[PROOF STEP]
by(simp add: f_def)
[PROOF STATE]
proof (state)
this:
f (Suc ?n) = plus_current (f ?n) (SOME f'. current (\<Gamma> \<ominus> f ?n) f' \<and> d_OUT f' (enum ?n) = weight (\<Gamma> \<ominus> f ?n) (enum ?n) \<and> \<not> hindered (\<Gamma> \<ominus> f ?n \<ominus> f'))

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have f: "current \<Gamma> (f n)"
    and sat: "\<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m)"
    and unhindered: "\<not> hindered (\<Gamma> \<ominus> f n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (f n) &&& (\<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m)) &&& \<not> hindered (\<Gamma> \<ominus> f n)
[PROOF STEP]
proof(induction n)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. current \<Gamma> (f 0)
 2. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 3. \<not> hindered (\<Gamma> \<ominus> f 0)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 5. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 6. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. current \<Gamma> (f 0)
 2. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 3. \<not> hindered (\<Gamma> \<ominus> f 0)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 5. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 6. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. current \<Gamma> (f 0)
 2. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 3. \<not> hindered (\<Gamma> \<ominus> f 0)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 5. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 6. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. current \<Gamma> (f 0)
 2. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 3. \<not> hindered (\<Gamma> \<ominus> f 0)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 5. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 6. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (f 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f 0)

goal (5 subgoals):
 1. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 2. \<not> hindered (\<Gamma> \<ominus> f 0)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 4. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 5. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f 0)

goal (5 subgoals):
 1. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 2. \<not> hindered (\<Gamma> \<ominus> f 0)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 4. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 5. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f 0)

goal (5 subgoals):
 1. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 2. \<not> hindered (\<Gamma> \<ominus> f 0)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 4. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 5. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
m < 0

goal (5 subgoals):
 1. \<And>m. m < 0 \<Longrightarrow> d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
 2. \<not> hindered (\<Gamma> \<ominus> f 0)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 4. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 5. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
m < 0

goal (1 subgoal):
 1. d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d_OUT (f 0) (enum m) = weight \<Gamma> (enum m)

goal (4 subgoals):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 3. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m2 < 0 \<Longrightarrow> d_OUT (f 0) (enum ?m2) = weight \<Gamma> (enum ?m2)

goal (4 subgoals):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 3. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?m2 < 0 \<Longrightarrow> d_OUT (f 0) (enum ?m2) = weight \<Gamma> (enum ?m2)

goal (4 subgoals):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 3. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 3. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 4. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
[PROOF STEP]
using unhindered
[PROOF STATE]
proof (prove)
using this:
\<not> hindered \<Gamma>

goal (1 subgoal):
 1. \<not> hindered (\<Gamma> \<ominus> f 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> hindered (\<Gamma> \<ominus> f 0)

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> hindered (\<Gamma> \<ominus> f 0)

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f n)
?m < n \<Longrightarrow> d_OUT (f n) (enum ?m) = weight \<Gamma> (enum ?m)
\<not> hindered (\<Gamma> \<ominus> f n)

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
interpret \<Gamma>: countable_bipartite_web "\<Gamma> \<ominus> f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f n)
[PROOF STEP]
using Suc.IH(1)
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (f n)

goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f n)
[PROOF STEP]
by(rule countable_bipartite_web_minus_web)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
define f' where "f' = Eps (?P (f n) (enum n))"
[PROOF STATE]
proof (state)
this:
f' = (SOME f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f'))

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
have "Ex (?P (f n) (enum n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
using Suc.IH(3)
[PROOF STATE]
proof (prove)
using this:
\<not> hindered (\<Gamma> \<ominus> f n)

goal (1 subgoal):
 1. \<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
by(rule \<Gamma>.unhindered_saturate1)(simp add: enum_A)
[PROOF STATE]
proof (state)
this:
\<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
hence "?P (f n) (enum n) f'"
[PROOF STATE]
proof (prove)
using this:
\<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (1 subgoal):
 1. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
unfolding f'_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (1 subgoal):
 1. current (\<Gamma> \<ominus> f n) (SOME f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')) \<and> d_OUT (SOME f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')) (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> (SOME f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')))
[PROOF STEP]
by(rule someI_ex)
[PROOF STATE]
proof (state)
this:
current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
hence f': "current (\<Gamma> \<ominus> f n) f'"
      and OUT: "d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n)"
      and unhindered': "\<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')"
[PROOF STATE]
proof (prove)
using this:
current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (1 subgoal):
 1. current (\<Gamma> \<ominus> f n) f' &&& d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) &&& \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
current (\<Gamma> \<ominus> f n) f'
d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n)
\<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
have f_Suc: "f (Suc n) = plus_current (f n) f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc n) = plus_current (f n) f'
[PROOF STEP]
by(simp add: f'_def f_Suc)
[PROOF STATE]
proof (state)
this:
f (Suc n) = plus_current (f n) f'

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f (Suc n) = plus_current (f n) f'

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> current \<Gamma> (f (Suc n))
 2. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 3. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (f (Suc n))
[PROOF STEP]
unfolding f_Suc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current \<Gamma> (plus_current (f n) f')
[PROOF STEP]
using Suc.IH(1) f'
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (f n)
current (\<Gamma> \<ominus> f n) f'

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

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f (Suc n))

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
note f'' = this
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f (Suc n))

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f (Suc n))

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case (2 m)
[PROOF STATE]
proof (state)
this:
m < Suc n

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
have "d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)
[PROOF STEP]
using f''
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (f (Suc n))

goal (1 subgoal):
 1. d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)
[PROOF STEP]
by(rule currentD_weight_OUT)
[PROOF STATE]
proof (state)
this:
d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
have "weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
proof(cases "m = n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
 2. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
m = n

goal (2 subgoals):
 1. m = n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
 2. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m = n

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
unfolding f_Suc
[PROOF STATE]
proof (prove)
using this:
m = n

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (plus_current (f n) f') (enum m)
[PROOF STEP]
using OUT True
[PROOF STATE]
proof (prove)
using this:
m = n
d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n)
m = n

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (plus_current (f n) f') (enum m)
[PROOF STEP]
by(simp add: d_OUT_def nn_integral_add enum_A add_diff_self_ennreal less_imp_le)
[PROOF STATE]
proof (state)
this:
weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)

goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
m \<noteq> n

goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
hence "m < n"
[PROOF STATE]
proof (prove)
using this:
m \<noteq> n

goal (1 subgoal):
 1. m < n
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
m \<noteq> n
m < Suc n

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

goal (1 subgoal):
 1. m \<noteq> n \<Longrightarrow> weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
using Suc.IH(2)[OF \<open>m < n\<close>]
[PROOF STATE]
proof (prove)
using this:
m < n
d_OUT (f n) (enum m) = weight \<Gamma> (enum m)

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
unfolding f_Suc
[PROOF STATE]
proof (prove)
using this:
m < n
d_OUT (f n) (enum m) = weight \<Gamma> (enum m)

goal (1 subgoal):
 1. weight \<Gamma> (enum m) \<le> d_OUT (plus_current (f n) f') (enum m)
[PROOF STEP]
by(simp add: d_OUT_def nn_integral_add add_increasing2 )
[PROOF STATE]
proof (state)
this:
weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)

goal (2 subgoals):
 1. \<And>n m. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n); m < Suc n\<rbrakk> \<Longrightarrow> d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
 2. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)
weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
d_OUT (f (Suc n)) (enum m) \<le> weight \<Gamma> (enum m)
weight \<Gamma> (enum m) \<le> d_OUT (f (Suc n)) (enum m)

goal (1 subgoal):
 1. d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)
[PROOF STEP]
by(rule antisym)
[PROOF STATE]
proof (state)
this:
d_OUT (f (Suc n)) (enum m) = weight \<Gamma> (enum m)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m2 < Suc n \<Longrightarrow> d_OUT (f (Suc n)) (enum ?m2) = weight \<Gamma> (enum ?m2)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?m2 < Suc n \<Longrightarrow> d_OUT (f (Suc n)) (enum ?m2) = weight \<Gamma> (enum ?m2)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>n. \<lbrakk>current \<Gamma> (f n); \<And>m. m < n \<Longrightarrow> d_OUT (f n) (enum m) = weight \<Gamma> (enum m); \<not> hindered (\<Gamma> \<ominus> f n)\<rbrakk> \<Longrightarrow> \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindered (\<Gamma> \<ominus> f (Suc n))
[PROOF STEP]
unfolding f_Suc minus_plus_current[OF Suc.IH(1) f']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
by(rule unhindered')
[PROOF STATE]
proof (state)
this:
\<not> hindered (\<Gamma> \<ominus> f (Suc n))

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> hindered (\<Gamma> \<ominus> f (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
current \<Gamma> (f ?n)
?m < ?n1 \<Longrightarrow> d_OUT (f ?n1) (enum ?m) = weight \<Gamma> (enum ?m)
\<not> hindered (\<Gamma> \<ominus> f ?n)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
interpret \<Gamma>: countable_bipartite_web "\<Gamma> \<ominus> f n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f n)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> (f ?n)

goal (1 subgoal):
 1. countable_bipartite_web (\<Gamma> \<ominus> f n)
[PROOF STEP]
by(rule countable_bipartite_web_minus_web)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have Ex_P: "Ex (?P (f n) (enum n))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
using unhindered
[PROOF STATE]
proof (prove)
using this:
\<not> hindered (\<Gamma> \<ominus> f ?n)

goal (1 subgoal):
 1. \<exists>f'. current (\<Gamma> \<ominus> f n) f' \<and> d_OUT f' (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> f')
[PROOF STEP]
by(rule \<Gamma>.unhindered_saturate1)(simp add: enum_A)
[PROOF STATE]
proof (state)
this:
\<exists>f'. current (\<Gamma> \<ominus> f ?n) f' \<and> d_OUT f' (enum ?n) = weight (\<Gamma> \<ominus> f ?n) (enum ?n) \<and> \<not> hindered (\<Gamma> \<ominus> f ?n \<ominus> f')

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have f_mono: "f n \<le> f (Suc n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<le> f (Suc n)
[PROOF STEP]
using someI_ex[OF Ex_P, of n]
[PROOF STATE]
proof (prove)
using this:
current (\<Gamma> \<ominus> f n) (SOME x. current (\<Gamma> \<ominus> f n) x \<and> d_OUT x (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> x)) \<and> d_OUT (SOME x. current (\<Gamma> \<ominus> f n) x \<and> d_OUT x (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> x)) (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> (SOME x. current (\<Gamma> \<ominus> f n) x \<and> d_OUT x (enum n) = weight (\<Gamma> \<ominus> f n) (enum n) \<and> \<not> hindered (\<Gamma> \<ominus> f n \<ominus> x)))

goal (1 subgoal):
 1. f n \<le> f (Suc n)
[PROOF STEP]
by(auto simp add: le_fun_def f_Suc enum_A intro: add_increasing2 dest: )
[PROOF STATE]
proof (state)
this:
f ?n \<le> f (Suc ?n)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
hence incseq: "incseq f"
[PROOF STATE]
proof (prove)
using this:
f ?n \<le> f (Suc ?n)

goal (1 subgoal):
 1. incseq f
[PROOF STEP]
by(rule incseq_SucI)
[PROOF STATE]
proof (state)
this:
incseq f

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
hence chain: "Complete_Partial_Order.chain (\<le>) (range f)"
[PROOF STATE]
proof (prove)
using this:
incseq f

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) (range f)
[PROOF STEP]
by(rule incseq_chain_range)
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) (range f)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
define g where "g = Sup (range f)"
[PROOF STATE]
proof (state)
this:
g = \<Squnion> range f

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have "support_flow g \<subseteq> \<^bold>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_flow g \<subseteq> \<^bold>E
[PROOF STEP]
by (auto simp add: g_def support_flow.simps currentD_outside [OF f] image_comp elim: contrapos_pp)
[PROOF STATE]
proof (state)
this:
support_flow g \<subseteq> \<^bold>E

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
support_flow g \<subseteq> \<^bold>E
[PROOF STEP]
have countable_g: "countable (support_flow g)"
[PROOF STATE]
proof (prove)
using this:
support_flow g \<subseteq> \<^bold>E

goal (1 subgoal):
 1. countable (support_flow g)
[PROOF STEP]
by(rule countable_subset) simp
[PROOF STATE]
proof (state)
this:
countable (support_flow g)

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
with chain _ _
[PROOF STATE]
proof (chain)
picking this:
Complete_Partial_Order.chain (\<le>) (range f)
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
countable (support_flow g)
[PROOF STEP]
have g: "current \<Gamma> g"
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) (range f)
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
countable (support_flow g)

goal (1 subgoal):
 1. current \<Gamma> g
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) (range f)
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
countable (support_flow (\<Squnion> range f))

goal (1 subgoal):
 1. current \<Gamma> (\<Squnion> range f)
[PROOF STEP]
by(rule current_Sup)(auto simp add: f)
[PROOF STATE]
proof (state)
this:
current \<Gamma> g

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
current \<Gamma> g

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
have "d_OUT g x = weight \<Gamma> x" if "x \<in> A \<Gamma>" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT g x = weight \<Gamma> x
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d_OUT g x \<le> weight \<Gamma> x
 2. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
show "d_OUT g x \<le> weight \<Gamma> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_OUT g x \<le> weight \<Gamma> x
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> g

goal (1 subgoal):
 1. d_OUT g x \<le> weight \<Gamma> x
[PROOF STEP]
by(rule currentD_weight_OUT)
[PROOF STATE]
proof (state)
this:
d_OUT g x \<le> weight \<Gamma> x

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
have "countable (A \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (A \<Gamma>)
[PROOF STEP]
using A_vertex
[PROOF STATE]
proof (prove)
using this:
A \<Gamma> \<subseteq> \<^bold>V

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

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
from that subset_range_from_nat_into[OF this]
[PROOF STATE]
proof (chain)
picking this:
x \<in> A \<Gamma>
A \<Gamma> \<subseteq> range (from_nat_into (A \<Gamma>))
[PROOF STEP]
obtain n where "x = enum n"
[PROOF STATE]
proof (prove)
using this:
x \<in> A \<Gamma>
A \<Gamma> \<subseteq> range (from_nat_into (A \<Gamma>))

goal (1 subgoal):
 1. (\<And>n. x = enum n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding enum_def
[PROOF STATE]
proof (prove)
using this:
x \<in> A \<Gamma>
A \<Gamma> \<subseteq> range (from_nat_into (A \<Gamma>))

goal (1 subgoal):
 1. (\<And>n. x = from_nat_into (A \<Gamma>) n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = enum n

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
with sat[of n "Suc n"]
[PROOF STATE]
proof (chain)
picking this:
n < Suc n \<Longrightarrow> d_OUT (f (Suc n)) (enum n) = weight \<Gamma> (enum n)
x = enum n
[PROOF STEP]
have "d_OUT (f (Suc n)) x \<ge> weight \<Gamma> x"
[PROOF STATE]
proof (prove)
using this:
n < Suc n \<Longrightarrow> d_OUT (f (Suc n)) (enum n) = weight \<Gamma> (enum n)
x = enum n

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT (f (Suc n)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
weight \<Gamma> x \<le> d_OUT (f (Suc n)) x

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
weight \<Gamma> x \<le> d_OUT (f (Suc n)) x
[PROOF STEP]
show "weight \<Gamma> x \<le> d_OUT g x"
[PROOF STATE]
proof (prove)
using this:
weight \<Gamma> x \<le> d_OUT (f (Suc n)) x

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
using countable_g
[PROOF STATE]
proof (prove)
using this:
weight \<Gamma> x \<le> d_OUT (f (Suc n)) x
countable (support_flow g)

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT g x
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
weight \<Gamma> x \<le> d_OUT (f (Suc n)) x
countable (support_flow (\<Squnion> range f))

goal (1 subgoal):
 1. weight \<Gamma> x \<le> d_OUT (\<Squnion> range f) x
[PROOF STEP]
by(subst d_OUT_Sup[OF chain])(auto intro: SUP_upper2)
[PROOF STATE]
proof (state)
this:
weight \<Gamma> x \<le> d_OUT g x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Gamma> \<Longrightarrow> d_OUT g ?x = weight \<Gamma> ?x

goal (1 subgoal):
 1. A \<Gamma> \<noteq> {} \<Longrightarrow> linkable \<Gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
current \<Gamma> g
?x \<in> A \<Gamma> \<Longrightarrow> d_OUT g ?x = weight \<Gamma> ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
current \<Gamma> g
?x \<in> A \<Gamma> \<Longrightarrow> d_OUT g ?x = weight \<Gamma> ?x

goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
by(auto simp add: web_flow_iff linkage.simps)
[PROOF STATE]
proof (state)
this:
linkable \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem loose_linkable: \<comment> \<open>Theorem 6.2\<close>
  assumes "loose \<Gamma>"
  shows "linkable \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
interpret bi: countable_bipartite_web "bipartite_web_of \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (bipartite_web_of \<Gamma>)
[PROOF STEP]
by(rule countable_bipartite_web_of)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
have "\<not> hindered (bipartite_web_of \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> hindered (bipartite_web_of \<Gamma>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
loose \<Gamma>

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

goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> hindered (bipartite_web_of \<Gamma>)
[PROOF STEP]
have "linkable (bipartite_web_of \<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
\<not> hindered (bipartite_web_of \<Gamma>)

goal (1 subgoal):
 1. linkable (bipartite_web_of \<Gamma>)
[PROOF STEP]
by(rule bi.unhindered_linkable)
[PROOF STATE]
proof (state)
this:
linkable (bipartite_web_of \<Gamma>)

goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
linkable (bipartite_web_of \<Gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linkable (bipartite_web_of \<Gamma>)

goal (1 subgoal):
 1. linkable \<Gamma>
[PROOF STEP]
by(rule linkable_bipartite_web_ofD) simp
[PROOF STATE]
proof (state)
this:
linkable \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_orthogonal_current: \<comment> \<open>Lemma 4.15\<close>
  "\<exists>f S. web_flow \<Gamma> f \<and> separating \<Gamma> S \<and> orthogonal_current \<Gamma> f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. web_flow \<Gamma> f \<and> separating \<Gamma> S \<and> orthogonal_current \<Gamma> f S
[PROOF STEP]
by(rule ex_orthogonal_current')(rule countable_web.loose_linkable[OF countable_web_quotient_web])


[STATEMENT]
lemma max_flow_min_cut':
  assumes source_in: "\<And>x. \<not> edge \<Delta> x (source \<Delta>)"
  and sink_out: "\<And>y. \<not> edge \<Delta> (sink \<Delta>) y"
  and undead: "\<And>x y. edge \<Delta> x y \<Longrightarrow> (\<exists>z. edge \<Delta> y z) \<or> (\<exists>z. edge \<Delta> z x)"
  and source_sink: "\<not> edge \<Delta> (source \<Delta>) (sink \<Delta>)"
  and no_loop: "\<And>x. \<not> edge \<Delta> x x"
  and capacity_pos: "\<And>e. e \<in> \<^bold>E \<Longrightarrow> capacity \<Delta> e > 0"
  shows "\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
by(rule max_flow_min_cut')(rule countable_web.ex_orthogonal_current[OF countable_web_web_of_network], fact+)


[STATEMENT]
lemma max_flow_min_cut'':
  assumes sink_out: "\<And>y. \<not> edge \<Delta> (sink \<Delta>) y"
  and source_in: "\<And>x. \<not> edge \<Delta> x (source \<Delta>)"
  and no_loop: "\<And>x. \<not> edge \<Delta> x x"
  and capacity_pos: "\<And>e. e \<in> \<^bold>E \<Longrightarrow> capacity \<Delta> e > 0"
  shows "\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
interpret antiparallel_edges \<Delta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antiparallel_edges \<Delta>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
interpret \<Delta>'': countable_network \<Delta>''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_network \<Delta>''
[PROOF STEP]
by(rule \<Delta>''_countable_network)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "\<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S
[PROOF STEP]
by(rule \<Delta>''.max_flow_min_cut')(auto simp add: sink_out source_in no_loop capacity_pos elim: edg.cases)
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f S. flow \<Delta>'' f \<and> 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> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S

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

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "flow \<Delta> (collect f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
flow \<Delta>'' f

goal (1 subgoal):
 1. flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
[PROOF STEP]
by(rule flow_collect)
[PROOF STATE]
proof (state)
this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "cut \<Delta> (cut' S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut \<Delta> (Vertex -` S)
[PROOF STEP]
using cut
[PROOF STATE]
proof (prove)
using this:
cut \<Delta>'' S

goal (1 subgoal):
 1. cut \<Delta> (Vertex -` S)
[PROOF STEP]
by(rule cut_cut')
[PROOF STATE]
proof (state)
this:
cut \<Delta> (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cut \<Delta> (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "orthogonal \<Delta> (collect f) (cut' S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
using ortho f
[PROOF STATE]
proof (prove)
using this:
orthogonal \<Delta>'' f S
flow \<Delta>'' f

goal (1 subgoal):
 1. orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
by(rule orthogonal_cut')
[PROOF STATE]
proof (state)
this:
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
cut \<Delta> (Vertex -` S)
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
cut \<Delta> (Vertex -` S)
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_flow_min_cut''':
  assumes sink_out: "\<And>y. \<not> edge \<Delta> (sink \<Delta>) y"
  and source_in: "\<And>x. \<not> edge \<Delta> x (source \<Delta>)"
  and capacity_pos: "\<And>e. e \<in> \<^bold>E \<Longrightarrow> capacity \<Delta> e > 0"
  shows "\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
interpret antiparallel_edges \<Delta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antiparallel_edges \<Delta>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
interpret \<Delta>'': countable_network \<Delta>''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_network \<Delta>''
[PROOF STEP]
by(rule \<Delta>''_countable_network)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "\<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S
[PROOF STEP]
by(rule \<Delta>''.max_flow_min_cut'')(auto simp add: sink_out source_in capacity_pos elim: edg.cases)
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta>'' f \<and> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f S. flow \<Delta>'' f \<and> 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> cut \<Delta>'' S \<and> orthogonal \<Delta>'' f S

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

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "flow \<Delta> (collect f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
flow \<Delta>'' f

goal (1 subgoal):
 1. flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
[PROOF STEP]
by(rule flow_collect)
[PROOF STATE]
proof (state)
this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "cut \<Delta> (cut' S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut \<Delta> (Vertex -` S)
[PROOF STEP]
using cut
[PROOF STATE]
proof (prove)
using this:
cut \<Delta>'' S

goal (1 subgoal):
 1. cut \<Delta> (Vertex -` S)
[PROOF STEP]
by(rule cut_cut')
[PROOF STATE]
proof (state)
this:
cut \<Delta> (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cut \<Delta> (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "orthogonal \<Delta> (collect f) (cut' S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
using ortho f
[PROOF STATE]
proof (prove)
using this:
orthogonal \<Delta>'' f S
flow \<Delta>'' f

goal (1 subgoal):
 1. orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
by(rule orthogonal_cut')
[PROOF STATE]
proof (state)
this:
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
cut \<Delta> (Vertex -` S)
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
flow \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y))
cut \<Delta> (Vertex -` S)
orthogonal \<Delta> (\<lambda>(x, y). f (Edge x y, Vertex y)) (Vertex -` S)

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem max_flow_min_cut:
  "\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
interpret \<Delta>''': countable_network \<Delta>'''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_network \<Delta>'''
[PROOF STEP]
by(rule \<Delta>'''_countable_network)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
have "\<exists>f S. flow \<Delta>''' f \<and> cut \<Delta>''' S \<and> orthogonal \<Delta>''' f S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. flow \<Delta>''' f \<and> cut \<Delta>''' S \<and> orthogonal \<Delta>''' f S
[PROOF STEP]
by(rule \<Delta>'''.max_flow_min_cut''') auto
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta>''' f \<and> cut \<Delta>''' S \<and> orthogonal \<Delta>''' f S

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f S. flow \<Delta>''' f \<and> 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> cut \<Delta>''' S \<and> orthogonal \<Delta>''' f S

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

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
from flow_\<Delta>'''[OF this]
[PROOF STATE]
proof (chain)
picking this:
flow \<Delta> f
cut \<Delta> S
orthogonal \<Delta> f S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
flow \<Delta> f
cut \<Delta> S
orthogonal \<Delta> f S

goal (1 subgoal):
 1. \<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f S. flow \<Delta> f \<and> cut \<Delta> S \<and> orthogonal \<Delta> f S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_\<beta>00[simp]: "vec_of_basis_enum \<beta>00 = vector_\<beta>00"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<beta>00 = vector_\<beta>00
[PROOF STEP]
by (auto simp add: \<beta>00_def vector_\<beta>00_def)


[STATEMENT]
lemma vec_of_ell2_\<beta>00[simp, code]: "vec_of_ell2 \<beta>00 = vector_\<beta>00"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_ell2 \<beta>00 = vector_\<beta>00
[PROOF STEP]
by (simp add: vec_of_ell2_def)


[STATEMENT]
lemma norm_\<beta>00[simp]: "norm \<beta>00 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm \<beta>00 = 1
[PROOF STEP]
by eval


[STATEMENT]
lemma vec_of_basis_enum_ketplus[simp]: "vec_of_basis_enum ketplus = vector_ketplus"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum |+\<rangle> = vector_ketplus
[PROOF STEP]
by (auto simp add: ketplus_def vector_ketplus_def)


[STATEMENT]
lemma vec_of_ell2_ketplus[simp, code]: "vec_of_ell2 ketplus = vector_ketplus"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_ell2 |+\<rangle> = vector_ketplus
[PROOF STEP]
by (simp add: vec_of_ell2_def)


[STATEMENT]
lemma [simp, code]: "mat_of_cblinfun pauliX = matrix_pauliX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun pauliX = matrix_pauliX
[PROOF STEP]
apply (auto simp add: pauliX_def matrix_pauliX_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat (mat_of_rows_list 2 [[0, 1], [1, 0]])) = mat_of_rows_list 2 [[0, 1], [1, 0]]
[PROOF STEP]
apply (subst cblinfun_of_mat_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mat_of_rows_list 2 [[0, 1], [1, 0]] \<in> carrier_mat (length canonical_basis) (length canonical_basis)
 2. mat_of_rows_list 2 [[0, 1], [1, 0]] = mat_of_rows_list 2 [[0, 1], [1, 0]]
[PROOF STEP]
by (auto)


[STATEMENT]
lemma pauliX_adjoint[simp]: "pauliX* = pauliX"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pauliX* = pauliX
[PROOF STEP]
by eval


[STATEMENT]
lemma pauliXX[simp]: "pauliX o\<^sub>C\<^sub>L pauliX = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pauliX o\<^sub>C\<^sub>L pauliX = id_cblinfun
[PROOF STEP]
by eval


[STATEMENT]
lemma [simp, code]: "mat_of_cblinfun pauliZ = matrix_pauliZ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun pauliZ = matrix_pauliZ
[PROOF STEP]
apply (auto simp add: pauliZ_def matrix_pauliZ_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat (mat_of_rows_list 2 [[1, 0], [0, - 1]])) = mat_of_rows_list 2 [[1, 0], [0, - 1]]
[PROOF STEP]
apply (subst cblinfun_of_mat_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mat_of_rows_list 2 [[1, 0], [0, - 1]] \<in> carrier_mat (length canonical_basis) (length canonical_basis)
 2. mat_of_rows_list 2 [[1, 0], [0, - 1]] = mat_of_rows_list 2 [[1, 0], [0, - 1]]
[PROOF STEP]
by (auto)


[STATEMENT]
lemma pauliZ_adjoint[simp]: "pauliZ* = pauliZ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pauliZ* = pauliZ
[PROOF STEP]
by eval


[STATEMENT]
lemma pauliZZ[simp]: "pauliZ o\<^sub>C\<^sub>L pauliZ = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pauliZ o\<^sub>C\<^sub>L pauliZ = id_cblinfun
[PROOF STEP]
by eval


[STATEMENT]
lemma [simp, code]: "mat_of_cblinfun hadamard = matrix_hadamard"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun hadamard = matrix_hadamard
[PROOF STEP]
apply (auto simp add: hadamard_def matrix_hadamard_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat (mat_of_rows_list 2 [[1 / complex_of_real (sqrt 2), 1 / complex_of_real (sqrt 2)], [1 / complex_of_real (sqrt 2), - (1 / complex_of_real (sqrt 2))]])) = mat_of_rows_list 2 [[1 / complex_of_real (sqrt 2), 1 / complex_of_real (sqrt 2)], [1 / complex_of_real (sqrt 2), - (1 / complex_of_real (sqrt 2))]]
[PROOF STEP]
apply (subst cblinfun_of_mat_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mat_of_rows_list 2 [[1 / complex_of_real (sqrt 2), 1 / complex_of_real (sqrt 2)], [1 / complex_of_real (sqrt 2), - (1 / complex_of_real (sqrt 2))]] \<in> carrier_mat (length canonical_basis) (length canonical_basis)
 2. mat_of_rows_list 2 [[1 / complex_of_real (sqrt 2), 1 / complex_of_real (sqrt 2)], [1 / complex_of_real (sqrt 2), - (1 / complex_of_real (sqrt 2))]] = mat_of_rows_list 2 [[1 / complex_of_real (sqrt 2), 1 / complex_of_real (sqrt 2)], [1 / complex_of_real (sqrt 2), - (1 / complex_of_real (sqrt 2))]]
[PROOF STEP]
by (auto)


[STATEMENT]
lemma hada_adj[simp]: "hadamard* = hadamard"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hadamard* = hadamard
[PROOF STEP]
by eval


[STATEMENT]
lemma [simp, code]: "mat_of_cblinfun CNOT = matrix_CNOT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun CNOT = matrix_CNOT
[PROOF STEP]
apply (auto simp add: CNOT_def matrix_CNOT_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat (mat_of_rows_list 4 [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]])) = mat_of_rows_list 4 [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]]
[PROOF STEP]
apply (subst cblinfun_of_mat_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mat_of_rows_list 4 [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]] \<in> carrier_mat (length canonical_basis) (length canonical_basis)
 2. mat_of_rows_list 4 [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]] = mat_of_rows_list 4 [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]]
[PROOF STEP]
by (auto)


[STATEMENT]
lemma [simp]: "CNOT* = CNOT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CNOT* = CNOT
[PROOF STEP]
by eval


[STATEMENT]
lemma cnot_apply[simp]: \<open>CNOT *\<^sub>V ket (i,j) = ket (i,j+i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CNOT *\<^sub>V ket (i, j) = ket (i, j + i)
[PROOF STEP]
apply (rule spec[where x=i], rule spec[where x=j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. CNOT *\<^sub>V ket (xa, x) = ket (xa, x + xa)
[PROOF STEP]
by eval


[STATEMENT]
lemma mat_of_cblinfun_Uswap[simp, code]: "mat_of_cblinfun Uswap = matrix_Uswap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun Uswap = matrix_Uswap
[PROOF STEP]
apply (auto simp add: Uswap_def matrix_Uswap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat (mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]])) = mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]]
[PROOF STEP]
apply (subst cblinfun_of_mat_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]] \<in> carrier_mat (length canonical_basis) (length canonical_basis)
 2. mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]] = mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]]
[PROOF STEP]
by (auto)


[STATEMENT]
lemma dim_col_Uswap[simp]: "dim_col matrix_Uswap = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col matrix_Uswap = 4
[PROOF STEP]
unfolding matrix_Uswap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]]) = 4
[PROOF STEP]
by simp


[STATEMENT]
lemma dim_row_Uswap[simp]: "dim_row matrix_Uswap = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row matrix_Uswap = 4
[PROOF STEP]
unfolding matrix_Uswap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_rows_list 4 [[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]]) = 4
[PROOF STEP]
by simp


[STATEMENT]
lemma Uswap_adjoint[simp]: "Uswap* = Uswap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Uswap* = Uswap
[PROOF STEP]
by eval


[STATEMENT]
lemma Uswap_involution[simp]: "Uswap o\<^sub>C\<^sub>L Uswap = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Uswap o\<^sub>C\<^sub>L Uswap = id_cblinfun
[PROOF STEP]
by eval


[STATEMENT]
lemma unitary_Uswap[simp]: "unitary Uswap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary Uswap
[PROOF STEP]
unfolding unitary_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Uswap* o\<^sub>C\<^sub>L Uswap = id_cblinfun \<and> Uswap o\<^sub>C\<^sub>L Uswap* = id_cblinfun
[PROOF STEP]
by simp


[STATEMENT]
lemma Uswap_apply[simp]: \<open>Uswap *\<^sub>V s \<otimes>\<^sub>s t = t \<otimes>\<^sub>s s\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Uswap *\<^sub>V s \<otimes>\<^sub>s t = t \<otimes>\<^sub>s s
[PROOF STEP]
apply (rule clinear_equal_ket[where f=\<open>\<lambda>s. Uswap *\<^sub>V s \<otimes>\<^sub>s t\<close>, THEN fun_cong])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. clinear (\<lambda>s. Uswap *\<^sub>V s \<otimes>\<^sub>s t)
 2. clinear ((\<otimes>\<^sub>s) t)
 3. \<And>i. Uswap *\<^sub>V ket i \<otimes>\<^sub>s t = t \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (simp add: cblinfun.add_right clinearI tensor_ell2_add1 tensor_ell2_scaleC1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear ((\<otimes>\<^sub>s) t)
 2. \<And>i. Uswap *\<^sub>V ket i \<otimes>\<^sub>s t = t \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (simp add: clinear_tensor_ell21)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Uswap *\<^sub>V ket i \<otimes>\<^sub>s t = t \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (rule clinear_equal_ket[where f=\<open>\<lambda>t. Uswap *\<^sub>V _ \<otimes>\<^sub>s t\<close>, THEN fun_cong])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i. clinear (\<lambda>t. Uswap *\<^sub>V ket i \<otimes>\<^sub>s t)
 2. \<And>i. clinear (\<lambda>a. a \<otimes>\<^sub>s ket i)
 3. \<And>i ia. Uswap *\<^sub>V ket i \<otimes>\<^sub>s ket ia = ket ia \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (simp add: cblinfun.add_right clinearI tensor_ell2_add2 tensor_ell2_scaleC2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. clinear (\<lambda>a. a \<otimes>\<^sub>s ket i)
 2. \<And>i ia. Uswap *\<^sub>V ket i \<otimes>\<^sub>s ket ia = ket ia \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (simp add: clinear_tensor_ell22)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. Uswap *\<^sub>V ket i \<otimes>\<^sub>s ket ia = ket ia \<otimes>\<^sub>s ket i
[PROOF STEP]
apply (rule basis_enum_eq_vec_of_basis_enumI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. vec_of_basis_enum (Uswap *\<^sub>V ket i \<otimes>\<^sub>s ket ia) = vec_of_basis_enum (ket ia \<otimes>\<^sub>s ket i)
[PROOF STEP]
apply (simp add: mat_of_cblinfun_cblinfun_apply vec_of_basis_enum_ket)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. matrix_Uswap *\<^sub>v unit_vec 4 (enum_idx (i, ia)) = unit_vec 4 (enum_idx (ia, i))
[PROOF STEP]
by (case_tac i; case_tac ia; hypsubst_thin; normalization)


[STATEMENT]
lemma closure_bounded_linear_image_subset_eq:
  assumes f: "bounded_linear f"
  shows "closure (f ` closure S) = closure (f ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (f ` closure S) = closure (f ` S)
[PROOF STEP]
by (meson closed_closure closure_bounded_linear_image_subset closure_minimal closure_mono closure_subset f image_mono subset_antisym)


[STATEMENT]
lemma not_singleton_real_normed_is_perfect_space[simp]: \<open>class.perfect_space (open :: 'a::{not_singleton,real_normed_vector} set \<Rightarrow> bool)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.perfect_space open
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> open {x}
[PROOF STEP]
by (metis UNIV_not_singleton clopen closed_singleton empty_not_insert)


[STATEMENT]
lemma infsum_bounded_linear:
  assumes \<open>bounded_linear f\<close>
  assumes \<open>g summable_on S\<close>
  shows \<open>infsum (f \<circ> g) S = f (infsum g S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infsum (f \<circ> g) S = f (infsum g S)
[PROOF STEP]
apply (rule infsum_comm_additive)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. additive f
 2. isCont f (infsum g S)
 3. g summable_on S
[PROOF STEP]
using assms blinfun_apply_induct blinfun.additive_right
[PROOF STATE]
proof (prove)
using this:
bounded_linear f
g summable_on S
\<lbrakk>?y \<in> {f. bounded_linear f}; \<And>x. ?P (blinfun_apply x)\<rbrakk> \<Longrightarrow> ?P ?y
additive (blinfun_apply ?a)

goal (3 subgoals):
 1. additive f
 2. isCont f (infsum g S)
 3. g summable_on S
[PROOF STEP]
by (auto simp: linear_continuous_within)


[STATEMENT]
lemma has_sum_bounded_linear:
  assumes \<open>bounded_linear f\<close>
  assumes \<open>has_sum g S x\<close>
  shows \<open>has_sum (f o g) S (f x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sum (f \<circ> g) S (f x)
[PROOF STEP]
apply (rule has_sum_comm_additive)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. additive f
 2. f \<midarrow>x\<rightarrow> f x
 3. has_sum g S x
[PROOF STEP]
using assms blinfun_apply_induct blinfun.additive_right
[PROOF STATE]
proof (prove)
using this:
bounded_linear f
has_sum g S x
\<lbrakk>?y \<in> {f. bounded_linear f}; \<And>x. ?P (blinfun_apply x)\<rbrakk> \<Longrightarrow> ?P ?y
additive (blinfun_apply ?a)

goal (3 subgoals):
 1. additive f
 2. f \<midarrow>x\<rightarrow> f x
 3. has_sum g S x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_linear f; has_sum g S x; \<And>y P. \<lbrakk>bounded_linear y; \<And>x. P (blinfun_apply x)\<rbrakk> \<Longrightarrow> P y; \<And>a. additive (blinfun_apply a)\<rbrakk> \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
using isCont_def linear_continuous_at
[PROOF STATE]
proof (prove)
using this:
isCont ?f ?a = ?f \<midarrow>?a\<rightarrow> ?f ?a
bounded_linear ?f \<Longrightarrow> isCont ?f ?a

goal (1 subgoal):
 1. \<lbrakk>bounded_linear f; has_sum g S x; \<And>y P. \<lbrakk>bounded_linear y; \<And>x. P (blinfun_apply x)\<rbrakk> \<Longrightarrow> P y; \<And>a. additive (blinfun_apply a)\<rbrakk> \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma abs_summable_on_bounded_linear:
  assumes \<open>bounded_linear f\<close>
  assumes \<open>g abs_summable_on S\<close>
  shows \<open>(f o g) abs_summable_on S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
have bound: \<open>norm (f (g x)) \<le> onorm f * norm (g x)\<close> for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (f (g x)) \<le> onorm f * norm (g x)
[PROOF STEP]
apply (rule onorm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear f
[PROOF STEP]
by (simp add: assms(1))
[PROOF STATE]
proof (state)
this:
norm (f (g ?x)) \<le> onorm f * norm (g ?x)

goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
g abs_summable_on S
[PROOF STEP]
have \<open>(\<lambda>x. onorm f *\<^sub>R g x) abs_summable_on S\<close>
[PROOF STATE]
proof (prove)
using this:
g abs_summable_on S

goal (1 subgoal):
 1. (\<lambda>x. onorm f *\<^sub>R g x) abs_summable_on S
[PROOF STEP]
by (auto intro!: summable_on_cmult_right)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. onorm f *\<^sub>R g x) abs_summable_on S

goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. onorm f *\<^sub>R g x) abs_summable_on S
[PROOF STEP]
have \<open>(\<lambda>x. f (g x)) abs_summable_on S\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. onorm f *\<^sub>R g x) abs_summable_on S

goal (1 subgoal):
 1. (\<lambda>x. f (g x)) abs_summable_on S
[PROOF STEP]
apply (rule abs_summable_on_comparison_test)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> norm (f (g x)) \<le> norm (onorm f *\<^sub>R g x)
[PROOF STEP]
using bound
[PROOF STATE]
proof (prove)
using this:
norm (f (g ?x)) \<le> onorm f * norm (g ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> norm (f (g x)) \<le> norm (onorm f *\<^sub>R g x)
[PROOF STEP]
by (auto simp: assms(1) onorm_pos_le)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (g x)) abs_summable_on S

goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f (g x)) abs_summable_on S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f (g x)) abs_summable_on S

goal (1 subgoal):
 1. f \<circ> g abs_summable_on S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> g abs_summable_on S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norm_plus_leq_norm_prod: \<open>norm (a + b) \<le> sqrt 2 * norm (a, b)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
have \<open>(norm (a + b))\<^sup>2 \<le> (norm a + norm b)\<^sup>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm (a + b))\<^sup>2 \<le> (norm a + norm b)\<^sup>2
[PROOF STEP]
using norm_triangle_ineq
[PROOF STATE]
proof (prove)
using this:
norm (?x + ?y) \<le> norm ?x + norm ?y

goal (1 subgoal):
 1. (norm (a + b))\<^sup>2 \<le> (norm a + norm b)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(norm (a + b))\<^sup>2 \<le> (norm a + norm b)\<^sup>2

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(norm (a + b))\<^sup>2 \<le> (norm a + norm b)\<^sup>2

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
have \<open>\<dots> \<le> 2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm a + norm b)\<^sup>2 \<le> 2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2)
[PROOF STEP]
by (smt (verit, best) power2_sum sum_squares_bound)
[PROOF STATE]
proof (state)
this:
(norm a + norm b)\<^sup>2 \<le> 2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2)

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(norm a + norm b)\<^sup>2 \<le> 2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2)

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
have \<open>\<dots> \<le> (sqrt 2 * norm (a, b))\<^sup>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2) \<le> (sqrt 2 * norm (a, b))\<^sup>2
[PROOF STEP]
by (auto simp: power_mult_distrib norm_prod_def simp del: power_mono_iff)
[PROOF STATE]
proof (state)
this:
2 * ((norm a)\<^sup>2 + (norm b)\<^sup>2) \<le> (sqrt 2 * norm (a, b))\<^sup>2

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(norm (a + b))\<^sup>2 \<le> (sqrt 2 * norm (a, b))\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(norm (a + b))\<^sup>2 \<le> (sqrt 2 * norm (a, b))\<^sup>2

goal (1 subgoal):
 1. norm (a + b) \<le> sqrt 2 * norm (a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (a + b) \<le> sqrt 2 * norm (a, b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_norm1:
  assumes \<open>(UNIV::'a::real_normed_vector set) \<noteq> {0}\<close>
  shows \<open>\<exists>x::'a. norm x = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
have \<open>\<exists>x::'a. x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<noteq> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
UNIV \<noteq> {0::'a}

goal (1 subgoal):
 1. \<exists>x. x \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<noteq> (0::'a)
[PROOF STEP]
obtain x::'a where \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>x. x \<noteq> (0::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
hence \<open>norm x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'a)

goal (1 subgoal):
 1. norm x \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm x \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
hence \<open>(norm x) / (norm x) = 1\<close>
[PROOF STATE]
proof (prove)
using this:
norm x \<noteq> 0

goal (1 subgoal):
 1. norm x / norm x = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm x / norm x = 1

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm x / norm x = 1

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
have \<open>(norm x) / (norm x) = norm (x /\<^sub>R (norm x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x / norm x = norm (x /\<^sub>R norm x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm x / norm x = norm (x /\<^sub>R norm x)

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm x / norm x = 1
norm x / norm x = norm (x /\<^sub>R norm x)
[PROOF STEP]
have \<open>norm (x /\<^sub>R (norm x)) = 1\<close>
[PROOF STATE]
proof (prove)
using this:
norm x / norm x = 1
norm x / norm x = norm (x /\<^sub>R norm x)

goal (1 subgoal):
 1. norm (x /\<^sub>R norm x) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (x /\<^sub>R norm x) = 1

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (x /\<^sub>R norm x) = 1

goal (1 subgoal):
 1. \<exists>x. norm x = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. norm x = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bdd_above_norm_f:
  assumes "bounded_linear f"
  shows \<open>bdd_above {norm (f x) |x. norm x = 1}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above {norm (f x) |x. norm x = 1}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above {norm (f x) |x. norm x = 1}
[PROOF STEP]
have \<open>\<exists>M. \<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> M\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. \<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded_linear f

goal (1 subgoal):
 1. \<exists>M. \<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> M
[PROOF STEP]
by (metis bounded_linear.axioms(2) bounded_linear_axioms_def)
[PROOF STATE]
proof (state)
this:
\<exists>M. \<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> M

goal (1 subgoal):
 1. bdd_above {norm (f x) |x. norm x = 1}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> M

goal (1 subgoal):
 1. bdd_above {norm (f x) |x. norm x = 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bdd_above {norm (f x) |x. norm x = 1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tso_store_inv_eq_imp:
  "eq_imp (\<lambda>p s. mem_store_buffers (s sys) p)
          tso_store_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp sys_mem_store_buffers tso_store_inv
[PROOF STEP]
by (simp add: eq_imp_def tso_store_inv_def)


[STATEMENT]
lemma tso_store_invD[simp]:
  "tso_store_inv s \<Longrightarrow> \<not>sys_mem_store_buffers gc s = mw_Mutate r f r' # ws"
  "tso_store_inv s \<Longrightarrow> \<not>sys_mem_store_buffers gc s = mw_Mutate_Payload r f pl # ws"
  "tso_store_inv s \<Longrightarrow> \<not>sys_mem_store_buffers (mutator m) s = mw_fA fl # ws"
  "tso_store_inv s \<Longrightarrow> \<not>sys_mem_store_buffers (mutator m) s = mw_fM fl # ws"
  "tso_store_inv s \<Longrightarrow> \<not>sys_mem_store_buffers (mutator m) s = mw_Phase ph # ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((tso_store_inv s \<Longrightarrow> sys_mem_store_buffers gc s \<noteq> mw_Mutate r f r' # ws) &&& (tso_store_inv s \<Longrightarrow> sys_mem_store_buffers gc s \<noteq> mw_Mutate_Payload r f pl # ws)) &&& (tso_store_inv s \<Longrightarrow> sys_mem_store_buffers (mutator m) s \<noteq> mw_fA fl # ws) &&& (tso_store_inv s \<Longrightarrow> sys_mem_store_buffers (mutator m) s \<noteq> mw_fM fl # ws) &&& (tso_store_inv s \<Longrightarrow> sys_mem_store_buffers (mutator m) s \<noteq> mw_Phase ph # ws)
[PROOF STEP]
by (auto simp: tso_store_inv_def dest!: spec[where x=m])


[STATEMENT]
lemma mut_do_store_action[simp]:
  "\<lbrakk> sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s \<rbrakk> \<Longrightarrow> fA (do_store_action w (s sys)) = sys_fA s"
  "\<lbrakk> sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s \<rbrakk> \<Longrightarrow> fM (do_store_action w (s sys)) = sys_fM s"
  "\<lbrakk> sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s \<rbrakk> \<Longrightarrow> phase (do_store_action w (s sys)) = sys_phase s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s\<rbrakk> \<Longrightarrow> fA (do_store_action w (s sys)) = sys_fA s) &&& (\<lbrakk>sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s\<rbrakk> \<Longrightarrow> fM (do_store_action w (s sys)) = sys_fM s) &&& (\<lbrakk>sys_mem_store_buffers (mutator m) s = w # ws; tso_store_inv s\<rbrakk> \<Longrightarrow> phase (do_store_action w (s sys)) = sys_phase s)
[PROOF STEP]
by (auto simp: do_store_action_def split: mem_store_action.splits)


[STATEMENT]
lemma tso_store_inv_sys_load_Mut[simp]:
  assumes "tso_store_inv s"
  assumes "(ract, v) \<in> { (mr_fM, mv_Mark (Some (sys_fM s))), (mr_fA, mv_Mark (Some (sys_fA s))), (mr_Phase, mv_Phase (sys_phase s)) }"
  shows "sys_load (mutator m) ract (s sys) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sys_load (mutator m) ract (s sys) = v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
tso_store_inv s
(ract, v) \<in> {(mr_fM, mv_Mark (Some (sys_fM s))), (mr_fA, mv_Mark (Some (sys_fA s))), (mr_Phase, mv_Phase (sys_phase s))}

goal (1 subgoal):
 1. sys_load (mutator m) ract (s sys) = v
[PROOF STEP]
apply (clarsimp simp: sys_load_def fold_stores_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s)\<rbrakk> \<Longrightarrow> do_load_action ract (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) = v
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. do_load_action ract (fr (s sys)) = v" and Q="mut_writes"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s); x \<in> set (sys_mem_store_buffers (mutator m) s)\<rbrakk> \<Longrightarrow> mut_writes x
 2. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s)\<rbrakk> \<Longrightarrow> do_load_action ract (id (s sys)) = v
 3. \<And>x sa. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s); mut_writes x; do_load_action ract (sa (s sys)) = v\<rbrakk> \<Longrightarrow> do_load_action ract ((do_store_action x \<circ> sa) (s sys)) = v
[PROOF STEP]
apply (fastforce simp: tso_store_inv_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s)\<rbrakk> \<Longrightarrow> do_load_action ract (id (s sys)) = v
 2. \<And>x sa. \<lbrakk>tso_store_inv s; ract = mr_fM \<and> v = mv_Mark (Some (sys_fM s)) \<or> ract = mr_fA \<and> v = mv_Mark (Some (sys_fA s)) \<or> ract = mr_Phase \<and> v = mv_Phase (sys_phase s); mut_writes x; do_load_action ract (sa (s sys)) = v\<rbrakk> \<Longrightarrow> do_load_action ract ((do_store_action x \<circ> sa) (s sys)) = v
[PROOF STEP]
apply (auto simp: do_load_action_def split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done