[STATEMENT]
lemma infinite_reward:
  fixes s F
  defines "N \<equiv> Prob0 S (svalid F)" (is "_ \<equiv> Prob0 S ?F")
  defines "Y \<equiv> Prob1 N S (svalid F)"
  assumes s: "s \<in> S" "s \<notin> Y"
  shows "(\<integral>\<^sup>+\<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
assume "(AE \<omega> in T s. ev (HLD ?F) \<omega>)"
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (ev (HLD (svalid F)))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
with AE_T_enabled
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (T ?s) (enabled ?s)
almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
have "(AE \<omega> in T s. (HLD S suntil HLD ?F) \<omega>)"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T ?s) (enabled ?s)
almost_everywhere (T s) (ev (HLD (svalid F)))

goal (1 subgoal):
 1. almost_everywhere (T s) (HLD S suntil HLD (svalid F))
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>enabled s \<omega>; ev (HLD (svalid F)) \<omega>\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>enabled s \<omega>; ev (HLD (svalid F)) \<omega>\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
assume "ev (HLD ?F) \<omega>" "enabled s \<omega>"
[PROOF STATE]
proof (state)
this:
ev (HLD (svalid F)) \<omega>
enabled s \<omega>

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>enabled s \<omega>; ev (HLD (svalid F)) \<omega>\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
from this \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
ev (HLD (svalid F)) \<omega>
enabled s \<omega>
s \<in> S
[PROOF STEP]
show "(HLD S suntil HLD ?F) \<omega>"
[PROOF STATE]
proof (prove)
using this:
ev (HLD (svalid F)) \<omega>
enabled s \<omega>
s \<in> S

goal (1 subgoal):
 1. (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
proof (induction arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs s. \<lbrakk>HLD (svalid F) xs; enabled s xs; s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) xs
 2. \<And>xs s. \<lbrakk>ev (HLD (svalid F)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) (stl xs); enabled s xs; s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) xs
[PROOF STEP]
case (step \<omega>)
[PROOF STATE]
proof (state)
this:
ev (HLD (svalid F)) (stl \<omega>)
\<lbrakk>enabled ?s1 (stl \<omega>); ?s1 \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) (stl \<omega>)
enabled s \<omega>
s \<in> S

goal (2 subgoals):
 1. \<And>xs s. \<lbrakk>HLD (svalid F) xs; enabled s xs; s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) xs
 2. \<And>xs s. \<lbrakk>ev (HLD (svalid F)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) (stl xs); enabled s xs; s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
using E_closed step.IH[of "shd \<omega>"] step.prems
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
\<lbrakk>enabled (shd \<omega>) (stl \<omega>); shd \<omega> \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) (stl \<omega>)
enabled s \<omega>
s \<in> S

goal (1 subgoal):
 1. (HLD S suntil HLD (svalid F)) \<omega>
[PROOF STEP]
by (auto simp: subset_eq enabled.simps[of s] suntil.simps[of _ _ \<omega>] HLD_iff)
[PROOF STATE]
proof (state)
this:
(HLD S suntil HLD (svalid F)) \<omega>

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>HLD (svalid F) xs; enabled s xs; s \<in> S\<rbrakk> \<Longrightarrow> (HLD S suntil HLD (svalid F)) xs
[PROOF STEP]
qed (auto intro: suntil.intros)
[PROOF STATE]
proof (state)
this:
(HLD S suntil HLD (svalid F)) \<omega>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (HLD S suntil HLD (svalid F))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (ev (HLD (svalid F))) \<Longrightarrow> almost_everywhere (T s) (HLD S suntil HLD (svalid F))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (ev (HLD (svalid F))) \<Longrightarrow> almost_everywhere (T s) (HLD S suntil HLD (svalid F))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
have "\<not> (AE \<omega> in T s. (HLD S suntil HLD ?F) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
using s svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> Y
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. \<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
unfolding N_def Y_def
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> Prob1 (Prob0 S (svalid F)) S (svalid F)
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. \<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
by (simp add: Prob1_iff)
[PROOF STATE]
proof (state)
this:
\<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (T s) (ev (HLD (svalid F))) \<Longrightarrow> almost_everywhere (T s) (HLD S suntil HLD (svalid F))
\<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
have *: "\<not> (AE \<omega> in T s. ev (HLD ?F) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T s) (ev (HLD (svalid F))) \<Longrightarrow> almost_everywhere (T s) (HLD S suntil HLD (svalid F))
\<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))

goal (1 subgoal):
 1. \<not> (AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T s) (ev (HLD (svalid F))) \<Longrightarrow> almost_everywhere (T s) (HLD S suntil HLD (svalid F))
\<not> (AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>))
s \<in> S

goal (1 subgoal):
 1. \<not> (AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>))
[PROOF STEP]
by (cases "s \<in> ?F") (auto simp add: suntil_Stream ev_Stream)
[PROOF STATE]
proof (state)
this:
\<not> (AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>))

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
from nn_integral_PInf_AE[OF _ this] \<open>s\<in>S\<close>
[PROOF STATE]
proof (chain)
picking this:
T.random_variable s borel (\<lambda>\<omega>. reward (Future F) (s ## \<omega>)) \<Longrightarrow> AE x in T s. reward (Future F) (s ## x) \<noteq> \<infinity>
s \<in> S
[PROOF STEP]
have "AE \<omega> in T s. ev (HLD ?F) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
T.random_variable s borel (\<lambda>\<omega>. reward (Future F) (s ## \<omega>)) \<Longrightarrow> AE x in T s. reward (Future F) (s ## x) \<noteq> \<infinity>
s \<in> S

goal (1 subgoal):
 1. AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
by (simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>)

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<not> (AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>))
AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> (AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>))
AE \<omega> in T s. ev (HLD (svalid F)) (s ## \<omega>)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma existence_of_ExpFuture:
  fixes s F
  assumes N_def: "N \<equiv> Prob0 S (svalid F)" (is "_ \<equiv> Prob0 S ?F")
  assumes Y_def: "Y \<equiv> Prob1 N S (svalid F)"
  assumes s: "s \<in> S" "s \<notin> S - (Y - ?F)"
  shows "enn2real (\<integral>\<^sup>+\<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) =
    (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+\<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
let ?R = "reward (Future F)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<notin> S - (Y - svalid F)
[PROOF STEP]
have "s \<in> Prob1 (Prob0 S ?F) S ?F"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (1 subgoal):
 1. s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)
[PROOF STEP]
unfolding Y_def N_def
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> S - (Prob1 (Prob0 S (svalid F)) S (svalid F) - svalid F)

goal (1 subgoal):
 1. s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)
[PROOF STEP]
have AE_until: "AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)

goal (1 subgoal):
 1. AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
using Prob1_iff[of S ?F] svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
s \<in> Prob1 (Prob0 S (svalid F)) S (svalid F)
\<lbrakk>S \<subseteq> S; svalid F \<subseteq> S\<rbrakk> \<Longrightarrow> Prob1 (Prob0 S (svalid F)) S (svalid F) = {s \<in> S. AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)}
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<notin> S - (Y - svalid F)
[PROOF STEP]
have "s \<notin> ?F"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (1 subgoal):
 1. s \<notin> svalid F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<notin> svalid F

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
let ?E = "\<lambda>s'. \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
have *: "(\<Sum>s'\<in>S. \<tau> s s' * ?E s') = (\<Sum>s'\<in>S. ennreal (\<tau> s s' * enn2real (?E s')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s') = (\<Sum>s'\<in>S. ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s')))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> ennreal (\<tau> s x) * \<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x = ennreal (\<tau> s x * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x))
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> ennreal (\<tau> s x) * \<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x = ennreal (\<tau> s x * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x))
[PROOF STEP]
assume "s' \<in> S"
[PROOF STATE]
proof (state)
this:
s' \<in> S

goal (2 subgoals):
 1. S = S
 2. \<And>x. x \<in> S \<Longrightarrow> ennreal (\<tau> s x) * \<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x = ennreal (\<tau> s x * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (x ## \<omega>) \<partial>T x))
[PROOF STEP]
show "\<tau> s s' * ?E s' = ennreal (\<tau> s s' * enn2real (?E s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 2. \<not> ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
assume "\<tau> s s' \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<tau> s s' \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 2. \<not> ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
with \<open>s \<in> S\<close> \<open>s' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s' \<in> S
\<tau> s s' \<noteq> 0
[PROOF STEP]
have "s' \<in> E s"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s' \<in> S
\<tau> s s' \<noteq> 0

goal (1 subgoal):
 1. s' \<in> E s
[PROOF STEP]
by (simp add: set_pmf_iff)
[PROOF STATE]
proof (state)
this:
s' \<in> E s

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 2. \<not> ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
from \<open>s \<notin> ?F\<close> AE_until
[PROOF STATE]
proof (chain)
picking this:
s \<notin> svalid F
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
have "AE \<omega> in T s. (HLD S suntil HLD ?F) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid F
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)

goal (1 subgoal):
 1. AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
using svalid_subset_S \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid F
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
svalid ?F \<subseteq> S
s \<in> S

goal (1 subgoal):
 1. AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 2. \<not> ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
with nn_integral_reward_finite[OF \<open>s' \<in> S\<close>, of F] \<open>s \<in> S\<close> \<open>s' \<in> E s\<close> \<open>s \<notin> ?F\<close>
[PROOF STATE]
proof (chain)
picking this:
AE \<omega> in T s'. (HLD S suntil HLD (svalid F)) (s' ## \<omega>) \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>
s \<in> S
s' \<in> E s
s \<notin> svalid F
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)
[PROOF STEP]
have "?E s' \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in T s'. (HLD S suntil HLD (svalid F)) (s' ## \<omega>) \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>
s \<in> S
s' \<in> E s
s \<notin> svalid F
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>
[PROOF STEP]
by (simp add: AE_T_iff[of _ s] AE_measure_pmf_iff suntil_Stream
                 del: reward.simps)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 2. \<not> ?P \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' \<noteq> \<infinity>

goal (1 subgoal):
 1. ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
by (cases "?E s'") (auto simp: ennreal_mult)
[PROOF STATE]
proof (state)
this:
ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))

goal (1 subgoal):
 1. \<not> \<tau> s s' \<noteq> 0 \<Longrightarrow> ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s' = ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))

goal (1 subgoal):
 1. S = S
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. ennreal (\<tau> s s') * \<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s') = (\<Sum>s'\<in>S. ennreal (\<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s')))

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
have "AE \<omega> in T s. ?R (s ## \<omega>) = \<rho> s + \<iota> s (shd \<omega>) + ?R \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE \<omega> in T s. reward (Future F) (s ## \<omega>) = ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega>
[PROOF STEP]
using \<open>s \<notin> svalid F\<close>
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid F

goal (1 subgoal):
 1. AE \<omega> in T s. reward (Future F) (s ## \<omega>) = ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega>
[PROOF STEP]
by (auto simp: ev_Stream )
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. reward (Future F) (s ## \<omega>) = ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega>

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE \<omega> in T s. reward (Future F) (s ## \<omega>) = ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega>
[PROOF STEP]
have "(\<integral>\<^sup>+\<omega>. ?R (s ## \<omega>) \<partial>T s) = (\<integral>\<^sup>+\<omega>. (\<rho> s + \<iota> s (shd \<omega>)) + ?R \<omega> \<partial>T s)"
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in T s. reward (Future F) (s ## \<omega>) = ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega>

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s
[PROOF STEP]
by (rule nn_integral_cong_AE)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+\<omega>. \<rho> s + \<iota> s (shd \<omega>) \<partial>T s) +
    (\<integral>\<^sup>+\<omega>. ?R \<omega> \<partial>T s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s = \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F))
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s = \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F))
[PROOF STEP]
by (subst nn_integral_add)
       (auto simp add: space_PiM PiE_iff simp del: reward.simps)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s = \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F))

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. ennreal (\<rho> s + \<iota> s (shd \<omega>)) + reward (Future F) \<omega> \<partial>T s = \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F))

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
have "\<dots> = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + (\<integral>\<^sup>+\<omega>. ?R \<omega> \<partial>T s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F)) = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F)) = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))
[PROOF STEP]
by (subst nn_integral_eq_sum)
       (auto simp: field_simps sum.distrib sum_distrib_left[symmetric] ennreal_mult[symmetric] sum_nonneg)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (\<rho> s + \<iota> s (shd x)) \<partial>T s + integral\<^sup>N (T s) (reward (Future F)) = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
apply (simp del: reward.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F)) \<Longrightarrow> enn2real (ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F))) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
apply (subst nn_integral_eq_sum[OF \<open>s \<in> S\<close> reward_measurable])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + integral\<^sup>N (T s) (reward (Future F)) \<Longrightarrow> enn2real (ennreal (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) + (\<Sum>t\<in>S. ennreal (\<tau> s t) * \<integral>\<^sup>+ x. reward (Future F) (t ## x) \<partial>T t)) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
apply (simp del: reward.simps ennreal_plus add: * ennreal_plus[symmetric] sum_nonneg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uniqueness_of_ExpFuture:
  fixes F
  assumes N_def: "N \<equiv> Prob0 S (svalid F)" (is "_ \<equiv> Prob0 S ?F")
  assumes Y_def: "Y \<equiv> Prob1 N S (svalid F)"
  assumes const_def: "const \<equiv> \<lambda>s. if s \<in> Y \<and> s \<notin> svalid F then - \<rho> s - (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s') else 0"
  assumes sol: "\<And>s. s\<in>S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> ?F) s s' * l s') = const s"
  shows "\<forall>s\<in>S. l s = enn2real (\<integral>\<^sup>+\<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)"
    (is "\<forall>s\<in>S. l s = enn2real (\<integral>\<^sup>+\<omega>. ?R (s ## \<omega>) \<partial>T s)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
proof (rule unique)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. ?\<Phi> \<subseteq> S
 2. ?\<Psi> \<subseteq> S
 3. ?N \<subseteq> S
 4. Prob0 ?\<Phi> ?\<Psi> \<subseteq> ?N
 5. ?\<Psi> \<subseteq> ?N
 6. \<And>s. \<lbrakk>s \<in> S; s \<notin> ?N\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 7. \<And>s. \<lbrakk>s \<in> S; s \<notin> ?N\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 8. \<And>s. s \<in> ?N \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
show "S \<subseteq> S" "?F \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> S &&& svalid F \<subseteq> S
[PROOF STEP]
using svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. S \<subseteq> S &&& svalid F \<subseteq> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subseteq> S
svalid F \<subseteq> S

goal (6 subgoals):
 1. ?N \<subseteq> S
 2. Prob0 S (svalid F) \<subseteq> ?N
 3. svalid F \<subseteq> ?N
 4. \<And>s. \<lbrakk>s \<in> S; s \<notin> ?N\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 5. \<And>s. \<lbrakk>s \<in> S; s \<notin> ?N\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 6. \<And>s. s \<in> ?N \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
show "S - (Y - ?F) \<subseteq> S" "Prob0 S ?F \<subseteq> S - (Y - ?F)" "?F \<subseteq> S - (Y - ?F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - (Y - svalid F) \<subseteq> S &&& Prob0 S (svalid F) \<subseteq> S - (Y - svalid F) &&& svalid F \<subseteq> S - (Y - svalid F)
[PROOF STEP]
using svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. S - (Y - svalid F) \<subseteq> S &&& Prob0 S (svalid F) \<subseteq> S - (Y - svalid F) &&& svalid F \<subseteq> S - (Y - svalid F)
[PROOF STEP]
by (auto simp add: Y_def N_def Prob1_iff)
       (auto simp add: Prob0_iff dest!: T.AE_contr)
[PROOF STATE]
proof (state)
this:
S - (Y - svalid F) \<subseteq> S
Prob0 S (svalid F) \<subseteq> S - (Y - svalid F)
svalid F \<subseteq> S - (Y - svalid F)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 3. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 3. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 3. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
assume "s \<in> S" "s \<notin> S - (Y - ?F)"
[PROOF STATE]
proof (state)
this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
 3. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<notin> S - (Y - svalid F)
[PROOF STEP]
show "enn2real (\<integral>\<^sup>+\<omega>. ?R (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) =
    (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+\<omega>. ?R (s' ## \<omega>) \<partial>T s'))"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
by (rule existence_of_ExpFuture[OF N_def Y_def])
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s' ## \<omega>) \<partial>T s'))

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
assume "s \<in> S" "s \<notin> S - (Y - ?F)"
[PROOF STATE]
proof (state)
this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<notin> S - (Y - svalid F)
[PROOF STEP]
have "s \<in> Y" "s \<notin> ?F"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> S - (Y - svalid F)

goal (1 subgoal):
 1. s \<in> Y &&& s \<notin> svalid F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> Y
s \<notin> svalid F

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
have "(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') =
    (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s')
[PROOF STEP]
by (auto intro!: sum.cong simp: field_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s')

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s')

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
have "\<dots> = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s
[PROOF STEP]
by (simp add: sum_subtractf single_l)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. \<tau> s s' * l s' - (if s' = s then 1 else 0) * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s
[PROOF STEP]
have "l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s') = (\<Sum>s'\<in>S. \<tau> s s' * l s') - l s

goal (1 subgoal):
 1. l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> S - (Y - svalid F)\<rbrakk> \<Longrightarrow> l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')
[PROOF STEP]
show "l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')"
[PROOF STATE]
proof (prove)
using this:
l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')

goal (1 subgoal):
 1. l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
[PROOF STEP]
using sol[OF \<open>s \<in> S\<close>] \<open>s \<in> Y\<close> \<open>s \<notin> ?F\<close>
[PROOF STATE]
proof (prove)
using this:
l s = (\<Sum>s'\<in>S. \<tau> s s' * l s') - (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * l s')
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid F) s s' * l s') = const s
s \<in> Y
s \<notin> svalid F

goal (1 subgoal):
 1. l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')
[PROOF STEP]
by (simp add: const_def LES_def)
[PROOF STATE]
proof (state)
this:
l s - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * l s')

goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
assume s: "s \<in> S - (Y - ?F)"
[PROOF STATE]
proof (state)
this:
s \<in> S - (Y - svalid F)

goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
with sol[of s]
[PROOF STATE]
proof (chain)
picking this:
s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid F) s s' * l s') = const s
s \<in> S - (Y - svalid F)
[PROOF STEP]
have "l s = 0"
[PROOF STATE]
proof (prove)
using this:
s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid F) s s' * l s') = const s
s \<in> S - (Y - svalid F)

goal (1 subgoal):
 1. l s = 0
[PROOF STEP]
by (cases "s \<in> ?F") (simp_all add: const_def LES_def single_l)
[PROOF STATE]
proof (state)
this:
l s = 0

goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l s = 0

goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
have "0 = enn2real (\<integral>\<^sup>+\<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
 2. \<not> ?P \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
assume "s \<in> ?F"
[PROOF STATE]
proof (state)
this:
s \<in> svalid F

goal (2 subgoals):
 1. ?P \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
 2. \<not> ?P \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> svalid F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> svalid F

goal (1 subgoal):
 1. 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
by (simp add: HLD_iff ev_Stream)
[PROOF STATE]
proof (state)
this:
0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)

goal (1 subgoal):
 1. s \<notin> svalid F \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> svalid F \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
assume "s \<notin> ?F"
[PROOF STATE]
proof (state)
this:
s \<notin> svalid F

goal (1 subgoal):
 1. s \<notin> svalid F \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
with s
[PROOF STATE]
proof (chain)
picking this:
s \<in> S - (Y - svalid F)
s \<notin> svalid F
[PROOF STEP]
have "s \<in> S - Y"
[PROOF STATE]
proof (prove)
using this:
s \<in> S - (Y - svalid F)
s \<notin> svalid F

goal (1 subgoal):
 1. s \<in> S - Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> S - Y

goal (1 subgoal):
 1. s \<notin> svalid F \<Longrightarrow> 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
with infinite_reward[of s F]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>s \<in> S; s \<notin> Prob1 (Prob0 S (svalid F)) S (svalid F)\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
s \<in> S - Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s \<in> S; s \<notin> Prob1 (Prob0 S (svalid F)) S (svalid F)\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = \<infinity>
s \<in> S - Y

goal (1 subgoal):
 1. 0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
by (simp add: Y_def N_def del: reward.simps)
[PROOF STATE]
proof (state)
this:
0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)

goal (1 subgoal):
 1. \<And>s. s \<in> S - (Y - svalid F) \<Longrightarrow> l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
show "l s = enn2real (\<integral>\<^sup>+\<omega>. ?R (s ## \<omega>) \<partial>T s)"
[PROOF STATE]
proof (prove)
using this:
l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)

goal (1 subgoal):
 1. l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l s = enn2real (\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s)

goal:
No subgoals!
[PROOF STEP]
qed