[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R22) a = 1 / 2 &&& pmf (sds R22) b = 0) &&& pmf (sds R22) c = 0 &&& pmf (sds R22) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R22) a = 1 / 2
 2. pmf (sds R22) b = 0
 3. pmf (sds R22) c = 0
 4. pmf (sds R22) d = 1 / 2
[PROOF STEP]
from R33_R5.strategyproofness(1) R33.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R5) a < pmf (sds R33) a \<or> pmf (sds R5) a + pmf (sds R5) b < pmf (sds R33) a + pmf (sds R33) b) \<or> pmf (sds R5) a = pmf (sds R33) a \<and> pmf (sds R5) a + pmf (sds R5) b = pmf (sds R33) a + pmf (sds R33) b
pmf (sds R33) b = 0
[PROOF STEP]
have "1/2 \<le> pmf (sds R33) a"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R5) a < pmf (sds R33) a \<or> pmf (sds R5) a + pmf (sds R5) b < pmf (sds R33) a + pmf (sds R33) b) \<or> pmf (sds R5) a = pmf (sds R33) a \<and> pmf (sds R5) a + pmf (sds R5) b = pmf (sds R33) a + pmf (sds R33) b
pmf (sds R33) b = 0

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R28) a = 1 / 2 &&& pmf (sds R28) b = 0) &&& pmf (sds R28) c = 0 &&& pmf (sds R28) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R28) a = 1 / 2
 2. pmf (sds R28) b = 0
 3. pmf (sds R28) c = 0
 4. pmf (sds R28) d = 1 / 2
[PROOF STEP]
have "pmf (sds R28) a \<le> pmf (sds R32) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R28) a \<le> pmf (sds R32) d
[PROOF STEP]
using R32_R28.strategyproofness(1) lottery_conditions[OF R32.wf]
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R28) a < pmf (sds R32) d \<or> pmf (sds R28) a + (pmf (sds R28) c + pmf (sds R28) d) < pmf (sds R32) d + (pmf (sds R32) b + pmf (sds R32) a)) \<or> pmf (sds R28) a = pmf (sds R32) d \<and> pmf (sds R28) a + (pmf (sds R28) c + pmf (sds R28) d) = pmf (sds R32) d + (pmf (sds R32) b + pmf (sds R32) a)
0 \<le> pmf (sds R32) a
0 \<le> pmf (sds R32) b
0 \<le> pmf (sds R32) c
0 \<le> pmf (sds R32) d
pmf (sds R32) a + pmf (sds R32) b + pmf (sds R32) c + pmf (sds R32) d = 1

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

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

goal (1 subgoal):
 1. pmf (sds R32) d = pmf (sds R28) a
[PROOF STEP]
using R28_R32.strategyproofness(1) lottery_conditions[OF R32.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R28) a \<le> pmf (sds R32) d
(pmf (sds R32) d < pmf (sds R28) a \<or> pmf (sds R32) d + pmf (sds R32) b < pmf (sds R28) a + pmf (sds R28) c) \<or> pmf (sds R32) d = pmf (sds R28) a \<and> pmf (sds R32) d + pmf (sds R32) b = pmf (sds R28) a + pmf (sds R28) c
0 \<le> pmf (sds R32) a
0 \<le> pmf (sds R32) b
0 \<le> pmf (sds R32) c
0 \<le> pmf (sds R32) d
pmf (sds R32) a + pmf (sds R32) b + pmf (sds R32) c + pmf (sds R32) d = 1

goal (1 subgoal):
 1. pmf (sds R32) d = pmf (sds R28) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R32) d = pmf (sds R28) a

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R39) a = 1 / 2 &&& pmf (sds R39) b = 0) &&& pmf (sds R39) c = 0 &&& pmf (sds R39) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R39) a = 1 / 2
 2. pmf (sds R39) b = 0
 3. pmf (sds R39) c = 0
 4. pmf (sds R39) d = 1 / 2
[PROOF STEP]
from R28_R39.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R39) a < pmf (sds R28) a \<or> pmf (sds R39) a + pmf (sds R39) c < pmf (sds R28) a + pmf (sds R28) b) \<or> pmf (sds R39) a = pmf (sds R28) a \<and> pmf (sds R39) a + pmf (sds R39) c = pmf (sds R28) a + pmf (sds R28) b
[PROOF STEP]
show "pmf (sds R39) c = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R39) a < pmf (sds R28) a \<or> pmf (sds R39) a + pmf (sds R39) c < pmf (sds R28) a + pmf (sds R28) b) \<or> pmf (sds R39) a = pmf (sds R28) a \<and> pmf (sds R39) a + pmf (sds R39) c = pmf (sds R28) a + pmf (sds R28) b

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R2) a = 1 / 2 &&& pmf (sds R2) b = 0) &&& pmf (sds R2) c = 0 &&& pmf (sds R2) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R2) a = 1 / 2
 2. pmf (sds R2) b = 0
 3. pmf (sds R2) c = 0
 4. pmf (sds R2) d = 1 / 2
[PROOF STEP]
from R1_R2.strategyproofness(1) R2_R1.strategyproofness(1) lottery_conditions[OF R2.wf] lottery_conditions[OF R1.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R2) d + pmf (sds R2) c \<le> pmf (sds R1) d + pmf (sds R1) c
(pmf (sds R1) d + pmf (sds R1) c < pmf (sds R2) d + pmf (sds R2) c \<or> pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) < pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a)) \<or> pmf (sds R1) d + pmf (sds R1) c = pmf (sds R2) d + pmf (sds R2) c \<and> pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) = pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a)
0 \<le> pmf (sds R2) a
0 \<le> pmf (sds R2) b
0 \<le> pmf (sds R2) c
0 \<le> pmf (sds R2) d
pmf (sds R2) a + pmf (sds R2) b + pmf (sds R2) c + pmf (sds R2) d = 1
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 R2) a = 1/2" "pmf (sds R2) c + pmf (sds R2) d = 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R2) d + pmf (sds R2) c \<le> pmf (sds R1) d + pmf (sds R1) c
(pmf (sds R1) d + pmf (sds R1) c < pmf (sds R2) d + pmf (sds R2) c \<or> pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) < pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a)) \<or> pmf (sds R1) d + pmf (sds R1) c = pmf (sds R2) d + pmf (sds R2) c \<and> pmf (sds R1) d + (pmf (sds R1) c + pmf (sds R1) a) = pmf (sds R2) d + (pmf (sds R2) c + pmf (sds R2) a)
0 \<le> pmf (sds R2) a
0 \<le> pmf (sds R2) b
0 \<le> pmf (sds R2) c
0 \<le> pmf (sds R2) d
pmf (sds R2) a + pmf (sds R2) b + pmf (sds R2) c + pmf (sds R2) d = 1
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 R2) a = 1 / 2 &&& pmf (sds R2) c + pmf (sds R2) d = 1 / 2
[PROOF STEP]
by (auto simp: algebra_simps simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R2) a = 1 / 2
pmf (sds R2) c + pmf (sds R2) d = 1 / 2

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R42) a = 0 &&& pmf (sds R42) b = 0) &&& pmf (sds R42) c = 1 / 2 &&& pmf (sds R42) d = 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R42) a = 0
 2. pmf (sds R42) b = 0
 3. pmf (sds R42) c = 1 / 2
 4. pmf (sds R42) d = 1 / 2
[PROOF STEP]
from R17_R5.strategyproofness(1) lottery_conditions[OF R17.wf] R17.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R5) c + pmf (sds R5) a \<le> pmf (sds R17) c + pmf (sds R17) a
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 R17) b = 0
[PROOF STEP]
have "pmf (sds R17) d \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R5) c + pmf (sds R5) a \<le> pmf (sds R17) c + pmf (sds R17) a
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 R17) b = 0

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

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

goal (4 subgoals):
 1. pmf (sds R42) a = 0
 2. pmf (sds R42) b = 0
 3. pmf (sds R42) c = 1 / 2
 4. pmf (sds R42) d = 1 / 2
[PROOF STEP]
from R5_R17.strategyproofness(1) R17.support 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 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 "pmf (sds R17) d \<ge> 1/2"
[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 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. 1 / 2 \<le> pmf (sds R17) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R17) d

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

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

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

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

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

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

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

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

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

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

goal (4 subgoals):
 1. pmf (sds R42) a = 0
 2. pmf (sds R42) b = 0
 3. pmf (sds R42) c = 1 / 2
 4. pmf (sds R42) d = 1 / 2
[PROOF STEP]
from R17_R11.strategyproofness(1) R11.support R17.support
       lottery_conditions[OF R11.wf] lottery_conditions[OF R17.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R11) c + pmf (sds R11) a \<le> pmf (sds R17) c + pmf (sds R17) a
pmf (sds R11) b = 0
pmf (sds R17) b = 0
0 \<le> pmf (sds R11) a
0 \<le> pmf (sds R11) b
0 \<le> pmf (sds R11) c
0 \<le> pmf (sds R11) d
pmf (sds R11) a + pmf (sds R11) b + pmf (sds R11) c + pmf (sds R11) 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 "pmf (sds R11) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R11) c + pmf (sds R11) a \<le> pmf (sds R17) c + pmf (sds R17) a
pmf (sds R11) b = 0
pmf (sds R17) b = 0
0 \<le> pmf (sds R11) a
0 \<le> pmf (sds R11) b
0 \<le> pmf (sds R11) c
0 \<le> pmf (sds R11) d
pmf (sds R11) a + pmf (sds R11) b + pmf (sds R11) c + pmf (sds R11) 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. 1 / 2 \<le> pmf (sds R11) d
[PROOF STEP]
by (auto simp: R17_d)
[PROOF STATE]
proof (state)
this:
1 / 2 \<le> pmf (sds R11) d

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

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

goal (4 subgoals):
 1. pmf (sds R42) a = 0
 2. pmf (sds R42) b = 0
 3. pmf (sds R42) c = 1 / 2
 4. pmf (sds R42) d = 1 / 2
[PROOF STEP]
with R42_R11.strategyproofness(1) R11.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R11) d < pmf (sds R42) c \<or> pmf (sds R11) d + pmf (sds R11) b < pmf (sds R42) c + pmf (sds R42) a) \<or> pmf (sds R11) d = pmf (sds R42) c \<and> pmf (sds R11) d + pmf (sds R11) b = pmf (sds R42) c + pmf (sds R42) a
pmf (sds R11) b = 0
pmf (sds R42) a + pmf (sds R42) c \<le> pmf (sds R11) d
[PROOF STEP]
have E: "pmf (sds R11) d \<le> pmf (sds R42) c"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R11) d < pmf (sds R42) c \<or> pmf (sds R11) d + pmf (sds R11) b < pmf (sds R42) c + pmf (sds R42) a) \<or> pmf (sds R11) d = pmf (sds R42) c \<and> pmf (sds R11) d + pmf (sds R11) b = pmf (sds R42) c + pmf (sds R42) a
pmf (sds R11) b = 0
pmf (sds R42) a + pmf (sds R42) c \<le> pmf (sds R11) d

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

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

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

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

goal (4 subgoals):
 1. pmf (sds R42) a = 0
 2. pmf (sds R42) b = 0
 3. pmf (sds R42) c = 1 / 2
 4. pmf (sds R42) d = 1 / 2
[PROOF STEP]
from R17_R3.strategyproofness(1) R3.support R17.support
       lottery_conditions[OF R17.wf] lottery_conditions[OF R3.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R3) c + pmf (sds R3) a \<le> pmf (sds R17) c + pmf (sds R17) a
pmf (sds R3) b = 0
pmf (sds R17) b = 0
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
0 \<le> pmf (sds R3) a
0 \<le> pmf (sds R3) b
0 \<le> pmf (sds R3) c
0 \<le> pmf (sds R3) d
pmf (sds R3) a + pmf (sds R3) b + pmf (sds R3) c + pmf (sds R3) d = 1
[PROOF STEP]
have "pmf (sds R3) d \<ge> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R3) c + pmf (sds R3) a \<le> pmf (sds R17) c + pmf (sds R17) a
pmf (sds R3) b = 0
pmf (sds R17) b = 0
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
0 \<le> pmf (sds R3) a
0 \<le> pmf (sds R3) b
0 \<le> pmf (sds R3) c
0 \<le> pmf (sds R3) d
pmf (sds R3) a + pmf (sds R3) b + pmf (sds R3) c + pmf (sds R3) d = 1

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R37) a = 1 / 2 &&& pmf (sds R37) b = 0) &&& pmf (sds R37) c = 1 / 2 &&& pmf (sds R37) d = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R37) a = 1 / 2
 2. pmf (sds R37) b = 0
 3. pmf (sds R37) c = 1 / 2
 4. pmf (sds R37) d = 0
[PROOF STEP]
from R37_R42.strategyproofness(1) lottery_conditions[OF R37.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R42) d < pmf (sds R37) a \<or> pmf (sds R42) d + pmf (sds R42) b < pmf (sds R37) a + pmf (sds R37) b) \<or> pmf (sds R42) d = pmf (sds R37) a \<and> pmf (sds R42) d + pmf (sds R42) b = pmf (sds R37) a + pmf (sds R37) b
0 \<le> pmf (sds R37) a
0 \<le> pmf (sds R37) b
0 \<le> pmf (sds R37) c
0 \<le> pmf (sds R37) d
pmf (sds R37) a + pmf (sds R37) b + pmf (sds R37) c + pmf (sds R37) d = 1
[PROOF STEP]
have "pmf (sds R37) a = 1/2 \<or> pmf (sds R37) a + pmf (sds R37) b > 1/2"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R42) d < pmf (sds R37) a \<or> pmf (sds R42) d + pmf (sds R42) b < pmf (sds R37) a + pmf (sds R37) b) \<or> pmf (sds R42) d = pmf (sds R37) a \<and> pmf (sds R42) d + pmf (sds R42) b = pmf (sds R37) a + pmf (sds R37) b
0 \<le> pmf (sds R37) a
0 \<le> pmf (sds R37) b
0 \<le> pmf (sds R37) c
0 \<le> pmf (sds R37) d
pmf (sds R37) a + pmf (sds R37) b + pmf (sds R37) c + pmf (sds R37) d = 1

goal (1 subgoal):
 1. pmf (sds R37) a = 1 / 2 \<or> 1 / 2 < pmf (sds R37) a + pmf (sds R37) b
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R37) a = 1 / 2 \<or> 1 / 2 < pmf (sds R37) a + pmf (sds R37) b

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

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

goal (1 subgoal):
 1. pmf (sds R37) c = 1 / 2 \<or> 1 / 2 < pmf (sds R37) c + pmf (sds R37) d
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R37) c = 1 / 2 \<or> 1 / 2 < pmf (sds R37) c + pmf (sds R37) d

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. pmf (sds R24) a = 0 &&& pmf (sds R24) b = 0 &&& pmf (sds R24) d = 1 - pmf (sds R24) c
[PROOF STEP]
by (auto simp del: pmf_nonneg)


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (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 STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
 2. pmf (sds R34) b = pmf (sds R24) c
 3. pmf (sds R34) c = 0
 4. pmf (sds R34) d = 0
[PROOF STEP]
from R24_R34.strategyproofness(1) lottery_conditions[OF R34.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R34) b < pmf (sds R24) c \<or> pmf (sds R34) b + pmf (sds R34) d < pmf (sds R24) c + pmf (sds R24) a) \<or> pmf (sds R34) b = pmf (sds R24) c \<and> pmf (sds R34) b + pmf (sds R34) d = pmf (sds R24) c + pmf (sds R24) a
0 \<le> pmf (sds R34) a
0 \<le> pmf (sds R34) b
0 \<le> pmf (sds R34) c
0 \<le> pmf (sds R34) d
pmf (sds R34) a + pmf (sds R34) b + pmf (sds R34) c + pmf (sds R34) d = 1
[PROOF STEP]
have "pmf (sds R34) b \<le> pmf (sds R24) c"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R34) b < pmf (sds R24) c \<or> pmf (sds R34) b + pmf (sds R34) d < pmf (sds R24) c + pmf (sds R24) a) \<or> pmf (sds R34) b = pmf (sds R24) c \<and> pmf (sds R34) b + pmf (sds R34) d = pmf (sds R24) c + pmf (sds R24) a
0 \<le> pmf (sds R34) a
0 \<le> pmf (sds R34) b
0 \<le> pmf (sds R34) c
0 \<le> pmf (sds R34) d
pmf (sds R34) a + pmf (sds R34) b + pmf (sds R34) c + pmf (sds R34) d = 1

goal (1 subgoal):
 1. pmf (sds R34) b \<le> pmf (sds R24) c
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R34) b \<le> pmf (sds R24) c

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

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

goal (1 subgoal):
 1. pmf (sds R24) c \<le> pmf (sds R34) b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R24) c \<le> pmf (sds R34) b

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

goal (1 subgoal):
 1. pmf (sds R34) b = pmf (sds R24) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R34) b = pmf (sds R24) c

goal (3 subgoals):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
 2. pmf (sds R34) c = 0
 3. pmf (sds R34) d = 0
[PROOF STEP]
from R34_R24.strategyproofness(1) bc lottery_conditions[OF R34.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R24) c < pmf (sds R34) b \<or> pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) < pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a)) \<or> pmf (sds R24) c = pmf (sds R34) b \<and> pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) = pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a)
pmf (sds R34) b = pmf (sds R24) c
0 \<le> pmf (sds R34) a
0 \<le> pmf (sds R34) b
0 \<le> pmf (sds R34) c
0 \<le> pmf (sds R34) d
pmf (sds R34) a + pmf (sds R34) b + pmf (sds R34) c + pmf (sds R34) d = 1
[PROOF STEP]
show "pmf (sds R34) c = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R24) c < pmf (sds R34) b \<or> pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) < pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a)) \<or> pmf (sds R24) c = pmf (sds R34) b \<and> pmf (sds R24) c + (pmf (sds R24) a + pmf (sds R24) d) = pmf (sds R34) b + (pmf (sds R34) d + pmf (sds R34) a)
pmf (sds R34) b = pmf (sds R24) c
0 \<le> pmf (sds R34) a
0 \<le> pmf (sds R34) b
0 \<le> pmf (sds R34) c
0 \<le> pmf (sds R34) d
pmf (sds R34) a + pmf (sds R34) b + pmf (sds R34) c + pmf (sds R34) d = 1

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

goal (2 subgoals):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
 2. pmf (sds R34) d = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pmf (sds R34) c = 0

goal (2 subgoals):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
 2. pmf (sds R34) d = 0
[PROOF STEP]
from R24_R34.strategyproofness(1) bc
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R34) b < pmf (sds R24) c \<or> pmf (sds R34) b + pmf (sds R34) d < pmf (sds R24) c + pmf (sds R24) a) \<or> pmf (sds R34) b = pmf (sds R24) c \<and> pmf (sds R34) b + pmf (sds R34) d = pmf (sds R24) c + pmf (sds R24) a
pmf (sds R34) b = pmf (sds R24) c
[PROOF STEP]
show "pmf (sds R34) d = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R34) b < pmf (sds R24) c \<or> pmf (sds R34) b + pmf (sds R34) d < pmf (sds R24) c + pmf (sds R24) a) \<or> pmf (sds R34) b = pmf (sds R24) c \<and> pmf (sds R34) b + pmf (sds R34) d = pmf (sds R24) c + pmf (sds R24) a
pmf (sds R34) b = pmf (sds R24) c

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

goal (1 subgoal):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R34) c = 0
pmf (sds R34) d = 0
[PROOF STEP]
show "pmf (sds R34) a = 1 - pmf (sds R24) c"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R34) c = 0
pmf (sds R34) d = 0

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

goal (1 subgoal):
 1. pmf (sds R34) a = 1 - pmf (sds R24) c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R34) a = 1 - pmf (sds R24) c

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. pmf (sds R14) b = 0 &&& pmf (sds R14) d = 0 &&& pmf (sds R14) c = 1 - pmf (sds R14) a
[PROOF STEP]
by (auto simp del: pmf_nonneg)


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

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


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

goal (1 subgoal):
 1. pmf (sds R20) a = 0 &&& pmf (sds R20) c = 0 &&& pmf (sds R20) d = 1 - pmf (sds R20) b
[PROOF STEP]
by (auto simp del: pmf_nonneg)


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

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


[STATEMENT]
lemma R16_R12: "pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R12) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R12) a
[PROOF STEP]
using R12_R16.strategyproofness(1) R16.support lottery_conditions[OF R16.wf]
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R16) c + pmf (sds R16) a < pmf (sds R12) c + pmf (sds R12) a \<or> pmf (sds R16) c + (pmf (sds R16) a + pmf (sds R16) d) < pmf (sds R12) c + (pmf (sds R12) a + pmf (sds R12) d)) \<or> pmf (sds R16) c + pmf (sds R16) a = pmf (sds R12) c + pmf (sds R12) a \<and> pmf (sds R16) c + (pmf (sds R16) a + pmf (sds R16) d) = pmf (sds R12) c + (pmf (sds R12) a + pmf (sds R12) d)
pmf (sds R16) b = 0
0 \<le> pmf (sds R16) a
0 \<le> pmf (sds R16) b
0 \<le> pmf (sds R16) c
0 \<le> pmf (sds R16) d
pmf (sds R16) a + pmf (sds R16) b + pmf (sds R16) c + pmf (sds R16) d = 1

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


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

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

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R12) a

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
from R44_R40.strategyproofness(1) lottery_conditions[OF R40.wf] R40.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R40) c + pmf (sds R40) d \<le> pmf (sds R44) d + pmf (sds R44) c
0 \<le> pmf (sds R40) a
0 \<le> pmf (sds R40) b
0 \<le> pmf (sds R40) c
0 \<le> pmf (sds R40) d
pmf (sds R40) a + pmf (sds R40) b + pmf (sds R40) c + pmf (sds R40) d = 1
pmf (sds R40) b = 0
[PROOF STEP]
have "pmf (sds R12) a \<le> pmf (sds R40) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R40) c + pmf (sds R40) d \<le> pmf (sds R44) d + pmf (sds R44) c
0 \<le> pmf (sds R40) a
0 \<le> pmf (sds R40) b
0 \<le> pmf (sds R40) c
0 \<le> pmf (sds R40) d
pmf (sds R40) a + pmf (sds R40) b + pmf (sds R40) c + pmf (sds R40) d = 1
pmf (sds R40) b = 0

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

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R12) a \<le> pmf (sds R40) a

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
from R9_R40.strategyproofness(1) R9.support R40.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R40) b + pmf (sds R40) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R9) b = 0
pmf (sds R40) b = 0
[PROOF STEP]
have "pmf (sds R40) a \<le> pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R40) b + pmf (sds R40) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R9) b = 0
pmf (sds R40) b = 0

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

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

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

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

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

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

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R9) a
pmf (sds R14) a \<le> pmf (sds R16) a
[PROOF STEP]
have "pmf (sds R16) c \<le> pmf (sds R9) a - pmf (sds R14) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R9) a
pmf (sds R14) a \<le> pmf (sds R16) a

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

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R16) c \<le> pmf (sds R9) a - pmf (sds R14) a

goal (3 subgoals):
 1. pmf (sds R16) b = 0
 2. pmf (sds R16) c = 0
 3. pmf (sds R16) d = 1 - pmf (sds R16) a
[PROOF STEP]
from R14_R9.strategyproofness(1) R9.support lottery_conditions[OF R9.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R9) a < pmf (sds R14) a \<or> pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d \<or> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) \<or> pmf (sds R9) a = pmf (sds R14) a \<and> pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d \<and> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)
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
[PROOF STEP]
have "pmf (sds R9) a - pmf (sds R14) a \<le> 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R9) a < pmf (sds R14) a \<or> pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d \<or> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) \<or> pmf (sds R9) a = pmf (sds R14) a \<and> pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d \<and> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)
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

goal (1 subgoal):
 1. pmf (sds R9) a - pmf (sds R14) a \<le> 0
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R9) a - pmf (sds R14) a \<le> 0

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R12_R14: "pmf (sds R14) a \<le> pmf (sds R12) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R14) a \<le> pmf (sds R12) a
[PROOF STEP]
using R14_R16.strategyproofness(1) R16_R12
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R16) c < pmf (sds R14) d \<or> pmf (sds R16) c + pmf (sds R16) d < pmf (sds R14) d + pmf (sds R14) c) \<or> pmf (sds R16) c = pmf (sds R14) d \<and> pmf (sds R16) c + pmf (sds R16) d = pmf (sds R14) d + pmf (sds R14) c
pmf (sds R16) c + pmf (sds R16) a \<le> pmf (sds R12) a

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


[STATEMENT]
lemma R12_a [simp]: "pmf (sds R12) a = pmf (sds R9) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
from R44_R40.strategyproofness(1) R40.support lottery_conditions[OF R40.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R40) c + pmf (sds R40) d \<le> pmf (sds R44) d + pmf (sds R44) c
pmf (sds R40) b = 0
0 \<le> pmf (sds R40) a
0 \<le> pmf (sds R40) b
0 \<le> pmf (sds R40) c
0 \<le> pmf (sds R40) d
pmf (sds R40) a + pmf (sds R40) b + pmf (sds R40) c + pmf (sds R40) d = 1
[PROOF STEP]
have "pmf (sds R12) a \<le> pmf (sds R40) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R40) c + pmf (sds R40) d \<le> pmf (sds R44) d + pmf (sds R44) c
pmf (sds R40) b = 0
0 \<le> pmf (sds R40) a
0 \<le> pmf (sds R40) b
0 \<le> pmf (sds R40) c
0 \<le> pmf (sds R40) d
pmf (sds R40) a + pmf (sds R40) b + pmf (sds R40) c + pmf (sds R40) d = 1

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

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R12) a \<le> pmf (sds R40) a

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
from R9_R40.strategyproofness(1) R9.support R40.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R40) b + pmf (sds R40) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R9) b = 0
pmf (sds R40) b = 0
[PROOF STEP]
have "pmf (sds R40) a \<le> pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R40) b + pmf (sds R40) a \<le> pmf (sds R9) b + pmf (sds R9) a
pmf (sds R9) b = 0
pmf (sds R40) b = 0

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

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R12) a \<le> pmf (sds R9) a
[PROOF STEP]
have B: "pmf (sds R12) a \<le> pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R12) a \<le> pmf (sds R9) a

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

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pmf (sds R12) a \<le> pmf (sds R9) a

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
from R14_R9.strategyproofness(1) lottery_conditions[OF R9.wf] R9.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R9) a < pmf (sds R14) a \<or> pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d \<or> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) \<or> pmf (sds R9) a = pmf (sds R14) a \<and> pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d \<and> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)
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
pmf (sds R9) b = 0
[PROOF STEP]
have "pmf (sds R9) a \<le> pmf (sds R14) a"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R9) a < pmf (sds R14) a \<or> pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d \<or> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) \<or> pmf (sds R9) a = pmf (sds R14) a \<and> pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d \<and> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)
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
pmf (sds R9) b = 0

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

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
with R12_R14
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R14) a \<le> pmf (sds R12) a
pmf (sds R9) a \<le> pmf (sds R14) a
[PROOF STEP]
have "pmf (sds R9) a \<le> pmf (sds R12) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R14) a \<le> pmf (sds R12) a
pmf (sds R9) a \<le> pmf (sds R14) a

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

goal (1 subgoal):
 1. pmf (sds R12) a = pmf (sds R9) a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R12) a \<le> pmf (sds R9) a
pmf (sds R9) a \<le> pmf (sds R12) a
[PROOF STEP]
show "pmf (sds R12) a = pmf (sds R9) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R12) a \<le> pmf (sds R9) a
pmf (sds R9) a \<le> pmf (sds R12) a

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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
[PROOF STEP]
using R12_R14 R14_R9.strategyproofness(1) lottery_conditions[OF R9.wf] R9.support
[PROOF STATE]
proof (prove)
using this:
pmf (sds R14) a \<le> pmf (sds R12) a
(pmf (sds R9) a < pmf (sds R14) a \<or> pmf (sds R9) a + pmf (sds R9) d < pmf (sds R14) a + pmf (sds R14) d \<or> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) < pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)) \<or> pmf (sds R9) a = pmf (sds R14) a \<and> pmf (sds R9) a + pmf (sds R9) d = pmf (sds R14) a + pmf (sds R14) d \<and> pmf (sds R9) a + (pmf (sds R9) d + pmf (sds R9) c) = pmf (sds R14) a + (pmf (sds R14) d + pmf (sds R14) c)
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
pmf (sds R9) b = 0

goal (1 subgoal):
 1. (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
[PROOF STEP]
by auto


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

goal (1 subgoal):
 1. pmf (sds R23) b = 0 &&& pmf (sds R23) c = 0 &&& pmf (sds R23) d = 1 - pmf (sds R23) a
[PROOF STEP]
by (auto simp del: pmf_nonneg)


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (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 STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R35) a = pmf (sds R21) a
 2. pmf (sds R35) b = 0
 3. pmf (sds R35) c = 0
 4. pmf (sds R35) d = 1 - pmf (sds R21) a
[PROOF STEP]
from R35_R21.strategyproofness(1) R35.support
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a) \<le> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a)
pmf (sds R35) b = 0
[PROOF STEP]
have "pmf (sds R21) a \<le> pmf (sds R35) a + pmf (sds R35) c"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a) \<le> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a)
pmf (sds R35) b = 0

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

goal (4 subgoals):
 1. pmf (sds R35) a = pmf (sds R21) a
 2. pmf (sds R35) b = 0
 3. pmf (sds R35) c = 0
 4. pmf (sds R35) d = 1 - pmf (sds R21) a
[PROOF STEP]
with R21_R35.strategyproofness(1) R35.support lottery_conditions[OF R35.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R35) c < pmf (sds R21) c \<or> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) < pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a)) \<or> pmf (sds R35) c = pmf (sds R21) c \<and> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) = pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a)
pmf (sds R35) b = 0
0 \<le> pmf (sds R35) a
0 \<le> pmf (sds R35) b
0 \<le> pmf (sds R35) c
0 \<le> pmf (sds R35) d
pmf (sds R35) a + pmf (sds R35) b + pmf (sds R35) c + pmf (sds R35) d = 1
pmf (sds R21) a \<le> pmf (sds R35) a + pmf (sds R35) c
[PROOF STEP]
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"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R35) c < pmf (sds R21) c \<or> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) < pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a)) \<or> pmf (sds R35) c = pmf (sds R21) c \<and> pmf (sds R35) c + (pmf (sds R35) b + pmf (sds R35) a) = pmf (sds R21) c + (pmf (sds R21) b + pmf (sds R21) a)
pmf (sds R35) b = 0
0 \<le> pmf (sds R35) a
0 \<le> pmf (sds R35) b
0 \<le> pmf (sds R35) c
0 \<le> pmf (sds R35) d
pmf (sds R35) a + pmf (sds R35) b + pmf (sds R35) c + pmf (sds R35) d = 1
pmf (sds R21) a \<le> pmf (sds R35) a + pmf (sds R35) c

goal (1 subgoal):
 1. (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 STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (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 STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R18) a = pmf (sds R14) a
 2. pmf (sds R18) b = 0
 3. pmf (sds R18) d = 0
 4. pmf (sds R18) c = 1 - pmf (sds R14) a
[PROOF STEP]
from R23_R12.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R12) c + pmf (sds R12) a \<le> pmf (sds R23) c + pmf (sds R23) a
[PROOF STEP]
have R21_R23: "pmf (sds R21) a \<le> pmf (sds R23) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R12) c + pmf (sds R12) a \<le> pmf (sds R23) c + pmf (sds R23) a

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

goal (4 subgoals):
 1. pmf (sds R18) a = pmf (sds R14) a
 2. pmf (sds R18) b = 0
 3. pmf (sds R18) d = 0
 4. pmf (sds R18) c = 1 - pmf (sds R14) a
[PROOF STEP]
from R23_R18.strategyproofness(1)
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R18) c + pmf (sds R18) d \<le> pmf (sds R23) d + pmf (sds R23) c
[PROOF STEP]
have "pmf (sds R18) d \<le> pmf (sds R21) a - pmf (sds R23) a"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R18) c + pmf (sds R18) d \<le> pmf (sds R23) d + pmf (sds R23) c

goal (1 subgoal):
 1. pmf (sds R18) d \<le> pmf (sds R21) a - pmf (sds R23) a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R18) d \<le> pmf (sds R21) a - pmf (sds R23) a

goal (4 subgoals):
 1. pmf (sds R18) a = pmf (sds R14) a
 2. pmf (sds R18) b = 0
 3. pmf (sds R18) d = 0
 4. pmf (sds R18) c = 1 - pmf (sds R14) a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R18) d \<le> pmf (sds R21) a - pmf (sds R23) a

goal (4 subgoals):
 1. pmf (sds R18) a = pmf (sds R14) a
 2. pmf (sds R18) b = 0
 3. pmf (sds R18) d = 0
 4. pmf (sds R18) c = 1 - pmf (sds R14) a
[PROOF STEP]
from R21_R23
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R21) a \<le> pmf (sds R23) a
[PROOF STEP]
have "\<dots> \<le> 0"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R21) a \<le> pmf (sds R23) a

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

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

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

goal (3 subgoals):
 1. pmf (sds R18) a = pmf (sds R14) a
 2. pmf (sds R18) b = 0
 3. pmf (sds R18) c = 1 - pmf (sds R14) a
[PROOF STEP]
with lottery_conditions[OF R18.wf] R18.support
[PROOF STATE]
proof (chain)
picking this:
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 R18) b = 0
pmf (sds R18) d = 0
[PROOF STEP]
show "pmf (sds R18) a = pmf (sds R14) a"
         "pmf (sds R18) c = 1 - pmf (sds R14) a"
[PROOF STATE]
proof (prove)
using this:
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 R18) b = 0
pmf (sds R18) d = 0

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

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


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. (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 STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
from R30_R21.strategyproofness(1) R30.support lottery_conditions[OF R30.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R21) b + pmf (sds R21) a < pmf (sds R30) b + pmf (sds R30) a \<or> pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) < pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d)) \<or> pmf (sds R21) b + pmf (sds R21) a = pmf (sds R30) b + pmf (sds R30) a \<and> pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) = pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d)
pmf (sds R30) b = 0
0 \<le> pmf (sds R30) a
0 \<le> pmf (sds R30) b
0 \<le> pmf (sds R30) c
0 \<le> pmf (sds R30) d
pmf (sds R30) a + pmf (sds R30) b + pmf (sds R30) c + pmf (sds R30) d = 1
[PROOF STEP]
have "pmf (sds R4) c + pmf (sds R21) a \<le> pmf (sds R4) c + pmf (sds R30) a"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R21) b + pmf (sds R21) a < pmf (sds R30) b + pmf (sds R30) a \<or> pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) < pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d)) \<or> pmf (sds R21) b + pmf (sds R21) a = pmf (sds R30) b + pmf (sds R30) a \<and> pmf (sds R21) b + (pmf (sds R21) a + pmf (sds R21) d) = pmf (sds R30) b + (pmf (sds R30) a + pmf (sds R30) d)
pmf (sds R30) b = 0
0 \<le> pmf (sds R30) a
0 \<le> pmf (sds R30) b
0 \<le> pmf (sds R30) c
0 \<le> pmf (sds R30) d
pmf (sds R30) a + pmf (sds R30) b + pmf (sds R30) c + pmf (sds R30) d = 1

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

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c + pmf (sds R21) a \<le> pmf (sds R4) c + pmf (sds R30) a

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c + pmf (sds R21) a \<le> pmf (sds R4) c + pmf (sds R30) a

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
have "pmf (sds R30) a \<le> pmf (sds R47) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R30) a \<le> pmf (sds R47) a
[PROOF STEP]
using R47_R30.strategyproofness(1) R30.support R47.support
             lottery_conditions[OF R4.wf] lottery_conditions[OF R47.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R30) b + pmf (sds R30) a \<le> pmf (sds R47) b + pmf (sds R47) a
pmf (sds R30) b = 0
pmf (sds R47) b = 0
0 \<le> pmf (sds R4) a
0 \<le> pmf (sds R4) b
0 \<le> pmf (sds R4) c
0 \<le> pmf (sds R4) d
pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1

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

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pmf (sds R30) a \<le> pmf (sds R47) a

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

goal (1 subgoal):
 1. pmf (sds R4) c \<le> pmf (sds R47) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c \<le> pmf (sds R47) c

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R30) a \<le> pmf (sds R47) a
pmf (sds R4) c \<le> pmf (sds R47) c
[PROOF STEP]
have "pmf (sds R4) c + pmf (sds R30) a \<le> 1 - pmf (sds R47) d"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R30) a \<le> pmf (sds R47) a
pmf (sds R4) c \<le> pmf (sds R47) c

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

goal (1 subgoal):
 1. pmf (sds R4) c + pmf (sds R30) a \<le> 1 - pmf (sds R47) d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c + pmf (sds R30) a \<le> 1 - pmf (sds R47) d

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c + pmf (sds R30) a \<le> 1 - pmf (sds R47) d

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

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

goal (1 subgoal):
 1. pmf (sds R4) c + pmf (sds R14) a \<le> 1
[PROOF STEP]
by (auto simp del: pmf_nonneg)
[PROOF STATE]
proof (state)
this:
pmf (sds R4) c + pmf (sds R14) a \<le> 1

goal (4 subgoals):
 1. pmf (sds R4) a = pmf (sds R21) a
 2. pmf (sds R4) b = 0
 3. pmf (sds R4) c = 1 - pmf (sds R4) a
 4. pmf (sds R4) d = 0
[PROOF STEP]
with R4_R18.strategyproofness(1) lottery_conditions[OF R4.wf] R4.support
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R18) c < pmf (sds R4) c \<or> pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) < pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a)) \<or> pmf (sds R18) c = pmf (sds R4) c \<and> pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) = pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a)
0 \<le> pmf (sds R4) a
0 \<le> pmf (sds R4) b
0 \<le> pmf (sds R4) c
0 \<le> pmf (sds R4) d
pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1
pmf (sds R4) b = 0
pmf (sds R4) c + pmf (sds R14) a \<le> 1
[PROOF STEP]
show "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 STATE]
proof (prove)
using this:
(pmf (sds R18) c < pmf (sds R4) c \<or> pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) < pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a)) \<or> pmf (sds R18) c = pmf (sds R4) c \<and> pmf (sds R18) c + (pmf (sds R18) b + pmf (sds R18) a) = pmf (sds R4) c + (pmf (sds R4) b + pmf (sds R4) a)
0 \<le> pmf (sds R4) a
0 \<le> pmf (sds R4) b
0 \<le> pmf (sds R4) c
0 \<le> pmf (sds R4) d
pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1
pmf (sds R4) b = 0
pmf (sds R4) c + pmf (sds R14) a \<le> 1

goal (1 subgoal):
 1. (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 STEP]
by auto
[PROOF STATE]
proof (state)
this:
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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. pmf (sds R26) a = pmf (sds R8) d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R26) a = pmf (sds R8) d

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R21_R47: "pmf (sds R21) d \<le> pmf (sds R47) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R21) d \<le> pmf (sds R47) c
[PROOF STEP]
using R4_R47.strategyproofness(1) R4.support R47.support
         lottery_conditions[OF R4.wf] lottery_conditions[OF R47.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R47) d + pmf (sds R47) a \<le> pmf (sds R4) d + pmf (sds R4) a
pmf (sds R4) b = 0
pmf (sds R47) b = 0
0 \<le> pmf (sds R4) a
0 \<le> pmf (sds R4) b
0 \<le> pmf (sds R4) c
0 \<le> pmf (sds R4) d
pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1

goal (1 subgoal):
 1. pmf (sds R21) d \<le> pmf (sds R47) c
[PROOF STEP]
by auto


[STATEMENT]
lemma R30 [simp]: "pmf (sds R30) a = pmf (sds R47) a" "pmf (sds R30) b = 0"
  "pmf (sds R30) c = 0" "pmf (sds R30) d = 1 - pmf (sds R47) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pmf (sds R30) a = pmf (sds R47) a &&& pmf (sds R30) b = 0) &&& pmf (sds R30) c = 0 &&& pmf (sds R30) d = 1 - pmf (sds R47) a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. pmf (sds R30) a = pmf (sds R47) a
 2. pmf (sds R30) b = 0
 3. pmf (sds R30) c = 0
 4. pmf (sds R30) d = 1 - pmf (sds R47) a
[PROOF STEP]
have A: "pmf (sds R30) a \<le> pmf (sds R47) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R30) a \<le> pmf (sds R47) a
[PROOF STEP]
using R47_R30.strategyproofness(1) R30.support R47.support
           lottery_conditions[OF R4.wf] lottery_conditions[OF R47.wf]
[PROOF STATE]
proof (prove)
using this:
pmf (sds R30) b + pmf (sds R30) a \<le> pmf (sds R47) b + pmf (sds R47) a
pmf (sds R30) b = 0
pmf (sds R47) b = 0
0 \<le> pmf (sds R4) a
0 \<le> pmf (sds R4) b
0 \<le> pmf (sds R4) c
0 \<le> pmf (sds R4) d
pmf (sds R4) a + pmf (sds R4) b + pmf (sds R4) c + pmf (sds R4) d = 1
0 \<le> pmf (sds R47) a
0 \<le> pmf (sds R47) b
0 \<le> pmf (sds R47) c
0 \<le> pmf (sds R47) d
pmf (sds R47) a + pmf (sds R47) b + pmf (sds R47) c + pmf (sds R47) d = 1

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

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

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

goal:
No subgoals!
[PROOF STEP]
(* tricky step! *)
[PROOF STATE]
proof (state)
this:
pmf (sds R30) a = pmf (sds R47) a
pmf (sds R30) b = 0
pmf (sds R30) c = 0
pmf (sds R30) d = 1 - pmf (sds R47) a

goal:
No subgoals!
[PROOF STEP]
qed