[STATEMENT]
lemma sstart_sets: "sstart S xs \<in> sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sstart S xs \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
sstart S xs \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
note Cons[measurable]
[PROOF STATE]
proof (state)
this:
sstart S xs \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
have "sstart S (x # xs) =
    {s\<in>space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}
[PROOF STEP]
by (simp add: set_eq_iff space_stream_space)
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) = {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs}

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
have "\<dots> \<in> sets (stream_space (count_space UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs} \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
{s \<in> space (stream_space (count_space UNIV)). shd s = x \<and> stl s \<in> sstart S xs} \<in> sets (stream_space (count_space UNIV))

goal (2 subgoals):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
 2. \<And>a xs. sstart S xs \<in> sets (stream_space (count_space UNIV)) \<Longrightarrow> sstart S (a # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sstart S (x # xs) \<in> sets (stream_space (count_space UNIV))

goal (1 subgoal):
 1. sstart S [] \<in> sets (stream_space (count_space UNIV))
[PROOF STEP]
qed (simp add: streams_sets)