[STATEMENT]
lemma bind_I_K_eq_M: "K.T' I = distr M K.S (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))" (is "_ = ?D")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K.T' I = distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))
[PROOF STEP]
proof (rule stream_space_eq_sstart)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
note streams_sets[measurable]
[PROOF STATE]
proof (state)
this:
?X \<in> sets ?M \<Longrightarrow> streams ?X \<in> sets (stream_space ?M)

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
note measurable_abs_UNIV[measurable (raw)]
[PROOF STATE]
proof (state)
this:
(\<And>n. ?f n \<in> ?M \<rightarrow>\<^sub>M ?N n) \<Longrightarrow> (\<lambda>\<omega> n. ?f n \<omega>) \<in> ?M \<rightarrow>\<^sub>M Pi\<^sub>M UNIV ?N

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
note sstart_sets[measurable]
[PROOF STATE]
proof (state)
this:
sstart ?S ?xs \<in> sets (stream_space (count_space UNIV))

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sstart ?S ?xs \<in> sets (stream_space (count_space UNIV))

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
assume "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
from K.AE_T_enabled[of s]
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (K.T s) (K.enabled s)
[PROOF STEP]
have "AE \<omega> in K.T s. \<omega> \<in> streams S"
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (K.T s) (K.enabled s)

goal (1 subgoal):
 1. AE \<omega> in K.T s. \<omega> \<in> streams S
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. K.enabled s \<omega> \<Longrightarrow> \<omega> \<in> streams S
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. K.enabled s \<omega> \<Longrightarrow> \<omega> \<in> streams S
[PROOF STEP]
assume "K.enabled s \<omega>"
[PROOF STATE]
proof (state)
this:
K.enabled s \<omega>

goal (1 subgoal):
 1. \<And>\<omega>. K.enabled s \<omega> \<Longrightarrow> \<omega> \<in> streams S
[PROOF STEP]
from this \<open>s\<in>S\<close>
[PROOF STATE]
proof (chain)
picking this:
K.enabled s \<omega>
s \<in> S
[PROOF STEP]
show "\<omega> \<in> streams S"
[PROOF STATE]
proof (prove)
using this:
K.enabled s \<omega>
s \<in> S

goal (1 subgoal):
 1. \<omega> \<in> streams S
[PROOF STEP]
proof (coinduction arbitrary: s \<omega>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s \<omega>. \<lbrakk>K.enabled s \<omega>; s \<in> S\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)
[PROOF STEP]
case streams
[PROOF STATE]
proof (state)
this:
K.enabled s \<omega>
s \<in> S

goal (1 subgoal):
 1. \<And>s \<omega>. \<lbrakk>K.enabled s \<omega>; s \<in> S\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K.enabled s \<omega>
s \<in> S
[PROOF STEP]
have 1: "pmf (K s) (shd \<omega>) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
K.enabled s \<omega>
s \<in> S

goal (1 subgoal):
 1. pmf (K s) (shd \<omega>) \<noteq> 0
[PROOF STEP]
by (simp add: K.enabled.simps[of s] set_pmf_iff)
[PROOF STATE]
proof (state)
this:
pmf (K s) (shd \<omega>) \<noteq> 0

goal (1 subgoal):
 1. \<And>s \<omega>. \<lbrakk>K.enabled s \<omega>; s \<in> S\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)
[PROOF STEP]
have "shd \<omega> \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shd \<omega> \<in> S
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> shd \<omega> \<in> S
 2. \<not> ?P \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
assume "\<exists>n. 0 < \<P>(\<omega> in M. X n \<omega> = s)"
[PROOF STATE]
proof (state)
this:
\<exists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (2 subgoals):
 1. ?P \<Longrightarrow> shd \<omega> \<in> S
 2. \<not> ?P \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}
[PROOF STEP]
obtain n where "0 < \<P>(\<omega> in M. X n \<omega> = s)"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (1 subgoal):
 1. (\<And>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (2 subgoals):
 1. ?P \<Longrightarrow> shd \<omega> \<in> S
 2. \<not> ?P \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
pmf (K s) (shd \<omega>) \<noteq> 0
0 < prob {\<omega> \<in> space M. X n \<omega> = s}
[PROOF STEP]
have 2: "\<P>(\<omega>' in M. X (Suc n) \<omega>' = shd \<omega> \<and> X n \<omega>' = s) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
pmf (K s) (shd \<omega>) \<noteq> 0
0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (1 subgoal):
 1. prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} \<noteq> 0
[PROOF STEP]
by (simp add: pmf_K cond_prob_def)
[PROOF STATE]
proof (state)
this:
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> shd \<omega> \<in> S
 2. \<not> ?P \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
show "shd \<omega> \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shd \<omega> \<in> S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. shd \<omega> \<notin> S \<Longrightarrow> False
[PROOF STEP]
assume "shd \<omega> \<notin> S"
[PROOF STATE]
proof (state)
this:
shd \<omega> \<notin> S

goal (1 subgoal):
 1. shd \<omega> \<notin> S \<Longrightarrow> False
[PROOF STEP]
with S(2)[of "Suc n"]
[PROOF STATE]
proof (chain)
picking this:
AE x in M. X (Suc n) x \<in> S
shd \<omega> \<notin> S
[PROOF STEP]
have "\<P>(\<omega>' in M. X (Suc n) \<omega>' = shd \<omega> \<and> X n \<omega>' = s) = 0"
[PROOF STATE]
proof (prove)
using this:
AE x in M. X (Suc n) x \<in> S
shd \<omega> \<notin> S

goal (1 subgoal):
 1. prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} = 0
[PROOF STEP]
by (intro M.prob_eq_0_AE) auto
[PROOF STATE]
proof (state)
this:
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} = 0

goal (1 subgoal):
 1. shd \<omega> \<notin> S \<Longrightarrow> False
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} \<noteq> 0
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} \<noteq> 0
prob {\<omega>'' \<in> space M. X (Suc n) \<omega>'' = shd \<omega> \<and> X n \<omega>'' = s} = 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
shd \<omega> \<in> S

goal (1 subgoal):
 1. \<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s} \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s} \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
assume "\<not> (\<exists>n. 0 < \<P>(\<omega> in M. X n \<omega> = s))"
[PROOF STATE]
proof (state)
this:
\<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (1 subgoal):
 1. \<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s} \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}
[PROOF STEP]
have "pmf (K s) (shd \<omega>) = indicator {shd \<omega>} s"
[PROOF STATE]
proof (prove)
using this:
\<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s}

goal (1 subgoal):
 1. pmf (K s) (shd \<omega>) = indicat_real {shd \<omega>} s
[PROOF STEP]
by (intro pmf_K2) (auto simp: not_less measure_le_0_iff)
[PROOF STATE]
proof (state)
this:
pmf (K s) (shd \<omega>) = indicat_real {shd \<omega>} s

goal (1 subgoal):
 1. \<nexists>n. 0 < prob {\<omega> \<in> space M. X n \<omega> = s} \<Longrightarrow> shd \<omega> \<in> S
[PROOF STEP]
with 1 \<open>s\<in>S\<close>
[PROOF STATE]
proof (chain)
picking this:
pmf (K s) (shd \<omega>) \<noteq> 0
s \<in> S
pmf (K s) (shd \<omega>) = indicat_real {shd \<omega>} s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pmf (K s) (shd \<omega>) \<noteq> 0
s \<in> S
pmf (K s) (shd \<omega>) = indicat_real {shd \<omega>} s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
shd \<omega> \<in> S

goal (1 subgoal):
 1. \<And>s \<omega>. \<lbrakk>K.enabled s \<omega>; s \<in> S\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)
[PROOF STEP]
with streams
[PROOF STATE]
proof (chain)
picking this:
K.enabled s \<omega>
s \<in> S
shd \<omega> \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
K.enabled s \<omega>
s \<in> S
shd \<omega> \<in> S

goal (1 subgoal):
 1. \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)
[PROOF STEP]
by (cases \<omega>) (auto simp: K.enabled.simps[of s])
[PROOF STATE]
proof (state)
this:
\<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>sa \<omega>. s = \<omega> \<and> K.enabled sa \<omega> \<and> sa \<in> S) \<or> s \<in> streams S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<omega> \<in> streams S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE \<omega> in K.T s. \<omega> \<in> streams S

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s14 \<in> S \<Longrightarrow> AE \<omega> in K.T ?s14. \<omega> \<in> streams S

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
note AE_streams = this
[PROOF STATE]
proof (state)
this:
?s14 \<in> S \<Longrightarrow> AE \<omega> in K.T ?s14. \<omega> \<in> streams S

goal (8 subgoals):
 1. countable ?S
 2. prob_space (K.T' I)
 3. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 4. AE x in K.T' I. x \<in> streams ?S
 5. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 6. sets (K.T' I) = sets (stream_space (count_space UNIV))
 7. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
show "prob_space (K.T' I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (K.T' I)
[PROOF STEP]
by (rule K.prob_space_T')
[PROOF STATE]
proof (state)
this:
prob_space (K.T' I)

goal (7 subgoals):
 1. countable ?S
 2. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
 3. AE x in K.T' I. x \<in> streams ?S
 4. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 5. sets (K.T' I) = sets (stream_space (count_space UNIV))
 6. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 7. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
show "prob_space ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))
[PROOF STEP]
by (rule M.prob_space_distr) simp
[PROOF STATE]
proof (state)
this:
prob_space (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)))

goal (6 subgoals):
 1. countable ?S
 2. AE x in K.T' I. x \<in> streams ?S
 3. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams ?S
 4. sets (K.T' I) = sets (stream_space (count_space UNIV))
 5. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 6. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart ?S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart ?S xs)
[PROOF STEP]
show "AE x in K.T' I. x \<in> streams S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in K.T' I. x \<in> streams S
[PROOF STEP]
by (auto simp add: K.AE_T' set_pmf_iff I_in_S AE_distr_iff streams_Stream intro!: AE_streams)
[PROOF STATE]
proof (state)
this:
AE x in K.T' I. x \<in> streams S

goal (5 subgoals):
 1. countable S
 2. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams S
 3. sets (K.T' I) = sets (stream_space (count_space UNIV))
 4. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 5. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
show "AE x in ?D. x \<in> streams S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams S
[PROOF STEP]
by (simp add: AE_distr_iff to_stream_in_streams AE_all_countable S)
[PROOF STATE]
proof (state)
this:
AE x in distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>)). x \<in> streams S

goal (4 subgoals):
 1. countable S
 2. sets (K.T' I) = sets (stream_space (count_space UNIV))
 3. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 4. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
show "sets (K.T' I) = sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (K.T' I) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by (simp add: K.sets_T')
[PROOF STATE]
proof (state)
this:
sets (K.T' I) = sets (stream_space (count_space UNIV))

goal (3 subgoals):
 1. countable S
 2. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
 3. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
show "sets ?D = sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sets (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) = sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
fix xs'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
assume "xs' \<noteq> []" "xs' \<in> lists S"
[PROOF STATE]
proof (state)
this:
xs' \<noteq> []
xs' \<in> lists S

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs' \<noteq> []
xs' \<in> lists S
[PROOF STEP]
obtain s xs where xs': "xs' = s # xs" and s: "s \<in> S" and xs: "xs \<in> lists S"
[PROOF STATE]
proof (prove)
using this:
xs' \<noteq> []
xs' \<in> lists S

goal (1 subgoal):
 1. (\<And>s xs. \<lbrakk>xs' = s # xs; s \<in> S; xs \<in> lists S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: neq_Nil_conv del: in_listsD)
[PROOF STATE]
proof (state)
this:
xs' = s # xs
s \<in> S
xs \<in> lists S

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "emeasure (K.T' I) (sstart S xs') = (\<integral>\<^sup>+s. emeasure (K.T s) {\<omega>\<in>space K.S. s ## \<omega> \<in> sstart S xs'} \<partial>I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T' I) (sstart S xs') = \<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I
[PROOF STEP]
by (rule K.emeasure_T') measurable
[PROOF STATE]
proof (state)
this:
emeasure (K.T' I) (sstart S xs') = \<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T' I) (sstart S xs') = \<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+s'. emeasure (K.T s) (sstart S xs) * indicator {s} s' \<partial>I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I = \<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I
[PROOF STEP]
by (intro arg_cong2[where f=emeasure] nn_integral_cong)
       (auto split: split_indicator simp: emeasure_distr vimage_def space_stream_space neq_Nil_conv xs')
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I = \<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ s. emeasure (K.T s) {\<omega> \<in> space (stream_space (count_space UNIV)). s ## \<omega> \<in> sstart S xs'} \<partial>measure_pmf I = \<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "\<dots> = pmf I s * emeasure (K.T s) (sstart S xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I = ennreal (pmf I s) * emeasure (K.T s) (sstart S xs)
[PROOF STEP]
by (auto simp add: max_def emeasure_pmf_single intro: mult_ac)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I = ennreal (pmf I s) * emeasure (K.T s) (sstart S xs)

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+s'\<in>{s}. emeasure (K.T s) (sstart S xs)\<partial>measure_pmf I = ennreal (pmf I s) * emeasure (K.T s) (sstart S xs)

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "emeasure (K.T s) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((s#xs)!i)) (xs!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T s) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i))
[PROOF STEP]
using xs s
[PROOF STATE]
proof (prove)
using this:
xs \<in> lists S
s \<in> S

goal (1 subgoal):
 1. emeasure (K.T s) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i))
[PROOF STEP]
proof (induction arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S []) = ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i))
 2. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S []) = ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i))
 2. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. emeasure (K.T s) (sstart S []) = ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i))
[PROOF STEP]
by (simp add: K.T.emeasure_eq_1_AE AE_streams)
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S []) = ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i))

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
case (Cons t xs)
[PROOF STATE]
proof (state)
this:
t \<in> S
xs \<in> lists S
?s12 \<in> S \<Longrightarrow> emeasure (K.T ?s12) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((?s12 # xs) ! i)) (xs ! i))
s \<in> S

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
have "emeasure (K.T s) (sstart S (t # xs)) =
      emeasure (K.T s) {x\<in>space (K.T s). shd x = t \<and> stl x \<in> sstart S xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T s) (sstart S (t # xs)) = emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs}
[PROOF STEP]
by (intro arg_cong2[where f=emeasure]) (auto simp: space_stream_space)
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S (t # xs)) = emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs}

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S (t # xs)) = emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs}

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+t'. emeasure (K.T t') {x\<in>space K.S. t' = t \<and> x \<in> sstart S xs} \<partial>K s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs} = \<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s)
[PROOF STEP]
by (subst K.emeasure_Collect_T) auto
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs} = \<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s)

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) {x \<in> space (K.T s). shd x = t \<and> stl x \<in> sstart S xs} = \<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s)

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+t'. emeasure (K.T t) (sstart S xs) * indicator {t} t' \<partial>K s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s) = \<integral>\<^sup>+t'\<in>{t}. emeasure (K.T t) (sstart S xs)\<partial>measure_pmf (K s)
[PROOF STEP]
by (intro nn_integral_cong) (auto split: split_indicator simp: space_stream_space)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s) = \<integral>\<^sup>+t'\<in>{t}. emeasure (K.T t) (sstart S xs)\<partial>measure_pmf (K s)

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ t'. emeasure (K.T t') {x \<in> space (stream_space (count_space UNIV)). t' = t \<and> x \<in> sstart S xs} \<partial>measure_pmf (K s) = \<integral>\<^sup>+t'\<in>{t}. emeasure (K.T t) (sstart S xs)\<partial>measure_pmf (K s)

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
have "\<dots> = emeasure (K.T t) (sstart S xs) * pmf (K s) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+t'\<in>{t}. emeasure (K.T t) (sstart S xs)\<partial>measure_pmf (K s) = emeasure (K.T t) (sstart S xs) * ennreal (pmf (K s) t)
[PROOF STEP]
by (simp add: emeasure_pmf_single max_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+t'\<in>{t}. emeasure (K.T t) (sstart S xs)\<partial>measure_pmf (K s) = emeasure (K.T t) (sstart S xs) * ennreal (pmf (K s) t)

goal (1 subgoal):
 1. \<And>a l s. \<lbrakk>a \<in> S; l \<in> lists S; \<And>s. s \<in> S \<Longrightarrow> emeasure (K.T s) (sstart S l) = ennreal (\<Prod>i<length l. pmf (K ((s # l) ! i)) (l ! i)); s \<in> S\<rbrakk> \<Longrightarrow> emeasure (K.T s) (sstart S (a # l)) = ennreal (\<Prod>i<length (a # l). pmf (K ((s # a # l) ! i)) ((a # l) ! i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (K.T s) (sstart S (t # xs)) = emeasure (K.T t) (sstart S xs) * ennreal (pmf (K s) t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
emeasure (K.T s) (sstart S (t # xs)) = emeasure (K.T t) (sstart S xs) * ennreal (pmf (K s) t)

goal (1 subgoal):
 1. emeasure (K.T s) (sstart S (t # xs)) = ennreal (\<Prod>i<length (t # xs). pmf (K ((s # t # xs) ! i)) ((t # xs) ! i))
[PROOF STEP]
by (simp add: lessThan_Suc_eq_insert_0 zero_notin_Suc_image prod.reindex Cons
        prod_nonneg ennreal_mult[symmetric])
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S (t # xs)) = ennreal (\<Prod>i<length (t # xs). pmf (K ((s # t # xs) ! i)) ((t # xs) ! i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i))

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T s) (sstart S xs) = ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i))

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "pmf I s * ennreal (\<Prod>i<length xs. pmf (K ((s#xs)!i)) (xs!i)) =
    \<P>(x in M. \<forall>i\<le>length xs. X i x = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})
[PROOF STEP]
using xs s
[PROOF STATE]
proof (prove)
using this:
xs \<in> lists S
s \<in> S

goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length []. X i x = [s] ! i})
 2. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<in> lists S
s \<in> S

goal (2 subgoals):
 1. \<lbrakk>[] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length []. X i x = [s] ! i})
 2. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
have "pmf I s = prob {x \<in> space M. X 0 x = s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf I s = prob {x \<in> space M. X 0 x = s}
[PROOF STEP]
by transfer (simp add: vimage_def Int_def measure_distr conj_commute)
[PROOF STATE]
proof (state)
this:
pmf I s = prob {x \<in> space M. X 0 x = s}

goal (2 subgoals):
 1. \<lbrakk>[] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length []. X i x = [s] ! i})
 2. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf I s = prob {x \<in> space M. X 0 x = s}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pmf I s = prob {x \<in> space M. X 0 x = s}

goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length []. X i x = [s] ! i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length []. pmf (K ([s] ! i)) ([] ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length []. X i x = [s] ! i})

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
case (snoc t xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})
xs @ [t] \<in> lists S
s \<in> S

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
let ?l = "length xs" and ?lt = "length (xs @ [t])" and ?xs' = "s # xs @ [t]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
have "ennreal (pmf I s) * (\<Prod>i<?lt. pmf (K ((?xs') ! i)) ((xs @ [t]) ! i)) =
      (ennreal (pmf I s) * (\<Prod>i<?l. pmf (K ((s # xs) ! i)) (xs ! i))) * pmf (K ((s # xs) ! ?l)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t)
[PROOF STEP]
by (simp add: lessThan_Suc mult_ac nth_append append_Cons[symmetric] prod_nonneg ennreal_mult[symmetric]
               del: append_Cons)
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
have "\<dots> = \<P>(x in M. \<forall>i\<le>?l. X i x = (s # xs) ! i) * pmf (K ((s # xs) ! ?l)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t)
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})
xs @ [t] \<in> lists S
s \<in> S

goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t)
[PROOF STEP]
by (simp add: ennreal_mult[symmetric])
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) * ennreal (pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
have "\<dots> = \<P>(x in M. \<forall>i\<le>?lt. X i x = (?xs') ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
assume "\<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i) = 0"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
have "\<P>(x in M. \<forall>i\<le>?lt. X i x = (?xs') ! i) \<le> \<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
[PROOF STATE]
proof (state)
this:
prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
have "\<P>(x in M. \<forall>i\<le>?l. X i x = (s # xs) ! i) \<le> \<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
[PROOF STATE]
proof (state)
this:
prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (2 subgoals):
 1. ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
 2. \<not> ?P \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} = 0
prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} = 0
prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
by (simp add: measure_le_0_iff)
[PROOF STATE]
proof (state)
this:
ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
assume "\<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0
[PROOF STEP]
have *: "0 < \<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0

goal (1 subgoal):
 1. 0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
unfolding less_le
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<and> 0 \<noteq> prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
have "\<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i) \<le> \<P>(\<omega> in M. X ?l \<omega> = (s # xs) ! ?l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs}
[PROOF STEP]
by (intro M.finite_measure_mono) (auto simp: nth_append nth_Cons split: nat.split)
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs}

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs}
[PROOF STEP]
have "\<P>(\<omega> in M. X ?l \<omega> = (s # xs) ! ?l) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<le> prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs}

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs} \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs} \<noteq> 0

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs} \<noteq> 0
[PROOF STEP]
have "pmf (K ((s # xs) ! ?l)) t = \<P>(\<omega> in M. X ?lt \<omega> = ?xs' ! ?lt \<bar> X ?l \<omega> = (s # xs) ! ?l)"
[PROOF STATE]
proof (prove)
using this:
prob {\<omega> \<in> space M. X (length xs) \<omega> = (s # xs) ! length xs} \<noteq> 0

goal (1 subgoal):
 1. pmf (K ((s # xs) ! length xs)) t = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs)
[PROOF STEP]
by (subst pmf_K) (auto simp: less_le)
[PROOF STATE]
proof (state)
this:
pmf (K ((s # xs) ! length xs)) t = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (K ((s # xs) ! length xs)) t = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
have "\<dots> = \<P>(\<omega> in M. X ?lt \<omega> = ?xs' ! ?lt \<bar> \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs) = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i)
[PROOF STEP]
using * MC[of ?l "\<lambda>i. (s # xs) ! i" "?xs' ! ?lt"]
[PROOF STATE]
proof (prove)
using this:
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
prob {\<omega> \<in> space M. \<forall>t\<le>length xs. X t \<omega> = (s # xs) ! t} \<noteq> 0 \<Longrightarrow> cond_prob M (\<lambda>\<omega>. X (Suc (length xs)) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>t\<le>length xs. X t \<omega> = (s # xs) ! t) = cond_prob M (\<lambda>\<omega>. X (Suc (length xs)) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs)

goal (1 subgoal):
 1. cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs) = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs) = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. X (length xs) \<omega> = (s # xs) ! length xs) = cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i)

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
have "\<dots> = \<P>(\<omega> in M. \<forall>i\<le>?lt. X i \<omega> = ?xs' ! i) / \<P>(\<omega> in M. \<forall>i\<le>?l. X i \<omega> = (s # xs) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i) = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
unfolding cond_prob_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob {\<omega> \<in> space M. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t]) \<and> (\<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i)} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
by (intro arg_cong2[where f="(/)"] arg_cong2[where f=measure]) (auto simp: nth_Cons nth_append split: nat.splits)
[PROOF STATE]
proof (state)
this:
cond_prob M (\<lambda>\<omega>. X (length (xs @ [t])) \<omega> = (s # xs @ [t]) ! length (xs @ [t])) (\<lambda>\<omega>. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i) = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i} \<noteq> 0 \<Longrightarrow> ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pmf (K ((s # xs) ! length xs)) t = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pmf (K ((s # xs) ! length xs)) t = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
pmf (K ((s # xs) ! length xs)) t = prob {\<omega> \<in> space M. \<forall>i\<le>length (xs @ [t]). X i \<omega> = (s # xs @ [t]) ! i} / prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}
0 < prob {\<omega> \<in> space M. \<forall>i\<le>length xs. X i \<omega> = (s # xs) ! i}

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i} * pmf (K ((s # xs) ! length xs)) t) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>xs \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}); xs @ [x] \<in> lists S; s \<in> S\<rbrakk> \<Longrightarrow> ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [x]). pmf (K ((s # xs @ [x]) ! i)) ((xs @ [x]) ! i)) = ennreal (prob {xa \<in> space M. \<forall>i\<le>length (xs @ [x]). X i xa = (s # xs @ [x]) ! i})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})

goal (1 subgoal):
 1. ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length (xs @ [t]). pmf (K ((s # xs @ [t]) ! i)) ((xs @ [t]) ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length (xs @ [t]). X i x = (s # xs @ [t]) ! i})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf I s) * ennreal (\<Prod>i<length xs. pmf (K ((s # xs) ! i)) (xs ! i)) = ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i})

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
have "\<dots> = emeasure ?D (sstart S xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
have "AE x in M. \<forall>i. X i x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<forall>i. X i x \<in> S
[PROOF STEP]
using S(2)
[PROOF STATE]
proof (prove)
using this:
AE x in M. X ?n x \<in> S

goal (1 subgoal):
 1. AE x in M. \<forall>i. X i x \<in> S
[PROOF STEP]
by (simp add: AE_all_countable)
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>i. X i x \<in> S

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<forall>i. X i x \<in> S
[PROOF STEP]
have "AE x in M. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')"
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<forall>i. X i x \<in> S

goal (1 subgoal):
 1. AE x in M. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>i. X i x \<in> S \<Longrightarrow> (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>i. X i x \<in> S \<Longrightarrow> (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
assume "\<forall>i. X i x \<in> S"
[PROOF STATE]
proof (state)
this:
\<forall>i. X i x \<in> S

goal (1 subgoal):
 1. \<And>x. \<forall>i. X i x \<in> S \<Longrightarrow> (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. X i x \<in> S
[PROOF STEP]
have "to_stream (\<lambda>n. X n x) \<in> streams S"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. X i x \<in> S

goal (1 subgoal):
 1. to_stream (\<lambda>n. X n x) \<in> streams S
[PROOF STEP]
by (auto simp: streams_iff_snth to_stream_def)
[PROOF STATE]
proof (state)
this:
to_stream (\<lambda>n. X n x) \<in> streams S

goal (1 subgoal):
 1. \<And>x. \<forall>i. X i x \<in> S \<Longrightarrow> (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
to_stream (\<lambda>n. X n x) \<in> streams S
[PROOF STEP]
show "(\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')"
[PROOF STATE]
proof (prove)
using this:
to_stream (\<lambda>n. X n x) \<in> streams S

goal (1 subgoal):
 1. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
by (simp add: sstart_eq xs' to_stream_def less_Suc_eq_le del: sstart.simps(1) in_sstart)
[PROOF STATE]
proof (state)
this:
(\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE x in M. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<forall>i\<le>length xs. X i x = (s # xs) ! i) = (to_stream (\<lambda>n. X n x) \<in> sstart S xs')

goal (1 subgoal):
 1. ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
by (auto simp: emeasure_distr M.emeasure_eq_measure intro!: M.finite_measure_eq_AE)
[PROOF STATE]
proof (state)
this:
ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (prob {x \<in> space M. \<forall>i\<le>length xs. X i x = (s # xs) ! i}) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')

goal (2 subgoals):
 1. countable S
 2. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists S\<rbrakk> \<Longrightarrow> emeasure (K.T' I) (sstart S xs) = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (K.T' I) (sstart S xs') = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
show "emeasure (K.T' I) (sstart S xs') = emeasure ?D (sstart S xs')"
[PROOF STATE]
proof (prove)
using this:
emeasure (K.T' I) (sstart S xs') = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')

goal (1 subgoal):
 1. emeasure (K.T' I) (sstart S xs') = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
emeasure (K.T' I) (sstart S xs') = emeasure (distr M (stream_space (count_space UNIV)) (\<lambda>\<omega>. to_stream (\<lambda>n. X n \<omega>))) (sstart S xs')

goal (1 subgoal):
 1. countable S
[PROOF STEP]
qed (rule S)