[STATEMENT]
lemma reduction_step1':
  shows "\<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (\<lambda> view. (A1 view (m0,m1))))) True -
                  spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1 view (m0,m1))))) True\<bar>
                        \<le> adv_OT12"
  (is "?lhs \<le> adv_OT12")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
have int1: "integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True)"
    and int2: "integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True) &&& integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)
[PROOF STEP]
by(rule measure_spmf.integrable_const_bound[where B=1]; simp add: pmf_le_1)+
[PROOF STATE]
proof (state)
this:
integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True)
integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
have "?lhs =
            \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True
              - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>
[PROOF STEP]
apply(subst (1 2) spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>(LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True) - (LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>
[PROOF STEP]
using int1 int2
[PROOF STATE]
proof (prove)
using this:
integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True)
integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)

goal (1 subgoal):
 1. \<bar>(LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True) - (LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True)\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
have "... \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
               \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>
[PROOF STEP]
by(rule integral_abs_bound[THEN order_trans]; simp add: split_beta)
[PROOF STATE]
proof (state)
this:
\<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>
\<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>
[PROOF STEP]
have "?lhs \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
                      \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> = \<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar>
\<bar>LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). spmf (case x of (m0, m1) \<Rightarrow> R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True - spmf (case x of (m0, m1) \<Rightarrow> S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
have "LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf).
                \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view::'v_OT121. A1 view x)) True
                    - spmf (S1_OT12 x () \<bind> (\<lambda>view::'v_OT121. A1 view x)) True\<bar> \<le> adv_OT12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> adv_OT12
[PROOF STEP]
apply(rule integral_mono[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) (\<lambda>x. \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>)
 2. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 3. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 4. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
apply(rule measure_spmf.integrable_const_bound[where B=2])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. AE x in measure_spmf (pair_spmf coin_spmf coin_spmf). norm \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> 2
 2. (\<lambda>x. \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>) \<in> borel_measurable (measure_spmf (pair_spmf coin_spmf coin_spmf))
 3. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 4. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 5. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<bar>spmf (R1_OT12 (a, b) c0 \<bind> (\<lambda>view. A1 view (a, b))) True - spmf (S1_OT12 (a, b) () \<bind> (\<lambda>view. A1 view (a, b))) True\<bar> \<le> 2
 2. (\<lambda>x. \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>) \<in> borel_measurable (measure_spmf (pair_spmf coin_spmf coin_spmf))
 3. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 4. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 5. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
apply(rule abs_triangle_ineq4[THEN order_trans])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<bar>spmf (R1_OT12 (a, b) c0 \<bind> (\<lambda>view. A1 view (a, b))) True\<bar> + \<bar>spmf (S1_OT12 (a, b) () \<bind> (\<lambda>view. A1 view (a, b))) True\<bar> \<le> 2
 2. (\<lambda>x. \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>) \<in> borel_measurable (measure_spmf (pair_spmf coin_spmf coin_spmf))
 3. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 4. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 5. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
subgoal for m0 m1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> + \<bar>spmf (S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> 2
[PROOF STEP]
using pmf_le_1[of "R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))" "Some True"]
        pmf_le_1[of "S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))" "Some True"]
[PROOF STATE]
proof (prove)
using this:
spmf (R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True \<le> 1
spmf (S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True \<le> 1

goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> + \<bar>spmf (S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1))) True\<bar> \<le> 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>x. \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>) \<in> borel_measurable (measure_spmf (pair_spmf coin_spmf coin_spmf))
 2. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 3. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 4. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. integrable (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1
 2. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g1 x
 3. integral\<^sup>L (measure_spmf (pair_spmf coin_spmf coin_spmf)) ?g1 \<le> adv_OT12
[PROOF STEP]
apply(rule measure_spmf.integrable_const)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> ?g17
 2. LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). ?g17 \<le> adv_OT12
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> space (measure_spmf (pair_spmf coin_spmf coin_spmf)) \<Longrightarrow> \<bar>spmf (R1_OT12 (a, b) c0 \<bind> (\<lambda>view. A1 view (a, b))) True - spmf (S1_OT12 (a, b) () \<bind> (\<lambda>view. A1 view (a, b))) True\<bar> \<le> ?g17
 2. LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). ?g17 \<le> adv_OT12
[PROOF STEP]
apply(rule OT_12_P1_assms_bound'[rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). adv_OT12 \<le> adv_OT12
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> adv_OT12

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>
LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> adv_OT12
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar>
LINT x|measure_spmf (pair_spmf coin_spmf coin_spmf). \<bar>spmf (R1_OT12 x c0 \<bind> (\<lambda>view. A1 view x)) True - spmf (S1_OT12 x () \<bind> (\<lambda>view. A1 view x)) True\<bar> \<le> adv_OT12

goal (1 subgoal):
 1. \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar> \<le> adv_OT12

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduction_step2:
  shows "\<exists> A1. \<bar>spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True\<bar> =
          \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1 view (m0,m1))))) True -
            spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
define A1' where "A1' == \<lambda> (view :: 'v_OT121) (m0,m1). do {
    S2 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a :: 'v_OT121 \<leftarrow> S1_OT12 (S2,S3) ();
    c :: 'v_OT121 \<leftarrow> R1_OT12 (S4, S5) c1;
    let R = (M, (S2,S3, m0, m1, S4, S5), a, view, c);
    D R}"
[PROOF STATE]
proof (state)
this:
A1' \<equiv> \<lambda>view (m0, m1). coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. Let (M, (S2, S3, m0, m1, S4, S5), a, view, c) D))))))

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
have "\<bar>spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True\<bar> =
       \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1' view (m0,m1))))) True -
        spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1' view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
have "(bind_spmf (R1_14_interm1 M (c0, c1)) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1' view (m0,m1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1_14_interm1 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
unfolding R1_14_interm1_def R1_14_interm2_def A1'_def Let_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S0, S1) () \<bind> (\<lambda>a. R1_OT12 (S2, S3) (snd (c0, c1)) \<bind> (\<lambda>b. R1_OT12 (S4, S5) (snd (c0, c1)) \<bind> (\<lambda>c. return_spmf (M, (S0, S1, S2, S3, S4, S5), a, b, c)))))))))) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>p. R1_OT12 (fst p, snd p) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (S2, S3, fst (fst p, snd p), snd (fst p, snd p), S4, S5), a, view, c)))))))))
[PROOF STEP]
apply(simp add: pair_spmf_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (S2, S3, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (yb, S3, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
R1_14_interm1 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R1_14_interm1 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
have "(bind_spmf (R1_14_interm2 M (c0, c1)) D) =  (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1' view (m0,m1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
unfolding R1_14_interm1_def R1_14_interm2_def A1'_def Let_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S0, S1) () \<bind> (\<lambda>a. S1_OT12 (S2, S3) () \<bind> (\<lambda>b. R1_OT12 (S4, S5) (snd (c0, c1)) \<bind> (\<lambda>c. return_spmf (M, (S0, S1, S2, S3, S4, S5), a, b, c)))))))))) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>p. S1_OT12 (fst p, snd p) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (S2, S3, fst (fst p, snd p), snd (fst p, snd p), S4, S5), a, view, c)))))))))
[PROOF STEP]
apply(simp add: pair_spmf_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (S2, S3, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, S3) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (yb, S3, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, S4, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. R1_OT12 (yd, S5) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, yd, S5), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>view. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, yd, ye), a, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (y, ya) () \<bind> (\<lambda>view. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (yb, yc, y, ya, yd, ye), yf, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>"  in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (ya, yc) () \<bind> (\<lambda>yf. S1_OT12 (y, yb) () \<bind> (\<lambda>view. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (ya, yc, y, yb, yd, ye), yf, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (ya, yb) () \<bind> (\<lambda>yf. S1_OT12 (y, yc) () \<bind> (\<lambda>view. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (ya, yb, y, yc, yd, ye), yf, view, c))))))))))
[PROOF STEP]
apply(rewrite in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, yb) () \<bind> (\<lambda>yf. S1_OT12 (ya, yc) () \<bind> (\<lambda>view. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (y, yb, ya, yc, yd, ye), yf, view, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>"  in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>view. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, yc, yd, ye), yf, view, c))))))))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R1_14_interm1 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R1_14_interm1 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A1. \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduction_step3:
  shows "\<exists> A1. \<bar>spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) True\<bar> =
          \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1 view (m0,m1))))) True -
            spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
define A1' where "A1' == \<lambda> (view :: 'v_OT121) (m0,m1). do {
    S2 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a :: 'v_OT121 \<leftarrow> S1_OT12 (S2,S3) ();
    b :: 'v_OT121 \<leftarrow> S1_OT12 (S4, S5) ();
    let R = (M, (S2,S3, S4, S5,m0, m1), a, b, view);
    D R}"
[PROOF STATE]
proof (state)
this:
A1' \<equiv> \<lambda>view (m0, m1). coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. Let (M, (S2, S3, S4, S5, m0, m1), a, b, view) D))))))

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
have "\<bar>spmf (bind_spmf (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) True\<bar> =
       \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1' view (m0,m1))))) True -
        spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1' view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
have "(bind_spmf (R1_14_interm2 M (c0, c1)) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A1' view (m0,m1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
unfolding  R1_14_interm2_def A1'_def Let_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S0, S1) () \<bind> (\<lambda>a. S1_OT12 (S2, S3) () \<bind> (\<lambda>b. R1_OT12 (S4, S5) (snd (c0, c1)) \<bind> (\<lambda>c. return_spmf (M, (S0, S1, S2, S3, S4, S5), a, b, c)))))))))) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>p. R1_OT12 (fst p, snd p) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (S2, S3, S4, S5, fst (fst p, snd p), snd (fst p, snd p)), a, b, view)))))))))
[PROOF STEP]
apply(simp add: pair_spmf_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (S2, S3, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (yb, S3, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (yb, yc, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (yd, S5) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (yd, ye) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, ye, y, ya), a, b, view))))))))))
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. R1_OT12 (yd, ye) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. R1_OT12 (y, ya) c1 \<bind> (\<lambda>view. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (yd, ye) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, ye, y, ya), a, b, view))))))))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
have "(bind_spmf (S1_14 M out) D) = (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1' view (m0,m1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S1_14 M out \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
unfolding S1_14_def Let_def A1'_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S0, S1) () \<bind> (\<lambda>a. S1_OT12 (S2, S3) () \<bind> (\<lambda>b. S1_OT12 (S4, S5) () \<bind> (\<lambda>c. return_spmf (M, (S0, S1, S2, S3, S4, S5), a, b, c)))))))))) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>p. S1_OT12 (fst p, snd p) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (S2, S3, S4, S5, fst (fst p, snd p), snd (fst p, snd p)), a, b, view)))))))))
[PROOF STEP]
apply(simp add: pair_spmf_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (S2, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (S2, S3, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, S3) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (yb, S3, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (S4, S5) () \<bind> (\<lambda>b. D (M, (yb, yc, S4, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S5. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (yd, S5) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, S5, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>view. S1_OT12 (yb, yc) () \<bind> (\<lambda>a. S1_OT12 (yd, ye) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, ye, y, ya), a, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (y, ya) () \<bind> (\<lambda>view. S1_OT12 (yd, ye) () \<bind> (\<lambda>b. D (M, (yb, yc, yd, ye, y, ya), yf, b, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (y, ya, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (ya, y) () \<bind> (\<lambda>yf. S1_OT12 (yb, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (ya, y, yb, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, y) () \<bind> (\<lambda>yf. S1_OT12 (ya, yc) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (yb, y, ya, yc, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yc, y) () \<bind> (\<lambda>yf. S1_OT12 (ya, yb) () \<bind> (\<lambda>yg. S1_OT12 (yd, ye) () \<bind> (\<lambda>yh. D (M, (yc, y, ya, yb, yd, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yd, y) () \<bind> (\<lambda>yf. S1_OT12 (ya, yb) () \<bind> (\<lambda>yg. S1_OT12 (yc, ye) () \<bind> (\<lambda>yh. D (M, (yd, y, ya, yb, yc, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yd, y) () \<bind> (\<lambda>yf. S1_OT12 (yb, ya) () \<bind> (\<lambda>yg. S1_OT12 (yc, ye) () \<bind> (\<lambda>yh. D (M, (yd, y, yb, ya, yc, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yd, y) () \<bind> (\<lambda>yf. S1_OT12 (yc, ya) () \<bind> (\<lambda>yg. S1_OT12 (yb, ye) () \<bind> (\<lambda>yh. D (M, (yd, y, yc, ya, yb, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yc, y) () \<bind> (\<lambda>yf. S1_OT12 (yd, ya) () \<bind> (\<lambda>yg. S1_OT12 (yb, ye) () \<bind> (\<lambda>yh. D (M, (yc, y, yd, ya, yb, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yc, y) () \<bind> (\<lambda>yf. S1_OT12 (yd, ya) () \<bind> (\<lambda>yg. S1_OT12 (yb, ye) () \<bind> (\<lambda>yh. D (M, (yc, y, yd, ya, yb, ye), yf, yg, yh)))))))))) = coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (yb, yc) () \<bind> (\<lambda>yf. S1_OT12 (yd, ye) () \<bind> (\<lambda>yg. S1_OT12 (y, ya) () \<bind> (\<lambda>view. D (M, (yb, yc, yd, ye, y, ya), yf, yg, view))))))))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
S1_14 M out \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
S1_14 M out \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R1_14_interm2 M (c0, c1) \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))
S1_14 M out \<bind> D = pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))

goal (1 subgoal):
 1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A1. \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>

goal:
No subgoals!
[PROOF STEP]
qed