[STATEMENT]
lemma reduction_P1_interm:
  shows "\<bar>spmf (bind_spmf (R1_14 M (c0,c1)) (D)) True - spmf (bind_spmf (S1_14 M out) (D)) True\<bar> \<le> 3 * adv_OT12"
    (is "?lhs \<le> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
have lhs: "?lhs \<le> \<bar>spmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True\<bar> +
                     \<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 (R1_14_interm2 M (c0, c1)) D) True - spmf (bind_spmf (S1_14 M out) D) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
obtain A1 where A1: "\<bar>spmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 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) 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>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<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> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reduction_step1
[PROOF STATE]
proof (prove)
using this:
\<exists>A1. \<bar>spmf (R1_14 ?M (?c0.0, ?c1.0) \<bind> ?D) True - spmf (R1_14_interm1 ?M (?c0.0, ?c1.0) \<bind> ?D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) ?c0.0 \<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. (\<And>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<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> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<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>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
obtain A2 where A2: "\<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. (A2 view (m0,m1))))) True -
                          spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A2 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A2. \<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. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reduction_step2
[PROOF STATE]
proof (prove)
using this:
\<exists>A1. \<bar>spmf (R1_14_interm1 ?M (?c0.0, ?c1.0) \<bind> ?D) True - spmf (R1_14_interm2 ?M (?c0.0, ?c1.0) \<bind> ?D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) ?c1.0 \<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. (\<And>A2. \<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. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[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. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
obtain A3 where A3: "\<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. (A3 view (m0,m1))))) True -
                          spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A3 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A3. \<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. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reduction_step3
[PROOF STATE]
proof (prove)
using this:
\<exists>A1. \<bar>spmf (R1_14_interm2 ?M (?c0.0, ?c1.0) \<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.0 \<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. (\<And>A3. \<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. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[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. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
have lhs_bound: "?lhs \<le> \<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> +
                   \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A2 view (m0,m1))))) True -
                    spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A2 view (m0,m1))))) True\<bar> +
                     \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A3 view (m0,m1))))) True -
                      spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A3 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<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>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> + \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>
[PROOF STEP]
using A1 A2 A3 lhs
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<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>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. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar>
\<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. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm1 M (c0, c1) \<bind> D) True - spmf (R1_14_interm2 M (c0, c1) \<bind> D) True\<bar> + \<bar>spmf (R1_14_interm2 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<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>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> + \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<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>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> + \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
have bound1: "\<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"
    and bound2: "\<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A2 view (m0,m1))))) True -
                  spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A2 view (m0,m1))))) True\<bar>
                      \<le> adv_OT12"
    and bound3: "\<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c1) (\<lambda> view. (A3 view (m0,m1))))) True -
        spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A3 view (m0,m1))))) True\<bar> \<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 &&& \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<le> adv_OT12 &&& \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
using reduction_step1'
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) ?c0.0 \<bind> (\<lambda>view. ?A1.0 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. ?A1.0 view (m0, m1)))) 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 &&& \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<le> adv_OT12 &&& \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<le> adv_OT12
[PROOF STEP]
by auto
[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
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<le> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<le> adv_OT12

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
thus ?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> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<le> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<le> adv_OT12

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
using reduction_step1' lhs_bound
[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> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> \<le> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar> \<le> adv_OT12
\<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) ?c0.0 \<bind> (\<lambda>view. ?A1.0 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. ?A1.0 view (m0, m1)))) True\<bar> \<le> adv_OT12
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> \<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>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A2 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A2 view (m0, m1)))) True\<bar> + \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c1 \<bind> (\<lambda>view. A3 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A3 view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (S1_14 M out \<bind> D) True\<bar> \<le> 3 * adv_OT12

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduction_P1: "\<bar>spmf (bind_spmf (R1_14 M (c0,c1)) (D)) True
                        - spmf (funct_OT_14 M (c0,c1) \<bind> (\<lambda> (out1,out2). S1_14 M out1 \<bind> (\<lambda> view. D view))) True\<bar>
                              \<le> 3 * adv_OT12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (funct_OT_14 M (c0, c1) \<bind> (\<lambda>(out1, out2). S1_14 M out1 \<bind> D)) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
by(simp add: funct_OT_14_def split_def Let_def reduction_P1_interm )


[STATEMENT]
lemma coin_coin: "map_spmf (\<lambda> S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
have lhs: "?lhs = map_spmf (\<lambda> S0. S0 \<oplus> (S3 \<oplus> m1)) coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
have op_eq: "... = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf
[PROOF STEP]
by (metis xor_bool_def)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
have "... = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf
[PROOF STEP]
using xor_uni_samp
[PROOF STATE]
proof (prove)
using this:
map_spmf ((\<oplus>) ?y) coin_spmf = map_spmf (\<lambda>b. b) coin_spmf

goal (1 subgoal):
 1. map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
using op_eq
[PROOF STATE]
proof (prove)
using this:
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf
map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf = coin_spmf
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf ((\<oplus>) (S3 \<oplus> m1)) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coin_coin': "map_spmf (\<lambda> S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
have "map_spmf (\<lambda> S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda> S3. S3 \<oplus> S0 \<oplus> m1) coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S3. S3 \<oplus> S0 \<oplus> m1) coin_spmf
[PROOF STEP]
by (metis xor_left_commute)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S3. S3 \<oplus> S0 \<oplus> m1) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S3. S3 \<oplus> S0 \<oplus> m1) coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
using coin_coin
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = map_spmf (\<lambda>S3. S3 \<oplus> S0 \<oplus> m1) coin_spmf
map_spmf (\<lambda>S0. S0 \<oplus> ?S3.0 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf = coin_spmf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_R2_14: "lossless_spmf (R2_14 M C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (R2_14 M C)
[PROOF STEP]
by(simp add: R2_14_def split_def lossless_R2_12)


[STATEMENT]
lemma lossless_S2_14: "lossless_spmf (S2_14 c out)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (S2_14 c out)
[PROOF STEP]
by(simp add: S2_14_def lossless_S2_12 split_def)


[STATEMENT]
lemma P2_OT_14_FT: "R2_14 (m0,m1,m2,m3) (False,True) = funct_OT_14 (m0,m1,m2,m3) (False,True) \<bind> (\<lambda> (out1, out2). S2_14 (False,True) out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
have "R2_14 (m0,m1,m2,m3) (False,True) =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> map_spmf (\<lambda> S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 \<leftarrow> map_spmf (\<lambda> S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
have "... =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 \<leftarrow> coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin'
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. ?S0.0 \<oplus> S3 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
have "... =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 :: bool \<leftarrow> coin_spmf;
    a3 \<leftarrow> map_spmf (\<lambda> S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
have "... =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 :: bool \<leftarrow> coin_spmf;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((False,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S0. S0 \<oplus> ?S3.0 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R2_14 (m0, m1, m2, m3) (False, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R2_14 (m0, m1, m2, m3) (False, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. map_spmf (\<lambda>S1. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((False, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)
[PROOF STEP]
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, True) = funct_OT_14 (m0, m1, m2, m3) (False, True) \<bind> (\<lambda>(out1, out2). S2_14 (False, True) out2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P2_OT_14_TT: "R2_14 (m0,m1,m2,m3) (True,True) = funct_OT_14 (m0,m1,m2,m3) (True,True) \<bind> (\<lambda> (out1, out2). S2_14 (True,True) out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
have "R2_14 (m0,m1,m2,m3) (True,True) =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> map_spmf (\<lambda> S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 \<leftarrow> map_spmf (\<lambda> S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm Let_def)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, True) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
have "... = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    let a1 = S0 \<oplus> S3 \<oplus> m1;
    a2 \<leftarrow> coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin'
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. ?S0.0 \<oplus> S3 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. map_spmf (\<lambda>S2. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in map_spmf (\<lambda>S4. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
have "... = do {
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    a1 :: bool \<leftarrow> map_spmf (\<lambda> S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf;
    a2 \<leftarrow> coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. let a1 = S0 \<oplus> S3 \<oplus> m1 in coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
have "... = do {
    S1 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    a1 :: bool \<leftarrow> coin_spmf;
    a2 \<leftarrow> coin_spmf;
    let a3 = S1 \<oplus> S5 \<oplus> m3;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 True S3;
    c :: 'v_OT122 \<leftarrow> S2_OT12 True S5;
    return_spmf ((True,True), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S0. S0 \<oplus> ?S3.0 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R2_14 (m0, m1, m2, m3) (True, True) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R2_14 (m0, m1, m2, m3) (True, True) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. map_spmf (\<lambda>S0. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. let a3 = S1 \<oplus> S5 \<oplus> m3 in S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 True S3 \<bind> (\<lambda>b. S2_OT12 True S5 \<bind> (\<lambda>c. return_spmf ((True, True), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)
[PROOF STEP]
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, True) = funct_OT_14 (m0, m1, m2, m3) (True, True) \<bind> (\<lambda>(out1, out2). S2_14 (True, True) out2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P2_OT_14_FF: "R2_14 (m0,m1,m2,m3) (False, False) = funct_OT_14 (m0,m1,m2,m3) (False, False) \<bind> (\<lambda> (out1, out2). S2_14 (False, False) out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
have "R2_14 (m0,m1,m2,m3) (False,False) =  do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> map_spmf (\<lambda> S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> map_spmf (\<lambda> S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def R2_14_def inf_th_OT12_P2 funct_OT_12_def OT_12_P2_assm Let_def)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
have "... = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
[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>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin'
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. ?S0.0 \<oplus> S3 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
have "... = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> coin_spmf;
    a2 :: bool \<leftarrow> map_spmf (\<lambda> S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
[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>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
have "... = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> coin_spmf;
    a2 :: bool \<leftarrow> coin_spmf;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 False S0;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((False,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S0. S0 \<oplus> ?S3.0 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R2_14 (m0, m1, m2, m3) (False, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R2_14 (m0, m1, m2, m3) (False, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. map_spmf (\<lambda>S1. S1 \<oplus> S4 \<oplus> m2) coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a2. coin_spmf \<bind> (\<lambda>a3. S2_OT12 False S0 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((False, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)
[PROOF STEP]
by(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (False, False) = funct_OT_14 (m0, m1, m2, m3) (False, False) \<bind> (\<lambda>(out1, out2). S2_14 (False, False) out2)

goal:
No subgoals!
[PROOF STEP]
qed