[STATEMENT]
lemma Theorem_11_Pd'_tax:
  shows "\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)) \<Longrightarrow> False
[PROOF STEP]
let ?Z = "TruePref_tax.cop ds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x))

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x))
[PROOF STEP]
have "Xd x \<notin> Xd ` ?Z"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x))

goal (1 subgoal):
 1. Xd x \<notin> Xd ` TruePref_tax.cop ds
[PROOF STEP]
using Pd'_range Pd'_linear[of "Xd x"] Pd'_d'_x
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x))
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
Linear_order (Pd' (Xd x))
x \<in> Field (Pd' (Xd x))

goal (1 subgoal):
 1. Xd x \<notin> Xd ` TruePref_tax.cop ds
[PROOF STEP]
unfolding order_on_defs
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x))
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
((Refl (Pd' (Xd x)) \<and> trans (Pd' (Xd x))) \<and> antisym (Pd' (Xd x))) \<and> Total (Pd' (Xd x))
x \<in> Field (Pd' (Xd x))

goal (1 subgoal):
 1. Xd x \<notin> Xd ` TruePref_tax.cop ds
[PROOF STEP]
by - (clarsimp, drule (1) bspec,
          fastforce simp: Pd'_tax_def above_def Refl_Field_Restr dest: refl_onD
                   dest!: CH_range' TruePref_tax.fp_cop_F_range_inv')
[PROOF STATE]
proof (state)
this:
Xd x \<notin> Xd ` TruePref_tax.cop ds

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases "Singleton_for_d.stable_on ds ?Z")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Singleton_for_d.stable_on ds (TruePref_tax.cop ds)

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Singleton_for_d.stable_on ds (TruePref_tax.cop ds)

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
from Theorem_10_fp_cop_F[OF X x, of "Xd x"] X
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>Singleton_for_d.cop ds. (x, y) \<in> Pd_singletons_for_ds X {Xd x} (Xd x)
stable_on ds X
[PROOF STEP]
have "x \<in> CH (Singleton_for_d.fp_cop_F ds)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>Singleton_for_d.cop ds. (x, y) \<in> Pd_singletons_for_ds X {Xd x} (Xd x)
stable_on ds X

goal (1 subgoal):
 1. x \<in> Singleton_for_d.cop ds
[PROOF STEP]
by (force simp: Pd_singletons_for_ds_simps dX_def dest: inj_onD stable_on_allocation)
[PROOF STATE]
proof (state)
this:
x \<in> Singleton_for_d.cop ds

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
with Singleton_for_d.fp_cop_F_allocation
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd (Singleton_for_d.cop ?ds)
x \<in> Singleton_for_d.cop ds
[PROOF STEP]
have "Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd (Singleton_for_d.cop ?ds)
x \<in> Singleton_for_d.cop ds

goal (1 subgoal):
 1. Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}
[PROOF STEP]
by (meson Singleton_for_d.Cd_single Singleton_for_d.Cd_singleton Singleton_for_d.fp_cop_F_range_inv'
                TruePref_tax.CH_range')
[PROOF STATE]
proof (state)
this:
Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
with Singleton_for_d.Theorem_1[of ds]
[PROOF STATE]
proof (chain)
picking this:
Singleton_for_d.stable_on ds (Singleton_for_d.cop ds)
Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}
[PROOF STEP]
have "x \<in> Y" if "Singleton_for_d.stable_on ds Y" for Y
[PROOF STATE]
proof (prove)
using this:
Singleton_for_d.stable_on ds (Singleton_for_d.cop ds)
Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}

goal (1 subgoal):
 1. x \<in> Y
[PROOF STEP]
using Singleton_for_d.Theorem_6_fp_cop_F(1)[where ds="ds" and X="Y" and d="Xd x"] that Xd_x_ds x
            card_Suc_eq[where A="Singleton_for_d.Cd (Xd x) Y" and k=0] stable_on_allocation[OF X]
[PROOF STATE]
proof (prove)
using this:
Singleton_for_d.stable_on ds (Singleton_for_d.cop ds)
Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}
\<lbrakk>Singleton_for_d.stable_on ds Y; Xd x \<in> ds\<rbrakk> \<Longrightarrow> card (Singleton_for_d.Cd (Xd x) Y) = card (Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds))
Singleton_for_d.stable_on ds Y
Xd x \<in> ds
x \<in> X
(card (Singleton_for_d.Cd (Xd x) Y) = Suc 0) = (\<exists>b B. Singleton_for_d.Cd (Xd x) Y = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}))
inj_on Xd X

goal (1 subgoal):
 1. x \<in> Y
[PROOF STEP]
by (fastforce simp: Singleton_for_d.Cd_singleton[symmetric] Pd_singletons_for_ds_simps dX_def
                    dest: Singleton_for_d.Cd_range' inj_onD)
[PROOF STATE]
proof (state)
this:
Singleton_for_d.stable_on ds ?Y \<Longrightarrow> x \<in> ?Y

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Singleton_for_d.stable_on ds ?Y \<Longrightarrow> x \<in> ?Y

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
note \<open>Xd x \<notin> Xd ` ?Z\<close>
[PROOF STATE]
proof (state)
this:
Xd x \<notin> Xd ` TruePref_tax.cop ds

goal (2 subgoals):
 1. Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Singleton_for_d.stable_on ds (TruePref_tax.cop ds)
Singleton_for_d.stable_on ds ?Y \<Longrightarrow> x \<in> ?Y
Xd x \<notin> Xd ` TruePref_tax.cop ds
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Singleton_for_d.stable_on ds (TruePref_tax.cop ds)
Singleton_for_d.stable_on ds ?Y \<Longrightarrow> x \<in> ?Y
Xd x \<notin> Xd ` TruePref_tax.cop ds

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
note \<open>\<not>Singleton_for_d.stable_on ds ?Z\<close>
[PROOF STATE]
proof (state)
this:
\<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> Singleton_for_d.stable_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases rule: Singleton_for_d.not_stable_on_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> Singleton_for_d.individually_rational_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
case not_individually_rational
[PROOF STATE]
proof (state)
this:
\<not> Singleton_for_d.individually_rational_on ds (TruePref_tax.cop ds)

goal (2 subgoals):
 1. \<not> Singleton_for_d.individually_rational_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
 2. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
with TruePref_tax.Theorem_1[of ds] \<open>Xd x \<notin> Xd ` ?Z\<close>
[PROOF STATE]
proof (chain)
picking this:
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
\<not> Singleton_for_d.individually_rational_on ds (TruePref_tax.cop ds)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
\<not> Singleton_for_d.individually_rational_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding TruePref_tax.stable_on_def Singleton_for_d.individually_rational_on_def
                  TruePref_tax.individually_rational_on_def Singleton_for_d.CD_on_def
[PROOF STATE]
proof (prove)
using this:
(TruePref_tax.CD_on ds (TruePref_tax.cop ds) = TruePref_tax.cop ds \<and> Singleton_for_d.CH (TruePref_tax.cop ds) = TruePref_tax.cop ds) \<and> TruePref_tax.stable_no_blocking_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
\<not> ((\<Union>d\<in>ds. Singleton_for_d.Cd d (TruePref_tax.cop ds)) = TruePref_tax.cop ds \<and> Singleton_for_d.CH (TruePref_tax.cop ds) = TruePref_tax.cop ds)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest: Singleton_for_d.Cd_range')
           (metis TruePref_tax.mem_CD_on_Cd TruePref_tax_Cd_not_x image_eqI)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
case not_no_blocking
[PROOF STATE]
proof (state)
this:
\<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds)
[PROOF STEP]
obtain h X'' where "Singleton_for_d.blocking_on ds ?Z h X''"
[PROOF STATE]
proof (prove)
using this:
\<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds)

goal (1 subgoal):
 1. (\<And>h X''. Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Singleton_for_d.stable_no_blocking_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>h X'. \<not> Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X')

goal (1 subgoal):
 1. (\<And>h X''. Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X''

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
have "TruePref_tax.blocking_on ds ?Z h X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TruePref_tax.blocking_on ds (TruePref_tax.cop ds) h X''
[PROOF STEP]
proof(rule TruePref_tax.blocking_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h (TruePref_tax.cop ds)
 2. X'' = Ch h (TruePref_tax.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h (TruePref_tax.cop ds)
 2. X'' = Ch h (TruePref_tax.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
assume "y \<in> X''"
[PROOF STATE]
proof (state)
this:
y \<in> X''

goal (3 subgoals):
 1. X'' \<noteq> Ch h (TruePref_tax.cop ds)
 2. X'' = Ch h (TruePref_tax.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
with \<open>Singleton_for_d.blocking_on ds ?Z h X''\<close>
[PROOF STATE]
proof (chain)
picking this:
Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X''
y \<in> X''
[PROOF STEP]
have YYY: "y \<in> Singleton_for_d.CD_on ds (?Z \<union> X'')"
[PROOF STATE]
proof (prove)
using this:
Singleton_for_d.blocking_on ds (TruePref_tax.cop ds) h X''
y \<in> X''

goal (1 subgoal):
 1. y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
unfolding Singleton_for_d.blocking_on_def
[PROOF STATE]
proof (prove)
using this:
X'' \<noteq> Ch h (TruePref_tax.cop ds) \<and> X'' = Ch h (TruePref_tax.cop ds \<union> X'') \<and> X'' \<subseteq> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
y \<in> X''

goal (1 subgoal):
 1. y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')

goal (3 subgoals):
 1. X'' \<noteq> Ch h (TruePref_tax.cop ds)
 2. X'' = Ch h (TruePref_tax.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
show "y \<in> TruePref_tax.CD_on ds (?Z \<union> X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
proof(cases "Xd y = Xd x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Xd y = Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
 2. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Xd y = Xd x

goal (2 subgoals):
 1. Xd y = Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
 2. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
with inj_on_eq_iff[OF stable_on_allocation x] X YYY
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stable_on ?ds2 X; ?y \<in> X\<rbrakk> \<Longrightarrow> (Xd x = Xd ?y) = (x = ?y)
stable_on ds X
y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
Xd y = Xd x
[PROOF STEP]
have "y = x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stable_on ?ds2 X; ?y \<in> X\<rbrakk> \<Longrightarrow> (Xd x = Xd ?y) = (x = ?y)
stable_on ds X
y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
Xd y = Xd x

goal (1 subgoal):
 1. y = x
[PROOF STEP]
by (fastforce simp: Singleton_for_d.mem_CD_on_Cd Pd_singletons_for_ds_simps dX_def
                          dest: Singleton_for_d.Cd_range')
[PROOF STATE]
proof (state)
this:
y = x

goal (2 subgoals):
 1. Xd y = Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
 2. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
with X Xd_x_ds TruePref_tax.Theorem_1[of ds] \<open>Xd x \<notin> Xd ` ?Z\<close> \<open>y \<in> X''\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
Xd x \<in> ds
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
y \<in> X''
y = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
Xd x \<in> ds
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
y \<in> X''
y = x

goal (1 subgoal):
 1. y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
using Singleton_for_d.blocking_on_allocation[OF \<open>Singleton_for_d.blocking_on ds ?Z h X''\<close>]
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
Xd x \<in> ds
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
Xd x \<notin> Xd ` TruePref_tax.cop ds
y \<in> X''
y = x
inj_on Xd X''

goal (1 subgoal):
 1. y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
by (clarsimp simp: TruePref_tax.mem_CD_on_Cd TruePref_tax.Cd_greatest greatest_def Pd'_tax_x)
               (metis TruePref_tax.Pd_range' image_eqI inj_on_contraD TruePref_tax.Pd_refl)
[PROOF STATE]
proof (state)
this:
y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')

goal (1 subgoal):
 1. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Xd y \<noteq> Xd x

goal (1 subgoal):
 1. Xd y \<noteq> Xd x \<Longrightarrow> y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
with YYY
[PROOF STATE]
proof (chain)
picking this:
y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
Xd y \<noteq> Xd x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> Singleton_for_d.CD_on ds (TruePref_tax.cop ds \<union> X'')
Xd y \<noteq> Xd x

goal (1 subgoal):
 1. y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
by (simp add: Singleton_for_d.mem_CD_on_Cd TruePref_tax.mem_CD_on_Cd TruePref_tax_Cd_not_x)
[PROOF STATE]
proof (state)
this:
y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> TruePref_tax.CD_on ds (TruePref_tax.cop ds \<union> X'')

goal (2 subgoals):
 1. X'' \<noteq> Ch h (TruePref_tax.cop ds)
 2. X'' = Ch h (TruePref_tax.cop ds \<union> X'')
[PROOF STEP]
qed (use \<open>Singleton_for_d.blocking_on ds ?Z h X''\<close> in \<open>simp_all add: Singleton_for_d.blocking_on_def\<close>)
[PROOF STATE]
proof (state)
this:
TruePref_tax.blocking_on ds (TruePref_tax.cop ds) h X''

goal (1 subgoal):
 1. \<not> Singleton_for_d.stable_no_blocking_on ds (TruePref_tax.cop ds) \<Longrightarrow> False
[PROOF STEP]
with TruePref_tax.Theorem_1[of ds]
[PROOF STATE]
proof (chain)
picking this:
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
TruePref_tax.blocking_on ds (TruePref_tax.cop ds) h X''
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
TruePref_tax.blocking_on ds (TruePref_tax.cop ds) h X''

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: TruePref_tax.blocking_on_imp_not_stable)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Theorem_11_fp_cop_F:
  shows "\<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
from Theorem_11_Pd'_tax
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)
[PROOF STEP]
obtain y where y: "y \<in> CH (TruePref_tax.fp_cop_F ds)"
            and xy: "(x, y) \<in> Pd'_tax (Xd x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>TruePref_tax.cop ds. (x, y) \<in> Pd'_tax (Xd x)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> TruePref_tax.cop ds; (x, y) \<in> Pd'_tax (Xd x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
y \<in> TruePref_tax.cop ds
(x, y) \<in> Pd'_tax (Xd x)

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
from TruePref_tax.stable_on_range'[OF TruePref_tax.Theorem_1]
[PROOF STATE]
proof (chain)
picking this:
?x \<in> TruePref_tax.cop ?ds \<Longrightarrow> ?x \<in> Field (Pd'_tax (Xd ?x))
[PROOF STEP]
have "dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x) \<subseteq> Field (Pd' (Xd x))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> TruePref_tax.cop ?ds \<Longrightarrow> ?x \<in> Field (Pd'_tax (Xd ?x))

goal (1 subgoal):
 1. Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x) \<subseteq> Field (Pd' (Xd x))
[PROOF STEP]
by (clarsimp simp: dX_def) (metis (no_types, opaque_lifting) Pd'_tax_Pd' contra_subsetD mono_Field)
[PROOF STATE]
proof (state)
this:
Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x) \<subseteq> Field (Pd' (Xd x))

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x) \<subseteq> Field (Pd' (Xd x))

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
from TruePref_tax.fp_cop_F_allocation[of ds] Pd'_tax_Pd' y xy
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd (TruePref_tax.cop ds)
Pd'_tax ?d \<subseteq> Pd' ?d
y \<in> TruePref_tax.cop ds
(x, y) \<in> Pd'_tax (Xd x)
[PROOF STEP]
have "Above (Pd' (Xd x)) (dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x))
     \<subseteq> Above (Pd'_tax (Xd x)) (dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x))"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd (TruePref_tax.cop ds)
Pd'_tax ?d \<subseteq> Pd' ?d
y \<in> TruePref_tax.cop ds
(x, y) \<in> Pd'_tax (Xd x)

goal (1 subgoal):
 1. Above (Pd' (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x)) \<subseteq> Above (Pd'_tax (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x))
[PROOF STEP]
by - (rule Pd'_Above; fastforce simp: dX_singular above_def dest: TruePref_tax.Pd_Xd)
[PROOF STATE]
proof (state)
this:
Above (Pd' (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x)) \<subseteq> Above (Pd'_tax (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x))

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Above (Pd' (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x)) \<subseteq> Above (Pd'_tax (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x))

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
note Pd'_linear Pd'_range TruePref_tax.Theorem_1[of ds] y
[PROOF STATE]
proof (state)
this:
Linear_order (Pd' ?d)
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
y \<in> TruePref_tax.cop ds

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x) \<subseteq> Field (Pd' (Xd x))
Above (Pd' (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x)) \<subseteq> Above (Pd'_tax (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x))
Linear_order (Pd' ?d)
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
y \<in> TruePref_tax.cop ds
[PROOF STEP]
have z: "\<exists>z\<in>CH (TruePref.fp_cop_F ds). (y, z) \<in> Pd' (Xd y)"
[PROOF STATE]
proof (prove)
using this:
Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x) \<subseteq> Field (Pd' (Xd x))
Above (Pd' (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x)) \<subseteq> Above (Pd'_tax (Xd x)) (Singleton_for_d.dX (TruePref_tax.cop ds) (Xd x))
Linear_order (Pd' ?d)
Field (Pd' ?d) \<subseteq> {x. Xd x = ?d}
TruePref_tax.stable_on ds (TruePref_tax.cop ds)
y \<in> TruePref_tax.cop ds

goal (1 subgoal):
 1. \<exists>z\<in>TruePref.cop ds. (y, z) \<in> Pd' (Xd y)
[PROOF STEP]
by - (rule TruePref_tax.Pd_above_irrelevant[where d'="Xd x" and X="CH (TruePref_tax.fp_cop_F ds)"];
          simp add: Pd'_tax_def)
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>TruePref.cop ds. (y, z) \<in> Pd' (Xd y)

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
from Pd'_linear xy z
[PROOF STATE]
proof (chain)
picking this:
Linear_order (Pd' ?d)
(x, y) \<in> Pd'_tax (Xd x)
\<exists>z\<in>TruePref.cop ds. (y, z) \<in> Pd' (Xd y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd' ?d)
(x, y) \<in> Pd'_tax (Xd x)
\<exists>z\<in>TruePref.cop ds. (y, z) \<in> Pd' (Xd y)

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
unfolding Pd'_tax_def order_on_defs
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd' ?d) \<and> trans (Pd' ?d)) \<and> antisym (Pd' ?d)) \<and> Total (Pd' ?d)
(x, y) \<in> (Pd'(Xd x := Restr (Pd' (Xd x)) (above (Pd' (Xd x)) x))) (Xd x)
\<exists>z\<in>TruePref.cop ds. (y, z) \<in> Pd' (Xd y)

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
by clarsimp (metis TruePref.Pd_Xd transE)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Theorem_11:
  shows "\<exists>y\<in>match (TruePref.gfp_F ds). (x, y) \<in> Pd' (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>TruePref.match (TruePref.gfp_F ds). (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
using Theorem_11_fp_cop_F TruePref.Theorem_15_match
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>TruePref.cop ds. (x, y) \<in> Pd' (Xd x)
TruePref.match (TruePref.gfp_F ?ds) = TruePref.cop ?ds

goal (1 subgoal):
 1. \<exists>y\<in>TruePref.match (TruePref.gfp_F ds). (x, y) \<in> Pd' (Xd x)
[PROOF STEP]
by simp


[STATEMENT]
lemma strategy_proofI:
  assumes "\<And>Pd Pd' Ch d y. \<lbrakk> mechanism_domain Pd Ch; mechanism_domain (Pd(d:=Pd')) Ch; d \<in> ds;
                             y \<in> \<phi> (Pd(d := Pd')) Ch ds; y \<in> Field (Pd d);
                             \<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d \<rbrakk> \<Longrightarrow> False"
  shows "strategy_proof ds \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strategy_proof ds \<phi>
[PROOF STEP]
unfolding strategy_proof_def AboveS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Pd Ch. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch \<longrightarrow> \<not> (\<exists>d\<in>ds. \<exists>Pd'. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch \<and> (\<exists>y\<in>\<phi> (Pd(d := Pd')) Ch ds. y \<in> {b \<in> Field (Pd d). \<forall>a\<in>dX (\<phi> Pd Ch ds) d. b \<noteq> a \<and> (a, b) \<in> Pd d}))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd ?Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (?Pd(?d := ?Pd')) ?Ch; ?d \<in> ds; ?y \<in> \<phi> (?Pd(?d := ?Pd')) ?Ch ds; ?y \<in> Field (?Pd ?d); \<forall>x\<in>dX (\<phi> ?Pd ?Ch ds) ?d. x \<noteq> ?y \<and> (x, ?y) \<in> ?Pd ?d\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>Pd Ch. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch \<longrightarrow> \<not> (\<exists>d\<in>ds. \<exists>Pd'. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch \<and> (\<exists>y\<in>\<phi> (Pd(d := Pd')) Ch ds. y \<in> {b \<in> Field (Pd d). \<forall>a\<in>dX (\<phi> Pd Ch ds) d. b \<noteq> a \<and> (a, b) \<in> Pd d}))
[PROOF STEP]
by blast


[STATEMENT]
theorem fp_cop_F_strategy_proof:
  shows "strategy_proof ds Contracts.cop" (is "strategy_proof _ ?\<phi>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strategy_proof ds (\<lambda>Pd Ch ds. Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds))
[PROOF STEP]
proof %invisible (rule strategy_proofI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix Pd Pd' Ch d y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A: "mechanism_domain Pd Ch" and B: "mechanism_domain (Pd(d:=Pd')) Ch"
     and y: "y \<in> ?\<phi> (Pd(d := Pd')) Ch ds" "y \<in> Field (Pd d)" "\<forall>x\<in>dX (?\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d"
[PROOF STATE]
proof (state)
this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds)
y \<in> Field (Pd d)
\<forall>x\<in>dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
[PROOF STEP]
interpret TruePref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
[PROOF STATE]
proof (prove)
using this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>TruePref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from B
[PROOF STATE]
proof (chain)
picking this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
[PROOF STEP]
interpret ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd(d := Pd')" Ch
[PROOF STATE]
proof (prove)
using this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from B y
[PROOF STATE]
proof (chain)
picking this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
y \<in> ManiPref.cop ds
y \<in> Field (Pd d)
\<forall>x\<in>ManiPref.dX (TruePref.cop ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d
[PROOF STEP]
interpret ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh "Pd(d := Pd')" Ch y "?\<phi> (Pd(d := Pd')) Ch ds" ds Pd
[PROOF STATE]
proof (prove)
using this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
y \<in> ManiPref.cop ds
y \<in> Field (Pd d)
\<forall>x\<in>ManiPref.dX (TruePref.cop ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh (Pd(d := Pd')) Ch y (ManiPref.cop ds) ds Pd
[PROOF STEP]
by unfold_locales (simp_all add: FieldI2 TruePref.Pd_Xd TruePref.Pd_linear TruePref.Pd_range' subsetI ManiPref.Theorem_1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ManiPref.Theorem_11_fp_cop_F
[PROOF STATE]
proof (chain)
picking this:
\<exists>ya\<in>TruePref.cop ds. (y, ya) \<in> Pd (Xd y)
[PROOF STEP]
obtain z where "z \<in> TruePref.cop ds" "(y, z) \<in> Pd (Xd y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ya\<in>TruePref.cop ds. (y, ya) \<in> Pd (Xd y)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> TruePref.cop ds; (y, z) \<in> Pd (Xd y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
z \<in> TruePref.cop ds
(y, z) \<in> Pd (Xd y)

goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> Contracts.CH Ch (Contracts.fp_cop_F (Pd(d := Pd')) Ch ds); y \<in> Field (Pd d); \<forall>x\<in>ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with TruePref.Pd_linear TruePref.stable_on_allocation[OF TruePref.Theorem_1[of ds]] TruePref.Pd_Xd TruePref.Pd_range' y
[PROOF STATE]
proof (chain)
picking this:
\<forall>d. Linear_order (Pd d)
inj_on Xd (TruePref.cop ds)
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
y \<in> ManiPref.cop ds
y \<in> Field (Pd d)
\<forall>x\<in>ManiPref.dX (TruePref.cop ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d
z \<in> TruePref.cop ds
(y, z) \<in> Pd (Xd y)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Linear_order (Pd d)
inj_on Xd (TruePref.cop ds)
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
y \<in> ManiPref.cop ds
y \<in> Field (Pd d)
\<forall>x\<in>ManiPref.dX (TruePref.cop ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d
z \<in> TruePref.cop ds
(y, z) \<in> Pd (Xd y)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding order_on_defs antisym_def dX_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d. ((Refl (Pd d) \<and> trans (Pd d)) \<and> (\<forall>x y. (x, y) \<in> Pd d \<longrightarrow> (y, x) \<in> Pd d \<longrightarrow> x = y)) \<and> Total (Pd d)
inj_on Xd (TruePref.cop ds)
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
y \<in> ManiPref.cop ds
y \<in> Field (Pd d)
\<forall>x\<in>{x \<in> TruePref.cop ds. Xd x = d}. x \<noteq> y \<and> (x, y) \<in> Pd d
z \<in> TruePref.cop ds
(y, z) \<in> Pd (Xd y)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma group_strategy_proofI:
  assumes "\<And>Pd Pd' Ch ds'. \<lbrakk> mechanism_domain Pd Ch; mechanism_domain (override_on Pd Pd' ds') Ch; ds' \<subseteq> ds; ds' \<noteq> {};
                             \<forall>d\<in>ds'. \<exists>y\<in>\<phi> (override_on Pd Pd' ds') Ch ds. y \<in> AboveS (Pd d) (dX (\<phi> Pd Ch ds) d) \<rbrakk> \<Longrightarrow> False"
  shows "group_strategy_proof ds \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_strategy_proof ds \<phi>
[PROOF STEP]
unfolding group_strategy_proof_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Pd Ch. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch \<longrightarrow> \<not> (\<exists>ds'\<subseteq>ds. ds' \<noteq> {} \<and> (\<exists>Pd'. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pd' ds') Ch \<and> (\<forall>d\<in>ds'. \<exists>y\<in>\<phi> (override_on Pd Pd' ds') Ch ds. y \<in> AboveS (Pd d) (dX (\<phi> Pd Ch ds) d))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd ?Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on ?Pd ?Pd' ?ds') ?Ch; ?ds' \<subseteq> ds; ?ds' \<noteq> {}; \<forall>d\<in>?ds'. \<exists>y\<in>\<phi> (override_on ?Pd ?Pd' ?ds') ?Ch ds. y \<in> AboveS (?Pd d) (dX (\<phi> ?Pd ?Ch ds) d)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>Pd Ch. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch \<longrightarrow> \<not> (\<exists>ds'\<subseteq>ds. ds' \<noteq> {} \<and> (\<exists>Pd'. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pd' ds') Ch \<and> (\<forall>d\<in>ds'. \<exists>y\<in>\<phi> (override_on Pd Pd' ds') Ch ds. y \<in> AboveS (Pd d) (dX (\<phi> Pd Ch ds) d))))
[PROOF STEP]
by blast


[STATEMENT]
lemma group_strategy_proof_strategy_proof:
  assumes "group_strategy_proof ds \<phi>"
  shows "strategy_proof ds \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strategy_proof ds \<phi>
[PROOF STEP]
proof %invisible (rule strategy_proofI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> \<phi> (Pd(d := Pd')) Ch ds; y \<in> Field (Pd d); \<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix Pd Pd' Ch d y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> \<phi> (Pd(d := Pd')) Ch ds; y \<in> Field (Pd d); \<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "mechanism_domain Pd Ch" "mechanism_domain (Pd(d := Pd')) Ch" "d \<in> ds"
         "y \<in> \<phi> (Pd(d := Pd')) Ch ds" "y \<in> Field (Pd d)" "\<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d"
[PROOF STATE]
proof (state)
this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
d \<in> ds
y \<in> \<phi> (Pd(d := Pd')) Ch ds
y \<in> Field (Pd d)
\<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<And>Pd Pd' Ch d y. \<lbrakk>ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch; ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch; d \<in> ds; y \<in> \<phi> (Pd(d := Pd')) Ch ds; y \<in> Field (Pd d); \<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
group_strategy_proof ds \<phi>
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
d \<in> ds
y \<in> \<phi> (Pd(d := Pd')) Ch ds
y \<in> Field (Pd d)
\<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
group_strategy_proof ds \<phi>
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
d \<in> ds
y \<in> \<phi> (Pd(d := Pd')) Ch ds
y \<in> Field (Pd d)
\<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding group_strategy_proof_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch \<longrightarrow> \<not> (\<exists>ds'\<subseteq>ds. ds' \<noteq> {} \<and> (\<exists>Pd'. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pd' ds') Ch \<and> (\<forall>d\<in>ds'. \<exists>y\<in>\<phi> (override_on Pd Pd' ds') Ch ds. y \<in> AboveS (Pd d) (dX (\<phi> Pd Ch ds) d))))
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd(d := Pd')) Ch
d \<in> ds
y \<in> \<phi> (Pd(d := Pd')) Ch ds
y \<in> Field (Pd d)
\<forall>x\<in>dX (\<phi> Pd Ch ds) d. x \<noteq> y \<and> (x, y) \<in> Pd d

goal (1 subgoal):
 1. False
[PROOF STEP]
by (clarsimp dest!: spec[where x=Pd] spec[where x=Ch])
       (fastforce simp: override_on_insert AboveS_def dest!: spec[where x="{d}"])
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shuffle_to_top_Field:
  assumes "allocation Y"
  shows "Field (shuffle_to_top Y d) = Field (Pd d) \<union> dX Y d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (shuffle_to_top Y d) = Field (Pd d) \<union> dX Y d
[PROOF STEP]
unfolding shuffle_to_top_def Field_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Domain (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) \<union> Range (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) = Domain (Pd d) \<union> Range (Pd d) \<union> dX Y d
[PROOF STEP]
using dX_empty_or_singleton[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>d. dX Y d = {} \<or> (\<exists>x. dX Y d = {x})

goal (1 subgoal):
 1. Domain (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) \<union> Range (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) = Domain (Pd d) \<union> Range (Pd d) \<union> dX Y d
[PROOF STEP]
by (auto simp: Domain.simps; meson FieldI2 equalityE Pd_refl)


[STATEMENT]
lemma shuffle_to_top_Total:
  assumes "allocation Y"
  shows "Total (shuffle_to_top Y d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Total (shuffle_to_top Y d)
[PROOF STEP]
using Pd_linear'[of d] dX_empty_or_singleton[OF assms]
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd d)
\<forall>d. dX Y d = {} \<or> (\<exists>x. dX Y d = {x})

goal (1 subgoal):
 1. Total (shuffle_to_top Y d)
[PROOF STEP]
unfolding order_on_defs total_on_def shuffle_to_top_Field[OF assms]
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd d) \<and> trans (Pd d)) \<and> antisym (Pd d)) \<and> (\<forall>x\<in>Field (Pd d). \<forall>y\<in>Field (Pd d). x \<noteq> y \<longrightarrow> (x, y) \<in> Pd d \<or> (y, x) \<in> Pd d)
\<forall>d. dX Y d = {} \<or> (\<exists>x. dX Y d = {x})

goal (1 subgoal):
 1. \<forall>x\<in>Field (Pd d) \<union> dX Y d. \<forall>y\<in>Field (Pd d) \<union> dX Y d. x \<noteq> y \<longrightarrow> (x, y) \<in> shuffle_to_top Y d \<or> (y, x) \<in> shuffle_to_top Y d
[PROOF STEP]
by (auto simp: shuffle_to_top_def Domain.simps dest: refl_onD)


[STATEMENT]
lemma shuffle_to_top_linear:
  assumes "allocation Y"
  shows "Linear_order (shuffle_to_top Y d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (shuffle_to_top Y d)
[PROOF STEP]
using Pd_linear'[of d] dX_empty_or_singleton[OF assms] shuffle_to_top_Total[OF assms]
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd d)
\<forall>d. dX Y d = {} \<or> (\<exists>x. dX Y d = {x})
Total (shuffle_to_top Y ?d)

goal (1 subgoal):
 1. Linear_order (shuffle_to_top Y d)
[PROOF STEP]
unfolding shuffle_to_top_def order_on_defs
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd d) \<and> trans (Pd d)) \<and> antisym (Pd d)) \<and> Total (Pd d)
\<forall>d. dX Y d = {} \<or> (\<exists>x. dX Y d = {x})
Total (Pd ?d - dX Y ?d \<times> UNIV \<union> (Domain (Pd ?d) \<union> dX Y ?d) \<times> dX Y ?d)

goal (1 subgoal):
 1. ((Refl (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) \<and> trans (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d)) \<and> antisym (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d)) \<and> Total (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d)
[PROOF STEP]
by (auto simp: Field_def intro!: antisymI refl_onI transI dest: refl_onD antisymD elim: transE)


[STATEMENT]
lemma shuffle_to_top_range:
  shows "Field (shuffle_to_top Y d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (shuffle_to_top Y d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
unfolding shuffle_to_top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd_range dX_range
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<forall>d. dX ?X d \<subseteq> {x. Xd x = d}

goal (1 subgoal):
 1. Field (Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (force simp: Field_def)


[STATEMENT]
lemma shuffle_to_top_range':
  assumes "(x, y) \<in> shuffle_to_top Y d"
  shows "x \<in> Field (Pd d) \<union> dX Y d \<and> y \<in> Field (Pd d) \<union> dX Y d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Field (Pd d) \<union> dX Y d \<and> y \<in> Field (Pd d) \<union> dX Y d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> shuffle_to_top Y d

goal (1 subgoal):
 1. x \<in> Field (Pd d) \<union> dX Y d \<and> y \<in> Field (Pd d) \<union> dX Y d
[PROOF STEP]
unfolding shuffle_to_top_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> Pd d - dX Y d \<times> UNIV \<union> (Domain (Pd d) \<union> dX Y d) \<times> dX Y d

goal (1 subgoal):
 1. x \<in> Field (Pd d) \<union> dX Y d \<and> y \<in> Field (Pd d) \<union> dX Y d
[PROOF STEP]
by (auto intro: FieldI1 FieldI2)


[STATEMENT]
lemma Pd_shuffle_to_top_linear:
  assumes "allocation Y"
  shows "Linear_order (Pd_shuffle_to_top ds' Y d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (Pd_shuffle_to_top ds' Y d)
[PROOF STEP]
unfolding Pd_shuffle_to_top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (override_on Pd (shuffle_to_top Y) ds' d)
[PROOF STEP]
using Pd_linear shuffle_to_top_linear[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Linear_order (Pd d)
Linear_order (shuffle_to_top Y ?d)

goal (1 subgoal):
 1. Linear_order (override_on Pd (shuffle_to_top Y) ds' d)
[PROOF STEP]
by (cases "d \<in> ds'") simp_all


[STATEMENT]
lemma Pd_shuffle_to_top_range:
  shows "Field (Pd_shuffle_to_top ds' Y d) \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd_shuffle_to_top ds' Y d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
unfolding Pd_shuffle_to_top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (override_on Pd (shuffle_to_top Y) ds' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
using Pd_range shuffle_to_top_range
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Field (shuffle_to_top ?Y ?d) \<subseteq> {x. Xd x = ?d}

goal (1 subgoal):
 1. Field (override_on Pd (shuffle_to_top Y) ds' d) \<subseteq> {x. Xd x = d}
[PROOF STEP]
by (cases "d \<in> ds'") simp_all


[STATEMENT]
lemma Pd_shuffle_to_top_simps:
  shows "Pd_shuffle_to_top (insert d ds') Y = (Pd_shuffle_to_top ds' Y)(d := shuffle_to_top Y d)"
    and "d \<in> ds' \<Longrightarrow> Pd_shuffle_to_top ds' Y d = shuffle_to_top Y d"
    and "d \<notin> ds' \<Longrightarrow> Pd_shuffle_to_top ds' Y d = Pd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pd_shuffle_to_top (insert d ds') Y = (Pd_shuffle_to_top ds' Y)(d := shuffle_to_top Y d) &&& (d \<in> ds' \<Longrightarrow> Pd_shuffle_to_top ds' Y d = shuffle_to_top Y d) &&& (d \<notin> ds' \<Longrightarrow> Pd_shuffle_to_top ds' Y d = Pd d)
[PROOF STEP]
unfolding Pd_shuffle_to_top_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. override_on Pd (shuffle_to_top Y) (insert d ds') = (override_on Pd (shuffle_to_top Y) ds')(d := shuffle_to_top Y d) &&& (d \<in> ds' \<Longrightarrow> override_on Pd (shuffle_to_top Y) ds' d = shuffle_to_top Y d) &&& (d \<notin> ds' \<Longrightarrow> override_on Pd (shuffle_to_top Y) ds' d = Pd d)
[PROOF STEP]
by (simp_all add: override_on_insert)


[STATEMENT]
lemma Pd_shuffle_to_top_Field:
  assumes "allocation Y"
  shows "Field (Pd_shuffle_to_top ds' Y d) = Field (Pd d) \<union> (if d \<in> ds' then dX Y d else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd_shuffle_to_top ds' Y d) = Field (Pd d) \<union> (if d \<in> ds' then dX Y d else {})
[PROOF STEP]
by (simp add: Pd_shuffle_to_top_simps shuffle_to_top_Field[OF assms])


[STATEMENT]
lemma Above_shuffle_to_top:
  assumes "x \<in> Above (shuffle_to_top Y (Xd x)) X"
  assumes "y \<in> Y"
  assumes "allocation Y"
  assumes "y \<in> X"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Above (shuffle_to_top Y (Xd x)) X
y \<in> Y
inj_on Xd Y
y \<in> X

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding Above_def shuffle_to_top_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {b \<in> Field (Pd (Xd x) - dX Y (Xd x) \<times> UNIV \<union> (Domain (Pd (Xd x)) \<union> dX Y (Xd x)) \<times> dX Y (Xd x)). \<forall>a\<in>X. (a, b) \<in> Pd (Xd x) - dX Y (Xd x) \<times> UNIV \<union> (Domain (Pd (Xd x)) \<union> dX Y (Xd x)) \<times> dX Y (Xd x)}
y \<in> Y
inj_on Xd Y
y \<in> X

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (fastforce simp: dX_singular dest: Pd_Xd dX_range' Pd_range' inj_onD)