[STATEMENT]
lemma \<T>_return_eq:
  shows
    "\<T> p s = do {
  a \<leftarrow> measure_pmf (p [] s);
  s' \<leftarrow> measure_pmf (K (s,a));
  w \<leftarrow> T (\<pi>_Suc p (s,a)) (return_pmf s');
  return S ((s,a)##w)
}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
have "\<T> p s = do {
    a \<leftarrow> measure_pmf (p [] s);
    \<omega> \<leftarrow> T (\<pi>_Suc p (s, a)) (K (s, a));
   return S ((s, a) ## \<omega>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))
[PROOF STEP]
using \<T>_eq_return
[PROOF STATE]
proof (prove)
using this:
\<T> ?p ?s = measure_pmf (?p [] ?s) \<bind> (\<lambda>y. T (\<pi>_Suc ?p (?s, y)) (K (?s, y)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((?s, y) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
have "\<dots> =  do {
    a \<leftarrow> measure_pmf (p [] s);
    s' \<leftarrow> measure_pmf (K (s, a));
    \<omega> \<leftarrow> T (\<pi>_Suc p (s, a)) (return_pmf s');
   return S ((s, a) ## \<omega>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
unfolding \<T>_return
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> \<T> (\<pi>_Suc p (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. measure_pmf (return_pmf s') \<bind> \<T> (\<pi>_Suc p (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
by (subst bind_assoc[of _ _ S _ S]) (auto simp add: \<T>_def \<T>_return[symmetric])
[PROOF STATE]
proof (state)
this:
measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))

goal:
No subgoals!
[PROOF STEP]
qed