# Theory SDS_Impossibility

```(*
File:   SDS_Impossibility.thy
Author: Manuel Eberl <manuel@pruvisto.org>

The proof that there exists no anonymous and neutral SDS for at least
four voters and alternatives that satisfies SD-Efficiency and
SD-Strategy-Proofness.
*)

section ‹Incompatibility of SD-Efficiency and SD-Strategy-Proofness›

theory SDS_Impossibility
imports
Randomised_Social_Choice.SDS_Automation
Randomised_Social_Choice.Randomised_Social_Choice
begin

subsection ‹Preliminary Definitions›

locale sds_impossibility =
anonymous_sds agents alts sds +
neutral_sds agents alts sds +
sd_efficient_sds agents alts sds +
strategyproof_sds agents alts sds
for agents :: "'agent set" and alts :: "'alt set" and sds +
assumes agents_ge_4: "card agents ≥ 4"
and alts_ge_4:   "card alts ≥ 4"

locale sds_impossibility_4_4 = sds_impossibility agents alts sds
for agents :: "'agent set" and alts :: "'alt set" and sds +
fixes A1 A2 A3 A4 :: 'agent and a b c d :: 'alt
assumes distinct_agents: "distinct [A1, A2, A3, A4]"
and distinct_alts: "distinct [a, b, c, d]"
and agents: "agents = {A1, A2, A3, A4}"
and alts:   "alts   = {a, b, c, d}"
begin

lemma an_sds: "an_sds agents alts sds" by unfold_locales
lemma ex_post_efficient_sds: "ex_post_efficient_sds agents alts sds" by unfold_locales
lemma sd_efficient_sds: "sd_efficient_sds agents alts sds" by unfold_locales
lemma strategyproof_an_sds: "strategyproof_an_sds agents alts sds" by unfold_locales

lemma distinct_agents' [simp]:
"A1 ≠ A2" "A1 ≠ A3" "A1 ≠ A4" "A2 ≠ A1" "A2 ≠ A3" "A2 ≠ A4"
"A3 ≠ A1" "A3 ≠ A2" "A3 ≠ A4" "A4 ≠ A1" "A4 ≠ A2" "A4 ≠ A3"
using distinct_agents by auto

lemma distinct_alts' [simp]:
"a ≠ b" "a ≠ c" "a ≠ d" "b ≠ a" "b ≠ c" "b ≠ d"
"c ≠ a" "c ≠ b" "c ≠ d" "d ≠ a" "d ≠ b" "d ≠ c"
using distinct_alts by auto

lemma card_agents [simp]: "card agents = 4" and card_alts [simp]: "card alts = 4"
using distinct_agents distinct_alts by (simp_all add: agents alts)

lemma in_agents [simp]: "A1 ∈ agents" "A2 ∈ agents" "A3 ∈ agents" "A4 ∈ agents"

lemma in_alts [simp]: "a ∈ alts" "b ∈ alts" "c ∈ alts" "d ∈ alts"

lemma agent_iff: "x ∈ agents ⟷ x ∈ {A1, A2, A3, A4}"
"(∀x∈agents. P x) ⟷ P A1 ∧ P A2 ∧ P A3 ∧ P A4"
"(∃x∈agents. P x) ⟷ P A1 ∨ P A2 ∨ P A3 ∨ P A4"

lemma alt_iff: "x ∈ alts ⟷ x ∈ {a,b,c,d}"
"(∀x∈alts. P x) ⟷ P a ∧ P b ∧ P c ∧ P d"
"(∃x∈alts. P x) ⟷ P a ∨ P b ∨ P c ∨ P d"

subsection ‹Definition of Preference Profiles and Fact Gathering›

preference_profile
agents: agents
alts:   alts
where R1  = A1: [c, d], [a, b]    A2: [b, d], a, c      A3: a, b, [c, d]      A4: [a, c], [b, d]
and R2  = A1: [a, c], [b, d]    A2: [c, d], a, b      A3: [b, d], a, c      A4: a, b, [c, d]
and R3  = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: d, [a, b], c      A4: c, a, [b, d]
and R4  = A1: [a, b], [c, d]    A2: [a, d], [b, c]    A3: c, [a, b], d      A4: d, c, [a, b]
and R5  = A1: [c, d], [a, b]    A2: [a, b], [c, d]    A3: [a, c], d, b      A4: d, [a, b], c
and R6  = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [a, c], [b, d]    A4: d, b, a, c
and R7  = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: a, c, d, b        A4: d, [a, b], c
and R8  = A1: [a, b], [c, d]    A2: [a, c], [b, d]    A3: d, [a, b], c      A4: d, c, [a, b]
and R9  = A1: [a, b], [c, d]    A2: [a, d], c, b      A3: d, c, [a, b]      A4: [a, b, c], d
and R10 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [a, c], d, b      A4: [b, d], a, c
and R11 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: d, [a, b], c      A4: c, a, b, d
and R12 = A1: [c, d], [a, b]    A2: [a, b], [c, d]    A3: [a, c], d, b      A4: [a, b, d], c
and R13 = A1: [a, c], [b, d]    A2: [c, d], a, b      A3: [b, d], a, c      A4: a, b, d, c
and R14 = A1: [a, b], [c, d]    A2: d, c, [a, b]      A3: [a, b, c], d      A4: a, d, c, b
and R15 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [b, d], a, c      A4: a, c, d, b
and R16 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: a, c, d, b        A4: [a, b, d], c
and R17 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [a, c], [b, d]    A4: d, [a, b], c
and R18 = A1: [a, b], [c, d]    A2: [a, d], [b, c]    A3: [a, b, c], d      A4: d, c, [a, b]
and R19 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [b, d], a, c      A4: [a, c], [b, d]
and R20 = A1: [b, d], a, c      A2: b, a, [c, d]      A3: a, c, [b, d]      A4: d, c, [a, b]
and R21 = A1: [a, d], c, b      A2: d, c, [a, b]      A3: c, [a, b], d      A4: a, b, [c, d]
and R22 = A1: [a, c], d, b      A2: d, c, [a, b]      A3: d, [a, b], c      A4: a, b, [c, d]
and R23 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: [a, c], [b, d]    A4: [a, b, d], c
and R24 = A1: [c, d], [a, b]    A2: d, b, a, c        A3: c, a, [b, d]      A4: b, a, [c, d]
and R25 = A1: [c, d], [a, b]    A2: [b, d], a, c      A3: a, b, [c, d]      A4: a, c, [b, d]
and R26 = A1: [b, d], [a, c]    A2: [c, d], [a, b]    A3: a, b, [c, d]      A4: a, c, [b, d]
and R27 = A1: [a, b], [c, d]    A2: [b, d], a, c      A3: [a, c], [b, d]    A4: [c, d], a, b
and R28 = A1: [c, d], a, b      A2: [b, d], a, c      A3: a, b, [c, d]      A4: a, c, [b, d]
and R29 = A1: [a, c], d, b      A2: [b, d], a, c      A3: a, b, [c, d]      A4: d, c, [a, b]
and R30 = A1: [a, d], c, b      A2: d, c, [a, b]      A3: c, [a, b], d      A4: [a, b], d, c
and R31 = A1: [b, d], a, c      A2: [a, c], d, b      A3: c, d, [a, b]      A4: [a, b], c, d
and R32 = A1: [a, c], d, b      A2: d, c, [a, b]      A3: d, [a, b], c      A4: [a, b], d, c
and R33 = A1: [c, d], [a, b]    A2: [a, c], d, b      A3: a, b, [c, d]      A4: d, [a, b], c
and R34 = A1: [a, b], [c, d]    A2: a, c, d, b        A3: b, [a, d], c      A4: c, d, [a, b]
and R35 = A1: [a, d], c, b      A2: a, b, [c, d]      A3: [a, b, c], d      A4: d, c, [a, b]
and R36 = A1: [c, d], [a, b]    A2: [a, c], d, b      A3: [b, d], a, c      A4: a, b, [c, d]
and R37 = A1: [a, c], [b, d]    A2: [b, d], [a, c]    A3: a, b, [c, d]      A4: c, d, [a, b]
and R38 = A1: [c, d], a, b      A2: [b, d], a, c      A3: a, b, [c, d]      A4: [a, c], b, d
and R39 = A1: [a, c], d, b      A2: [b, d], a, c      A3: a, b, [c, d]      A4: [c, d], a, b
and R40 = A1: [a, d], c, b      A2: [a, b], c, d      A3: [a, b, c], d      A4: d, c, [a, b]
and R41 = A1: [a, d], c, b      A2: [a, b], d, c      A3: [a, b, c], d      A4: d, c, [a, b]
and R42 = A1: [c, d], [a, b]    A2: [a, b], [c, d]    A3: d, b, a, c        A4: c, a, [b, d]
and R43 = A1: [a, b], [c, d]    A2: [c, d], [a, b]    A3: d, [a, b], c      A4: a, [c, d], b
and R44 = A1: [c, d], [a, b]    A2: [a, c], d, b      A3: [a, b], d, c      A4: [a, b, d], c
and R45 = A1: [a, c], d, b      A2: [b, d], a, c      A3: [a, b], c, d      A4: [c, d], b, a
and R46 = A1: [b, d], a, c      A2: d, c, [a, b]      A3: [a, c], [b, d]    A4: b, a, [c, d]
and R47 = A1: [a, b], [c, d]    A2: [a, d], c, b      A3: d, c, [a, b]      A4: c, [a, b], d

derive_orbit_equations (an_sds)
R10 R26 R27 R28 R29 R43 R45
by simp_all

prove_inefficient_supports (ex_post_efficient_sds sd_efficient_sds)
R3 [b] and R4 [b] and R5 [b] and R7 [b] and R8 [b] and
R9 [b] and R11 [b] and R12 [b] and R14 [b] and R16 [b] and
R17 [b] and R18 [b] and R21 [b] and R22 [b] and R23 [b] and
R30 [b] and R32 [b] and R33 [b] and R35 [b] and R40 [b] and
R41 [b] and R43 [b] and R44 [b] and R47 [b] and
R10 [c, b] witness: [a: 1 / 2, b: 0, c: 0, d: 1 / 2] and
R15 [c, b] witness: [a: 1 / 2, b: 0, c: 0, d: 1 / 2] and
R19 [c, b] witness: [a: 1 / 2, b: 0, c: 0, d: 1 / 2] and
R25 [b, c] witness: [c: 0, d: 1 / 2, a: 1 / 2, b: 0] and
R26 [c, b] witness: [b: 0, d: 1 / 2, a: 1 / 2, c: 0] and
R27 [c, b] witness: [a: 1 / 2, b: 0, c: 0, d: 1 / 2] and
R28 [b, c] witness: [c: 0, d: 1 / 2, a: 1 / 2, b: 0] and
R29 [b, c] witness: [a: 1 / 2, c: 0, d: 1 / 2, b: 0] and
R39 [b, c] witness: [a: 1 / 2, c: 0, d: 1 / 2, b: 0]

derive_strategyproofness_conditions (strategyproof_an_sds)
distance: 2
R1 R2 R3 R4 R5 R6 R7 R8 R9 R10 R11 R12 R13 R14 R15 R16 R17 R18 R19 R20
R21 R22 R23 R24 R25 R26 R27 R28 R29 R30 R31 R32 R33 R34 R35 R36 R37 R38 R39 R40
R41 R42 R43 R44 R45 R46 R47

lemma lottery_conditions:
assumes "is_pref_profile R"
shows   "pmf (sds R) a ≥ 0" "pmf (sds R) b ≥ 0" "pmf (sds R) c ≥ 0" "pmf (sds R) d ≥ 0"
"pmf (sds R) a + pmf (sds R) b + pmf (sds R) c + pmf (sds R) d = 1"
using lottery_prob_alts[OF sds_wf[OF assms]]
by (simp_all add: alts pmf_nonneg measure_measure_pmf_finite)

subsection ‹Main Proof›

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"
using R45.orbits lottery_conditions[OF R45.wf] by simp_all

lemma R10_bc [simp]: "pmf (sds R10) b = 0" "pmf (sds R10) c = 0"
using R10.support R10.orbits by auto

lemma R10_ad [simp]: "pmf (sds R10) a = 1/2" "pmf (sds R10) d = 1/2"
using lottery_conditions[OF R10.wf] R10_bc R10.orbits by simp_all

lemma R26_bc [simp]: "pmf (sds R26) b = 0" "pmf (sds R26) c = 0"
using R26.support R26.orbits by auto

lemma R26_d [simp]: "pmf (sds R26) d = 1 - pmf (sds R26) a"
using lottery_conditions[OF R26.wf] R26_bc by simp

lemma R27_bc [simp]: "pmf (sds R27) b = 0" "pmf (sds R27) c = 0"
using R27.support R27.orbits by auto

lemma R27_d [simp]: "pmf (sds R27) d = 1 - pmf (sds R27) a"
using lottery_conditions[OF R27.wf] R27_bc by simp

lemma R28_bc [simp]: "pmf (sds R28) b = 0" "pmf (sds R28) c = 0"
using R28.support R28.orbits by auto

lemma R28_d [simp]: "pmf (sds R28) d = 1 - pmf (sds R28) a"
using lottery_conditions[OF R28.wf] R28_bc by simp

lemma R29_bc [simp]: "pmf (sds R29) b = 0" "pmf (sds R29) c = 0"
using R29.support R29.orbits by auto

lemma R29_ac [simp]: "pmf (sds R29) a = 1/2" "pmf (sds R29) d = 1/2"
using lottery_conditions[OF R29.wf] R29_bc R29.orbits by simp_all

lemmas R43_bc [simp] = R43.support

lemma R43_ad [simp]: "pmf (sds R43) a = 1/2" "pmf (sds R43) d = 1/2"
using lottery_conditions[OF R43.wf] R43_bc R43.orbits by simp_all

lemma R39_b [simp]: "pmf (sds R39) b = 0"
proof -
{
assume [simp]: "pmf (sds R39) c = 0"
with R29_R39.strategyproofness(1)
have "pmf (sds R39) d ≤ 1/2" by auto
with R39_R29.strategyproofness(1) lottery_conditions[OF R39.wf]
have "pmf (sds R39) b = 0" by auto
}
with R39.support show ?thesis by blast
qed

lemma R36_a [simp]: "pmf (sds R36) a = 1/2" and R36_b [simp]: "pmf (sds R36) b = 0"
proof -
from R10_R36.strategyproofness(1) lottery_conditions[OF R36.wf]
have "pmf (sds R36) a + pmf (sds R36) b ≤ 1/2" by auto
with R36_R10.strategyproofness(1) lottery_conditions[OF R36.wf]
show "pmf (sds R36) a = 1/2" "pmf (sds R36) b = 0" by auto
qed

lemma R36_d [simp]: "pmf (sds R36) d = 1/2 - pmf (sds R36) c"
using lottery_conditions[OF R36.wf] by simp

lemma R39_a [simp]: "pmf (sds R39) a = 1/2"
proof -
from R36_R39.strategyproofness(1) lottery_conditions[OF R39.wf]
have "pmf (sds R39) a ≥ 1/2" by auto
with R39_R36.strategyproofness(1) lottery_conditions[OF R39.wf]
show ?thesis by auto
qed

lemma R39_d [simp]: "pmf (sds R39) d = 1/2 - pmf (sds R39) c"
using lottery_conditions[OF R39.wf] by simp

lemmas R12_b [simp] = R12.support

lemma R12_c [simp]: "pmf (sds R12) c = 0"
using R12_R10.strategyproofness(1) lottery_conditions[OF R12.wf]
by (auto simp del: pmf_nonneg)

lemma R12_d [simp]: "pmf (sds R12) d = 1 - pmf (sds R12) a"
using lottery_conditions[OF R12.wf] by simp

lemma R12_a_ge_one_half: "pmf (sds R12) a ≥ 1/2"
using R10_R12.strategyproofness(1) lottery_conditions[OF R12.wf]
by auto

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 -
from R12_R44.strategyproofness(1) R44.support have "pmf (sds R44) a ≤ pmf (sds R12) a" by simp
with R44_R12.strategyproofness(1) R44.support lottery_conditions[OF R44.wf]
show "pmf (sds R44) a = pmf (sds R12) a" "pmf (sds R44) c = 0"
"pmf (sds R44) d = 1 - pmf (sds R12) a" by (auto simp del: pmf_nonneg)
qed (insert R44.support, simp_all)

lemma R9_a [simp]: "pmf (sds R9) a = pmf (sds R35) a"
proof -
from R9_R35.strategyproofness(1) R35.support R9.support
have "pmf (sds R35) a ≤ pmf (sds R9) a" by simp
with R35_R9.strategyproofness(1) R9.support R35.support show ?thesis by simp
qed

lemma R18_c [simp]: "pmf (sds R18) c = pmf (sds R9) c"
proof -
from R18_R9.strategyproofness(1) R18.support R9.support
have "pmf (sds R18) d + pmf (sds R18) a ≥ pmf (sds R9) d + pmf (sds R9) a" by auto
with R9_R18.strategyproofness(1) R18.support R9.support
lottery_conditions[OF R9.wf] lottery_conditions[OF R18.wf]
show ?thesis by auto
qed

lemma R5_d_ge_one_half: "pmf (sds R5) d ≥ 1/2"
using R5_R10.strategyproofness(1) R5.support lottery_conditions[OF R5.wf] by auto

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 -
from R5_d_ge_one_half have "1/2 ≤ pmf (sds R5) d" by simp
also from R5_R17.strategyproofness(1) R17.support lottery_conditions[OF R5.wf] lottery_conditions[OF R17.wf]
have "… ≤ pmf (sds R17) d" by (auto simp del: pmf_nonneg)
also from R17_R7.strategyproofness(1) lottery_conditions[OF R7.wf] lottery_conditions[OF R17.wf] R7.support
have "pmf (sds R17) d ≤ pmf (sds R7) d" by (auto simp del: pmf_nonneg)
finally have "pmf (sds R7) d ≥ 1/2" .
with R7_R43.strategyproofness(1) lottery_conditions[OF R7.wf] R7.support
show "pmf (sds R7) a = 1/2" "pmf (sds R7) b = 0" "pmf (sds R7) c = 0" "pmf (sds R7) d = 1/2"
by auto
qed

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 -
from R5_R7.strategyproofness(1) lottery_conditions[OF R5.wf] R5.support
have "pmf (sds R5) d ≤ 1/2" by auto
with R5_d_ge_one_half show d: "pmf (sds R5) d = 1 / 2" by simp
with R5_R10.strategyproofness(1) lottery_conditions[OF R5.wf] R5.support
show "pmf (sds R5) c = 0" "pmf (sds R5) a = 1/2" by simp_all

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 -
{
assume "pmf (sds R15) b = 0"
with R10_R15.strategyproofness(1) lottery_conditions[OF R15.wf]
have "pmf (sds R15) a + pmf (sds R15) c ≤ 1/2" by auto
with R15_R10.strategyproofness(1) lottery_conditions[OF R15.wf]
have "pmf (sds R15) c = 0" by auto
}
with R15.support show [simp]: "pmf (sds R15) c = 0" by blast
with R15_R5.strategyproofness(1) lottery_conditions[OF R15.wf]
have "pmf (sds R15) a ≥ 1/2" by auto
moreover from R15_R7.strategyproofness(1) lottery_conditions[OF R15.wf]
have "pmf (sds R15) b + pmf (sds R15) d ≥ 1/2" by auto
ultimately show "pmf (sds R15) a = 1/2" using lottery_conditions[OF R15.wf] by auto
with R15_R5.strategyproofness(1) lottery_conditions[OF R15.wf]
show "pmf (sds R15) d = 1/2" "pmf (sds R15) b = 0" by auto
qed

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"
using R27_R13.strategyproofness(1) R13_R27.strategyproofness(1) lottery_conditions[OF R13.wf] by auto

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"
using R15_R13.strategyproofness(1) R13_R15.strategyproofness(1) R13_aux by simp_all

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"
by simp_all

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 -
have "pmf (sds R19) a = 1/2 ∧ pmf (sds R19) b = 0 ∧ pmf (sds R19) c = 0 ∧ pmf (sds R19) d = 1/2"
proof (rule disjE[OF R19.support]; safe)
assume [simp]: "pmf (sds R19) b = 0"
from R10_R19.strategyproofness(1) lottery_conditions[OF R19.wf]
have "pmf (sds R19) a + pmf (sds R19) c ≤ 1/2" by auto
moreover from R19_R10.strategyproofness(1)
have "pmf (sds R19) a + pmf (sds R19) c ≥ 1/2" by simp
ultimately show "pmf (sds R19) d = 1/2" using lottery_conditions[OF R19.wf] by simp
with R27_R19.strategyproofness(1) lottery_conditions[OF R19.wf]
show "pmf (sds R19) a = 1/2" "pmf (sds R19) c = 0" by auto
next
assume [simp]: "pmf (sds R19) c = 0"
from R19_R10.strategyproofness(1) have "pmf (sds R19) a ≥ 1/2" by auto
moreover from R19_R27.strategyproofness(1) have "pmf (sds R19) d ≥ 1/2" by auto
ultimately show "pmf (sds R19) a = 1/2" "pmf (sds R19) d = 1/2" "pmf (sds R19) b = 0"
using lottery_conditions[OF R19.wf] by (auto simp del: pmf_nonneg)
qed
thus "pmf (sds R19) a = 1/2" "pmf (sds R19) b = 0" "pmf (sds R19) c = 0" "pmf (sds R19) d = 1/2"
by blast+
qed

lemma R1 [simp]: "pmf (sds R1) a = 1/2" "pmf (sds R1) b = 0"
proof -
from R19_R1.strategyproofness(1) lottery_conditions[OF R1.wf]
have "pmf (sds R1) a + pmf (sds R1) b ≤ 1/2" by simp
with R1_R19.strategyproofness(1) lottery_conditions[OF R1.wf]
show "pmf (sds R1) a = 1/2" "pmf (sds R1) b = 0" by auto
qed

lemma R22 [simp]: "pmf (sds R22) a = 1/2" "pmf (sds R22) b = 0" "pmf (sds R22) c = 0" "pmf (sds R22) d = 1/2"
proof -
from R33_R5.strategyproofness(1) R33.support
have "1/2 ≤ pmf (sds R33) a" by auto
also from R33_R22.strategyproofness(1) R22.support R33.support
lottery_conditions[OF R22.wf] lottery_conditions[OF R33.wf]
have "… ≤ pmf (sds R22) a" by simp
finally show "pmf (sds R22) a = 1/2" "pmf (sds R22) b = 0" "pmf (sds R22) c = 0" "pmf (sds R22) d = 1/2"
using R22_R29.strategyproofness(1) lottery_conditions[OF R22.wf] by (auto simp del: pmf_nonneg)
qed

lemma R28 [simp]: "pmf (sds R28) a = 1/2" "pmf (sds R28) b = 0" "pmf (sds R28) c = 0" "pmf (sds R28) d = 1/2"
proof -
have "pmf (sds R28) a ≤ pmf (sds R32) d"
using R32_R28.strategyproofness(1) lottery_conditions[OF R32.wf] by auto
hence R32_d: "pmf (sds R32) d = pmf (sds R28) a"
using R28_R32.strategyproofness(1) lottery_conditions[OF R32.wf] by auto

from R22_R32.strategyproofness(1) lottery_conditions[OF R32.wf] R32.support
have "pmf (sds R32) a ≤ 1/2" by auto
with R32_R22.strategyproofness(1) lottery_conditions[OF R32.wf] R32.support
show "pmf (sds R28) a = 1/2" "pmf (sds R28) b = 0" "pmf (sds R28) c = 0" "pmf (sds R28) d = 1/2"
by (auto simp: R32_d simp del: pmf_nonneg)
qed

lemma R39 [simp]: "pmf (sds R39) a = 1/2" "pmf (sds R39) b = 0" "pmf (sds R39) c = 0" "pmf (sds R39) d = 1/2"
proof -
from R28_R39.strategyproofness(1) show "pmf (sds R39) c = 0" by simp
thus "pmf (sds R39) a = 1/2" "pmf (sds R39) b = 0" "pmf (sds R39) d = 1/2"
by simp_all
qed

lemma R2 [simp]: "pmf (sds R2) a = 1/2" "pmf (sds R2) b = 0" "pmf (sds R2) c = 0" "pmf (sds R2) d = 1/2"
proof -
from R1_R2.strategyproofness(1) R2_R1.strategyproofness(1) lottery_conditions[OF R2.wf] lottery_conditions[OF R1.wf]
have "pmf (sds R2) a = 1/2" "pmf (sds R2) c + pmf (sds R2) d = 1/2"
by (auto simp: algebra_simps simp del: pmf_nonneg)
with R39_R2.strategyproofness(1) lottery_conditions[OF R2.wf]
show "pmf (sds R2) a = 1/2" "pmf (sds R2) b = 0" "pmf (sds R2) c = 0" "pmf (sds R2) d = 1/2"
by auto
qed

lemma R42 [simp]: "pmf (sds R42) a = 0" "pmf (sds R42) b = 0" "pmf (sds R42) c = 1/2" "pmf (sds R42) d = 1/2"
proof -
from R17_R5.strategyproofness(1) lottery_conditions[OF R17.wf] R17.support
have "pmf (sds R17) d ≤ 1/2" by auto
moreover from R5_R17.strategyproofness(1) R17.support lottery_conditions[OF R17.wf]
have "pmf (sds R17) d ≥ 1/2" by auto
ultimately have R17_d: "pmf (sds R17) d = 1/2" by simp

from R6_R42.strategyproofness(1)
have "pmf (sds R42) a + pmf (sds R42) c ≤ pmf (sds R6) a + pmf (sds R6) c" by simp
also from R6_R19.strategyproofness(1) lottery_conditions[OF R6.wf]
have "pmf (sds R6) a + pmf (sds R6) c ≤ 1/2" by (auto simp del: pmf_nonneg)
finally have "pmf (sds R42) a + pmf (sds R42) c ≤ 1 / 2" .
moreover from R17_R11.strategyproofness(1) R11.support R17.support
lottery_conditions[OF R11.wf] lottery_conditions[OF R17.wf]
have "pmf (sds R11) d ≥ 1/2" by (auto simp: R17_d)
ultimately have "pmf (sds R42) a + pmf (sds R42) c ≤ pmf (sds R11) d" by simp
with R42_R11.strategyproofness(1) R11.support
have E: "pmf (sds R11) d ≤ pmf (sds R42) c" by auto
with ‹pmf (sds R11) d ≥ 1/2› have "pmf (sds R42) c ≥ 1/2" by simp
moreover from R17_R3.strategyproofness(1) R3.support R17.support
lottery_conditions[OF R17.wf] lottery_conditions[OF R3.wf]
have "pmf (sds R3) d ≥ 1/2" by (auto simp: R17_d)
ultimately show "pmf (sds R42) a = 0" "pmf (sds R42) b = 0" "pmf (sds R42) c = 1/2" "pmf (sds R42) d = 1/2"
using R42_R3.strategyproofness(1) lottery_conditions[OF R3.wf] lottery_conditions[OF R42.wf]
by linarith+
qed

lemma R37 [simp]: "pmf (sds R37) a = 1/2" "pmf (sds R37) b = 0" "pmf (sds R37) c = 1/2" "pmf (sds R37) d = 0"
proof -
from R37_R42.strategyproofness(1) lottery_conditions[OF R37.wf]
have "pmf (sds R37) a = 1/2 ∨ pmf (sds R37) a + pmf (sds R37) b > 1/2"
by (auto simp del: pmf_nonneg)
moreover from R37_R42.strategyproofness(2) lottery_conditions[OF R37.wf]
have "pmf (sds R37) c = 1/2 ∨ pmf (sds R37) c + pmf (sds R37) d > 1/2"
by (auto simp del: pmf_nonneg)
ultimately show "pmf (sds R37) a = 1/2" "pmf (sds R37) b = 0" "pmf (sds R37) c = 1/2" "pmf (sds R37) d = 0"
using lottery_conditions[OF R37.wf] by (auto simp del: pmf_nonneg)
qed

lemma R24 [simp]: "pmf (sds R24) a = 0" "pmf (sds R24) b = 0" "pmf (sds R24) d = 1 - pmf (sds R24) c"
using R42_R24.strategyproofness(1) lottery_conditions[OF R24.wf] by (auto simp del: pmf_nonneg)

lemma R34 [simp]:
"pmf (sds R34) a = 1 - pmf (sds R24) c" "pmf (sds R34) b = pmf (sds R24) c"
"pmf (sds R34) c = 0" "pmf (sds R34) d = 0"
proof -
from R24_R34.strategyproofness(1) lottery_conditions[OF R34.wf]
have "pmf (sds R34) b ≤ pmf (sds R24) c" by (auto simp del: pmf_nonneg)
moreover from R34_R24.strategyproofness(1) lottery_conditions[OF R34.wf]
have "pmf (sds R34) b ≥ pmf (sds R24) c" by auto
ultimately show bc: "pmf (sds R34) b = pmf (sds R24) c" by simp
from R34_R24.strategyproofness(1) bc lottery_conditions[OF R34.wf]
show "pmf (sds R34) c = 0" by auto
moreover from R24_R34.strategyproofness(1) bc show "pmf (sds R34) d = 0" by simp
ultimately show "pmf (sds R34) a = 1 - pmf (sds R24) c"
using bc lottery_conditions[OF R34.wf] by auto
qed

lemma R14 [simp]: "pmf (sds R14) b = 0" "pmf (sds R14) d = 0" "pmf (sds R14) c = 1 - pmf (sds R14) a"
using R14_R34.strategyproofness(1) R14.support lottery_conditions[OF R14.wf]
by (auto simp del: pmf_nonneg)

lemma R46 [simp]: "pmf (sds R46) a = 0" "pmf (sds R46) c = 0" "pmf (sds R46) d = 1 - pmf (sds R46) b"
using R46_R37.strategyproofness(1) lottery_conditions[OF R46.wf] by auto

lemma R20 [simp]: "pmf (sds R20) a = 0" "pmf (sds R20) c = 0" "pmf (sds R20) d = 1 - pmf (sds R20) b"
using R46_R20.strategyproofness(1) lottery_conditions[OF R20.wf] by (auto simp del: pmf_nonneg)

lemma R21 [simp]: "pmf (sds R21) d = 1 - pmf (sds R21) a" "pmf (sds R21) b = 0" "pmf (sds R21) c = 0"
using R20_R21.strategyproofness(1) lottery_conditions[OF R21.wf] by auto

lemma R16_R12: "pmf (sds R16) c + pmf (sds R16) a ≤ pmf (sds R12) a"
using R12_R16.strategyproofness(1) R16.support lottery_conditions[OF R16.wf] by auto

lemma R16 [simp]: "pmf (sds R16) b = 0" "pmf (sds R16) c = 0" "pmf (sds R16) d = 1 - pmf (sds R16) a"
proof -
from R16_R12 have "pmf (sds R16) c + pmf (sds R16) a ≤ pmf (sds R12) a" by simp
also from R44_R40.strategyproofness(1) lottery_conditions[OF R40.wf] R40.support
have "pmf (sds R12) a ≤ pmf (sds R40) a" by auto
also from R9_R40.strategyproofness(1) R9.support R40.support
have "pmf (sds R40) a ≤ pmf (sds R9) a" by auto
finally have "pmf (sds R16) c + pmf (sds R16) a ≤ pmf (sds R9) a" by simp
moreover from R14_R16.strategyproofness(1) R16.support lottery_conditions[OF R16.wf]
have "pmf (sds R16) a ≥ pmf (sds R14) a" by auto
ultimately have "pmf (sds R16) c ≤ pmf (sds R9) a - pmf (sds R14) a" by simp
also from R14_R9.strategyproofness(1) R9.support lottery_conditions[OF R9.wf]
have "pmf (sds R9) a - pmf (sds R14) a ≤ 0" by (auto simp del: pmf_nonneg)
finally show "pmf (sds R16) b = 0" "pmf (sds R16) c = 0" "pmf (sds R16) d = 1 - pmf (sds R16) a"
using lottery_conditions[OF R16.wf] R16.support by auto
qed

lemma R12_R14: "pmf (sds R14) a ≤ pmf (sds R12) a"
using R14_R16.strategyproofness(1) R16_R12 by auto

lemma R12_a [simp]: "pmf (sds R12) a = pmf (sds R9) a"
proof -
from R44_R40.strategyproofness(1) R40.support lottery_conditions[OF R40.wf]
have "pmf (sds R12) a ≤ pmf (sds R40) a" by auto
also from R9_R40.strategyproofness(1) R9.support R40.support
have "pmf (sds R40) a ≤ pmf (sds R9) a" by auto
finally have B: "pmf (sds R12) a ≤ pmf (sds R9) a" by simp
moreover from R14_R9.strategyproofness(1) lottery_conditions[OF R9.wf] R9.support
have "pmf (sds R9) a ≤ pmf (sds R14) a" by (auto simp del: pmf_nonneg)
with R12_R14 have "pmf (sds R9) a ≤ pmf (sds R12) a" by simp
ultimately show "pmf (sds R12) a = pmf (sds R9) a" by simp
qed

lemma R9 [simp]: "pmf (sds R9) b = 0" "pmf (sds R9) d = 0" "pmf (sds R14) a = pmf (sds R35) a" "pmf (sds R9) c = 1 - pmf (sds R35) a"
using R12_R14 R14_R9.strategyproofness(1) lottery_conditions[OF R9.wf] R9.support
by auto

lemma R23 [simp]: "pmf (sds R23) b = 0" "pmf (sds R23) c = 0" "pmf (sds R23) d = 1 - pmf (sds R23) a"
using R23_R19.strategyproofness(1) lottery_conditions[OF R23.wf] R23.support
by (auto simp del: pmf_nonneg)

lemma R35 [simp]: "pmf (sds R35) a = pmf (sds R21) a" "pmf (sds R35) b = 0" "pmf (sds R35) c = 0" "pmf (sds R35) d = 1 - pmf (sds R21) a"
proof -
from R35_R21.strategyproofness(1) R35.support
have "pmf (sds R21) a ≤ pmf (sds R35) a + pmf (sds R35) c" by auto
with R21_R35.strategyproofness(1) R35.support lottery_conditions[OF R35.wf]
show "pmf (sds R35) a = pmf (sds R21) a" "pmf (sds R35) b = 0"
"pmf (sds R35) c = 0" "pmf (sds R35) d = 1 - pmf (sds R21) a" by simp_all
qed

lemma R18 [simp]: "pmf (sds R18) a = pmf (sds R14) a" "pmf (sds R18) b = 0"
"pmf (sds R18) d = 0" "pmf (sds R18) c = 1 - pmf (sds R14) a"
proof -
from R23_R12.strategyproofness(1)
have R21_R23: "pmf (sds R21) a ≤ pmf (sds R23) a" by simp

from R23_R18.strategyproofness(1)
have "pmf (sds R18) d ≤ pmf (sds R21) a - pmf (sds R23) a" by simp
also from R21_R23 have "… ≤ 0" by simp
finally show "pmf (sds R18) d = 0" by simp
with lottery_conditions[OF R18.wf] R18.support
show "pmf (sds R18) a = pmf (sds R14) a"
"pmf (sds R18) c = 1 - pmf (sds R14) a" by auto
qed (insert R18.support, simp_all)

lemma R4 [simp]: "pmf (sds R4) a = pmf (sds R21) a" "pmf (sds R4) b = 0"
"pmf (sds R4) c = 1 - pmf (sds R4) a" "pmf (sds R4) d = 0"
proof -
from R30_R21.strategyproofness(1) R30.support lottery_conditions[OF R30.wf]
have "pmf (sds R4) c + pmf (sds R21) a ≤ pmf (sds R4) c + ```