[STATEMENT]
lemma expectation_gpv_le_inline:
  defines "expectation_gpv2 \<equiv> expectation_gpv 0 \<I>'"
  assumes callee: "\<And>s x. \<lbrakk> x \<in> outs_\<I> \<I>; I s \<rbrakk> \<Longrightarrow> plossless_gpv \<I>' (callee s x)"
    and WT_gpv: "\<I> \<turnstile>g gpv \<surd>"
    and I: "I s"
  shows "expectation_gpv 0 \<I> f gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> f gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
using WT_gpv I
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. expectation_gpv 0 \<I> f gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
proof(induction arbitrary: gpv s rule: expectation_gpv_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. \<I> \<turnstile>g x \<surd> \<longrightarrow> (\<forall>xa. I xa \<longrightarrow> a x \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee x xa)))
 2. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> 0 \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
 3. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. lfp.admissible (\<lambda>a. \<forall>x. \<I> \<turnstile>g x \<surd> \<longrightarrow> (\<forall>xa. I xa \<longrightarrow> a x \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee x xa)))
 2. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> 0 \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
 3. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp.admissible (\<lambda>a. \<forall>x. \<I> \<turnstile>g x \<surd> \<longrightarrow> (\<forall>xa. I xa \<longrightarrow> a x \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee x xa)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lfp.admissible (\<lambda>a. \<forall>x. \<I> \<turnstile>g x \<surd> \<longrightarrow> (\<forall>xa. I xa \<longrightarrow> a x \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee x xa)))

goal (2 subgoals):
 1. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> 0 \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
 2. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (2 subgoals):
 1. \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> 0 \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
 2. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee gpv s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee gpv s)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
case (step expectation_gpv')
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv 0 \<I> f ?gpv
\<lbrakk>\<I> \<turnstile>g ?gpv \<surd>; I ?s\<rbrakk> \<Longrightarrow> expectation_gpv' ?gpv \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee ?gpv ?s)
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
expectation_gpv' ?gpv \<le> expectation_gpv 0 \<I> f ?gpv
\<lbrakk>\<I> \<turnstile>g ?gpv \<surd>; I ?s\<rbrakk> \<Longrightarrow> expectation_gpv' ?gpv \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee ?gpv ?s)
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
fix out c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
assume IO: "IO out c \<in> set_spmf (the_gpv gpv)"
[PROOF STATE]
proof (state)
this:
IO out c \<in> set_spmf (the_gpv gpv)

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
with step.prems (1)
[PROOF STATE]
proof (chain)
picking this:
\<I> \<turnstile>g gpv \<surd>
IO out c \<in> set_spmf (the_gpv gpv)
[PROOF STEP]
have out: "out \<in> outs_\<I> \<I>"
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
IO out c \<in> set_spmf (the_gpv gpv)

goal (1 subgoal):
 1. out \<in> outs_\<I> \<I>
[PROOF STEP]
by(rule WT_gpv_OutD)
[PROOF STATE]
proof (state)
this:
out \<in> outs_\<I> \<I>

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
have "(INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) = \<integral>\<^sup>+ generat. (INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) = \<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out))
[PROOF STEP]
using WT_callee[OF out, of s] callee[OF out, of s] \<open>I s\<close>
[PROOF STATE]
proof (prove)
using this:
I s \<Longrightarrow> \<I>' \<turnstile>g callee s out \<surd>
I s \<Longrightarrow> plossless_gpv \<I>' (callee s out)
I s

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) = \<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out))
[PROOF STEP]
by(clarsimp simp add: measure_spmf.emeasure_eq_measure plossless_iff_colossless_pfinite colossless_gpv_lossless_spmfD lossless_weight_spmfD)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) = \<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) = \<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
have "\<dots> \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow>
            \<integral>\<^sup>+ xx. (case xx of Inl (x, _) \<Rightarrow> f x
               | Inr (out', callee', rpv) \<Rightarrow> INF r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r'))
            \<partial>measure_spmf (inline1 callee (c x) s')
         | IO out' rpv \<Rightarrow> INF r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))
       \<partial>measure_spmf (the_gpv (callee s out))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))
[PROOF STEP]
proof(rule nn_integral_mono_AE; simp split!: generat.split)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
fix x s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
assume Pure: "Pure (x, s') \<in> set_spmf (the_gpv (callee s out))"
[PROOF STATE]
proof (state)
this:
Pure (x, s') \<in> set_spmf (the_gpv (callee s out))

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
hence "(x, s') \<in> results_gpv \<I>' (callee s out)"
[PROOF STATE]
proof (prove)
using this:
Pure (x, s') \<in> set_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. (x, s') \<in> results_gpv \<I>' (callee s out)
[PROOF STEP]
by(rule results_gpv.Pure)
[PROOF STATE]
proof (state)
this:
(x, s') \<in> results_gpv \<I>' (callee s out)

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
with results_callee[OF out, of s] \<open>I s\<close>
[PROOF STATE]
proof (chain)
picking this:
I s \<Longrightarrow> results_gpv \<I>' (callee s out) \<subseteq> responses_\<I> \<I> out \<times> {s. I s}
I s
(x, s') \<in> results_gpv \<I>' (callee s out)
[PROOF STEP]
have x: "x \<in> responses_\<I> \<I> out" and "I s'"
[PROOF STATE]
proof (prove)
using this:
I s \<Longrightarrow> results_gpv \<I>' (callee s out) \<subseteq> responses_\<I> \<I> out \<times> {s. I s}
I s
(x, s') \<in> results_gpv \<I>' (callee s out)

goal (1 subgoal):
 1. x \<in> responses_\<I> \<I> out &&& I s'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
x \<in> responses_\<I> \<I> out
I s'

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> responses_\<I> \<I> out
[PROOF STEP]
have "(INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> expectation_gpv' (c x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> responses_\<I> \<I> out

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> expectation_gpv' (c x)
[PROOF STEP]
by(rule INF_lower)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> expectation_gpv' (c x)

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> expectation_gpv' (c x)

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
have "\<dots> \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv' (c x) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s')
[PROOF STEP]
by(rule step.IH)(rule WT_gpv_ContD[OF step.prems(1) IO x] step.prems \<open>I s'\<close>|assumption)+
[PROOF STATE]
proof (state)
this:
expectation_gpv' (c x) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s')

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
expectation_gpv' (c x) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s')

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ xx. (case xx of Inl (x, _) \<Rightarrow> f x
               | Inr (out', callee', rpv) \<Rightarrow> INF r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r'))
            \<partial>measure_spmf (inline1 callee (c x) s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s') = \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c x) s') = \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')
[PROOF STEP]
by(subst expectation_gpv.simps)(auto simp add: inline_sel split_def o_def intro!: nn_integral_cong split: generat.split sum.split)
[PROOF STATE]
proof (state)
this:
expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c x) s') = \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')

goal (2 subgoals):
 1. \<And>a b. Pure (a, b) \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (inline1 callee (c a) b)) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))
 2. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')
[PROOF STEP]
show "(INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s')

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
fix out' rpv
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
assume IO': "IO out' rpv \<in> set_spmf (the_gpv (callee s out))"
[PROOF STATE]
proof (state)
this:
IO out' rpv \<in> set_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
have "(INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (INF (r, s')\<in>(\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r')). expectation_gpv' (c r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r))
[PROOF STEP]
using IO' results_callee[OF out, of s] \<open>I s\<close>
[PROOF STATE]
proof (prove)
using this:
IO out' rpv \<in> set_spmf (the_gpv (callee s out))
I s \<Longrightarrow> results_gpv \<I>' (callee s out) \<subseteq> responses_\<I> \<I> out \<times> {s. I s}
I s

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r))
[PROOF STEP]
by(intro INF_mono)(auto intro: results_gpv.IO)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
have "\<dots> = (INF r'\<in>responses_\<I> \<I>' out'. INF (r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) = (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. \<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r))
[PROOF STEP]
by(simp add: INF_UNION)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) = (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. \<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>\<Union>r'\<in>responses_\<I> \<I>' out'. results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) = (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. \<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
have "\<dots> \<le> (INF r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. \<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))
[PROOF STEP]
proof(rule INF_mono, rule bexI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
fix r'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
assume r': "r' \<in> responses_\<I> \<I>' out'"
[PROOF STATE]
proof (state)
this:
r' \<in> responses_\<I> \<I>' out'

goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
have "(INF (r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (INF (r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s'))
[PROOF STEP]
using IO IO' step.prems out results_callee[OF out, of s] r'
[PROOF STATE]
proof (prove)
using this:
IO out c \<in> set_spmf (the_gpv gpv)
IO out' rpv \<in> set_spmf (the_gpv (callee s out))
\<I> \<turnstile>g gpv \<surd>
I s
out \<in> outs_\<I> \<I>
I s \<Longrightarrow> results_gpv \<I>' (callee s out) \<subseteq> responses_\<I> \<I> out \<times> {s. I s}
r' \<in> responses_\<I> \<I>' out'

goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s'))
[PROOF STEP]
by(auto intro!: INF_mono rev_bexI step.IH dest: WT_gpv_ContD intro: results_gpv.IO)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s'))

goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s'))

goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
have "\<dots> \<le>  expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s')) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r) s')) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')
[PROOF STEP]
using plossless_gpv_ContD[OF callee, OF out \<open>I s\<close> IO' r'] WT_callee[OF out \<open>I s\<close>] IO' r'
[PROOF STATE]
proof (prove)
using this:
\<I>' \<turnstile>g callee s out \<surd> \<Longrightarrow> plossless_gpv \<I>' (rpv r')
\<I>' \<turnstile>g callee s out \<surd>
IO out' rpv \<in> set_spmf (the_gpv (callee s out))
r' \<in> responses_\<I> \<I>' out'

goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r) s')) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')
[PROOF STEP]
by(intro plossless_INF_le_expectation_gpv)(auto intro: WT_gpv_ContD)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv2 (\<lambda>(x, s). f x) (inline callee (c r) s')) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')

goal (2 subgoals):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv (?r'2 m)). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv m)
 2. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> ?r'2 m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')
[PROOF STEP]
show "(INF (r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')

goal (1 subgoal):
 1. (\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')

goal (1 subgoal):
 1. \<And>m. m \<in> responses_\<I> \<I>' out' \<Longrightarrow> m \<in> responses_\<I> \<I>' out'
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r'\<in>responses_\<I> \<I>' out'. \<Sqinter>(r, s')\<in>results_gpv \<I>' (rpv r'). expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))

goal (1 subgoal):
 1. \<And>x21 x22. IO x21 x22 \<in> set_spmf (the_gpv (callee s out)) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' x21. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (x22 r'))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))
[PROOF STEP]
show "(INF r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))

goal (1 subgoal):
 1. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> (\<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (callee s out)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
(\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
IO ?out2 ?c2 \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> ?out2. expectation_gpv' (?c2 r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (?c2 x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (?c2 r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s ?out2))

goal (1 subgoal):
 1. \<And>expectation_gpv' gpv s. \<lbrakk>\<And>gpv. expectation_gpv' gpv \<le> expectation_gpv 0 \<I> f gpv; \<And>gpv s. \<lbrakk>\<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> expectation_gpv' gpv \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s); \<I> \<turnstile>g gpv \<surd>; I s\<rbrakk> \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>(x, s). f x) (inline callee gpv s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IO ?out2 ?c2 \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> ?out2. expectation_gpv' (?c2 r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (?c2 x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (?c2 r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s ?out2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
IO ?out2 ?c2 \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> ?out2. expectation_gpv' (?c2 r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (?c2 x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (?c2 r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s ?out2))

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee gpv s)
[PROOF STEP]
unfolding expectation_gpv2_def
[PROOF STATE]
proof (prove)
using this:
IO ?out2 ?c2 \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> ?out2. expectation_gpv' (?c2 r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (?c2 x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (?c2 r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s ?out2))

goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv 0 \<I>' (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee gpv s)
[PROOF STEP]
apply(rewrite expectation_gpv.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (c r)) \<partial>measure_spmf (the_gpv (inline callee gpv s)) + 0 * ennreal (pmf (the_gpv (inline callee gpv s)) None)
[PROOF STEP]
apply(rewrite inline_sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (c r)) \<partial>measure_spmf (map_spmf (\<lambda>result. case result of Inl xs \<Rightarrow> Pure xs | Inr (out, oracle, rpv) \<Rightarrow> IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, s'). inline callee (rpv x) s'))) (inline1 callee gpv s)) + 0 * ennreal (pmf (the_gpv (inline callee gpv s)) None)
[PROOF STEP]
apply(simp add: o_def pmf_map_spmf_None)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case case x of Inl x \<Rightarrow> Pure x | Inr (out, oracle, rpv) \<Rightarrow> IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline callee (rpv x) y)) of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (c r)) \<partial>measure_spmf (inline1 callee gpv s)
[PROOF STEP]
apply(rewrite sum.case_distrib[where h="case_generat _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case x of Inl x \<Rightarrow> case Pure x of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (c r) | Inr x \<Rightarrow> case case x of (out, oracle, rpv) \<Rightarrow> IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline callee (rpv x) y)) of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (c r)) \<partial>measure_spmf (inline1 callee gpv s)
[PROOF STEP]
apply(simp cong del: sum.case_cong_weak)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case x of Inl (xa, s) \<Rightarrow> f xa | Inr x \<Rightarrow> case case x of (out, oracle, rpv) \<Rightarrow> IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline callee (rpv x) y)) of Pure (xa, s) \<Rightarrow> f xa | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I>' out. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (c r)) \<partial>measure_spmf (inline1 callee gpv s)
[PROOF STEP]
apply(simp add: split_beta o_def cong del: sum.case_cong_weak)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case x of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>measure_spmf (inline1 callee gpv s)
[PROOF STEP]
apply(rewrite inline1.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case x of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>measure_spmf (the_gpv gpv \<bind> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv)))))
[PROOF STEP]
apply(rewrite measure_spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. (case x of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>measure_spmf (the_gpv gpv) \<bind> measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv))))
[PROOF STEP]
apply(rewrite nn_integral_bind[where B="measure_spmf _"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> (\<lambda>x. case x of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<in> borel_measurable (measure_spmf ?uu1339)
 2. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv)))) \<in> measure_spmf (the_gpv gpv) \<rightarrow>\<^sub>M subprob_algebra (measure_spmf ?uu1339)
 3. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case y of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>(measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv))))) x \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv)))) \<in> measure_spmf (the_gpv gpv) \<rightarrow>\<^sub>M subprob_algebra (measure_spmf ?uu1339)
 2. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case y of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>(measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv))))) x \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply(simp add: space_subprob_algebra)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r))) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case y of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>(measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv))))) x \<partial>measure_spmf (the_gpv gpv)
[PROOF STEP]
apply(rule nn_integral_mono_AE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ generat. (case generat of Pure (x, s') \<Rightarrow> \<integral>\<^sup>+ xx. (case xx of Inl (x, xa) \<Rightarrow> f x | Inr (out', callee', rpv) \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')) \<partial>measure_spmf (inline1 callee (c x) s') | IO out' rpv \<Rightarrow> \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r')) \<partial>measure_spmf (the_gpv (callee s out))) \<Longrightarrow> AE x in measure_spmf (the_gpv gpv). (case x of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> \<integral>\<^sup>+ y. (case y of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>(measure_spmf \<circ> case_generat (\<lambda>x. return_spmf (Inl (x, s))) (\<lambda>out rpv. the_gpv (callee s out) \<bind> case_generat (\<lambda>(x, y). inline1 callee (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv))))) x
[PROOF STEP]
apply(clarsimp split!: generat.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); Pure x1 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> f x1 \<le> integral\<^sup>N (measure_spmf (return_spmf (Inl (x1, s)))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))
 2. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s x21) \<bind> case_generat (\<lambda>(x, y). inline1 callee (x22 x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', x22))))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))
[PROOF STEP]
apply(simp add: measure_spmf_return_spmf nn_integral_return)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s x21) \<bind> case_generat (\<lambda>(x, y). inline1 callee (x22 x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', x22))))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))
[PROOF STEP]
apply(rewrite measure_spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s x21)) \<bind> measure_spmf \<circ> case_generat (\<lambda>(x, y). inline1 callee (x22 x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', x22)))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))
[PROOF STEP]
apply(simp add: nn_integral_bind[where B="measure_spmf _"] space_subprob_algebra)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. (case y of Inl x \<Rightarrow> f (fst x) | Inr x \<Rightarrow> \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)) \<partial>measure_spmf (case x of Pure (xa, xb) \<Rightarrow> inline1 callee (x22 xa) xb | IO out rpv' \<Rightarrow> return_spmf (Inr (out, rpv', x22))) \<partial>measure_spmf (the_gpv (callee s x21))
[PROOF STEP]
apply(subst generat.case_distrib[where h="measure_spmf"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> \<integral>\<^sup>+ x. integral\<^sup>N (case x of Pure x \<Rightarrow> measure_spmf (case x of (x, xa) \<Rightarrow> inline1 callee (x22 x) xa) | IO x1 x2 \<Rightarrow> measure_spmf (return_spmf (Inr (x1, x2, x22)))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa))) \<partial>measure_spmf (the_gpv (callee s x21))
[PROOF STEP]
apply(subst generat.case_distrib[where h="\<lambda>x. nn_integral x _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>\<And>out c. IO out c \<in> set_spmf (the_gpv gpv) \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s out))) (case_generat (\<lambda>(x, s'). integral\<^sup>N (measure_spmf (inline1 callee (c x) s')) (case_sum (\<lambda>(x, xa). f x) (\<lambda>(out', callee', rpv). \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r, s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (rpv r) s')) (callee' r')))) (\<lambda>out' rpv. \<Sqinter>r'\<in>responses_\<I> \<I>' out'. expectation_gpv 0 \<I>' (\<lambda>(r', s'). expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (c r') s')) (rpv r'))); IO x21 x22 \<in> set_spmf (the_gpv gpv)\<rbrakk> \<Longrightarrow> (\<Sqinter>r\<in>responses_\<I> \<I> x21. expectation_gpv' (x22 r)) \<le> integral\<^sup>N (measure_spmf (the_gpv (callee s x21))) (case_generat (\<lambda>x. integral\<^sup>N (measure_spmf (case x of (x, xa) \<Rightarrow> inline1 callee (x22 x) xa)) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))) (\<lambda>x1 x2. integral\<^sup>N (measure_spmf (return_spmf (Inr (x1, x2, x22)))) (case_sum (\<lambda>x. f (fst x)) (\<lambda>x. \<Sqinter>xa\<in>responses_\<I> \<I>' (fst x). expectation_gpv 0 \<I>' (\<lambda>xa. expectation_gpv 0 \<I>' (\<lambda>(x, s). f x) (inline callee (snd (snd x) (fst xa)) (snd xa))) (fst (snd x) xa)))))
[PROOF STEP]
apply(simp add: measure_spmf_return_spmf nn_integral_return split_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv gpv) + 0 * ennreal (pmf (the_gpv gpv) None) \<le> expectation_gpv2 (\<lambda>a. case a of (x, s) \<Rightarrow> f x) (inline callee gpv s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma plossless_inline:
  assumes lossless: "plossless_gpv \<I> gpv"
    and WT: "\<I> \<turnstile>g gpv \<surd>"
    and callee: "\<And>s x. \<lbrakk> I s; x \<in> outs_\<I> \<I> \<rbrakk> \<Longrightarrow> plossless_gpv \<I>' (callee s x)"
    and I: "I s"
  shows "plossless_gpv \<I>' (inline callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. plossless_gpv \<I>' (inline callee gpv s)
[PROOF STEP]
unfolding pgen_lossless_gpv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) = 1
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> 1
 2. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
have WT': "\<I>' \<turnstile>g inline callee gpv s \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>' \<turnstile>g inline callee gpv s \<surd>
[PROOF STEP]
using WT I
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>g gpv \<surd>
I s

goal (1 subgoal):
 1. \<I>' \<turnstile>g inline callee gpv s \<surd>
[PROOF STEP]
by(rule WT_gpv_inline_invar)
[PROOF STATE]
proof (state)
this:
\<I>' \<turnstile>g inline callee gpv s \<surd>

goal (2 subgoals):
 1. expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> 1
 2. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
from expectation_gpv_const_le[OF WT', of 0 1]
[PROOF STATE]
proof (chain)
picking this:
expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> max 1 0
[PROOF STEP]
show "expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> max 1 0

goal (1 subgoal):
 1. expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> 1
[PROOF STEP]
by(simp add: max_def)
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s) \<le> 1

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
have "1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
using lossless
[PROOF STATE]
proof (prove)
using this:
plossless_gpv \<I> gpv

goal (1 subgoal):
 1. 1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv
[PROOF STEP]
by(simp add: pgen_lossless_gpv_def)
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = expectation_gpv 0 \<I> (\<lambda>_. 1) gpv

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
have "\<dots> \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
by(rule expectation_gpv_le_inline[unfolded split_def]; rule callee I WT)
[PROOF STATE]
proof (state)
this:
expectation_gpv 0 \<I> (\<lambda>_. 1) gpv \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
show "1 \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)

goal (1 subgoal):
 1. 1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 \<le> expectation_gpv 0 \<I>' (\<lambda>_. 1) (inline callee gpv s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expectation_left_gpv [simp]:
  "expectation_gpv fail (\<I> \<oplus>\<^sub>\<I> \<I>') f (left_gpv gpv) = expectation_gpv fail \<I> f gpv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation_gpv fail (\<I> \<oplus>\<^sub>\<I> \<I>') f (left_gpv gpv) = expectation_gpv fail \<I> f gpv
[PROOF STEP]
proof(induction arbitrary: gpv rule: parallel_fixp_induct_1_1[OF complete_lattice_partial_function_definitions complete_lattice_partial_function_definitions expectation_gpv.mono expectation_gpv.mono expectation_gpv_def expectation_gpv_def, case_names adm bottom step])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (left_gpv xa) = snd x xa)
 2. \<And>gpv. \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (left_gpv xa) = snd x xa)
 2. \<And>gpv. \<Squnion> {} = \<Squnion> {}
 3. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (left_gpv xa) = snd x xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ccpo.admissible (prod_lub lfp.lub_fun lfp.lub_fun) (rel_prod lfp.le_fun lfp.le_fun) (\<lambda>x. \<forall>xa. fst x (left_gpv xa) = snd x xa)

goal (2 subgoals):
 1. \<And>gpv. \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>gpv. \<Squnion> {} = \<Squnion> {}
 2. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> {} = \<Squnion> {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Squnion> {} = \<Squnion> {}

goal (1 subgoal):
 1. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
case (step expectation_gpv' expectation_gpv'')
[PROOF STATE]
proof (state)
this:
expectation_gpv' (left_gpv ?gpv) = expectation_gpv'' ?gpv

goal (1 subgoal):
 1. \<And>fa g gpv. (\<And>gpv. fa (left_gpv gpv) = g gpv) \<Longrightarrow> integral\<^sup>N (measure_spmf (the_gpv (left_gpv gpv))) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. fa (c r))) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = integral\<^sup>N (measure_spmf (the_gpv gpv)) (case_generat f (\<lambda>out c. \<Sqinter>r\<in>responses_\<I> \<I> out. g (c r))) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (left_gpv gpv)) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)
[PROOF STEP]
by (auto simp add: pmf_map_spmf_None o_def case_map_generat image_comp
      split: generat.split intro!: nn_integral_cong_AE INF_cong step.IH)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> (\<I> \<oplus>\<^sub>\<I> \<I>') out. expectation_gpv' (c r)) \<partial>measure_spmf (the_gpv (left_gpv gpv)) + fail * ennreal (pmf (the_gpv (left_gpv gpv)) None) = \<integral>\<^sup>+ generat. (case generat of Pure x \<Rightarrow> f x | IO out c \<Rightarrow> \<Sqinter>r\<in>responses_\<I> \<I> out. expectation_gpv'' (c r)) \<partial>measure_spmf (the_gpv gpv) + fail * ennreal (pmf (the_gpv gpv) None)

goal:
No subgoals!
[PROOF STEP]
qed