[STATEMENT]
lemma reduce_weight_sel [simp]:
  "edge (reduce_weight \<Gamma> x r) = edge \<Gamma>"
  "A (reduce_weight \<Gamma> x r) = A \<Gamma>"
  "B (reduce_weight \<Gamma> x r) = B \<Gamma>"
  "vertex (reduce_weight \<Gamma> x r) = vertex \<Gamma>"
  "weight (reduce_weight \<Gamma> x r) y = (if x = y then weight \<Gamma> x - r else weight \<Gamma> y)"
  "web.more (reduce_weight \<Gamma> x r) = web.more \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (edge (reduce_weight \<Gamma> x r) = edge \<Gamma> &&& A (reduce_weight \<Gamma> x r) = A \<Gamma> &&& B (reduce_weight \<Gamma> x r) = B \<Gamma>) &&& vertex (reduce_weight \<Gamma> x r) = vertex \<Gamma> &&& weight (reduce_weight \<Gamma> x r) y = (if x = y then weight \<Gamma> x - ennreal r else weight \<Gamma> y) &&& web.more (reduce_weight \<Gamma> x r) = web.more \<Gamma>
[PROOF STEP]
by(simp_all add: reduce_weight_def zero_ennreal_def[symmetric] vertex_def fun_eq_iff)


[STATEMENT]
lemma essential_reduce_weight [simp]: "essential (reduce_weight \<Gamma> x r) = essential \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. essential (reduce_weight \<Gamma> x r) = essential \<Gamma>
[PROOF STEP]
by(simp add: fun_eq_iff essential_def)


[STATEMENT]
lemma roofed_reduce_weight [simp]: "roofed_gen (reduce_weight \<Gamma> x r) = roofed_gen \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. roofed_gen (reduce_weight \<Gamma> x r) = roofed_gen \<Gamma>
[PROOF STEP]
by(simp add: fun_eq_iff roofed_def)


[STATEMENT]
lemma notin_range_Inner:  "x \<notin> range Inner \<longleftrightarrow> x = SOURCE \<or> x = SINK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> range Inner) = (x = SOURCE \<or> x = vertex.SINK)
[PROOF STEP]
by(cases x) auto


[STATEMENT]
lemma inj_Inner [simp]: "\<And>A. inj_on Inner A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. inj_on Inner A
[PROOF STEP]
by(simp add: inj_on_def)