[STATEMENT]
lemma RF_TER_Sup:
  fixes \<Gamma> (structure)
  assumes f: "\<And>f. f \<in> Y \<Longrightarrow> current \<Gamma> f"
  and w: "\<And>f. f \<in> Y \<Longrightarrow> wave \<Gamma> f"
  and Y: "Complete_Partial_Order.chain (\<le>) Y" "Y \<noteq> {}" "countable (support_flow (Sup Y))"
  shows "RF (TER (Sup Y)) = RF (\<Union>f\<in>Y. TER f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RF (TER (\<Squnion> Y)) = RF (\<Union> (TER ` Y))
[PROOF STEP]
proof(rule set_eqI iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> RF (TER (\<Squnion> Y)) \<Longrightarrow> x \<in> RF (\<Union> (TER ` Y))
 2. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> RF (TER (\<Squnion> Y)) \<Longrightarrow> x \<in> RF (\<Union> (TER ` Y))
 2. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
assume x: "x \<in> RF (TER (Sup Y))"
[PROOF STATE]
proof (state)
this:
x \<in> RF (TER (\<Squnion> Y))

goal (2 subgoals):
 1. \<And>x. x \<in> RF (TER (\<Squnion> Y)) \<Longrightarrow> x \<in> RF (\<Union> (TER ` Y))
 2. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
have "x \<in> RF (RF (\<Union>f\<in>Y. TER f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> RF (RF (\<Union> (TER ` Y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
fix p y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
assume p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
from roofedD[OF x p y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p. z \<in> TER (\<Squnion> Y)) \<or> x \<in> TER (\<Squnion> Y)
[PROOF STEP]
obtain z where z: "z \<in> set (x # p)" and TER: "z \<in> TER (Sup Y)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p. z \<in> TER (\<Squnion> Y)) \<or> x \<in> TER (\<Squnion> Y)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> set (x # p); z \<in> TER (\<Squnion> Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> set (x # p)
z \<in> TER (\<Squnion> Y)

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
from TER
[PROOF STATE]
proof (chain)
picking this:
z \<in> TER (\<Squnion> Y)
[PROOF STEP]
have SINK: "z \<in> SINK f" if "f \<in> Y" for f
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (\<Squnion> Y)

goal (1 subgoal):
 1. z \<in> SINK f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (\<Squnion> Y)
f \<in> Y

goal (1 subgoal):
 1. z \<in> SINK f
[PROOF STEP]
by(auto simp add: SINK_Sup[OF Y])
[PROOF STATE]
proof (state)
this:
?f \<in> Y \<Longrightarrow> z \<in> SINK ?f

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
from Y(2)
[PROOF STATE]
proof (chain)
picking this:
Y \<noteq> {}
[PROOF STEP]
obtain f where y: "f \<in> Y"
[PROOF STATE]
proof (prove)
using this:
Y \<noteq> {}

goal (1 subgoal):
 1. (\<And>f. f \<in> Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> Y

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
show "(\<exists>z\<in>set p. z \<in> RF (\<Union>f\<in>Y. TER f)) \<or> x \<in> RF (\<Union>f\<in>Y. TER f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
proof(cases "\<exists>f\<in>Y. z \<in> RF (TER f)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>f\<in>Y. z \<in> RF (TER f) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
 2. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>f\<in>Y. z \<in> RF (TER f)

goal (2 subgoals):
 1. \<exists>f\<in>Y. z \<in> RF (TER f) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
 2. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>f\<in>Y. z \<in> RF (TER f)
[PROOF STEP]
obtain f where fY: "f \<in> Y" and zf: "z \<in> RF (TER f)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f\<in>Y. z \<in> RF (TER f)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> Y; z \<in> RF (TER f)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> Y
z \<in> RF (TER f)

goal (2 subgoals):
 1. \<exists>f\<in>Y. z \<in> RF (TER f) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
 2. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
from zf
[PROOF STATE]
proof (chain)
picking this:
z \<in> RF (TER f)
[PROOF STEP]
have "z \<in> RF (\<Union>f\<in>Y. TER f)"
[PROOF STATE]
proof (prove)
using this:
z \<in> RF (TER f)

goal (1 subgoal):
 1. z \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
by(rule in_roofed_mono)(auto intro: fY)
[PROOF STATE]
proof (state)
this:
z \<in> RF (\<Union> (TER ` Y))

goal (2 subgoals):
 1. \<exists>f\<in>Y. z \<in> RF (TER f) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
 2. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> set (x # p)
z \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> set (x # p)
z \<in> RF (\<Union> (TER ` Y))

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

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>f\<in>Y. z \<in> RF (TER f))

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
hence *: "d_IN f z = 0" if "f \<in> Y" for f
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>f\<in>Y. z \<in> RF (TER f))

goal (1 subgoal):
 1. d_IN f z = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>f\<in>Y. z \<in> RF (TER f))
f \<in> Y

goal (1 subgoal):
 1. d_IN f z = 0
[PROOF STEP]
by(auto intro: wave_not_RF_IN_zero[OF f w])
[PROOF STATE]
proof (state)
this:
?f \<in> Y \<Longrightarrow> d_IN ?f z = 0

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
hence "d_IN (Sup Y) z = 0"
[PROOF STATE]
proof (prove)
using this:
?f \<in> Y \<Longrightarrow> d_IN ?f z = 0

goal (1 subgoal):
 1. d_IN (\<Squnion> Y) z = 0
[PROOF STEP]
using Y(2)
[PROOF STATE]
proof (prove)
using this:
?f \<in> Y \<Longrightarrow> d_IN ?f z = 0
Y \<noteq> {}

goal (1 subgoal):
 1. d_IN (\<Squnion> Y) z = 0
[PROOF STEP]
by(simp add: d_IN_Sup[OF Y])
[PROOF STATE]
proof (state)
this:
d_IN (\<Squnion> Y) z = 0

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
with TER
[PROOF STATE]
proof (chain)
picking this:
z \<in> TER (\<Squnion> Y)
d_IN (\<Squnion> Y) z = 0
[PROOF STEP]
have "z \<in> SAT \<Gamma> f"
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (\<Squnion> Y)
d_IN (\<Squnion> Y) z = 0

goal (1 subgoal):
 1. z \<in> SAT \<Gamma> f
[PROOF STEP]
using *[OF y]
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (\<Squnion> Y)
d_IN (\<Squnion> Y) z = 0
d_IN f z = 0

goal (1 subgoal):
 1. z \<in> SAT \<Gamma> f
[PROOF STEP]
by(simp add: SAT.simps)
[PROOF STATE]
proof (state)
this:
z \<in> SAT \<Gamma> f

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
with SINK[OF y]
[PROOF STATE]
proof (chain)
picking this:
z \<in> SINK f
z \<in> SAT \<Gamma> f
[PROOF STEP]
have "z \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
z \<in> SINK f
z \<in> SAT \<Gamma> f

goal (1 subgoal):
 1. z \<in> TER f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> TER f

goal (1 subgoal):
 1. \<not> (\<exists>f\<in>Y. z \<in> RF (TER f)) \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
with z y
[PROOF STATE]
proof (chain)
picking this:
z \<in> set (x # p)
f \<in> Y
z \<in> TER f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> set (x # p)
f \<in> Y
z \<in> TER f

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
by(auto intro: roofed_greaterI)
[PROOF STATE]
proof (state)
this:
(\<exists>z\<in>set p. z \<in> RF (\<Union> (TER ` Y))) \<or> x \<in> RF (\<Union> (TER ` Y))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> RF (RF (\<Union> (TER ` Y)))

goal (2 subgoals):
 1. \<And>x. x \<in> RF (TER (\<Squnion> Y)) \<Longrightarrow> x \<in> RF (\<Union> (TER ` Y))
 2. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> RF (RF (\<Union> (TER ` Y)))
[PROOF STEP]
show "x \<in> RF (\<Union>f\<in>Y. TER f)"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (RF (\<Union> (TER ` Y)))

goal (1 subgoal):
 1. x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
unfolding roofed_idem
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (\<Union> (TER ` Y))

goal (1 subgoal):
 1. x \<in> RF (\<Union> (TER ` Y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> RF (\<Union> (TER ` Y))

goal (1 subgoal):
 1. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
assume x: "x \<in> RF (\<Union>f\<in>Y. TER f)"
[PROOF STATE]
proof (state)
this:
x \<in> RF (\<Union> (TER ` Y))

goal (1 subgoal):
 1. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
have "x \<in> RF (RF (TER (\<Squnion>Y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> RF (RF (TER (\<Squnion> Y)))
[PROOF STEP]
proof(rule roofedI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
fix p y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
assume p: "path \<Gamma> x p y" and y: "y \<in> B \<Gamma>"
[PROOF STATE]
proof (state)
this:
path \<Gamma> x p y
y \<in> B \<Gamma>

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
from roofedD[OF x p y]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>z\<in>set p. z \<in> \<Union> (TER ` Y)) \<or> x \<in> \<Union> (TER ` Y)
[PROOF STEP]
obtain z f where *: "z \<in> set (x # p)"
      and **: "f \<in> Y" and TER: "z \<in> TER f"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z\<in>set p. z \<in> \<Union> (TER ` Y)) \<or> x \<in> \<Union> (TER ` Y)

goal (1 subgoal):
 1. (\<And>z f. \<lbrakk>z \<in> set (x # p); f \<in> Y; z \<in> TER f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> set (x # p)
f \<in> Y
z \<in> TER f

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
have "z \<in> RF (TER (Sup Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
assume z: "z \<notin> RF (TER (Sup Y))"
[PROOF STATE]
proof (state)
this:
z \<notin> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
have "wave \<Gamma> (Sup Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wave \<Gamma> (\<Squnion> Y)
[PROOF STEP]
using Y(1-2) w Y(3)
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y
Y \<noteq> {}
?f \<in> Y \<Longrightarrow> wave \<Gamma> ?f
countable (support_flow (\<Squnion> Y))

goal (1 subgoal):
 1. wave \<Gamma> (\<Squnion> Y)
[PROOF STEP]
by(rule wave_lub)
[PROOF STATE]
proof (state)
this:
wave \<Gamma> (\<Squnion> Y)

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
hence "d_OUT (Sup Y) z = 0"
[PROOF STATE]
proof (prove)
using this:
wave \<Gamma> (\<Squnion> Y)

goal (1 subgoal):
 1. d_OUT (\<Squnion> Y) z = 0
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
wave \<Gamma> (\<Squnion> Y)
z \<notin> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. d_OUT (\<Squnion> Y) z = 0
[PROOF STEP]
by(rule waveD_OUT)
[PROOF STATE]
proof (state)
this:
d_OUT (\<Squnion> Y) z = 0

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
hence "z \<in> SINK (Sup Y)"
[PROOF STATE]
proof (prove)
using this:
d_OUT (\<Squnion> Y) z = 0

goal (1 subgoal):
 1. z \<in> SINK (\<Squnion> Y)
[PROOF STEP]
by(simp add: SINK.simps)
[PROOF STATE]
proof (state)
this:
z \<in> SINK (\<Squnion> Y)

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<in> SINK (\<Squnion> Y)

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
have "z \<in> SAT \<Gamma> (Sup Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> SAT \<Gamma> (\<Squnion> Y)
[PROOF STEP]
using TER SAT_Sup_upper[OF **, of \<Gamma>]
[PROOF STATE]
proof (prove)
using this:
z \<in> TER f
SAT \<Gamma> f \<subseteq> SAT \<Gamma> (\<Squnion> Y)

goal (1 subgoal):
 1. z \<in> SAT \<Gamma> (\<Squnion> Y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> SAT \<Gamma> (\<Squnion> Y)

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z \<in> SINK (\<Squnion> Y)
z \<in> SAT \<Gamma> (\<Squnion> Y)
[PROOF STEP]
have "z \<in> TER (Sup Y)"
[PROOF STATE]
proof (prove)
using this:
z \<in> SINK (\<Squnion> Y)
z \<in> SAT \<Gamma> (\<Squnion> Y)

goal (1 subgoal):
 1. z \<in> TER (\<Squnion> Y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> TER (\<Squnion> Y)

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
hence "z \<in> RF (TER (Sup Y))"
[PROOF STATE]
proof (prove)
using this:
z \<in> TER (\<Squnion> Y)

goal (1 subgoal):
 1. z \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
by(rule roofed_greaterI)
[PROOF STATE]
proof (state)
this:
z \<in> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. z \<notin> RF (TER (\<Squnion> Y)) \<Longrightarrow> False
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<notin> RF (TER (\<Squnion> Y))
z \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
z \<notin> RF (TER (\<Squnion> Y))
z \<in> RF (TER (\<Squnion> Y))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. \<And>p y. \<lbrakk>path \<Gamma> x p y; y \<in> B \<Gamma>\<rbrakk> \<Longrightarrow> (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
thus "(\<exists>z\<in>set p. z \<in> RF (TER (Sup Y))) \<or> x \<in> RF (TER (Sup Y))"
[PROOF STATE]
proof (prove)
using this:
z \<in> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. (\<exists>z\<in>set p. z \<in> RF (TER (\<Squnion> Y))) \<or> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
z \<in> RF (TER (\<Squnion> Y))
z \<in> set (x # p)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> RF (RF (TER (\<Squnion> Y)))

goal (1 subgoal):
 1. \<And>x. x \<in> RF (\<Union> (TER ` Y)) \<Longrightarrow> x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> RF (RF (TER (\<Squnion> Y)))
[PROOF STEP]
show "x \<in> RF (TER (\<Squnion>Y))"
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (RF (TER (\<Squnion> Y)))

goal (1 subgoal):
 1. x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
unfolding roofed_idem
[PROOF STATE]
proof (prove)
using this:
x \<in> RF (TER (\<Squnion> Y))

goal (1 subgoal):
 1. x \<in> RF (TER (\<Squnion> Y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> RF (TER (\<Squnion> Y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma u_A: "x \<in> A \<Gamma> \<Longrightarrow> u x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Gamma> \<Longrightarrow> u x = 0
[PROOF STEP]
using u_outside[of x] disjoint
[PROOF STATE]
proof (prove)
using this:
x \<notin> B \<Gamma> \<Longrightarrow> u x = 0
A \<Gamma> \<inter> B \<Gamma> = {}

goal (1 subgoal):
 1. x \<in> A \<Gamma> \<Longrightarrow> u x = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma u_finite: "u y \<noteq> \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y \<noteq> \<top>
[PROOF STEP]
proof(cases "y \<in> B \<Gamma>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
 2. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> B \<Gamma>

goal (2 subgoals):
 1. y \<in> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
 2. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
have "u y \<le> \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y \<le> \<epsilon>
[PROOF STEP]
unfolding \<epsilon>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u y \<le> integral\<^sup>N (count_space (B \<Gamma>)) u
[PROOF STEP]
by(rule nn_integral_ge_point)(simp add: True)
[PROOF STATE]
proof (state)
this:
u y \<le> \<epsilon>

goal (2 subgoals):
 1. y \<in> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
 2. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u y \<le> \<epsilon>

goal (2 subgoals):
 1. y \<in> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
 2. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
have "\<dots> < \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> < \<top>
[PROOF STEP]
using finite_\<epsilon>
[PROOF STATE]
proof (prove)
using this:
\<epsilon> \<noteq> \<top>

goal (1 subgoal):
 1. \<epsilon> < \<top>
[PROOF STEP]
by (simp add: less_top[symmetric])
[PROOF STATE]
proof (state)
this:
\<epsilon> < \<top>

goal (2 subgoals):
 1. y \<in> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
 2. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u y < \<top>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u y < \<top>

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

goal (1 subgoal):
 1. y \<notin> B \<Gamma> \<Longrightarrow> u y \<noteq> \<top>
[PROOF STEP]
qed(simp add: u_outside)