[STATEMENT]
lemma Prob1_iff:
  assumes "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S"
  shows "Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s\<in>S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}"
    (is "Prob1 ?P0 _ _ = {s\<in>S. ?pU s}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
note P0 = Prob0_iff_reachable[OF assms]
[PROOF STATE]
proof (state)
this:
Prob0 \<Phi> \<Psi> = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
have *: "\<Phi> - \<Psi> \<subseteq> S" "?P0 \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> - \<Psi> \<subseteq> S &&& Prob0 \<Phi> \<Psi> \<subseteq> S
[PROOF STEP]
using P0 assms
[PROOF STATE]
proof (prove)
using this:
Prob0 \<Phi> \<Psi> = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S

goal (1 subgoal):
 1. \<Phi> - \<Psi> \<subseteq> S &&& Prob0 \<Phi> \<Psi> \<subseteq> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Phi> - \<Psi> \<subseteq> S
Prob0 \<Phi> \<Psi> \<subseteq> S

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
have P0_subset: "S - \<Phi> - \<Psi> \<subseteq> ?P0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - \<Phi> - \<Psi> \<subseteq> Prob0 \<Phi> \<Psi>
[PROOF STEP]
unfolding P0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - \<Phi> - \<Psi> \<subseteq> {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
by (auto elim: converse_rtranclE)
[PROOF STATE]
proof (state)
this:
S - \<Phi> - \<Psi> \<subseteq> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
have "Prob1 ?P0 \<Phi> \<Psi> = {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> ?P0 = {}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}}
[PROOF STEP]
unfolding Prob0_iff_reachable[OF *] Prob1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}} = {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}}

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}}

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
have "\<dots> = {s\<in>S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}} = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
proof (intro Collect_cong conj_cong refl iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
assume s: "s \<in> S" "(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> ?P0 = {}"
[PROOF STATE]
proof (state)
this:
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
have "s \<notin> ?P0"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}

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

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
have "s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
s \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>
[PROOF STEP]
using P0_subset \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<notin> Prob0 \<Phi> \<Psi>
S - \<Phi> - \<Psi> \<subseteq> Prob0 \<Phi> \<Psi>
s \<in> S

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

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
assume "s \<in> \<Phi> - \<Psi>"
[PROOF STATE]
proof (state)
this:
s \<in> \<Phi> - \<Psi>

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
have "AE \<omega> in T s. ev (HLD (\<Psi> \<union> ?P0)) \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (T s) (ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)))
[PROOF STEP]
proof (rule AE_T_ev_HLD)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
assume s_t: "(s, t) \<in> acc_on (- (\<Psi> \<union> ?P0))"
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>*

goal (2 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
from \<open>s \<in> S\<close> s_t
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>*
[PROOF STEP]
have "t \<in> S"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>*

goal (1 subgoal):
 1. t \<in> S
[PROOF STEP]
by (rule E_rtrancl_closed) auto
[PROOF STATE]
proof (state)
this:
t \<in> S

goal (2 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
show "\<exists>t'\<in>\<Psi> \<union> ?P0. (t, t') \<in> acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. \<not> ?P \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
assume "t \<in> ?P0"
[PROOF STATE]
proof (state)
this:
t \<in> Prob0 \<Phi> \<Psi>

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
 2. \<not> ?P \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> Prob0 \<Phi> \<Psi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<in> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*

goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi> \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi> \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
assume "t \<notin> ?P0"
[PROOF STATE]
proof (state)
this:
t \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi> \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
with \<open>t\<in>S\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> S
t \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
obtain s where t_s: "(t, s) \<in> (SIGMA x:\<Phi>. E x)\<^sup>*" and "s \<in> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
t \<in> S
t \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>(t, s) \<in> (Sigma \<Phi> E)\<^sup>*; s \<in> \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding P0
[PROOF STATE]
proof (prove)
using this:
t \<in> S
t \<notin> {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>(t, s) \<in> (Sigma \<Phi> E)\<^sup>*; s \<in> \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(t, s) \<in> (Sigma \<Phi> E)\<^sup>*
s \<in> \<Psi>

goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi> \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
from t_s
[PROOF STATE]
proof (chain)
picking this:
(t, s) \<in> (Sigma \<Phi> E)\<^sup>*
[PROOF STEP]
have "(t, s) \<in> acc"
[PROOF STATE]
proof (prove)
using this:
(t, s) \<in> (Sigma \<Phi> E)\<^sup>*

goal (1 subgoal):
 1. (t, s) \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
by (rule rev_subsetD) (intro rtrancl_mono Sigma_mono, auto)
[PROOF STATE]
proof (state)
this:
(t, s) \<in> (Sigma UNIV E)\<^sup>*

goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi> \<Longrightarrow> \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
with \<open>s \<in> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<Psi>
(t, s) \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> \<Psi>
(t, s) \<in> (Sigma UNIV E)\<^sup>*

goal (1 subgoal):
 1. \<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t'\<in>\<Psi> \<union> Prob0 \<Phi> \<Psi>. (t, t') \<in> (Sigma UNIV E)\<^sup>*

goal (1 subgoal):
 1. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
have "acc_on (- (\<Psi> \<union> ?P0)) `` {s} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. (SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
by (auto intro: E_rtrancl_closed)
[PROOF STATE]
proof (state)
this:
(SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S

goal (1 subgoal):
 1. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
show "finite (acc_on (- (\<Psi> \<union> ?P0)) `` {s})"
[PROOF STATE]
proof (prove)
using this:
(SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S

goal (1 subgoal):
 1. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
using finite_S
[PROOF STATE]
proof (prove)
using this:
(SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s} \<subseteq> S
finite S

goal (1 subgoal):
 1. finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})
[PROOF STEP]
by (auto dest: finite_subset)
[PROOF STATE]
proof (state)
this:
finite ((SIGMA s:UNIV. E s \<inter> - (\<Psi> \<union> Prob0 \<Phi> \<Psi>))\<^sup>* `` {s})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)))

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (T s) (ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)))
[PROOF STEP]
have "AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) \<omega>"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T s) (ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)))

goal (1 subgoal):
 1. almost_everywhere (T s) (HLD \<Phi> suntil HLD \<Psi>)
[PROOF STEP]
using AE_T_enabled
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T s) (ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)))
almost_everywhere (T ?s) (enabled ?s)

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

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) \<omega>; enabled s \<omega>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) \<omega>
[PROOF STEP]
from this s \<open>s \<in> \<Phi> - \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) \<omega>
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>
[PROOF STEP]
show "(HLD \<Phi> suntil HLD \<Psi>) \<omega>"
[PROOF STATE]
proof (prove)
using this:
ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) \<omega>
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. (HLD \<Phi> suntil HLD \<Psi>) \<omega>
[PROOF STEP]
proof (induction arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs s. \<lbrakk>HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>) xs; enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
 2. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
case (base \<omega>)
[PROOF STATE]
proof (state)
this:
HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>) \<omega>
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (2 subgoals):
 1. \<And>xs s. \<lbrakk>HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>) xs; enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
 2. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>) \<omega>
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>) \<omega>
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. (HLD \<Phi> suntil HLD \<Psi>) \<omega>
[PROOF STEP]
by (auto simp: HLD_iff enabled.simps[of s] intro: suntil.intros)
[PROOF STATE]
proof (state)
this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
case (step \<omega>)
[PROOF STATE]
proof (state)
this:
ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl \<omega>)
\<lbrakk>enabled ?s1 (stl \<omega>); ?s1 \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {?s1} \<inter> Prob0 \<Phi> \<Psi> = {}; ?s1 \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl \<omega>)
\<lbrakk>enabled ?s1 (stl \<omega>); ?s1 \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {?s1} \<inter> Prob0 \<Phi> \<Psi> = {}; ?s1 \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>
[PROOF STEP]
have "(s, shd \<omega>) \<in> (Sigma (\<Phi> - \<Psi>) E)"
[PROOF STATE]
proof (prove)
using this:
ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl \<omega>)
\<lbrakk>enabled ?s1 (stl \<omega>); ?s1 \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {?s1} \<inter> Prob0 \<Phi> \<Psi> = {}; ?s1 \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. (s, shd \<omega>) \<in> Sigma (\<Phi> - \<Psi>) E
[PROOF STEP]
by (auto simp: enabled.simps[of s])
[PROOF STATE]
proof (state)
this:
(s, shd \<omega>) \<in> Sigma (\<Phi> - \<Psi>) E

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, shd \<omega>) \<in> Sigma (\<Phi> - \<Psi>) E
[PROOF STEP]
have *: "(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> ?P0 = {}"
[PROOF STATE]
proof (prove)
using this:
(s, shd \<omega>) \<in> Sigma (\<Phi> - \<Psi>) E

goal (1 subgoal):
 1. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
using step.prems
[PROOF STATE]
proof (prove)
using this:
(s, shd \<omega>) \<in> Sigma (\<Phi> - \<Psi>) E
enabled s \<omega>
s \<in> S
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
s \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
by (auto intro: converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
have "shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi>" "shd \<omega> \<in> S"
[PROOF STATE]
proof (prove)
using this:
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}

goal (1 subgoal):
 1. shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi> &&& shd \<omega> \<in> S
[PROOF STEP]
using P0_subset step.prems(1,2) E_closed
[PROOF STATE]
proof (prove)
using this:
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {shd \<omega>} \<inter> Prob0 \<Phi> \<Psi> = {}
S - \<Phi> - \<Psi> \<subseteq> Prob0 \<Phi> \<Psi>
enabled s \<omega>
s \<in> S
\<Union> (E ` S) \<subseteq> S

goal (1 subgoal):
 1. shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi> &&& shd \<omega> \<in> S
[PROOF STEP]
by (auto simp add: enabled.simps[of s])
[PROOF STATE]
proof (state)
this:
shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi>
shd \<omega> \<in> S

goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>ev (HLD (\<Psi> \<union> Prob0 \<Phi> \<Psi>)) (stl xs); \<And>s. \<lbrakk>enabled s (stl xs); s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl xs); enabled s xs; s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}; s \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi>
shd \<omega> \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi>
shd \<omega> \<in> S

goal (1 subgoal):
 1. (HLD \<Phi> suntil HLD \<Psi>) \<omega>
[PROOF STEP]
using step.prems(1) step.IH[OF _ _ *] \<open>shd \<omega> \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
shd \<omega> \<in> \<Phi> - \<Psi> \<or> shd \<omega> \<in> \<Psi>
shd \<omega> \<in> S
enabled s \<omega>
\<lbrakk>enabled (shd \<omega>) (stl \<omega>); shd \<omega> \<in> S; shd \<omega> \<in> \<Phi> - \<Psi>\<rbrakk> \<Longrightarrow> (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
shd \<omega> \<in> S

goal (1 subgoal):
 1. (HLD \<Phi> suntil HLD \<Psi>) \<omega>
[PROOF STEP]
by (auto simp add: suntil.simps[of _ _ \<omega>] HLD_iff[abs_def] enabled.simps[of s \<omega>])
[PROOF STATE]
proof (state)
this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (HLD \<Phi> suntil HLD \<Psi>)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s \<in> \<Phi> - \<Psi> \<Longrightarrow> almost_everywhere (T s) (HLD \<Phi> suntil HLD \<Psi>)

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>
s \<in> \<Phi> - \<Psi> \<Longrightarrow> almost_everywhere (T s) (HLD \<Phi> suntil HLD \<Psi>)
[PROOF STEP]
show "AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<Phi> - \<Psi> \<or> s \<in> \<Psi>
s \<in> \<Phi> - \<Psi> \<Longrightarrow> almost_everywhere (T s) (HLD \<Phi> suntil HLD \<Psi>)

goal (1 subgoal):
 1. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
[PROOF STEP]
by (cases "s \<in> \<Phi> - \<Psi>") (auto simp add: suntil_Stream)
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
assume s: "s \<in> S" "AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)"
[PROOF STATE]
proof (state)
this:
s \<in> S
AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s \<in> S
AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
assume "(s, t) \<in> (SIGMA s:\<Phi>-\<Psi>. E s)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
from this \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*
s \<in> S
[PROOF STEP]
have "(AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S"
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*
s \<in> S

goal (1 subgoal):
 1. (AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> (AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)) \<and> s \<in> S
 2. \<And>y z. \<lbrakk>(s, y) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*; (y, z) \<in> Sigma (\<Phi> - \<Psi>) E; s \<in> S \<Longrightarrow> (AE \<omega> in T y. (HLD \<Phi> suntil HLD \<Psi>) (y ## \<omega>)) \<and> y \<in> S; s \<in> S\<rbrakk> \<Longrightarrow> (AE \<omega> in T z. (HLD \<Phi> suntil HLD \<Psi>) (z ## \<omega>)) \<and> z \<in> S
[PROOF STEP]
case (step t u)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*
(t, u) \<in> Sigma (\<Phi> - \<Psi>) E
s \<in> S \<Longrightarrow> (AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S
s \<in> S

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> (AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)) \<and> s \<in> S
 2. \<And>y z. \<lbrakk>(s, y) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*; (y, z) \<in> Sigma (\<Phi> - \<Psi>) E; s \<in> S \<Longrightarrow> (AE \<omega> in T y. (HLD \<Phi> suntil HLD \<Psi>) (y ## \<omega>)) \<and> y \<in> S; s \<in> S\<rbrakk> \<Longrightarrow> (AE \<omega> in T z. (HLD \<Phi> suntil HLD \<Psi>) (z ## \<omega>)) \<and> z \<in> S
[PROOF STEP]
with E_closed
[PROOF STATE]
proof (chain)
picking this:
\<Union> (E ` S) \<subseteq> S
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*
(t, u) \<in> Sigma (\<Phi> - \<Psi>) E
s \<in> S \<Longrightarrow> (AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S
s \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
(s, t) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>*
(t, u) \<in> Sigma (\<Phi> - \<Psi>) E
s \<in> S \<Longrightarrow> (AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S
s \<in> S

goal (1 subgoal):
 1. (AE \<omega> in T u. (HLD \<Phi> suntil HLD \<Psi>) (u ## \<omega>)) \<and> u \<in> S
[PROOF STEP]
by (auto simp add: AE_T_iff[of _ t] suntil_Stream)
[PROOF STATE]
proof (state)
this:
(AE \<omega> in T u. (HLD \<Phi> suntil HLD \<Psi>) (u ## \<omega>)) \<and> u \<in> S

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> (AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)) \<and> s \<in> S
[PROOF STEP]
qed (insert s, auto)
[PROOF STATE]
proof (state)
this:
(AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S
[PROOF STEP]
have "t \<notin> ?P0"
[PROOF STATE]
proof (prove)
using this:
(AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S

goal (1 subgoal):
 1. t \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
unfolding Prob0_iff[OF assms]
[PROOF STATE]
proof (prove)
using this:
(AE \<omega> in T t. (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>)) \<and> t \<in> S

goal (1 subgoal):
 1. t \<notin> {s \<in> S. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
by (auto dest: T.AE_contr)
[PROOF STATE]
proof (state)
this:
t \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(s, ?t3) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* \<Longrightarrow> ?t3 \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, ?t3) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* \<Longrightarrow> ?t3 \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
show "(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}"
[PROOF STATE]
proof (prove)
using this:
(s, ?t3) \<in> (Sigma (\<Phi> - \<Psi>) E)\<^sup>* \<Longrightarrow> ?t3 \<notin> Prob0 \<Phi> \<Psi>

goal (1 subgoal):
 1. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{s \<in> S. (Sigma (\<Phi> - \<Psi>) E)\<^sup>* `` {s} \<inter> Prob0 \<Phi> \<Psi> = {}} = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}

goal (1 subgoal):
 1. Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Prob1 (Prob0 \<Phi> \<Psi>) \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prob_sum:
  "s \<in> S \<Longrightarrow> Measurable.pred R.S P \<Longrightarrow> \<P>(\<omega> in T s. P \<omega>) = (\<Sum>t\<in>S. \<tau> s t * \<P>(\<omega> in T t. P (t ## \<omega>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> S; Measurable.pred (stream_space (count_space UNIV)) P\<rbrakk> \<Longrightarrow> prob s P = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. P (t ## \<omega>)))
[PROOF STEP]
unfolding prob_T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> S; Measurable.pred (stream_space (count_space UNIV)) P\<rbrakk> \<Longrightarrow> measure_pmf.expectation (K s) (\<lambda>t. prob t (\<lambda>\<omega>. P (t ## \<omega>))) = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. P (t ## \<omega>)))
[PROOF STEP]
using E_closed
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S

goal (1 subgoal):
 1. \<lbrakk>s \<in> S; Measurable.pred (stream_space (count_space UNIV)) P\<rbrakk> \<Longrightarrow> measure_pmf.expectation (K s) (\<lambda>t. prob t (\<lambda>\<omega>. P (t ## \<omega>))) = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. P (t ## \<omega>)))
[PROOF STEP]
by (subst integral_measure_pmf[OF finite_S]) (auto simp: mult.commute)


[STATEMENT]
lemma nn_integral_eq_sum:
  "s \<in> S \<Longrightarrow> f \<in> borel_measurable R.S \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>T s) = (\<Sum>t\<in>S. \<tau> s t * (\<integral>\<^sup>+x. f (t ## x) \<partial>T t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> S; f \<in> borel_measurable (stream_space (count_space UNIV))\<rbrakk> \<Longrightarrow> integral\<^sup>N (T s) f = (\<Sum>t\<in>S. ennreal (\<tau> s t) * \<integral>\<^sup>+ x. f (t ## x) \<partial>T t)
[PROOF STEP]
unfolding nn_integral_T
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> S; f \<in> borel_measurable (stream_space (count_space UNIV))\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ t. \<integral>\<^sup>+ \<omega>. f (t ## \<omega>) \<partial>T t \<partial>measure_pmf (K s) = (\<Sum>t\<in>S. ennreal (\<tau> s t) * \<integral>\<^sup>+ x. f (t ## x) \<partial>T t)
[PROOF STEP]
using E_closed
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S

goal (1 subgoal):
 1. \<lbrakk>s \<in> S; f \<in> borel_measurable (stream_space (count_space UNIV))\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ t. \<integral>\<^sup>+ \<omega>. f (t ## \<omega>) \<partial>T t \<partial>measure_pmf (K s) = (\<Sum>t\<in>S. ennreal (\<tau> s t) * \<integral>\<^sup>+ x. f (t ## x) \<partial>T t)
[PROOF STEP]
by (subst nn_integral_measure_pmf_support[OF finite_S])
     (auto simp: mult.commute)


[STATEMENT]
lemma emeasure_T_space[simp]: "emeasure (T s) (space R.S) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (T s) (space (stream_space (count_space UNIV))) = 1
[PROOF STEP]
using T.emeasure_space_1
[PROOF STATE]
proof (prove)
using this:
emeasure (T ?s) (space (T ?s)) = 1

goal (1 subgoal):
 1. emeasure (T s) (space (stream_space (count_space UNIV))) = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma \<tau>_distr[simp]: "s \<in> S \<Longrightarrow> (\<Sum>t\<in>S. \<tau> s t) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> sum (\<tau> s) S = 1
[PROOF STEP]
using prob_sum[of s "\<lambda>_. True"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s \<in> S; Measurable.pred (stream_space (count_space UNIV)) (\<lambda>_. True)\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. True) = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. True))

goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> sum (\<tau> s) S = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma ProbU:
  "q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = \<P>(\<omega> in T q. pvalid (U k F1 F2) (q ## \<omega>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>))
[PROOF STEP]
proof (induct k arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q. q \<in> S \<Longrightarrow> ProbU q 0 (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U 0 F1 F2) (q ## \<omega>))
 2. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
q \<in> S

goal (2 subgoals):
 1. \<And>q. q \<in> S \<Longrightarrow> ProbU q 0 (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U 0 F1 F2) (q ## \<omega>))
 2. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
with T.prob_space
[PROOF STATE]
proof (chain)
picking this:
T.prob ?s (space (T ?s)) = 1
q \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
T.prob ?s (space (T ?s)) = 1
q \<in> S

goal (1 subgoal):
 1. ProbU q 0 (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U 0 F1 F2) (q ## \<omega>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ProbU q 0 (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U 0 F1 F2) (q ## \<omega>))

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
?q1 \<in> S \<Longrightarrow> ProbU ?q1 k (svalid F1) (svalid F2) = prob ?q1 (\<lambda>\<omega>. pvalid (U k F1 F2) (?q1 ## \<omega>))
q \<in> S

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
have "\<P>(\<omega> in T q. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) =
    (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then
      \<Sum>t\<in>S. \<tau> q t * \<P>(\<omega> in T t. pvalid (U k F1 F2) (t ## \<omega>)) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0)
[PROOF STEP]
using \<open>q \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> S

goal (1 subgoal):
 1. prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0)
[PROOF STEP]
by (subst prob_sum) simp_all
[PROOF STATE]
proof (state)
this:
prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0)

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0)

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
have "\<dots> = ProbU q (Suc k) (svalid F1) (svalid F2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0) = ProbU q (Suc k) (svalid F1) (svalid F2)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
?q1 \<in> S \<Longrightarrow> ProbU ?q1 k (svalid F1) (svalid F2) = prob ?q1 (\<lambda>\<omega>. pvalid (U k F1 F2) (?q1 ## \<omega>))
q \<in> S

goal (1 subgoal):
 1. (if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0) = ProbU q (Suc k) (svalid F1) (svalid F2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if q \<in> svalid F2 then 1 else if q \<in> svalid F1 then \<Sum>t\<in>S. \<tau> q t * prob t (\<lambda>\<omega>. pvalid (U k F1 F2) (t ## \<omega>)) else 0) = ProbU q (Suc k) (svalid F1) (svalid F2)

goal (1 subgoal):
 1. \<And>k q. \<lbrakk>\<And>q. q \<in> S \<Longrightarrow> ProbU q k (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U k F1 F2) (q ## \<omega>)); q \<in> S\<rbrakk> \<Longrightarrow> ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = ProbU q (Suc k) (svalid F1) (svalid F2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>)) = ProbU q (Suc k) (svalid F1) (svalid F2)

goal (1 subgoal):
 1. ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ProbU q (Suc k) (svalid F1) (svalid F2) = prob q (\<lambda>\<omega>. pvalid (U (Suc k) F1 F2) (q ## \<omega>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Prob0_imp_not_Psi:
  assumes "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S" "s \<in> Prob0 \<Phi> \<Psi>" shows "s \<notin> \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<notin> \<Psi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> \<Psi>
[PROOF STEP]
have "s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
using \<open>s \<in> Prob0 \<Phi> \<Psi>\<close> Prob0_subset_S
[PROOF STATE]
proof (prove)
using this:
s \<in> Prob0 \<Phi> \<Psi>
Prob0 ?\<Phi> ?\<Psi> \<subseteq> S

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

goal (1 subgoal):
 1. s \<notin> \<Psi>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S
s \<in> Prob0 \<Phi> \<Psi>
s \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S
s \<in> Prob0 \<Phi> \<Psi>
s \<in> S

goal (1 subgoal):
 1. s \<notin> \<Psi>
[PROOF STEP]
by (auto simp add: Prob0_iff suntil_Stream)
[PROOF STATE]
proof (state)
this:
s \<notin> \<Psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Psi_imp_not_Prob0:
  assumes "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S" shows "s \<in> \<Psi> \<Longrightarrow> s \<notin> Prob0 \<Phi> \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> \<Psi> \<Longrightarrow> s \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
using Prob0_imp_not_Psi[OF assms]
[PROOF STATE]
proof (prove)
using this:
?s \<in> Prob0 \<Phi> \<Psi> \<Longrightarrow> ?s \<notin> \<Psi>

goal (1 subgoal):
 1. s \<in> \<Psi> \<Longrightarrow> s \<notin> Prob0 \<Phi> \<Psi>
[PROOF STEP]
by metis


[STATEMENT]
lemma s0_in_S: "s0 \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s0 \<in> S
[PROOF STEP]
using S_not_empty
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}

goal (1 subgoal):
 1. s0 \<in> S
[PROOF STEP]
by (auto intro!: someI_ex[of "\<lambda>x. x \<in> S"])


[STATEMENT]
lemma nn_integral_reward_finite:
  assumes "s \<in> S"
  assumes until: "AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)"
  shows "(\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
have "(\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s) = (\<integral>\<^sup>+ \<omega>. reward_until (svalid F) s \<omega> \<partial>T s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = integral\<^sup>N (T s) (reward_until (svalid F) s)
[PROOF STEP]
using until
[PROOF STATE]
proof (prove)
using this:
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 = integral\<^sup>N (T s) (reward_until (svalid F) s)
[PROOF STEP]
by (auto intro!: nn_integral_cong_AE ev_suntil)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = integral\<^sup>N (T s) (reward_until (svalid F) s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s = integral\<^sup>N (T s) (reward_until (svalid F) s)

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
have "\<dots> \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
 2. \<not> ?P \<Longrightarrow> integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
[PROOF STEP]
assume "s \<notin> svalid F"
[PROOF STATE]
proof (state)
this:
s \<notin> svalid F

goal (2 subgoals):
 1. ?P \<Longrightarrow> integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
 2. \<not> ?P \<Longrightarrow> integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
[PROOF STEP]
proof (rule nn_integral_reward_until_finite)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite ((Sigma UNIV E)\<^sup>* `` {s})
 2. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>* \<Longrightarrow> ennreal (\<rho> t) < \<infinity>
 3. \<And>t t'. \<lbrakk>(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>*; t' \<in> E t\<rbrakk> \<Longrightarrow> ennreal (\<iota> t t') < \<infinity>
 4. almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
have "acc `` {s} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
using E_rtrancl_closed[of s _ _ E] \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s \<in> S; (s, ?t) \<in> (Sigma ?A E)\<^sup>*; \<And>x. x \<in> ?A \<Longrightarrow> E x \<subseteq> E x\<rbrakk> \<Longrightarrow> ?t \<in> S
s \<in> S

goal (1 subgoal):
 1. (Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S

goal (4 subgoals):
 1. finite ((Sigma UNIV E)\<^sup>* `` {s})
 2. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>* \<Longrightarrow> ennreal (\<rho> t) < \<infinity>
 3. \<And>t t'. \<lbrakk>(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>*; t' \<in> E t\<rbrakk> \<Longrightarrow> ennreal (\<iota> t t') < \<infinity>
 4. almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S
[PROOF STEP]
show "finite (acc `` {s})"
[PROOF STATE]
proof (prove)
using this:
(Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S

goal (1 subgoal):
 1. finite ((Sigma UNIV E)\<^sup>* `` {s})
[PROOF STEP]
using finite_S
[PROOF STATE]
proof (prove)
using this:
(Sigma UNIV E)\<^sup>* `` {s} \<subseteq> S
finite S

goal (1 subgoal):
 1. finite ((Sigma UNIV E)\<^sup>* `` {s})
[PROOF STEP]
by (auto dest: finite_subset)
[PROOF STATE]
proof (state)
this:
finite ((Sigma UNIV E)\<^sup>* `` {s})

goal (3 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>* \<Longrightarrow> ennreal (\<rho> t) < \<infinity>
 2. \<And>t t'. \<lbrakk>(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>*; t' \<in> E t\<rbrakk> \<Longrightarrow> ennreal (\<iota> t t') < \<infinity>
 3. almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
show "AE \<omega> in T s. (ev (HLD (svalid F))) \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
using until
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in T s. (HLD S suntil HLD (svalid F)) (s ## \<omega>)

goal (1 subgoal):
 1. almost_everywhere (T s) (ev (HLD (svalid F)))
[PROOF STEP]
by (auto simp add: suntil_Stream \<open>s \<notin> svalid F\<close> intro: ev_suntil)
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (ev (HLD (svalid F)))

goal (2 subgoals):
 1. \<And>t. (s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>* \<Longrightarrow> ennreal (\<rho> t) < \<infinity>
 2. \<And>t t'. \<lbrakk>(s, t) \<in> (SIGMA s:UNIV. E s \<inter> - svalid F)\<^sup>*; t' \<in> E t\<rbrakk> \<Longrightarrow> ennreal (\<iota> t t') < \<infinity>
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>

goal (1 subgoal):
 1. \<not> s \<notin> svalid F \<Longrightarrow> integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
integral\<^sup>N (T s) (reward_until (svalid F) s) \<noteq> \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
finally
[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. \<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. reward (Future F) (s ## \<omega>) \<partial>T s \<noteq> \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique:
  assumes in_S: "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S" "N \<subseteq> S" "Prob0 \<Phi> \<Psi> \<subseteq> N" "\<Psi> \<subseteq> N"
  assumes l1: "\<And>s. s \<in> S \<Longrightarrow> s \<notin> N \<Longrightarrow> l1 s - c s = (\<Sum>s'\<in>S. \<tau> s s' * l1 s')"
  assumes l2: "\<And>s. s \<in> S \<Longrightarrow> s \<notin> N \<Longrightarrow> l2 s - c s = (\<Sum>s'\<in>S. \<tau> s s' * l2 s')"
  assumes eq: "\<And>s. s \<in> N \<Longrightarrow> l1 s = l2 s"
  shows "\<forall>s\<in>S. l1 s = l2 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. l1 s = l2 s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
assume "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
show "l1 s = l2 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l1 s = l2 s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> l1 s = l2 s
 2. \<not> ?P \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
assume "s \<in> N"
[PROOF STATE]
proof (state)
this:
s \<in> N

goal (2 subgoals):
 1. ?P \<Longrightarrow> l1 s = l2 s
 2. \<not> ?P \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> N

goal (1 subgoal):
 1. l1 s = l2 s
[PROOF STEP]
by (rule eq)
[PROOF STATE]
proof (state)
this:
l1 s = l2 s

goal (1 subgoal):
 1. s \<notin> N \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> N \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
assume "s \<notin> N"
[PROOF STATE]
proof (state)
this:
s \<notin> N

goal (1 subgoal):
 1. s \<notin> N \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l1 s = l2 s
[PROOF STEP]
proof (rule unique_les[of _ "S - N" K N])
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. s \<in> S - N
 2. \<Union> (E ` (S - N)) \<subseteq> S - N \<union> N
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 4. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 5. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 6. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 7. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
 8. \<And>s. s \<in> N \<Longrightarrow> l1 s = l2 s
 9. finite ((\<lambda>x. l1 x - l2 x) ` (S - N \<union> N))
[PROOF STEP]
show "finite ((\<lambda>x. l1 x - l2 x) ` (S - N \<union> N))" "(\<Union>x\<in>S - N. E x) \<subseteq> S - N \<union> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>x. l1 x - l2 x) ` (S - N \<union> N)) &&& \<Union> (E ` (S - N)) \<subseteq> S - N \<union> N
[PROOF STEP]
using E_closed finite_S \<open>N \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
finite S
N \<subseteq> S

goal (1 subgoal):
 1. finite ((\<lambda>x. l1 x - l2 x) ` (S - N \<union> N)) &&& \<Union> (E ` (S - N)) \<subseteq> S - N \<union> N
[PROOF STEP]
by (auto dest: finite_subset)
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>x. l1 x - l2 x) ` (S - N \<union> N))
\<Union> (E ` (S - N)) \<subseteq> S - N \<union> N

goal (7 subgoals):
 1. s \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 4. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 5. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 6. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
 7. \<And>s. s \<in> N \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
show "\<And>s. s \<in> N \<Longrightarrow> l1 s = l2 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> N \<Longrightarrow> l1 s = l2 s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
?s1 \<in> N \<Longrightarrow> l1 ?s1 = l2 ?s1

goal (6 subgoals):
 1. s \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 4. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 5. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 6. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?s1 \<in> N \<Longrightarrow> l1 ?s1 = l2 ?s1

goal (6 subgoals):
 1. s \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 4. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 5. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 6. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 4. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 5. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 6. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
assume "s \<in> S - N"
[PROOF STATE]
proof (state)
this:
s \<in> S - N

goal (6 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l2
 3. \<And>s. s \<in> S - N \<Longrightarrow> integrable (measure_pmf (K s)) l1
 4. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 5. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 6. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
with E_closed finite_S
[PROOF STATE]
proof (chain)
picking this:
\<Union> (E ` S) \<subseteq> S
finite S
s \<in> S - N
[PROOF STEP]
show "integrable (K s) l1" "integrable (K s) l2"
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
finite S
s \<in> S - N

goal (1 subgoal):
 1. integrable (measure_pmf (K s)) l1 &&& integrable (measure_pmf (K s)) l2
[PROOF STEP]
by (auto intro!: integrable_measure_pmf_finite dest: finite_subset)
[PROOF STATE]
proof (state)
this:
integrable (measure_pmf (K s)) l1
integrable (measure_pmf (K s)) l2

goal (4 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 3. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 4. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
obtain t where "(t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>*) \<or> s \<in> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>s \<in> S - N\<close> in_S(4)
[PROOF STATE]
proof (prove)
using this:
s \<in> S - N
Prob0 \<Phi> \<Psi> \<subseteq> N

goal (1 subgoal):
 1. (\<And>t. t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Prob0_iff_reachable[OF in_S(1,2)]
[PROOF STATE]
proof (prove)
using this:
s \<in> S - N
{s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}} \<subseteq> N

goal (1 subgoal):
 1. (\<And>t. t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N

goal (4 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 3. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 4. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N

goal (4 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 3. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 4. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
have "(Sigma \<Phi> E)\<^sup>* \<subseteq> acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Sigma \<Phi> E)\<^sup>* \<subseteq> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
by (intro rtrancl_mono Sigma_mono) auto
[PROOF STATE]
proof (state)
this:
(Sigma \<Phi> E)\<^sup>* \<subseteq> (Sigma UNIV E)\<^sup>*

goal (4 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
 3. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 4. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N
(Sigma \<Phi> E)\<^sup>* \<subseteq> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
show "\<exists>t\<in>N. (s, t) \<in> acc"
[PROOF STATE]
proof (prove)
using this:
t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N
(Sigma \<Phi> E)\<^sup>* \<subseteq> (Sigma UNIV E)\<^sup>*

goal (1 subgoal):
 1. \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
using \<open>\<Psi> \<subseteq> N\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> \<Psi> \<and> (s, t) \<in> (Sigma \<Phi> E)\<^sup>* \<or> s \<in> N
(Sigma \<Phi> E)\<^sup>* \<subseteq> (Sigma UNIV E)\<^sup>*
\<Psi> \<subseteq> N

goal (1 subgoal):
 1. \<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>N. (s, t) \<in> (Sigma UNIV E)\<^sup>*

goal (3 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + ?c s
 3. \<And>s. s \<in> S - N \<Longrightarrow> l1 s = measure_pmf.expectation (K s) l1 + ?c s
[PROOF STEP]
show "l1 s = integral\<^sup>L (K s) l1 + c s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l1 s = measure_pmf.expectation (K s) l1 + c s
[PROOF STEP]
using E_closed l1 \<open>s \<in> S - N\<close>
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
\<lbrakk>?s1 \<in> S; ?s1 \<notin> N\<rbrakk> \<Longrightarrow> l1 ?s1 - c ?s1 = (\<Sum>s'\<in>S. \<tau> ?s1 s' * l1 s')
s \<in> S - N

goal (1 subgoal):
 1. l1 s = measure_pmf.expectation (K s) l1 + c s
[PROOF STEP]
by (subst integral_measure_pmf[OF finite_S]) (auto simp: subset_eq field_simps)
[PROOF STATE]
proof (state)
this:
l1 s = measure_pmf.expectation (K s) l1 + c s

goal (2 subgoals):
 1. s__ \<in> S - N
 2. \<And>s. s \<in> S - N \<Longrightarrow> l2 s = measure_pmf.expectation (K s) l2 + c s
[PROOF STEP]
show "l2 s = integral\<^sup>L (K s) l2 + c s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l2 s = measure_pmf.expectation (K s) l2 + c s
[PROOF STEP]
using E_closed l2 \<open>s \<in> S - N\<close>
[PROOF STATE]
proof (prove)
using this:
\<Union> (E ` S) \<subseteq> S
\<lbrakk>?s1 \<in> S; ?s1 \<notin> N\<rbrakk> \<Longrightarrow> l2 ?s1 - c ?s1 = (\<Sum>s'\<in>S. \<tau> ?s1 s' * l2 s')
s \<in> S - N

goal (1 subgoal):
 1. l2 s = measure_pmf.expectation (K s) l2 + c s
[PROOF STEP]
by (subst integral_measure_pmf[OF finite_S]) (auto simp: subset_eq field_simps)
[PROOF STATE]
proof (state)
this:
l2 s = measure_pmf.expectation (K s) l2 + c s

goal (1 subgoal):
 1. s__ \<in> S - N
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?sa3 \<in> S - N \<Longrightarrow> l2 ?sa3 = measure_pmf.expectation (K ?sa3) l2 + c ?sa3

goal (1 subgoal):
 1. s \<in> S - N
[PROOF STEP]
qed (insert \<open>s \<notin>  N\<close> \<open>s \<in> S\<close>, auto)
[PROOF STATE]
proof (state)
this:
l1 s = l2 s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l1 s = l2 s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uniqueness_of_ProbU:
  assumes sol:
    "\<forall>s\<in>S. (\<Sum>s'\<in>S. LES (Prob0 (svalid F1) (svalid F2) \<union> svalid F2) s s' * l s') =
      (if s \<in> svalid F2 then 1 else 0)"
  shows "\<forall>s\<in>S. l s = \<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[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> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 8. \<And>s. s \<in> ?N \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
show "svalid F1 \<subseteq> S" "svalid F2 \<subseteq> S"
    "Prob0 (svalid F1) (svalid F2) \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2"
    "svalid F2 \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2"
    "Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (svalid F1 \<subseteq> S &&& svalid F2 \<subseteq> S) &&& Prob0 (svalid F1) (svalid F2) \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 &&& svalid F2 \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 &&& Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<subseteq> S
[PROOF STEP]
using svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. (svalid F1 \<subseteq> S &&& svalid F2 \<subseteq> S) &&& Prob0 (svalid F1) (svalid F2) \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 &&& svalid F2 \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 &&& Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<subseteq> S
[PROOF STEP]
by (auto simp: Prob0_def)
[PROOF STATE]
proof (state)
this:
svalid F1 \<subseteq> S
svalid F2 \<subseteq> S
Prob0 (svalid F1) (svalid F2) \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2
svalid F2 \<subseteq> Prob0 (svalid F1) (svalid F2) \<union> svalid F2
Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<subseteq> S

goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
assume s: "s \<in> S" "s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2"
[PROOF STATE]
proof (state)
this:
s \<in> S
s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[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 (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[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 (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[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 (3 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> l s - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * l s')
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - ?c s = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 3. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[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]
show "l s - 0 = (\<Sum>s'\<in>S. \<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 - 0 = (\<Sum>s'\<in>S. \<tau> s s' * l s')
[PROOF STEP]
using sol[THEN bspec, of s] 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
s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (Prob0 (svalid F1) (svalid F2) \<union> svalid F2) s s' * l s') = (if s \<in> svalid F2 then 1 else 0)
s \<in> S
s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

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

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 2. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 2. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 2. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
assume s: "s \<in> S" "s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2"
[PROOF STATE]
proof (state)
this:
s \<in> S
s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2\<rbrakk> \<Longrightarrow> prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s' ## \<omega>)))
 2. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2
[PROOF STEP]
show "\<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 =
    (\<Sum>t\<in>S. \<tau> s t * \<P>(\<omega> in T t. pvalid (U\<^sup>\<infinity> F1 F2) (t ## \<omega>)))"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

goal (1 subgoal):
 1. prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (t ## \<omega>)))
[PROOF STEP]
unfolding Prob0_iff[OF svalid_subset_S svalid_subset_S]
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<notin> {s \<in> S. AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)} \<union> svalid F2

goal (1 subgoal):
 1. prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (t ## \<omega>)))
[PROOF STEP]
by (subst prob_sum) (auto simp add: suntil_Stream)
[PROOF STATE]
proof (state)
this:
prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) - 0 = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (t ## \<omega>)))

goal (1 subgoal):
 1. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
assume "s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2"
[PROOF STATE]
proof (state)
this:
s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

goal (1 subgoal):
 1. \<And>s. s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2
[PROOF STEP]
show "l s = \<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
using this:
s \<in> Prob0 (svalid F1) (svalid F2) \<union> svalid F2

goal (1 subgoal):
 1. l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
assume P0: "s \<in> Prob0 (svalid F1) (svalid F2)"
[PROOF STATE]
proof (state)
this:
s \<in> Prob0 (svalid F1) (svalid F2)

goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> Prob0 (svalid F1) (svalid F2)
[PROOF STEP]
have "s \<in> S" "AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<in> Prob0 (svalid F1) (svalid F2)

goal (1 subgoal):
 1. s \<in> S &&& AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)
[PROOF STEP]
unfolding Prob0_iff[OF svalid_subset_S svalid_subset_S]
[PROOF STATE]
proof (prove)
using this:
s \<in> {s \<in> S. AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)}

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

goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)
[PROOF STEP]
have "\<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
AE \<omega> in T s. \<not> (HLD (svalid F1) suntil HLD (svalid F2)) (s ## \<omega>)

goal (1 subgoal):
 1. prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0
[PROOF STEP]
by (intro T.prob_eq_0_AE) simp
[PROOF STATE]
proof (state)
this:
prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0

goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0

goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
have "l s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l s = 0
[PROOF STEP]
using \<open>s \<in> S\<close> P0 sol[THEN bspec, of s] Prob0_subset_S
        Prob0_imp_not_Psi[OF svalid_subset_S svalid_subset_S P0]
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<in> Prob0 (svalid F1) (svalid F2)
s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (Prob0 (svalid F1) (svalid F2) \<union> svalid F2) s s' * l s') = (if s \<in> svalid F2 then 1 else 0)
Prob0 ?\<Phi> ?\<Psi> \<subseteq> S
s \<notin> svalid F2

goal (1 subgoal):
 1. l s = 0
[PROOF STEP]
by (auto simp: LES_def single_l split: if_split_asm)
[PROOF STATE]
proof (state)
this:
l s = 0

goal (2 subgoals):
 1. s \<in> Prob0 (svalid F1) (svalid F2) \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
 2. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0
l s = 0
[PROOF STEP]
show "l s = \<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
using this:
prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>)) = 0
l s = 0

goal (1 subgoal):
 1. l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
assume s: "s \<in> svalid F2"
[PROOF STATE]
proof (state)
this:
s \<in> svalid F2

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<in> svalid F2

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
with svalid_subset_S
[PROOF STATE]
proof (chain)
picking this:
svalid ?F \<subseteq> S
s \<in> svalid F2
[PROOF STEP]
have "s \<in> S"
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S
s \<in> svalid F2

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

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
note Psi_imp_not_Prob0[OF svalid_subset_S svalid_subset_S s]
[PROOF STATE]
proof (state)
this:
s \<notin> Prob0 (svalid ?F2) (svalid F2)

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s \<in> svalid F2
s \<in> S
s \<notin> Prob0 (svalid ?F2) (svalid F2)
[PROOF STEP]
have "l s = 1"
[PROOF STATE]
proof (prove)
using this:
s \<in> svalid F2
s \<in> S
s \<notin> Prob0 (svalid ?F2) (svalid F2)

goal (1 subgoal):
 1. l s = 1
[PROOF STEP]
using sol[THEN bspec, of s]
[PROOF STATE]
proof (prove)
using this:
s \<in> svalid F2
s \<in> S
s \<notin> Prob0 (svalid ?F2) (svalid F2)
s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (Prob0 (svalid F1) (svalid F2) \<union> svalid F2) s s' * l s') = (if s \<in> svalid F2 then 1 else 0)

goal (1 subgoal):
 1. l s = 1
[PROOF STEP]
by (auto simp: LES_def single_l dest: Psi_imp_not_Prob0[OF svalid_subset_S svalid_subset_S])
[PROOF STATE]
proof (state)
this:
l s = 1

goal (1 subgoal):
 1. s \<in> svalid F2 \<Longrightarrow> l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l s = 1
[PROOF STEP]
show "l s = \<P>(\<omega> in T s. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))"
[PROOF STATE]
proof (prove)
using this:
l s = 1

goal (1 subgoal):
 1. l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
l s = 1
s \<in> svalid F2

goal (1 subgoal):
 1. l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))
[PROOF STEP]
by (simp add: suntil_Stream)
[PROOF STATE]
proof (state)
this:
l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l s = prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> F1 F2) (s ## \<omega>))

goal:
No subgoals!
[PROOF STEP]
qed