[STATEMENT]
lemma gtt_comp_asound:
  assumes "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  shows "agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<subseteq> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<subseteq> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
proof (intro subrelI, goal_cases LR)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
case (LR s t)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
obtain q where q: "q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s" "q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using LR
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: agtt_lang_def)
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
(* prepare symmetric cases: q |\<in>| gtt_states \<G>\<^sub>1 and q |\<in>| gtt_states \<G>\<^sub>2 *)
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
fix \<G>\<^sub>1 \<G>\<^sub>2 s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
assume as2: "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
      and 1: "q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm s)"
        "q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm t)" "q |\<in>| gtt_states \<G>\<^sub>1"
[PROOF STATE]
proof (state)
this:
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm s)
q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm t)
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
note st = GTT_comp_first[OF 1(1,3) as2]
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (fst \<G>\<^sub>1) (term_of_gterm s)

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
obtain u where u: "q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u)" "gtt_accept \<G>\<^sub>2 u t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u); gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using gtt_comp_sound_semi[OF as2 1[folded gta_der_def]]
[PROOF STATE]
proof (prove)
using this:
\<exists>u. q |\<in>| gta_der (snd \<G>\<^sub>1) u \<and> gtt_accept \<G>\<^sub>2 u t

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u); gtt_accept \<G>\<^sub>2 u t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: gta_der_def)
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u)
gtt_accept \<G>\<^sub>2 u t

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
have "(s, u) \<in> agtt_lang \<G>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, u) \<in> agtt_lang \<G>\<^sub>1
[PROOF STEP]
using st u(1)
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der (fst \<G>\<^sub>1) (term_of_gterm s)
q |\<in>| ta_der (snd \<G>\<^sub>1) (term_of_gterm u)

goal (1 subgoal):
 1. (s, u) \<in> agtt_lang \<G>\<^sub>1
[PROOF STEP]
by (auto simp: agtt_lang_def gta_der_def)
[PROOF STATE]
proof (state)
this:
(s, u) \<in> agtt_lang \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s, u) \<in> agtt_lang \<G>\<^sub>1

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
have "(u, t) \<in> gtt_lang \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, t) \<in> gtt_lang \<G>\<^sub>2
[PROOF STEP]
using u(2)
[PROOF STATE]
proof (prove)
using this:
gtt_accept \<G>\<^sub>2 u t

goal (1 subgoal):
 1. (u, t) \<in> gtt_lang \<G>\<^sub>2
[PROOF STEP]
by (auto simp: gtt_accept_def)
[PROOF STATE]
proof (state)
this:
(u, t) \<in> gtt_lang \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(s, u) \<in> agtt_lang \<G>\<^sub>1
(u, t) \<in> gtt_lang \<G>\<^sub>2
[PROOF STEP]
have "(s, t) \<in> agtt_lang \<G>\<^sub>1 O gmctxt_cl UNIV (agtt_lang \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
(s, u) \<in> agtt_lang \<G>\<^sub>1
(u, t) \<in> gtt_lang \<G>\<^sub>2

goal (1 subgoal):
 1. (s, t) \<in> agtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, t) \<in> agtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>gtt_states ?\<G>\<^sub>1'2 |\<inter>| gtt_states ?\<G>\<^sub>2'2 = {||}; q |\<in>| ta_der (fst (GTT_comp ?\<G>\<^sub>1'2 ?\<G>\<^sub>2'2)) (term_of_gterm ?sa2); q |\<in>| ta_der (snd (GTT_comp ?\<G>\<^sub>1'2 ?\<G>\<^sub>2'2)) (term_of_gterm ?ta2); q |\<in>| gtt_states ?\<G>\<^sub>1'2\<rbrakk> \<Longrightarrow> (?sa2, ?ta2) \<in> agtt_lang ?\<G>\<^sub>1'2 O gtt_lang ?\<G>\<^sub>2'2

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
note base = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>gtt_states ?\<G>\<^sub>1'2 |\<inter>| gtt_states ?\<G>\<^sub>2'2 = {||}; q |\<in>| ta_der (fst (GTT_comp ?\<G>\<^sub>1'2 ?\<G>\<^sub>2'2)) (term_of_gterm ?sa2); q |\<in>| ta_der (snd (GTT_comp ?\<G>\<^sub>1'2 ?\<G>\<^sub>2'2)) (term_of_gterm ?ta2); q |\<in>| gtt_states ?\<G>\<^sub>1'2\<rbrakk> \<Longrightarrow> (?sa2, ?ta2) \<in> agtt_lang ?\<G>\<^sub>1'2 O gtt_lang ?\<G>\<^sub>2'2

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
consider "q |\<in>| gtt_states \<G>\<^sub>1" | "q |\<in>| gtt_states \<G>\<^sub>2" | "q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> thesis; q |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> thesis; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> ?thesis; q |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> (x, y) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> ?thesis; q |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> ?thesis; q |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
using q assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>q |\<in>| gtt_states \<G>\<^sub>1 \<Longrightarrow> ?thesis; q |\<in>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
proof (cases, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 2. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 3. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>1

goal (3 subgoals):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 2. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 3. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>1

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
using base[of \<G>\<^sub>1 \<G>\<^sub>2 s t]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>1
\<lbrakk>gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| ta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm s); q |\<in>| ta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) (term_of_gterm t); q |\<in>| gtt_states \<G>\<^sub>1\<rbrakk> \<Longrightarrow> (s, t) \<in> agtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: gcomp_rel_def gta_der_def)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal (2 subgoals):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 2. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 2. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>2

goal (2 subgoals):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<in>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
 2. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
using base[of "prod.swap \<G>\<^sub>2" "prod.swap \<G>\<^sub>1" t s, THEN converseI]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<in>| gtt_states \<G>\<^sub>2
\<lbrakk>gtt_states (prod.swap \<G>\<^sub>2) |\<inter>| gtt_states (prod.swap \<G>\<^sub>1) = {||}; q |\<in>| ta_der (fst (GTT_comp (prod.swap \<G>\<^sub>2) (prod.swap \<G>\<^sub>1))) (term_of_gterm t); q |\<in>| ta_der (snd (GTT_comp (prod.swap \<G>\<^sub>2) (prod.swap \<G>\<^sub>1))) (term_of_gterm s); q |\<in>| gtt_states (prod.swap \<G>\<^sub>2)\<rbrakk> \<Longrightarrow> (s, t) \<in> (agtt_lang (prod.swap \<G>\<^sub>2) O gtt_lang (prod.swap \<G>\<^sub>1))\<inverse>

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: gcomp_rel_def converse_relcomp converse_agtt_lang gta_der_def gtt_states_def)
         (simp add: finter_commute funion_commute gtt_lang_swap prod.swap_def)+
[PROOF STATE]
proof (state)
this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal (1 subgoal):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. \<lbrakk>q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s; q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t; gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}; q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2\<rbrakk> \<Longrightarrow> (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
using fsubsetD[OF gtt_states_comp_union[of \<G>\<^sub>1 \<G>\<^sub>2], of q]
[PROOF STATE]
proof (prove)
using this:
q |\<in>| gta_der (fst (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) s
q |\<in>| gta_der (snd (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)) t
gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}
q |\<notin>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2
q |\<in>| gtt_states (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) \<Longrightarrow> q |\<in>| gtt_states \<G>\<^sub>1 |\<union>| gtt_states \<G>\<^sub>2

goal (1 subgoal):
 1. (s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
by (auto simp: gta_der_def gtt_states_def)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(s, t) \<in> gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gtt_comp_lang_complete:
  shows "gtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2 \<subseteq> gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2 \<subseteq> gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
using gmctxt_cl_mono_rel[OF gtt_comp_acomplete, of UNIV \<G>\<^sub>1 \<G>\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
gmctxt_cl UNIV (gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)) \<subseteq> gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)

goal (1 subgoal):
 1. gtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2 \<subseteq> gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2)
[PROOF STEP]
by (simp only: gcomp_rel[symmetric])


[STATEMENT]
lemma gtt_comp_alang:
  assumes "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  shows "agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
by (intro equalityI gtt_comp_asound[OF assms] gtt_comp_acomplete)


[STATEMENT]
lemma gtt_comp_lang:
  assumes "gtt_states \<G>\<^sub>1 |\<inter>| gtt_states \<G>\<^sub>2 = {||}"
  shows "gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) = gtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtt_lang (GTT_comp \<G>\<^sub>1 \<G>\<^sub>2) = gtt_lang \<G>\<^sub>1 O gtt_lang \<G>\<^sub>2
[PROOF STEP]
by (simp only: arg_cong[OF gtt_comp_alang[OF assms], of "gmctxt_cl UNIV"] gcomp_rel)


[STATEMENT]
lemma gtt_comp'_alang:
  shows "agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
have [simp]: "finj_on Inl (gtt_states \<G>\<^sub>1)" "finj_on Inr (gtt_states \<G>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finj_on Inl (gtt_states \<G>\<^sub>1) &&& finj_on Inr (gtt_states \<G>\<^sub>2)
[PROOF STEP]
by (auto simp add: finj_on.rep_eq)
[PROOF STATE]
proof (state)
this:
finj_on Inl (gtt_states \<G>\<^sub>1)
finj_on Inr (gtt_states \<G>\<^sub>2)

goal (1 subgoal):
 1. agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finj_on Inl (gtt_states \<G>\<^sub>1)
finj_on Inr (gtt_states \<G>\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finj_on Inl (gtt_states \<G>\<^sub>1)
finj_on Inr (gtt_states \<G>\<^sub>2)

goal (1 subgoal):
 1. agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)
[PROOF STEP]
by (subst gtt_comp_alang) (auto simp: agtt_lang_fmap_states_gtt)
[PROOF STATE]
proof (state)
this:
agtt_lang (GTT_comp' \<G>\<^sub>1 \<G>\<^sub>2) = gcomp_rel UNIV (agtt_lang \<G>\<^sub>1) (agtt_lang \<G>\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma an_sds: "an_sds agents alts sds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an_sds agents alts sds
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma ex_post_efficient_sds: "ex_post_efficient_sds agents alts sds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ex_post_efficient_sds agents alts sds
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma sd_efficient_sds: "sd_efficient_sds agents alts sds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sd_efficient_sds agents alts sds
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma strategyproof_an_sds: "strategyproof_an_sds agents alts sds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strategyproof_an_sds agents alts sds
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma distinct_agents' [simp]:
  "A1 \<noteq> A2" "A1 \<noteq> A3" "A1 \<noteq> A4" "A2 \<noteq> A1" "A2 \<noteq> A3" "A2 \<noteq> A4"
  "A3 \<noteq> A1" "A3 \<noteq> A2" "A3 \<noteq> A4" "A4 \<noteq> A1" "A4 \<noteq> A2" "A4 \<noteq> A3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A1 \<noteq> A2 &&& A1 \<noteq> A3 &&& A1 \<noteq> A4) &&& A2 \<noteq> A1 &&& A2 \<noteq> A3 &&& A2 \<noteq> A4) &&& (A3 \<noteq> A1 &&& A3 \<noteq> A2 &&& A3 \<noteq> A4) &&& A4 \<noteq> A1 &&& A4 \<noteq> A2 &&& A4 \<noteq> A3
[PROOF STEP]
using distinct_agents
[PROOF STATE]
proof (prove)
using this:
distinct [A1, A2, A3, A4]

goal (1 subgoal):
 1. ((A1 \<noteq> A2 &&& A1 \<noteq> A3 &&& A1 \<noteq> A4) &&& A2 \<noteq> A1 &&& A2 \<noteq> A3 &&& A2 \<noteq> A4) &&& (A3 \<noteq> A1 &&& A3 \<noteq> A2 &&& A3 \<noteq> A4) &&& A4 \<noteq> A1 &&& A4 \<noteq> A2 &&& A4 \<noteq> A3
[PROOF STEP]
by auto


[STATEMENT]
lemma distinct_alts' [simp]:
  "a \<noteq> b" "a \<noteq> c" "a \<noteq> d" "b \<noteq> a" "b \<noteq> c" "b \<noteq> d"
  "c \<noteq> a" "c \<noteq> b" "c \<noteq> d" "d \<noteq> a" "d \<noteq> b" "d \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a \<noteq> b &&& a \<noteq> c &&& a \<noteq> d) &&& b \<noteq> a &&& b \<noteq> c &&& b \<noteq> d) &&& (c \<noteq> a &&& c \<noteq> b &&& c \<noteq> d) &&& d \<noteq> a &&& d \<noteq> b &&& d \<noteq> c
[PROOF STEP]
using distinct_alts
[PROOF STATE]
proof (prove)
using this:
distinct [a, b, c, d]

goal (1 subgoal):
 1. ((a \<noteq> b &&& a \<noteq> c &&& a \<noteq> d) &&& b \<noteq> a &&& b \<noteq> c &&& b \<noteq> d) &&& (c \<noteq> a &&& c \<noteq> b &&& c \<noteq> d) &&& d \<noteq> a &&& d \<noteq> b &&& d \<noteq> c
[PROOF STEP]
by auto


[STATEMENT]
lemma card_agents [simp]: "card agents = 4" and card_alts [simp]: "card alts = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card agents = 4 &&& card alts = 4
[PROOF STEP]
using distinct_agents distinct_alts
[PROOF STATE]
proof (prove)
using this:
distinct [A1, A2, A3, A4]
distinct [a, b, c, d]

goal (1 subgoal):
 1. card agents = 4 &&& card alts = 4
[PROOF STEP]
by (simp_all add: agents alts)


[STATEMENT]
lemma in_agents [simp]: "A1 \<in> agents" "A2 \<in> agents" "A3 \<in> agents" "A4 \<in> agents"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A1 \<in> agents &&& A2 \<in> agents) &&& A3 \<in> agents &&& A4 \<in> agents
[PROOF STEP]
by (simp_all add: agents)


[STATEMENT]
lemma in_alts [simp]: "a \<in> alts" "b \<in> alts" "c \<in> alts" "d \<in> alts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in> alts &&& b \<in> alts) &&& c \<in> alts &&& d \<in> alts
[PROOF STEP]
by (simp_all add: alts)


[STATEMENT]
lemma agent_iff: "x \<in> agents \<longleftrightarrow> x \<in> {A1, A2, A3, A4}"
                 "(\<forall>x\<in>agents. P x) \<longleftrightarrow> P A1 \<and> P A2 \<and> P A3 \<and> P A4"
                 "(\<exists>x\<in>agents. P x) \<longleftrightarrow> P A1 \<or> P A2 \<or> P A3 \<or> P A4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> agents) = (x \<in> {A1, A2, A3, A4}) &&& (\<forall>x\<in>agents. P x) = (P A1 \<and> P A2 \<and> P A3 \<and> P A4) &&& (\<exists>x\<in>agents. P x) = (P A1 \<or> P A2 \<or> P A3 \<or> P A4)
[PROOF STEP]
by (auto simp add: agents)


[STATEMENT]
lemma alt_iff: "x \<in> alts \<longleftrightarrow> x \<in> {a,b,c,d}"
               "(\<forall>x\<in>alts. P x) \<longleftrightarrow> P a \<and> P b \<and> P c \<and> P d"
               "(\<exists>x\<in>alts. P x) \<longleftrightarrow> P a \<or> P b \<or> P c \<or> P d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> alts) = (x \<in> {a, b, c, d}) &&& (\<forall>x\<in>alts. P x) = (P a \<and> P b \<and> P c \<and> P d) &&& (\<exists>x\<in>alts. P x) = (P a \<or> P b \<or> P c \<or> P d)
[PROOF STEP]
by (auto simp add: alts)


[STATEMENT]
lemma lottery_conditions:
  assumes "is_pref_profile R"
  shows   "pmf (sds R) a \<ge> 0" "pmf (sds R) b \<ge> 0" "pmf (sds R) c \<ge> 0" "pmf (sds R) d \<ge> 0"
          "pmf (sds R) a + pmf (sds R) b + pmf (sds R) c + pmf (sds R) d = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> pmf (sds R) a &&& 0 \<le> pmf (sds R) b) &&& 0 \<le> pmf (sds R) c &&& 0 \<le> pmf (sds R) d &&& pmf (sds R) a + pmf (sds R) b + pmf (sds R) c + pmf (sds R) d = 1
[PROOF STEP]
using lottery_prob_alts[OF sds_wf[OF assms]]
[PROOF STATE]
proof (prove)
using this:
lottery_prob (sds R) alts = 1

goal (1 subgoal):
 1. (0 \<le> pmf (sds R) a &&& 0 \<le> pmf (sds R) b) &&& 0 \<le> pmf (sds R) c &&& 0 \<le> pmf (sds R) d &&& pmf (sds R) a + pmf (sds R) b + pmf (sds R) c + pmf (sds R) d = 1
[PROOF STEP]
by (simp_all add: alts pmf_nonneg measure_measure_pmf_finite)


[STATEMENT]
lemma R45 [simp]: "pmf (sds R45) a = 1/4" "pmf (sds R45) b = 1/4"
           "pmf (sds R45) c = 1/4" "pmf (sds R45) d = 1/4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R45) a = 1 / 4 &&& pmf (sds R45) b = 1 / 4) &&& pmf (sds R45) c = 1 / 4 &&& pmf (sds R45) d = 1 / 4
[PROOF STEP]
using R45.orbits lottery_conditions[OF R45.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R45) c = pmf (sds R45) a
pmf (sds R45) d = pmf (sds R45) a
pmf (sds R45) b = pmf (sds R45) a
0 \<le> pmf (sds R45) a
0 \<le> pmf (sds R45) b
0 \<le> pmf (sds R45) c
0 \<le> pmf (sds R45) d
pmf (sds R45) a + pmf (sds R45) b + pmf (sds R45) c + pmf (sds R45) d = 1

goal (1 subgoal):
 1. (pmf (sds R45) a = 1 / 4 &&& pmf (sds R45) b = 1 / 4) &&& pmf (sds R45) c = 1 / 4 &&& pmf (sds R45) d = 1 / 4
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R10_bc [simp]: "pmf (sds R10) b = 0" "pmf (sds R10) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R10) b = 0 &&& pmf (sds R10) c = 0
[PROOF STEP]
using R10.support R10.orbits
[PROOF STATE]
proof (prove)
using this:
pmf (sds R10) c = 0 \<or> pmf (sds R10) b = 0
pmf (sds R10) d = pmf (sds R10) a
pmf (sds R10) c = pmf (sds R10) b

goal (1 subgoal):
 1. pmf (sds R10) b = 0 &&& pmf (sds R10) c = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma R10_ad [simp]: "pmf (sds R10) a = 1/2" "pmf (sds R10) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R10) a = 1 / 2 &&& pmf (sds R10) d = 1 / 2
[PROOF STEP]
using lottery_conditions[OF R10.wf] R10_bc R10.orbits
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R10) a
0 \<le> pmf (sds R10) b
0 \<le> pmf (sds R10) c
0 \<le> pmf (sds R10) d
pmf (sds R10) a + pmf (sds R10) b + pmf (sds R10) c + pmf (sds R10) d = 1
pmf (sds R10) b = 0
pmf (sds R10) c = 0
pmf (sds R10) d = pmf (sds R10) a
pmf (sds R10) c = pmf (sds R10) b

goal (1 subgoal):
 1. pmf (sds R10) a = 1 / 2 &&& pmf (sds R10) d = 1 / 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R26_bc [simp]: "pmf (sds R26) b = 0" "pmf (sds R26) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R26) b = 0 &&& pmf (sds R26) c = 0
[PROOF STEP]
using R26.support R26.orbits
[PROOF STATE]
proof (prove)
using this:
pmf (sds R26) c = 0 \<or> pmf (sds R26) b = 0
pmf (sds R26) c = pmf (sds R26) b

goal (1 subgoal):
 1. pmf (sds R26) b = 0 &&& pmf (sds R26) c = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma R26_d [simp]: "pmf (sds R26) d = 1 - pmf (sds R26) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R26) d = 1 - pmf (sds R26) a
[PROOF STEP]
using lottery_conditions[OF R26.wf] R26_bc
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R26) a
0 \<le> pmf (sds R26) b
0 \<le> pmf (sds R26) c
0 \<le> pmf (sds R26) d
pmf (sds R26) a + pmf (sds R26) b + pmf (sds R26) c + pmf (sds R26) d = 1
pmf (sds R26) b = 0
pmf (sds R26) c = 0

goal (1 subgoal):
 1. pmf (sds R26) d = 1 - pmf (sds R26) a
[PROOF STEP]
by simp


[STATEMENT]
lemma R27_bc [simp]: "pmf (sds R27) b = 0" "pmf (sds R27) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R27) b = 0 &&& pmf (sds R27) c = 0
[PROOF STEP]
using R27.support R27.orbits
[PROOF STATE]
proof (prove)
using this:
pmf (sds R27) c = 0 \<or> pmf (sds R27) b = 0
pmf (sds R27) c = pmf (sds R27) b

goal (1 subgoal):
 1. pmf (sds R27) b = 0 &&& pmf (sds R27) c = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma R27_d [simp]: "pmf (sds R27) d = 1 - pmf (sds R27) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R27) d = 1 - pmf (sds R27) a
[PROOF STEP]
using lottery_conditions[OF R27.wf] R27_bc
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R27) a
0 \<le> pmf (sds R27) b
0 \<le> pmf (sds R27) c
0 \<le> pmf (sds R27) d
pmf (sds R27) a + pmf (sds R27) b + pmf (sds R27) c + pmf (sds R27) d = 1
pmf (sds R27) b = 0
pmf (sds R27) c = 0

goal (1 subgoal):
 1. pmf (sds R27) d = 1 - pmf (sds R27) a
[PROOF STEP]
by simp


[STATEMENT]
lemma R28_bc [simp]: "pmf (sds R28) b = 0" "pmf (sds R28) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R28) b = 0 &&& pmf (sds R28) c = 0
[PROOF STEP]
using R28.support R28.orbits
[PROOF STATE]
proof (prove)
using this:
pmf (sds R28) b = 0 \<or> pmf (sds R28) c = 0
pmf (sds R28) b = pmf (sds R28) c

goal (1 subgoal):
 1. pmf (sds R28) b = 0 &&& pmf (sds R28) c = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma R28_d [simp]: "pmf (sds R28) d = 1 - pmf (sds R28) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R28) d = 1 - pmf (sds R28) a
[PROOF STEP]
using lottery_conditions[OF R28.wf] R28_bc
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R28) a
0 \<le> pmf (sds R28) b
0 \<le> pmf (sds R28) c
0 \<le> pmf (sds R28) d
pmf (sds R28) a + pmf (sds R28) b + pmf (sds R28) c + pmf (sds R28) d = 1
pmf (sds R28) b = 0
pmf (sds R28) c = 0

goal (1 subgoal):
 1. pmf (sds R28) d = 1 - pmf (sds R28) a
[PROOF STEP]
by simp


[STATEMENT]
lemma R29_ac [simp]: "pmf (sds R29) a = 1/2" "pmf (sds R29) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R29) a = 1 / 2 &&& pmf (sds R29) d = 1 / 2
[PROOF STEP]
using lottery_conditions[OF R29.wf] R29_bc R29.orbits
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R29) a
0 \<le> pmf (sds R29) b
0 \<le> pmf (sds R29) c
0 \<le> pmf (sds R29) d
pmf (sds R29) a + pmf (sds R29) b + pmf (sds R29) c + pmf (sds R29) d = 1
pmf (sds R29) b = 0
pmf (sds R29) c = 0
pmf (sds R29) b = pmf (sds R29) c
pmf (sds R29) d = pmf (sds R29) a

goal (1 subgoal):
 1. pmf (sds R29) a = 1 / 2 &&& pmf (sds R29) d = 1 / 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R43_ad [simp]: "pmf (sds R43) a = 1/2" "pmf (sds R43) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R43) a = 1 / 2 &&& pmf (sds R43) d = 1 / 2
[PROOF STEP]
using lottery_conditions[OF R43.wf] R43_bc R43.orbits
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R43) a
0 \<le> pmf (sds R43) b
0 \<le> pmf (sds R43) c
0 \<le> pmf (sds R43) d
pmf (sds R43) a + pmf (sds R43) b + pmf (sds R43) c + pmf (sds R43) d = 1
pmf (sds R43) b = 0
pmf (sds R43) d = pmf (sds R43) a
pmf (sds R43) c = pmf (sds R43) b

goal (1 subgoal):
 1. pmf (sds R43) a = 1 / 2 &&& pmf (sds R43) d = 1 / 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R39_b [simp]: "pmf (sds R39) b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
assume [simp]: "pmf (sds R39) c = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R39) c = 0

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
with R29_R39.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R39) d < pmf (sds R29) a \<or> pmf (sds R39) d + pmf (sds R39) c < pmf (sds R29) a + pmf (sds R29) b) \<or> pmf (sds R39) d = pmf (sds R29) a \<and> pmf (sds R39) d + pmf (sds R39) c = pmf (sds R29) a + pmf (sds R29) b
pmf (sds R39) c = 0
[PROOF STEP]
have "pmf (sds R39) d \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R39) d < pmf (sds R29) a \<or> pmf (sds R39) d + pmf (sds R39) c < pmf (sds R29) a + pmf (sds R29) b) \<or> pmf (sds R39) d = pmf (sds R29) a \<and> pmf (sds R39) d + pmf (sds R39) c = pmf (sds R29) a + pmf (sds R29) b
pmf (sds R39) c = 0

goal (1 subgoal):
 1. pmf (sds R39) d \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R39) d \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
with R39_R29.strategyproofness(1) lottery_conditions[OF R39.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R29) a + pmf (sds R29) b < pmf (sds R39) d + pmf (sds R39) c \<or> pmf (sds R29) a + (pmf (sds R29) b + pmf (sds R29) d) < pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)) \<or> pmf (sds R29) a + pmf (sds R29) b = pmf (sds R39) d + pmf (sds R39) c \<and> pmf (sds R29) a + (pmf (sds R29) b + pmf (sds R29) d) = pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1
pmf (sds R39) d \<le> 1 / 2
[PROOF STEP]
have "pmf (sds R39) b = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R29) a + pmf (sds R29) b < pmf (sds R39) d + pmf (sds R39) c \<or> pmf (sds R29) a + (pmf (sds R29) b + pmf (sds R29) d) < pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)) \<or> pmf (sds R29) a + pmf (sds R29) b = pmf (sds R39) d + pmf (sds R39) c \<and> pmf (sds R29) a + (pmf (sds R29) b + pmf (sds R29) d) = pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1
pmf (sds R39) d \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R39) b = 0

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
pmf (sds R39) c = 0 \<Longrightarrow> pmf (sds R39) b = 0

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
with R39.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R39) b = 0 \<or> pmf (sds R39) c = 0
pmf (sds R39) c = 0 \<Longrightarrow> pmf (sds R39) b = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pmf (sds R39) b = 0 \<or> pmf (sds R39) c = 0
pmf (sds R39) c = 0 \<Longrightarrow> pmf (sds R39) b = 0

goal (1 subgoal):
 1. pmf (sds R39) b = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pmf (sds R39) b = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R36_d [simp]: "pmf (sds R36) d = 1/2 - pmf (sds R36) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R36) d = 1 / 2 - pmf (sds R36) c
[PROOF STEP]
using lottery_conditions[OF R36.wf]
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1

goal (1 subgoal):
 1. pmf (sds R36) d = 1 / 2 - pmf (sds R36) c
[PROOF STEP]
by simp


[STATEMENT]
lemma R39_a [simp]: "pmf (sds R39) a = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R39) a = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R39) a = 1 / 2
[PROOF STEP]
from R36_R39.strategyproofness(1) lottery_conditions[OF R39.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R39) d + pmf (sds R39) c \<le> pmf (sds R36) d + pmf (sds R36) c
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1
[PROOF STEP]
have "pmf (sds R39) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R39) d + pmf (sds R39) c \<le> pmf (sds R36) d + pmf (sds R36) c
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R39) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R39) a

goal (1 subgoal):
 1. pmf (sds R39) a = 1 / 2
[PROOF STEP]
with R39_R36.strategyproofness(1) lottery_conditions[OF R39.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R36) d + pmf (sds R36) c < pmf (sds R39) d + pmf (sds R39) c \<or> pmf (sds R36) d + (pmf (sds R36) c + pmf (sds R36) a) < pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)) \<or> pmf (sds R36) d + pmf (sds R36) c = pmf (sds R39) d + pmf (sds R39) c \<and> pmf (sds R36) d + (pmf (sds R36) c + pmf (sds R36) a) = pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1
1 / 2 \<le> pmf (sds R39) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R36) d + pmf (sds R36) c < pmf (sds R39) d + pmf (sds R39) c \<or> pmf (sds R36) d + (pmf (sds R36) c + pmf (sds R36) a) < pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)) \<or> pmf (sds R36) d + pmf (sds R36) c = pmf (sds R39) d + pmf (sds R39) c \<and> pmf (sds R36) d + (pmf (sds R36) c + pmf (sds R36) a) = pmf (sds R39) d + (pmf (sds R39) c + pmf (sds R39) a)
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1
1 / 2 \<le> pmf (sds R39) a

goal (1 subgoal):
 1. pmf (sds R39) a = 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R39) a = 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R39_d [simp]: "pmf (sds R39) d = 1/2 - pmf (sds R39) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R39) d = 1 / 2 - pmf (sds R39) c
[PROOF STEP]
using lottery_conditions[OF R39.wf]
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R39) a
0 \<le> pmf (sds R39) b
0 \<le> pmf (sds R39) c
0 \<le> pmf (sds R39) d
pmf (sds R39) a + pmf (sds R39) b + pmf (sds R39) c + pmf (sds R39) d = 1

goal (1 subgoal):
 1. pmf (sds R39) d = 1 / 2 - pmf (sds R39) c
[PROOF STEP]
by simp


[STATEMENT]
lemma R12_c [simp]: "pmf (sds R12) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R12) c = 0
[PROOF STEP]
using R12_R10.strategyproofness(1) lottery_conditions[OF R12.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) \<le> pmf (sds R12) d + (pmf (sds R12) b + pmf (sds R12) a)
0 \<le> pmf (sds R12) a
0 \<le> pmf (sds R12) b
0 \<le> pmf (sds R12) c
0 \<le> pmf (sds R12) d
pmf (sds R12) a + pmf (sds R12) b + pmf (sds R12) c + pmf (sds R12) d = 1

goal (1 subgoal):
 1. pmf (sds R12) c = 0
[PROOF STEP]
by (auto simp del: pmf_nonneg)


[STATEMENT]
lemma R12_d [simp]: "pmf (sds R12) d = 1 - pmf (sds R12) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R12) d = 1 - pmf (sds R12) a
[PROOF STEP]
using lottery_conditions[OF R12.wf]
[PROOF STATE]
proof (prove)
using this:
0 \<le> pmf (sds R12) a
0 \<le> pmf (sds R12) b
0 \<le> pmf (sds R12) c
0 \<le> pmf (sds R12) d
pmf (sds R12) a + pmf (sds R12) b + pmf (sds R12) c + pmf (sds R12) d = 1

goal (1 subgoal):
 1. pmf (sds R12) d = 1 - pmf (sds R12) a
[PROOF STEP]
by simp


[STATEMENT]
lemma R12_a_ge_one_half: "pmf (sds R12) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R12) a
[PROOF STEP]
using R10_R12.strategyproofness(1) lottery_conditions[OF R12.wf]
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R12) b + pmf (sds R12) d < pmf (sds R10) c + pmf (sds R10) a \<or> pmf (sds R12) b + (pmf (sds R12) d + pmf (sds R12) a) < pmf (sds R10) c + (pmf (sds R10) a + pmf (sds R10) d)) \<or> pmf (sds R12) b + pmf (sds R12) d = pmf (sds R10) c + pmf (sds R10) a \<and> pmf (sds R12) b + (pmf (sds R12) d + pmf (sds R12) a) = pmf (sds R10) c + (pmf (sds R10) a + pmf (sds R10) d)
0 \<le> pmf (sds R12) a
0 \<le> pmf (sds R12) b
0 \<le> pmf (sds R12) c
0 \<le> pmf (sds R12) d
pmf (sds R12) a + pmf (sds R12) b + pmf (sds R12) c + pmf (sds R12) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R12) a
[PROOF STEP]
by auto


[STATEMENT]
lemma R44 [simp]:
  "pmf (sds R44) a = pmf (sds R12) a" "pmf (sds R44) d = 1 - pmf (sds R12) a"
  "pmf (sds R44) b = 0" "pmf (sds R44) c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R44) a = pmf (sds R12) a &&& pmf (sds R44) d = 1 - pmf (sds R12) a) &&& pmf (sds R44) b = 0 &&& pmf (sds R44) c = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R44) a = pmf (sds R12) a
 2. pmf (sds R44) d = 1 - pmf (sds R12) a
 3. pmf (sds R44) b = 0
 4. pmf (sds R44) c = 0
[PROOF STEP]
from R12_R44.strategyproofness(1) R44.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R44) b + pmf (sds R44) a \<le> pmf (sds R12) b + pmf (sds R12) a
pmf (sds R44) b = 0
[PROOF STEP]
have "pmf (sds R44) a \<le> pmf (sds R12) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R44) b + pmf (sds R44) a \<le> pmf (sds R12) b + pmf (sds R12) a
pmf (sds R44) b = 0

goal (1 subgoal):
 1. pmf (sds R44) a \<le> pmf (sds R12) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R44) a \<le> pmf (sds R12) a

goal (4 subgoals):
 1. pmf (sds R44) a = pmf (sds R12) a
 2. pmf (sds R44) d = 1 - pmf (sds R12) a
 3. pmf (sds R44) b = 0
 4. pmf (sds R44) c = 0
[PROOF STEP]
with R44_R12.strategyproofness(1) R44.support lottery_conditions[OF R44.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R12) b + pmf (sds R12) a < pmf (sds R44) b + pmf (sds R44) a \<or> pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) < pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d)) \<or> pmf (sds R12) b + pmf (sds R12) a = pmf (sds R44) b + pmf (sds R44) a \<and> pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) = pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d)
pmf (sds R44) b = 0
0 \<le> pmf (sds R44) a
0 \<le> pmf (sds R44) b
0 \<le> pmf (sds R44) c
0 \<le> pmf (sds R44) d
pmf (sds R44) a + pmf (sds R44) b + pmf (sds R44) c + pmf (sds R44) d = 1
pmf (sds R44) a \<le> pmf (sds R12) a
[PROOF STEP]
show "pmf (sds R44) a = pmf (sds R12) a" "pmf (sds R44) c = 0"
         "pmf (sds R44) d = 1 - pmf (sds R12) a"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R12) b + pmf (sds R12) a < pmf (sds R44) b + pmf (sds R44) a \<or> pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) < pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d)) \<or> pmf (sds R12) b + pmf (sds R12) a = pmf (sds R44) b + pmf (sds R44) a \<and> pmf (sds R12) b + (pmf (sds R12) a + pmf (sds R12) d) = pmf (sds R44) b + (pmf (sds R44) a + pmf (sds R44) d)
pmf (sds R44) b = 0
0 \<le> pmf (sds R44) a
0 \<le> pmf (sds R44) b
0 \<le> pmf (sds R44) c
0 \<le> pmf (sds R44) d
pmf (sds R44) a + pmf (sds R44) b + pmf (sds R44) c + pmf (sds R44) d = 1
pmf (sds R44) a \<le> pmf (sds R12) a

goal (1 subgoal):
 1. pmf (sds R44) a = pmf (sds R12) a &&& pmf (sds R44) c = 0 &&& pmf (sds R44) d = 1 - pmf (sds R12) a
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R44) a = pmf (sds R12) a
pmf (sds R44) c = 0
pmf (sds R44) d = 1 - pmf (sds R12) a

goal (1 subgoal):
 1. pmf (sds R44) b = 0
[PROOF STEP]
qed (insert R44.support, simp_all)


[STATEMENT]
lemma R9_a [simp]: "pmf (sds R9) a = pmf (sds R35) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R9) a = pmf (sds R35) a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R9) a = pmf (sds R35) a
[PROOF STEP]
from R9_R35.strategyproofness(1) R35.support R9.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R35) b + pmf (sds R35) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R35) b = 0
pmf (sds R9) b = 0
[PROOF STEP]
have "pmf (sds R35) a \<le> pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R35) b + pmf (sds R35) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R35) b = 0
pmf (sds R9) b = 0

goal (1 subgoal):
 1. pmf (sds R35) a \<le> pmf (sds R9) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R35) a \<le> pmf (sds R9) a

goal (1 subgoal):
 1. pmf (sds R9) a = pmf (sds R35) a
[PROOF STEP]
with R35_R9.strategyproofness(1) R9.support R35.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R9) a < pmf (sds R35) a \<or> pmf (sds R9) a + pmf (sds R9) b < pmf (sds R35) a + pmf (sds R35) b) \<or> pmf (sds R9) a = pmf (sds R35) a \<and> pmf (sds R9) a + pmf (sds R9) b = pmf (sds R35) a + pmf (sds R35) b
pmf (sds R9) b = 0
pmf (sds R35) b = 0
pmf (sds R35) a \<le> pmf (sds R9) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R9) a < pmf (sds R35) a \<or> pmf (sds R9) a + pmf (sds R9) b < pmf (sds R35) a + pmf (sds R35) b) \<or> pmf (sds R9) a = pmf (sds R35) a \<and> pmf (sds R9) a + pmf (sds R9) b = pmf (sds R35) a + pmf (sds R35) b
pmf (sds R9) b = 0
pmf (sds R35) b = 0
pmf (sds R35) a \<le> pmf (sds R9) a

goal (1 subgoal):
 1. pmf (sds R9) a = pmf (sds R35) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R9) a = pmf (sds R35) a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R18_c [simp]: "pmf (sds R18) c = pmf (sds R9) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R18) c = pmf (sds R9) c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R18) c = pmf (sds R9) c
[PROOF STEP]
from R18_R9.strategyproofness(1) R18.support R9.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a
pmf (sds R18) b = 0
pmf (sds R9) b = 0
[PROOF STEP]
have "pmf (sds R18) d + pmf (sds R18) a \<ge> pmf (sds R9) d + pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a
pmf (sds R18) b = 0
pmf (sds R9) b = 0

goal (1 subgoal):
 1. pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a

goal (1 subgoal):
 1. pmf (sds R18) c = pmf (sds R9) c
[PROOF STEP]
with R9_R18.strategyproofness(1) R18.support R9.support
        lottery_conditions[OF R9.wf] lottery_conditions[OF R18.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R18) d + pmf (sds R18) a < pmf (sds R9) d + pmf (sds R9) a \<or> pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) < pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c)) \<or> pmf (sds R18) d + pmf (sds R18) a = pmf (sds R9) d + pmf (sds R9) a \<and> pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) = pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c)
pmf (sds R18) b = 0
pmf (sds R9) b = 0
0 \<le> pmf (sds R9) a
0 \<le> pmf (sds R9) b
0 \<le> pmf (sds R9) c
0 \<le> pmf (sds R9) d
pmf (sds R9) a + pmf (sds R9) b + pmf (sds R9) c + pmf (sds R9) d = 1
0 \<le> pmf (sds R18) a
0 \<le> pmf (sds R18) b
0 \<le> pmf (sds R18) c
0 \<le> pmf (sds R18) d
pmf (sds R18) a + pmf (sds R18) b + pmf (sds R18) c + pmf (sds R18) d = 1
pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R18) d + pmf (sds R18) a < pmf (sds R9) d + pmf (sds R9) a \<or> pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) < pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c)) \<or> pmf (sds R18) d + pmf (sds R18) a = pmf (sds R9) d + pmf (sds R9) a \<and> pmf (sds R18) d + (pmf (sds R18) a + pmf (sds R18) c) = pmf (sds R9) d + (pmf (sds R9) a + pmf (sds R9) c)
pmf (sds R18) b = 0
pmf (sds R9) b = 0
0 \<le> pmf (sds R9) a
0 \<le> pmf (sds R9) b
0 \<le> pmf (sds R9) c
0 \<le> pmf (sds R9) d
pmf (sds R9) a + pmf (sds R9) b + pmf (sds R9) c + pmf (sds R9) d = 1
0 \<le> pmf (sds R18) a
0 \<le> pmf (sds R18) b
0 \<le> pmf (sds R18) c
0 \<le> pmf (sds R18) d
pmf (sds R18) a + pmf (sds R18) b + pmf (sds R18) c + pmf (sds R18) d = 1
pmf (sds R9) d + pmf (sds R9) a \<le> pmf (sds R18) d + pmf (sds R18) a

goal (1 subgoal):
 1. pmf (sds R18) c = pmf (sds R9) c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R18) c = pmf (sds R9) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R5_d_ge_one_half: "pmf (sds R5) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R5) d
[PROOF STEP]
using R5_R10.strategyproofness(1) R5.support lottery_conditions[OF R5.wf]
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R10) a < pmf (sds R5) d \<or> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) < pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)) \<or> pmf (sds R10) a = pmf (sds R5) d \<and> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) = pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)
pmf (sds R5) b = 0
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R5) d
[PROOF STEP]
by auto


[STATEMENT]
lemma R7 [simp]: "pmf (sds R7) a = 1/2" "pmf (sds R7) b = 0" "pmf (sds R7) c = 0" "pmf (sds R7) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R7) a = 1 / 2 &&& pmf (sds R7) b = 0) &&& pmf (sds R7) c = 0 &&& pmf (sds R7) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
from R5_d_ge_one_half
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R5) d
[PROOF STEP]
have "1/2 \<le> pmf (sds R5) d"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R5) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R5) d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R5) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R5) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
from R5_R17.strategyproofness(1) R17.support lottery_conditions[OF R5.wf] lottery_conditions[OF R17.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R17) c + pmf (sds R17) a < pmf (sds R5) c + pmf (sds R5) a \<or> pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) \<or> pmf (sds R17) c + pmf (sds R17) a = pmf (sds R5) c + pmf (sds R5) a \<and> pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)
pmf (sds R17) b = 0
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
0 \<le> pmf (sds R17) a
0 \<le> pmf (sds R17) b
0 \<le> pmf (sds R17) c
0 \<le> pmf (sds R17) d
pmf (sds R17) a + pmf (sds R17) b + pmf (sds R17) c + pmf (sds R17) d = 1
[PROOF STEP]
have "\<dots> \<le> pmf (sds R17) d"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R17) c + pmf (sds R17) a < pmf (sds R5) c + pmf (sds R5) a \<or> pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) \<or> pmf (sds R17) c + pmf (sds R17) a = pmf (sds R5) c + pmf (sds R5) a \<and> pmf (sds R17) c + (pmf (sds R17) a + pmf (sds R17) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)
pmf (sds R17) b = 0
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
0 \<le> pmf (sds R17) a
0 \<le> pmf (sds R17) b
0 \<le> pmf (sds R17) c
0 \<le> pmf (sds R17) d
pmf (sds R17) a + pmf (sds R17) b + pmf (sds R17) c + pmf (sds R17) d = 1

goal (1 subgoal):
 1. pmf (sds R5) d \<le> pmf (sds R17) d
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R5) d \<le> pmf (sds R17) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R5) d \<le> pmf (sds R17) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
from R17_R7.strategyproofness(1) lottery_conditions[OF R7.wf] lottery_conditions[OF R17.wf] R7.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R7) c + pmf (sds R7) a \<le> pmf (sds R17) c + pmf (sds R17) a
0 \<le> pmf (sds R7) a
0 \<le> pmf (sds R7) b
0 \<le> pmf (sds R7) c
0 \<le> pmf (sds R7) d
pmf (sds R7) a + pmf (sds R7) b + pmf (sds R7) c + pmf (sds R7) d = 1
0 \<le> pmf (sds R17) a
0 \<le> pmf (sds R17) b
0 \<le> pmf (sds R17) c
0 \<le> pmf (sds R17) d
pmf (sds R17) a + pmf (sds R17) b + pmf (sds R17) c + pmf (sds R17) d = 1
pmf (sds R7) b = 0
[PROOF STEP]
have "pmf (sds R17) d \<le> pmf (sds R7) d"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R7) c + pmf (sds R7) a \<le> pmf (sds R17) c + pmf (sds R17) a
0 \<le> pmf (sds R7) a
0 \<le> pmf (sds R7) b
0 \<le> pmf (sds R7) c
0 \<le> pmf (sds R7) d
pmf (sds R7) a + pmf (sds R7) b + pmf (sds R7) c + pmf (sds R7) d = 1
0 \<le> pmf (sds R17) a
0 \<le> pmf (sds R17) b
0 \<le> pmf (sds R17) c
0 \<le> pmf (sds R17) d
pmf (sds R17) a + pmf (sds R17) b + pmf (sds R17) c + pmf (sds R17) d = 1
pmf (sds R7) b = 0

goal (1 subgoal):
 1. pmf (sds R17) d \<le> pmf (sds R7) d
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R17) d \<le> pmf (sds R7) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R7) d
[PROOF STEP]
have "pmf (sds R7) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R7) d

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R7) d
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R7) d

goal (4 subgoals):
 1. pmf (sds R7) a = 1 / 2
 2. pmf (sds R7) b = 0
 3. pmf (sds R7) c = 0
 4. pmf (sds R7) d = 1 / 2
[PROOF STEP]
with R7_R43.strategyproofness(1) lottery_conditions[OF R7.wf] R7.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R43) d < pmf (sds R7) a \<or> pmf (sds R43) d + pmf (sds R43) b < pmf (sds R7) a + pmf (sds R7) c \<or> pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) < pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d)) \<or> pmf (sds R43) d = pmf (sds R7) a \<and> pmf (sds R43) d + pmf (sds R43) b = pmf (sds R7) a + pmf (sds R7) c \<and> pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) = pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d)
0 \<le> pmf (sds R7) a
0 \<le> pmf (sds R7) b
0 \<le> pmf (sds R7) c
0 \<le> pmf (sds R7) d
pmf (sds R7) a + pmf (sds R7) b + pmf (sds R7) c + pmf (sds R7) d = 1
pmf (sds R7) b = 0
1 / 2 \<le> pmf (sds R7) d
[PROOF STEP]
show "pmf (sds R7) a = 1/2" "pmf (sds R7) b = 0" "pmf (sds R7) c = 0" "pmf (sds R7) d = 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R43) d < pmf (sds R7) a \<or> pmf (sds R43) d + pmf (sds R43) b < pmf (sds R7) a + pmf (sds R7) c \<or> pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) < pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d)) \<or> pmf (sds R43) d = pmf (sds R7) a \<and> pmf (sds R43) d + pmf (sds R43) b = pmf (sds R7) a + pmf (sds R7) c \<and> pmf (sds R43) d + (pmf (sds R43) b + pmf (sds R43) a) = pmf (sds R7) a + (pmf (sds R7) c + pmf (sds R7) d)
0 \<le> pmf (sds R7) a
0 \<le> pmf (sds R7) b
0 \<le> pmf (sds R7) c
0 \<le> pmf (sds R7) d
pmf (sds R7) a + pmf (sds R7) b + pmf (sds R7) c + pmf (sds R7) d = 1
pmf (sds R7) b = 0
1 / 2 \<le> pmf (sds R7) d

goal (1 subgoal):
 1. (pmf (sds R7) a = 1 / 2 &&& pmf (sds R7) b = 0) &&& pmf (sds R7) c = 0 &&& pmf (sds R7) d = 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R7) a = 1 / 2
pmf (sds R7) b = 0
pmf (sds R7) c = 0
pmf (sds R7) d = 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R5 [simp]: "pmf (sds R5) a = 1/2" "pmf (sds R5) b = 0" "pmf (sds R5) c = 0" "pmf (sds R5) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R5) a = 1 / 2 &&& pmf (sds R5) b = 0) &&& pmf (sds R5) c = 0 &&& pmf (sds R5) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R5) a = 1 / 2
 2. pmf (sds R5) b = 0
 3. pmf (sds R5) c = 0
 4. pmf (sds R5) d = 1 / 2
[PROOF STEP]
from R5_R7.strategyproofness(1) lottery_conditions[OF R5.wf] R5.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R7) c + pmf (sds R7) a < pmf (sds R5) c + pmf (sds R5) a \<or> pmf (sds R7) c + (pmf (sds R7) a + pmf (sds R7) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) \<or> pmf (sds R7) c + pmf (sds R7) a = pmf (sds R5) c + pmf (sds R5) a \<and> pmf (sds R7) c + (pmf (sds R7) a + pmf (sds R7) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
pmf (sds R5) b = 0
[PROOF STEP]
have "pmf (sds R5) d \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R7) c + pmf (sds R7) a < pmf (sds R5) c + pmf (sds R5) a \<or> pmf (sds R7) c + (pmf (sds R7) a + pmf (sds R7) d) < pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)) \<or> pmf (sds R7) c + pmf (sds R7) a = pmf (sds R5) c + pmf (sds R5) a \<and> pmf (sds R7) c + (pmf (sds R7) a + pmf (sds R7) d) = pmf (sds R5) c + (pmf (sds R5) a + pmf (sds R5) d)
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
pmf (sds R5) b = 0

goal (1 subgoal):
 1. pmf (sds R5) d \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R5) d \<le> 1 / 2

goal (4 subgoals):
 1. pmf (sds R5) a = 1 / 2
 2. pmf (sds R5) b = 0
 3. pmf (sds R5) c = 0
 4. pmf (sds R5) d = 1 / 2
[PROOF STEP]
with R5_d_ge_one_half
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R5) d
pmf (sds R5) d \<le> 1 / 2
[PROOF STEP]
show d: "pmf (sds R5) d = 1 / 2"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R5) d
pmf (sds R5) d \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R5) d = 1 / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R5) d = 1 / 2

goal (3 subgoals):
 1. pmf (sds R5) a = 1 / 2
 2. pmf (sds R5) b = 0
 3. pmf (sds R5) c = 0
[PROOF STEP]
with R5_R10.strategyproofness(1) lottery_conditions[OF R5.wf] R5.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R10) a < pmf (sds R5) d \<or> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) < pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)) \<or> pmf (sds R10) a = pmf (sds R5) d \<and> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) = pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
pmf (sds R5) b = 0
pmf (sds R5) d = 1 / 2
[PROOF STEP]
show "pmf (sds R5) c = 0" "pmf (sds R5) a = 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R10) a < pmf (sds R5) d \<or> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) < pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)) \<or> pmf (sds R10) a = pmf (sds R5) d \<and> pmf (sds R10) a + (pmf (sds R10) c + pmf (sds R10) d) = pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a)
0 \<le> pmf (sds R5) a
0 \<le> pmf (sds R5) b
0 \<le> pmf (sds R5) c
0 \<le> pmf (sds R5) d
pmf (sds R5) a + pmf (sds R5) b + pmf (sds R5) c + pmf (sds R5) d = 1
pmf (sds R5) b = 0
pmf (sds R5) d = 1 / 2

goal (1 subgoal):
 1. pmf (sds R5) c = 0 &&& pmf (sds R5) a = 1 / 2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
pmf (sds R5) c = 0
pmf (sds R5) a = 1 / 2

goal (1 subgoal):
 1. pmf (sds R5) b = 0
[PROOF STEP]
qed (simp_all add: R5.support)


[STATEMENT]
lemma R15 [simp]: "pmf (sds R15) a = 1/2" "pmf (sds R15) b = 0" "pmf (sds R15) c = 0" "pmf (sds R15) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R15) a = 1 / 2 &&& pmf (sds R15) b = 0) &&& pmf (sds R15) c = 0 &&& pmf (sds R15) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
assume "pmf (sds R15) b = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R15) b = 0

goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
with R10_R15.strategyproofness(1) lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R15) a + pmf (sds R15) c < pmf (sds R10) d + pmf (sds R10) b \<or> pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d) < pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)) \<or> pmf (sds R15) a + pmf (sds R15) c = pmf (sds R10) d + pmf (sds R10) b \<and> pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d) = pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) b = 0
[PROOF STEP]
have "pmf (sds R15) a + pmf (sds R15) c \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R15) a + pmf (sds R15) c < pmf (sds R10) d + pmf (sds R10) b \<or> pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d) < pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)) \<or> pmf (sds R15) a + pmf (sds R15) c = pmf (sds R10) d + pmf (sds R10) b \<and> pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d) = pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) b = 0

goal (1 subgoal):
 1. pmf (sds R15) a + pmf (sds R15) c \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R15) a + pmf (sds R15) c \<le> 1 / 2

goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
with R15_R10.strategyproofness(1) lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R10) d < pmf (sds R15) a \<or> pmf (sds R10) d + pmf (sds R10) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R10) d = pmf (sds R15) a \<and> pmf (sds R10) d + pmf (sds R10) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) a + pmf (sds R15) c \<le> 1 / 2
[PROOF STEP]
have "pmf (sds R15) c = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R10) d < pmf (sds R15) a \<or> pmf (sds R10) d + pmf (sds R10) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R10) d = pmf (sds R15) a \<and> pmf (sds R10) d + pmf (sds R10) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) a + pmf (sds R15) c \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R15) c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R15) c = 0

goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
pmf (sds R15) b = 0 \<Longrightarrow> pmf (sds R15) c = 0

goal (4 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) c = 0
 4. pmf (sds R15) d = 1 / 2
[PROOF STEP]
with R15.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R15) c = 0 \<or> pmf (sds R15) b = 0
pmf (sds R15) b = 0 \<Longrightarrow> pmf (sds R15) c = 0
[PROOF STEP]
show [simp]: "pmf (sds R15) c = 0"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R15) c = 0 \<or> pmf (sds R15) b = 0
pmf (sds R15) b = 0 \<Longrightarrow> pmf (sds R15) c = 0

goal (1 subgoal):
 1. pmf (sds R15) c = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pmf (sds R15) c = 0

goal (3 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) d = 1 / 2
[PROOF STEP]
with R15_R5.strategyproofness(1) lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R5) d < pmf (sds R15) a \<or> pmf (sds R5) d + pmf (sds R5) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R5) d = pmf (sds R15) a \<and> pmf (sds R5) d + pmf (sds R5) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) c = 0
[PROOF STEP]
have "pmf (sds R15) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R5) d < pmf (sds R15) a \<or> pmf (sds R5) d + pmf (sds R5) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R5) d = pmf (sds R15) a \<and> pmf (sds R5) d + pmf (sds R5) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) c = 0

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R15) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R15) a

goal (3 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) d = 1 / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R15) a

goal (3 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) d = 1 / 2
[PROOF STEP]
from R15_R7.strategyproofness(1) lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R7) d + pmf (sds R7) b < pmf (sds R15) d + pmf (sds R15) b \<or> pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) < pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a)) \<or> pmf (sds R7) d + pmf (sds R7) b = pmf (sds R15) d + pmf (sds R15) b \<and> pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) = pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
[PROOF STEP]
have "pmf (sds R15) b + pmf (sds R15) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R7) d + pmf (sds R7) b < pmf (sds R15) d + pmf (sds R15) b \<or> pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) < pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a)) \<or> pmf (sds R7) d + pmf (sds R7) b = pmf (sds R15) d + pmf (sds R15) b \<and> pmf (sds R7) d + (pmf (sds R7) b + pmf (sds R7) a) = pmf (sds R15) d + (pmf (sds R15) b + pmf (sds R15) a)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R15) b + pmf (sds R15) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R15) b + pmf (sds R15) d

goal (3 subgoals):
 1. pmf (sds R15) a = 1 / 2
 2. pmf (sds R15) b = 0
 3. pmf (sds R15) d = 1 / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R15) a
1 / 2 \<le> pmf (sds R15) b + pmf (sds R15) d
[PROOF STEP]
show "pmf (sds R15) a = 1/2"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R15) a
1 / 2 \<le> pmf (sds R15) b + pmf (sds R15) d

goal (1 subgoal):
 1. pmf (sds R15) a = 1 / 2
[PROOF STEP]
using lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R15) a
1 / 2 \<le> pmf (sds R15) b + pmf (sds R15) d
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1

goal (1 subgoal):
 1. pmf (sds R15) a = 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R15) a = 1 / 2

goal (2 subgoals):
 1. pmf (sds R15) b = 0
 2. pmf (sds R15) d = 1 / 2
[PROOF STEP]
with R15_R5.strategyproofness(1) lottery_conditions[OF R15.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R5) d < pmf (sds R15) a \<or> pmf (sds R5) d + pmf (sds R5) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R5) d = pmf (sds R15) a \<and> pmf (sds R5) d + pmf (sds R5) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) a = 1 / 2
[PROOF STEP]
show "pmf (sds R15) d = 1/2" "pmf (sds R15) b = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R5) d < pmf (sds R15) a \<or> pmf (sds R5) d + pmf (sds R5) b < pmf (sds R15) a + pmf (sds R15) c \<or> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) < pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)) \<or> pmf (sds R5) d = pmf (sds R15) a \<and> pmf (sds R5) d + pmf (sds R5) b = pmf (sds R15) a + pmf (sds R15) c \<and> pmf (sds R5) d + (pmf (sds R5) b + pmf (sds R5) a) = pmf (sds R15) a + (pmf (sds R15) c + pmf (sds R15) d)
0 \<le> pmf (sds R15) a
0 \<le> pmf (sds R15) b
0 \<le> pmf (sds R15) c
0 \<le> pmf (sds R15) d
pmf (sds R15) a + pmf (sds R15) b + pmf (sds R15) c + pmf (sds R15) d = 1
pmf (sds R15) a = 1 / 2

goal (1 subgoal):
 1. pmf (sds R15) d = 1 / 2 &&& pmf (sds R15) b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R15) d = 1 / 2
pmf (sds R15) b = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R13_aux: "pmf (sds R13) b = 0" "pmf (sds R13) c = 0" "pmf (sds R13) d = 1 - pmf (sds R13) a"
  and R27_R13 [simp]: "pmf (sds R27) a = pmf (sds R13) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R13) b = 0 &&& pmf (sds R13) c = 0 &&& pmf (sds R13) d = 1 - pmf (sds R13) a) &&& pmf (sds R27) a = pmf (sds R13) a
[PROOF STEP]
using R27_R13.strategyproofness(1) R13_R27.strategyproofness(1) lottery_conditions[OF R13.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R13) b + pmf (sds R13) a \<le> pmf (sds R27) c + pmf (sds R27) a
(pmf (sds R27) a < pmf (sds R13) a \<or> pmf (sds R27) a + pmf (sds R27) c < pmf (sds R13) a + pmf (sds R13) b \<or> pmf (sds R27) a + (pmf (sds R27) c + pmf (sds R27) d) < pmf (sds R13) a + (pmf (sds R13) b + pmf (sds R13) d)) \<or> pmf (sds R27) a = pmf (sds R13) a \<and> pmf (sds R27) a + pmf (sds R27) c = pmf (sds R13) a + pmf (sds R13) b \<and> pmf (sds R27) a + (pmf (sds R27) c + pmf (sds R27) d) = pmf (sds R13) a + (pmf (sds R13) b + pmf (sds R13) d)
0 \<le> pmf (sds R13) a
0 \<le> pmf (sds R13) b
0 \<le> pmf (sds R13) c
0 \<le> pmf (sds R13) d
pmf (sds R13) a + pmf (sds R13) b + pmf (sds R13) c + pmf (sds R13) d = 1

goal (1 subgoal):
 1. (pmf (sds R13) b = 0 &&& pmf (sds R13) c = 0 &&& pmf (sds R13) d = 1 - pmf (sds R13) a) &&& pmf (sds R27) a = pmf (sds R13) a
[PROOF STEP]
by auto


[STATEMENT]
lemma R13 [simp]: "pmf (sds R13) a = 1/2" "pmf (sds R13) b = 0" "pmf (sds R13) c = 0" "pmf (sds R13) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R13) a = 1 / 2 &&& pmf (sds R13) b = 0) &&& pmf (sds R13) c = 0 &&& pmf (sds R13) d = 1 / 2
[PROOF STEP]
using R15_R13.strategyproofness(1) R13_R15.strategyproofness(1) R13_aux
[PROOF STATE]
proof (prove)
using this:
pmf (sds R13) d + pmf (sds R13) b \<le> pmf (sds R15) d + pmf (sds R15) c
(pmf (sds R15) d + pmf (sds R15) c < pmf (sds R13) d + pmf (sds R13) b \<or> pmf (sds R15) d + (pmf (sds R15) c + pmf (sds R15) a) < pmf (sds R13) d + (pmf (sds R13) b + pmf (sds R13) a)) \<or> pmf (sds R15) d + pmf (sds R15) c = pmf (sds R13) d + pmf (sds R13) b \<and> pmf (sds R15) d + (pmf (sds R15) c + pmf (sds R15) a) = pmf (sds R13) d + (pmf (sds R13) b + pmf (sds R13) a)
pmf (sds R13) b = 0
pmf (sds R13) c = 0
pmf (sds R13) d = 1 - pmf (sds R13) a

goal (1 subgoal):
 1. (pmf (sds R13) a = 1 / 2 &&& pmf (sds R13) b = 0) &&& pmf (sds R13) c = 0 &&& pmf (sds R13) d = 1 / 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R27 [simp]: "pmf (sds R27) a = 1/2" "pmf (sds R27) b = 0" "pmf (sds R27) c = 0" "pmf (sds R27) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R27) a = 1 / 2 &&& pmf (sds R27) b = 0) &&& pmf (sds R27) c = 0 &&& pmf (sds R27) d = 1 / 2
[PROOF STEP]
by simp_all


[STATEMENT]
lemma R19 [simp]: "pmf (sds R19) a = 1/2" "pmf (sds R19) b = 0" "pmf (sds R19) c = 0" "pmf (sds R19) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R19) a = 1 / 2 &&& pmf (sds R19) b = 0) &&& pmf (sds R19) c = 0 &&& pmf (sds R19) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0
 4. pmf (sds R19) d = 1 / 2
[PROOF STEP]
have "pmf (sds R19) a = 1/2 \<and> pmf (sds R19) b = 0 \<and> pmf (sds R19) c = 0 \<and> pmf (sds R19) d = 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R19) a = 1 / 2 \<and> pmf (sds R19) b = 0 \<and> pmf (sds R19) c = 0 \<and> pmf (sds R19) d = 1 / 2
[PROOF STEP]
proof (rule disjE[OF R19.support]; safe)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
 6. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
assume [simp]: "pmf (sds R19) b = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R19) b = 0

goal (6 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
 6. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
from R10_R19.strategyproofness(1) lottery_conditions[OF R19.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R19) a + pmf (sds R19) c < pmf (sds R10) d + pmf (sds R10) b \<or> pmf (sds R19) a + (pmf (sds R19) c + pmf (sds R19) d) < pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)) \<or> pmf (sds R19) a + pmf (sds R19) c = pmf (sds R10) d + pmf (sds R10) b \<and> pmf (sds R19) a + (pmf (sds R19) c + pmf (sds R19) d) = pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1
[PROOF STEP]
have "pmf (sds R19) a + pmf (sds R19) c \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R19) a + pmf (sds R19) c < pmf (sds R10) d + pmf (sds R10) b \<or> pmf (sds R19) a + (pmf (sds R19) c + pmf (sds R19) d) < pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)) \<or> pmf (sds R19) a + pmf (sds R19) c = pmf (sds R10) d + pmf (sds R10) b \<and> pmf (sds R19) a + (pmf (sds R19) c + pmf (sds R19) d) = pmf (sds R10) d + (pmf (sds R10) b + pmf (sds R10) a)
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1

goal (1 subgoal):
 1. pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2

goal (6 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
 6. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2

goal (6 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
 6. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
from R19_R10.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R10) b + pmf (sds R10) d \<le> pmf (sds R19) c + pmf (sds R19) a
[PROOF STEP]
have "pmf (sds R19) a + pmf (sds R19) c \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R10) b + pmf (sds R10) d \<le> pmf (sds R19) c + pmf (sds R19) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R19) a + pmf (sds R19) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R19) a + pmf (sds R19) c

goal (6 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
 6. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2
1 / 2 \<le> pmf (sds R19) a + pmf (sds R19) c
[PROOF STEP]
show "pmf (sds R19) d = 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2
1 / 2 \<le> pmf (sds R19) a + pmf (sds R19) c

goal (1 subgoal):
 1. pmf (sds R19) d = 1 / 2
[PROOF STEP]
using lottery_conditions[OF R19.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R19) a + pmf (sds R19) c \<le> 1 / 2
1 / 2 \<le> pmf (sds R19) a + pmf (sds R19) c
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1

goal (1 subgoal):
 1. pmf (sds R19) d = 1 / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R19) d = 1 / 2

goal (5 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
 4. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 5. pmf (sds R19) b = 0 \<Longrightarrow> pmf (sds R19) c = 0
[PROOF STEP]
with R27_R19.strategyproofness(1) lottery_conditions[OF R19.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R19) d + pmf (sds R19) c < pmf (sds R27) d + pmf (sds R27) b \<or> pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) < pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a)) \<or> pmf (sds R19) d + pmf (sds R19) c = pmf (sds R27) d + pmf (sds R27) b \<and> pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) = pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a)
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1
pmf (sds R19) d = 1 / 2
[PROOF STEP]
show "pmf (sds R19) a = 1/2" "pmf (sds R19) c = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R19) d + pmf (sds R19) c < pmf (sds R27) d + pmf (sds R27) b \<or> pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) < pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a)) \<or> pmf (sds R19) d + pmf (sds R19) c = pmf (sds R27) d + pmf (sds R27) b \<and> pmf (sds R19) d + (pmf (sds R19) c + pmf (sds R19) a) = pmf (sds R27) d + (pmf (sds R27) b + pmf (sds R27) a)
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1
pmf (sds R19) d = 1 / 2

goal (1 subgoal):
 1. pmf (sds R19) a = 1 / 2 &&& pmf (sds R19) c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a = 1 / 2
pmf (sds R19) c = 0

goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
assume [simp]: "pmf (sds R19) c = 0"
[PROOF STATE]
proof (state)
this:
pmf (sds R19) c = 0

goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
from R19_R10.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R10) b + pmf (sds R10) d \<le> pmf (sds R19) c + pmf (sds R19) a
[PROOF STEP]
have "pmf (sds R19) a \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R10) b + pmf (sds R10) d \<le> pmf (sds R19) c + pmf (sds R19) a

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R19) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R19) a

goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R19) a

goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
from R19_R27.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R27) d + pmf (sds R27) b \<le> pmf (sds R19) d + pmf (sds R19) c
[PROOF STEP]
have "pmf (sds R19) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R27) d + pmf (sds R27) b \<le> pmf (sds R19) d + pmf (sds R19) c

goal (1 subgoal):
 1. 1 / 2 \<le> pmf (sds R19) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R19) d

goal (3 subgoals):
 1. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0 \<Longrightarrow> pmf (sds R19) d = 1 / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 / 2 \<le> pmf (sds R19) a
1 / 2 \<le> pmf (sds R19) d
[PROOF STEP]
show "pmf (sds R19) a = 1/2" "pmf (sds R19) d = 1/2" "pmf (sds R19) b = 0"
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R19) a
1 / 2 \<le> pmf (sds R19) d

goal (1 subgoal):
 1. pmf (sds R19) a = 1 / 2 &&& pmf (sds R19) d = 1 / 2 &&& pmf (sds R19) b = 0
[PROOF STEP]
using lottery_conditions[OF R19.wf]
[PROOF STATE]
proof (prove)
using this:
1 / 2 \<le> pmf (sds R19) a
1 / 2 \<le> pmf (sds R19) d
0 \<le> pmf (sds R19) a
0 \<le> pmf (sds R19) b
0 \<le> pmf (sds R19) c
0 \<le> pmf (sds R19) d
pmf (sds R19) a + pmf (sds R19) b + pmf (sds R19) c + pmf (sds R19) d = 1

goal (1 subgoal):
 1. pmf (sds R19) a = 1 / 2 &&& pmf (sds R19) d = 1 / 2 &&& pmf (sds R19) b = 0
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a = 1 / 2
pmf (sds R19) d = 1 / 2
pmf (sds R19) b = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a = 1 / 2 \<and> pmf (sds R19) b = 0 \<and> pmf (sds R19) c = 0 \<and> pmf (sds R19) d = 1 / 2

goal (4 subgoals):
 1. pmf (sds R19) a = 1 / 2
 2. pmf (sds R19) b = 0
 3. pmf (sds R19) c = 0
 4. pmf (sds R19) d = 1 / 2
[PROOF STEP]
thus "pmf (sds R19) a = 1/2" "pmf (sds R19) b = 0" "pmf (sds R19) c = 0" "pmf (sds R19) d = 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R19) a = 1 / 2 \<and> pmf (sds R19) b = 0 \<and> pmf (sds R19) c = 0 \<and> pmf (sds R19) d = 1 / 2

goal (1 subgoal):
 1. (pmf (sds R19) a = 1 / 2 &&& pmf (sds R19) b = 0) &&& pmf (sds R19) c = 0 &&& pmf (sds R19) d = 1 / 2
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
pmf (sds R19) a = 1 / 2
pmf (sds R19) b = 0
pmf (sds R19) c = 0
pmf (sds R19) d = 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R1 [simp]: "pmf (sds R1) a = 1/2" "pmf (sds R1) b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R1) a = 1 / 2 &&& pmf (sds R1) b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pmf (sds R1) a = 1 / 2
 2. pmf (sds R1) b = 0
[PROOF STEP]
from R19_R1.strategyproofness(1) lottery_conditions[OF R1.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R1) b + pmf (sds R1) a \<le> pmf (sds R19) b + pmf (sds R19) a
0 \<le> pmf (sds R1) a
0 \<le> pmf (sds R1) b
0 \<le> pmf (sds R1) c
0 \<le> pmf (sds R1) d
pmf (sds R1) a + pmf (sds R1) b + pmf (sds R1) c + pmf (sds R1) d = 1
[PROOF STEP]
have "pmf (sds R1) a + pmf (sds R1) b \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R1) b + pmf (sds R1) a \<le> pmf (sds R19) b + pmf (sds R19) a
0 \<le> pmf (sds R1) a
0 \<le> pmf (sds R1) b
0 \<le> pmf (sds R1) c
0 \<le> pmf (sds R1) d
pmf (sds R1) a + pmf (sds R1) b + pmf (sds R1) c + pmf (sds R1) d = 1

goal (1 subgoal):
 1. pmf (sds R1) a + pmf (sds R1) b \<le> 1 / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R1) a + pmf (sds R1) b \<le> 1 / 2

goal (2 subgoals):
 1. pmf (sds R1) a = 1 / 2
 2. pmf (sds R1) b = 0
[PROOF STEP]
with R1_R19.strategyproofness(1) lottery_conditions[OF R1.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R19) a < pmf (sds R1) a \<or> pmf (sds R19) a + pmf (sds R19) b < pmf (sds R1) a + pmf (sds R1) b) \<or> pmf (sds R19) a = pmf (sds R1) a \<and> pmf (sds R19) a + pmf (sds R19) b = pmf (sds R1) a + pmf (sds R1) b
0 \<le> pmf (sds R1) a
0 \<le> pmf (sds R1) b
0 \<le> pmf (sds R1) c
0 \<le> pmf (sds R1) d
pmf (sds R1) a + pmf (sds R1) b + pmf (sds R1) c + pmf (sds R1) d = 1
pmf (sds R1) a + pmf (sds R1) b \<le> 1 / 2
[PROOF STEP]
show "pmf (sds R1) a = 1/2" "pmf (sds R1) b = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R19) a < pmf (sds R1) a \<or> pmf (sds R19) a + pmf (sds R19) b < pmf (sds R1) a + pmf (sds R1) b) \<or> pmf (sds R19) a = pmf (sds R1) a \<and> pmf (sds R19) a + pmf (sds R19) b = pmf (sds R1) a + pmf (sds R1) b
0 \<le> pmf (sds R1) a
0 \<le> pmf (sds R1) b
0 \<le> pmf (sds R1) c
0 \<le> pmf (sds R1) d
pmf (sds R1) a + pmf (sds R1) b + pmf (sds R1) c + pmf (sds R1) d = 1
pmf (sds R1) a + pmf (sds R1) b \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R1) a = 1 / 2 &&& pmf (sds R1) b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R1) a = 1 / 2
pmf (sds R1) b = 0

goal:
No subgoals!
[PROOF STEP]
qed