[STATEMENT]
lemma E_inf_r:
  "step.E_inf s (r f) =
    lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
have "step.E_inf s (r f) =
    lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
unfolding rF_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (lfp (\<lambda>F \<omega>. if fst (shd \<omega>) = Skip then f (snd (shd \<omega>)) else F (stl \<omega>))) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
proof (rule step.E_inf_lfp[THEN fun_cong])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>(b, a). if fst b = Skip then f (snd b) else a) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
 2. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 3. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 4. \<And>s. finite (step s)
[PROOF STEP]
let ?F = "\<lambda>t x. (if fst t = Skip then f (snd t) else x)"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>(b, a). if fst b = Skip then f (snd b) else a) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
 2. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 3. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 4. \<And>s. finite (step s)
[PROOF STEP]
show "(\<lambda>(s, x). ?F s x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(s, x). if fst s = Skip then f (snd s) else x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
[PROOF STEP]
apply (simp add: measurable_split_conv split_beta')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if fst (fst x) = Skip then f (snd (fst x)) else snd x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
[PROOF STEP]
apply (intro borel_measurable_max borel_measurable_const measurable_If predE
         measurable_compose[OF measurable_snd] measurable_compose[OF measurable_fst])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>a. f (snd a)) \<in> borel_measurable (count_space UNIV)
 2. (\<lambda>a. a) \<in> borel_measurable borel
 3. Measurable.pred (count_space UNIV) (\<lambda>a. fst a = Skip)
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>(s, x). if fst s = Skip then f (snd s) else x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)

goal (3 subgoals):
 1. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 2. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 3. \<And>s. finite (step s)
[PROOF STEP]
show "\<And>s. sup_continuous (?F s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
[PROOF STEP]
by (auto simp: sup_continuous_def SUP_sup_distrib[symmetric] split: prod.split pgcl.split)
[PROOF STATE]
proof (state)
this:
sup_continuous (HOL.If (fst ?s2 = Skip) (f (snd ?s2)))

goal (2 subgoals):
 1. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 2. \<And>s. finite (step s)
[PROOF STEP]
show "\<And>F cfg. (\<integral>\<^sup>+\<omega>. ?F (state cfg) (F \<omega>) \<partial>step.T cfg) =
      ?F (state cfg) (nn_integral (step.T cfg) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F cfg. \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
[PROOF STEP]
by (auto simp: split: pgcl.split prod.split)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. (if fst (state ?cfg3) = Skip then f (snd (state ?cfg3)) else ?F3 \<omega>) \<partial>step.T ?cfg3 = (if fst (state ?cfg3) = Skip then f (snd (state ?cfg3)) else integral\<^sup>N (step.T ?cfg3) ?F3)

goal (1 subgoal):
 1. \<And>s. finite (step s)
[PROOF STEP]
qed (rule step_finite)
[PROOF STATE]
proof (state)
this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal:
No subgoals!
[PROOF STEP]
qed