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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed