[STATEMENT]
lemma Lemma_1:
  assumes "allocation Y"
  assumes III: "\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d)"
  shows "cop ds = Contracts.cop (Pd_shuffle_to_top ds'' Y) Ch ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds'' Y) Ch ds)
[PROOF STEP]
using finite[of ds''] subset_refl
[PROOF STATE]
proof (prove)
using this:
finite ds''
?A \<subseteq> ?A

goal (1 subgoal):
 1. cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds'' Y) Ch ds)
[PROOF STEP]
proof(induct ds'' rule: finite_subset_induct')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top {} Y) Ch ds)
 2. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top {} Y) Ch ds)
 2. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top {} Y) Ch ds)
[PROOF STEP]
by (simp add: Pd_shuffle_to_top_simps)
[PROOF STATE]
proof (state)
this:
cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top {} Y) Ch ds)

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
case (insert d ds')
[PROOF STATE]
proof (state)
this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds' Y) Ch ds)

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds' Y) Ch ds)
[PROOF STEP]
interpret Pds': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd_shuffle_to_top ds' Y" Ch
[PROOF STATE]
proof (prove)
using this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds' Y) Ch ds)

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_shuffle_to_top ds' Y) Ch
[PROOF STEP]
using %invisible Pd_shuffle_to_top_linear[OF \<open>allocation Y\<close>] Pd_shuffle_to_top_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
[PROOF STATE]
proof (prove)
using this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = CH (Contracts.fp_cop_F (Pd_shuffle_to_top ds' Y) Ch ds)
Linear_order (Pd_shuffle_to_top ?ds' Y ?d)
Field (Pd_shuffle_to_top ?ds' ?Y ?d) \<subseteq> {x. Xd x = ?d}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
\<forall>h X. inj_on Xd (Ch h X)
\<forall>h. unilateral_substitutes_on UNIV (Ch h)
\<forall>h. irc (Ch h)
\<forall>h. lad (Ch h)

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_shuffle_to_top ds' Y) Ch
[PROOF STEP]
by unfold_locales simp_all
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
let ?Z = "CH (Pds'.fp_cop_F ds)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
note IH = \<open>cop ds = ?Z\<close>
[PROOF STATE]
proof (state)
this:
cop ds = Pds'.cop ds

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
let ?Pd_shuffle_to_top = "Pd_shuffle_to_top (insert d ds') Y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = Pds'.cop ds
[PROOF STEP]
interpret Pdds': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd_shuffle_to_top Ch
[PROOF STATE]
proof (prove)
using this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = Pds'.cop ds

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_shuffle_to_top (insert d ds') Y) Ch
[PROOF STEP]
using %invisible Pd_shuffle_to_top_linear[OF \<open>allocation Y\<close>] Pd_shuffle_to_top_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
[PROOF STATE]
proof (prove)
using this:
finite ds'
d \<in> ds''
ds' \<subseteq> ds''
d \<notin> ds'
cop ds = Pds'.cop ds
Linear_order (Pd_shuffle_to_top ?ds' Y ?d)
Field (Pd_shuffle_to_top ?ds' ?Y ?d) \<subseteq> {x. Xd x = ?d}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
\<forall>h X. inj_on Xd (Ch h X)
\<forall>h. Pds'.unilateral_substitutes_on UNIV (Ch h)
\<forall>h. irc (Ch h)
\<forall>h. lad (Ch h)

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_shuffle_to_top (insert d ds') Y) Ch
[PROOF STEP]
by unfold_locales (simp_all add: Pd_shuffle_to_top_simps(1)[symmetric])
  \<comment> \<open>\citet[Lemma~1, for a single doctor]{HatfieldKojima:2010}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pdds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pdds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
have XXX: "?Z = CH (Pdds'.fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pds'.cop ds = Pdds'.cop ds
[PROOF STEP]
proof(rule Pdds'.doctor_optimal_match_unique[OF Pdds'.doctor_optimal_matchI Pdds'.fp_cop_F_doctor_optimal_match])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pdds'.stable_on ds (Pds'.cop ds)
 2. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
show "Pdds'.stable_on ds ?Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.stable_on ds (Pds'.cop ds)
[PROOF STEP]
proof(rule Pdds'.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pdds'.individually_rational_on ds (Pds'.cop ds)
 2. Pdds'.stable_no_blocking_on ds (Pds'.cop ds)
[PROOF STEP]
show "Pdds'.individually_rational_on ds ?Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.individually_rational_on ds (Pds'.cop ds)
[PROOF STEP]
proof(rule Pdds'.individually_rational_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pdds'.CD_on ds (Pds'.cop ds) = Pds'.cop ds
 2. Pdds'.CH (Pds'.cop ds) = Pds'.cop ds
[PROOF STEP]
show "Pdds'.CD_on ds ?Z = ?Z" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.CD_on ds (Pds'.cop ds) = Pds'.cop ds
[PROOF STEP]
proof(rule set_elem_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> Pdds'.CD_on ds (Pds'.cop ds) \<Longrightarrow> x \<in> Pds'.cop ds
 2. \<And>x. x \<in> Pds'.cop ds \<Longrightarrow> x \<in> Pdds'.CD_on ds (Pds'.cop ds)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> Pdds'.CD_on ds (Pds'.cop ds) \<Longrightarrow> x \<in> Pds'.cop ds
 2. \<And>x. x \<in> Pds'.cop ds \<Longrightarrow> x \<in> Pdds'.CD_on ds (Pds'.cop ds)
[PROOF STEP]
assume "x \<in> ?rhs"
[PROOF STATE]
proof (state)
this:
x \<in> Pds'.cop ds

goal (2 subgoals):
 1. \<And>x. x \<in> Pdds'.CD_on ds (Pds'.cop ds) \<Longrightarrow> x \<in> Pds'.cop ds
 2. \<And>x. x \<in> Pds'.cop ds \<Longrightarrow> x \<in> Pdds'.CD_on ds (Pds'.cop ds)
[PROOF STEP]
with \<open>allocation Y\<close> IH Pds'.Theorem_1[of ds] \<open>d \<notin> ds'\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
cop ds = Pds'.cop ds
Pds'.stable_on ds (Pds'.cop ds)
d \<notin> ds'
x \<in> Pds'.cop ds
[PROOF STEP]
show "x \<in> ?lhs"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
cop ds = Pds'.cop ds
Pds'.stable_on ds (Pds'.cop ds)
d \<notin> ds'
x \<in> Pds'.cop ds

goal (1 subgoal):
 1. x \<in> Pdds'.CD_on ds (Pds'.cop ds)
[PROOF STEP]
by (clarsimp simp: Pds'.stable_on_Xd Pdds'.mem_CD_on_Cd Pdds'.Cd_greatest greatest_def
                               Pd_shuffle_to_top_Field[OF \<open>allocation Y\<close>],
                simp add: Pd_shuffle_to_top_simps shuffle_to_top_def dX_def Set.Ball_def,
                metis stable_on_range'[OF Theorem_1[of ds]] inj_on_contraD[OF Pds'.fp_cop_F_allocation[of ds]]
                      fp_cop_F_worst[of _ ds] Pd_range' Pds'.CH_range')
[PROOF STATE]
proof (state)
this:
x \<in> Pdds'.CD_on ds (Pds'.cop ds)

goal (1 subgoal):
 1. \<And>x. x \<in> Pdds'.CD_on ds (Pds'.cop ds) \<Longrightarrow> x \<in> Pds'.cop ds
[PROOF STEP]
qed (meson IntE Pdds'.CD_on_range')
[PROOF STATE]
proof (state)
this:
Pdds'.CD_on ds (Pds'.cop ds) = Pds'.cop ds

goal (1 subgoal):
 1. Pdds'.CH (Pds'.cop ds) = Pds'.cop ds
[PROOF STEP]
show "CH ?Z = ?Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.CH (Pds'.cop ds) = Pds'.cop ds
[PROOF STEP]
by (simp add: CH_irc_idem)
[PROOF STATE]
proof (state)
this:
Pdds'.CH (Pds'.cop ds) = Pds'.cop ds

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pdds'.individually_rational_on ds (Pds'.cop ds)

goal (1 subgoal):
 1. Pdds'.stable_no_blocking_on ds (Pds'.cop ds)
[PROOF STEP]
show "Pdds'.stable_no_blocking_on ds ?Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.stable_no_blocking_on ds (Pds'.cop ds)
[PROOF STEP]
proof(rule Pdds'.stable_no_blocking_onI2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. Pdds'.blocking_on ds (Pds'.cop ds) h X'' \<Longrightarrow> False
[PROOF STEP]
fix h X''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. Pdds'.blocking_on ds (Pds'.cop ds) h X'' \<Longrightarrow> False
[PROOF STEP]
assume Pbo: "Pdds'.blocking_on ds ?Z h X''"
[PROOF STATE]
proof (state)
this:
Pdds'.blocking_on ds (Pds'.cop ds) h X''

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

goal (3 subgoals):
 1. X'' \<noteq> Ch h (Pds'.cop ds)
 2. X'' = Ch h (Pds'.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
note Pbos = Pdds'.blocking_on_allocation[OF \<open>Pdds'.blocking_on ds ?Z h X''\<close>]
                      Pdds'.blocking_on_CD_on'[OF \<open>Pdds'.blocking_on ds ?Z h X''\<close> \<open>x \<in> X''\<close>]
                      Pdds'.blocking_on_Cd[OF \<open>Pdds'.blocking_on ds ?Z h X''\<close>, where d="Xd x"]
[PROOF STATE]
proof (state)
this:
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')

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

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
from \<open>allocation Y\<close> III \<open>d \<in> ds''\<close> \<open>Xd x = d\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
Xd x = d
[PROOF STEP]
have "dX Y (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
Xd x = d

goal (1 subgoal):
 1. Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by clarsimp (metis AboveS_Pd_Xd AboveS_Field dX_range' inj_on_eq_iff)
[PROOF STATE]
proof (state)
this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
with \<open>allocation Y\<close> \<open>d \<notin> ds'\<close>
                          Pdds'.blocking_on_Field[OF \<open>Pdds'.blocking_on ds ?Z h X''\<close>, where d=d] \<open>Xd x = d\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
d \<notin> ds'
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top (insert d ds') Y d)
Xd x = d
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
have "dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
d \<notin> ds'
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top (insert d ds') Y d)
Xd x = d
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (1 subgoal):
 1. Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by (force simp: Pd_shuffle_to_top_simps shuffle_to_top_Field)
[PROOF STATE]
proof (state)
this:
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
note \<open>allocation Y\<close> bspec[OF III[unfolded IH] \<open>d \<in> ds''\<close>] \<open>d \<notin> ds'\<close> \<open>x \<in> X''\<close> \<open>Xd x = d\<close>
                          Pds'.stable_on_allocation[OF Pds'.Theorem_1] Pbos
[PROOF STATE]
proof (state)
this:
inj_on Xd Y
\<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
d \<notin> ds'
x \<in> X''
Xd x = d
inj_on Xd (Pds'.cop ?ds)
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
inj_on Xd Y
\<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
d \<notin> ds'
x \<in> X''
Xd x = d
inj_on Xd (Pds'.cop ?ds)
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
inj_on Xd Y
\<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
d \<notin> ds'
x \<in> X''
Xd x = d
inj_on Xd (Pds'.cop ?ds)
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')

goal (1 subgoal):
 1. x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
by (clarsimp simp: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_Above Pdds'.Cd_Above
                                 Int_Un_distrib2 Pd_shuffle_to_top_Field)
                 (clarsimp simp: Pd_shuffle_to_top_simps dX_singular dX_Int_Field_Pd;
                  fastforce simp: Above_def AboveS_def Pd_refl shuffle_to_top_def dX_def intro: FieldI1 dest: Pd_range' iff: inj_on_eq_iff)
[PROOF STATE]
proof (state)
this:
x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')

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

goal (1 subgoal):
 1. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
from Pbos \<open>Xd x \<noteq> d\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')
Xd x \<noteq> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X''
x \<in> Pdds'.CD_on ds (Pds'.cop ds \<union> X'')
Pdds'.dX X'' (Xd x) \<subseteq> Pdds'.Cd (Xd x) (Pds'.cop ds \<union> X'')
Xd x \<noteq> d

goal (1 subgoal):
 1. x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')
[PROOF STEP]
by (simp add: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_greatest Pdds'.Cd_greatest)
                 (simp add: Pd_shuffle_to_top_simps)
[PROOF STATE]
proof (state)
this:
x \<in> Pds'.CD_on ds (Pds'.cop ds \<union> X'')

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pdds'.stable_no_blocking_on ds (Pds'.cop ds)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pdds'.stable_on ds (Pds'.cop ds)

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
fix W w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
assume "Pdds'.stable_on ds W" "w \<in> W"
[PROOF STATE]
proof (state)
this:
Pdds'.stable_on ds W
w \<in> W

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
from III \<open>d \<in> ds''\<close> IH
[PROOF STATE]
proof (chain)
picking this:
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
cop ds = Pds'.cop ds
[PROOF STEP]
obtain y where Y: "y \<in> Y" "y \<in> AboveS (Pd d) (dX (Pds'.cop ds) d)" "Xd y = d"
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
cop ds = Pds'.cop ds

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> Y; y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d); Xd y = d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis AboveS_Pd_Xd)
[PROOF STATE]
proof (state)
this:
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Pdds'.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Pds'.cop ds. (x, y) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd x)
[PROOF STEP]
show "\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
proof(cases "y \<in> W")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> W

goal (2 subgoals):
 1. y \<in> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
note \<open>y \<in> W\<close>
[PROOF STATE]
proof (state)
this:
y \<in> W

goal (2 subgoals):
 1. y \<in> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
from \<open>d \<notin> ds'\<close> \<open>Pdds'.stable_on ds W\<close> Y \<open>y \<in> W\<close>
[PROOF STATE]
proof (chain)
picking this:
d \<notin> ds'
Pdds'.stable_on ds W
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
y \<in> W
[PROOF STEP]
interpret Pdds': ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs
                           Xd Xh "Pd_shuffle_to_top (insert d ds') Y" Ch y W ds "Pd_shuffle_to_top ds' Y"
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
Pdds'.stable_on ds W
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
y \<in> W

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh (Pd_shuffle_to_top (insert d ds') Y) Ch y W ds (Pd_shuffle_to_top ds' Y)
[PROOF STEP]
using %invisible Pds'.Pd_linear Pds'.Pd_range Pd_shuffle_to_top_simps Pd_range'
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
Pdds'.stable_on ds W
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
y \<in> W
\<forall>d. Linear_order (Pd_shuffle_to_top ds' Y d)
\<forall>d. Field (Pd_shuffle_to_top ds' Y d) \<subseteq> {x. Xd x = d}
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
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh (Pd_shuffle_to_top (insert d ds') Y) Ch y W ds (Pd_shuffle_to_top ds' Y)
[PROOF STEP]
unfolding AboveS_def
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
Pdds'.stable_on ds W
y \<in> Y
y \<in> {b \<in> Field (Pd d). \<forall>a\<in>Pdds'.dX (Pds'.cop ds) d. b \<noteq> a \<and> (a, b) \<in> Pd d}
Xd y = d
y \<in> W
\<forall>d. Linear_order (Pd_shuffle_to_top ds' Y d)
\<forall>d. Field (Pd_shuffle_to_top ds' Y d) \<subseteq> {x. Xd x = d}
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
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh (Pd_shuffle_to_top (insert d ds') Y) Ch y W ds (Pd_shuffle_to_top ds' Y)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
from \<open>d \<notin> ds'\<close> Y Pdds'.Theorem_11_fp_cop_F
[PROOF STATE]
proof (chain)
picking this:
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
\<exists>ya\<in>Pds'.cop ds. (y, ya) \<in> Pd_shuffle_to_top ds' Y (Xd y)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
\<exists>ya\<in>Pds'.cop ds. (y, ya) \<in> Pd_shuffle_to_top ds' Y (Xd y)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Pds'.stable_on_allocation[OF Pds'.Theorem_1[of ds]] Pd_linear Pd_range'
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
\<exists>ya\<in>Pds'.cop ds. (y, ya) \<in> Pd_shuffle_to_top ds' Y (Xd y)
inj_on Xd (Pds'.cop ds)
\<forall>d. Linear_order (Pd d)
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding order_on_defs antisym_def AboveS_def dX_def
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
y \<in> Y
y \<in> {b \<in> Field (Pd d). \<forall>a\<in>{x \<in> Pds'.cop ds. Xd x = d}. b \<noteq> a \<and> (a, b) \<in> Pd d}
Xd y = d
\<exists>ya\<in>Pds'.cop ds. (y, ya) \<in> Pd_shuffle_to_top ds' Y (Xd y)
inj_on Xd (Pds'.cop ds)
\<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)
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d

goal (1 subgoal):
 1. False
[PROOF STEP]
by (clarsimp simp: Pd_shuffle_to_top_simps) (blast dest: Pd_Xd)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. y \<in> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal (1 subgoal):
 1. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> W

goal (1 subgoal):
 1. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
note \<open>y \<notin> W\<close>
[PROOF STATE]
proof (state)
this:
y \<notin> W

goal (1 subgoal):
 1. y \<notin> W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
proof (cases "Pds'.stable_on ds W")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Pds'.stable_on ds W

goal (2 subgoals):
 1. Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
note \<open>Pds'.stable_on ds W\<close>
[PROOF STATE]
proof (state)
this:
Pds'.stable_on ds W

goal (2 subgoals):
 1. Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
with \<open>allocation Y\<close> \<open>d \<notin> ds'\<close> Y \<open>w \<in> W\<close> \<open>y \<notin> W\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
w \<in> W
y \<notin> W
Pds'.stable_on ds W
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
w \<in> W
y \<notin> W
Pds'.stable_on ds W

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
using Pds'.Theorem_5[OF \<open>Pds'.stable_on ds W\<close> \<open>w \<in> W\<close>]
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
d \<notin> ds'
y \<in> Y
y \<in> AboveS (Pd d) (Pdds'.dX (Pds'.cop ds) d)
Xd y = d
w \<in> W
y \<notin> W
Pds'.stable_on ds W
\<exists>y\<in>Pds'.cop ds. (w, y) \<in> Pd_shuffle_to_top ds' Y (Xd w)

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
by (auto 0 2 simp: Pd_shuffle_to_top_simps shuffle_to_top_def dX_def AboveS_def dest: Pd_range' inj_onD)
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal (1 subgoal):
 1. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Pds'.stable_on ds W

goal (1 subgoal):
 1. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
note \<open>\<not>Pds'.stable_on ds W\<close>
[PROOF STATE]
proof (state)
this:
\<not> Pds'.stable_on ds W

goal (1 subgoal):
 1. \<not> Pds'.stable_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Pds'.stable_on ds W
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> Pds'.stable_on ds W

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
proof(cases rule: Pds'.not_stable_on_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> Pds'.individually_rational_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case not_individually_rational
[PROOF STATE]
proof (state)
this:
\<not> Pds'.individually_rational_on ds W

goal (2 subgoals):
 1. \<not> Pds'.individually_rational_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
note Psos = Pdds'.stable_on_allocation[OF \<open>Pdds'.stable_on ds W\<close>]
                        Pdds'.stable_on_CH[OF \<open>Pdds'.stable_on ds W\<close>]
                        Pdds'.stable_on_Xd[OF \<open>Pdds'.stable_on ds W\<close>]
[PROOF STATE]
proof (state)
this:
inj_on Xd W
Pdds'.CH W = W
?x \<in> W \<Longrightarrow> Xd ?x \<in> ds

goal (2 subgoals):
 1. \<not> Pds'.individually_rational_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
have "x \<in> Pds'.Cd (Xd x) W" if "x \<in> W" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
proof(cases "Xd x = d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Xd x = d

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
with \<open>allocation Y\<close> \<open>allocation W\<close> Y(1,3) \<open>y \<notin> W\<close>
                   Pdds'.stable_on_range'[OF \<open>Pdds'.stable_on ds W\<close> \<open>x \<in> W\<close>] \<open>x \<in> W\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
inj_on Xd W
y \<in> Y
Xd y = d
y \<notin> W
x \<in> Field (Pd_shuffle_to_top (insert d ds') Y (Xd x))
x \<in> W
Xd x = d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
inj_on Xd W
y \<in> Y
Xd y = d
y \<notin> W
x \<in> Field (Pd_shuffle_to_top (insert d ds') Y (Xd x))
x \<in> W
Xd x = d

goal (1 subgoal):
 1. x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
by (force simp: Pd_shuffle_to_top_Field dest: dX_range' inj_onD intro: Pds'.Cd_single)
[PROOF STATE]
proof (state)
this:
x \<in> Pds'.Cd (Xd x) W

goal (1 subgoal):
 1. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Xd x \<noteq> d

goal (1 subgoal):
 1. Xd x \<noteq> d \<Longrightarrow> x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
with \<open>allocation Y\<close> \<open>allocation W\<close> Pdds'.stable_on_range'[OF \<open>Pdds'.stable_on ds W\<close> \<open>x \<in> W\<close>] \<open>x \<in> W\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
inj_on Xd W
x \<in> Field (Pd_shuffle_to_top (insert d ds') Y (Xd x))
x \<in> W
Xd x \<noteq> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
inj_on Xd W
x \<in> Field (Pd_shuffle_to_top (insert d ds') Y (Xd x))
x \<in> W
Xd x \<noteq> d

goal (1 subgoal):
 1. x \<in> Pds'.Cd (Xd x) W
[PROOF STEP]
by (auto simp: Pd_shuffle_to_top_Field intro!: Pds'.Cd_single)
[PROOF STATE]
proof (state)
this:
x \<in> Pds'.Cd (Xd x) W

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> W \<Longrightarrow> ?x \<in> Pds'.Cd (Xd ?x) W

goal (2 subgoals):
 1. \<not> Pds'.individually_rational_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
 2. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
with not_individually_rational \<open>Pdds'.CH W = W\<close> Psos(3)
[PROOF STATE]
proof (chain)
picking this:
\<not> Pds'.individually_rational_on ds W
Pdds'.CH W = W
?x \<in> W \<Longrightarrow> Xd ?x \<in> ds
?x \<in> W \<Longrightarrow> ?x \<in> Pds'.Cd (Xd ?x) W
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> Pds'.individually_rational_on ds W
Pdds'.CH W = W
?x \<in> W \<Longrightarrow> Xd ?x \<in> ds
?x \<in> W \<Longrightarrow> ?x \<in> Pds'.Cd (Xd ?x) W

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
unfolding Pds'.individually_rational_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (Pds'.CD_on ds W = W \<and> Pdds'.CH W = W)
Pdds'.CH W = W
?x \<in> W \<Longrightarrow> Xd ?x \<in> ds
?x \<in> W \<Longrightarrow> ?x \<in> Pds'.Cd (Xd ?x) W

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
by (auto simp: Pds'.mem_CD_on_Cd dest: Pds'.Cd_range')
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
case not_no_blocking
[PROOF STATE]
proof (state)
this:
\<not> Pds'.stable_no_blocking_on ds W

goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Pds'.stable_no_blocking_on ds W
[PROOF STEP]
obtain h X'' where Pbo: "Pds'.blocking_on ds W h X''"
[PROOF STATE]
proof (prove)
using this:
\<not> Pds'.stable_no_blocking_on ds W

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

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

goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
have "Pdds'.blocking_on ds W h X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pdds'.blocking_on ds W h X''
[PROOF STEP]
proof(rule Pdds'.blocking_onI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h W
 2. X'' = Ch h (W \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. X'' \<noteq> Ch h W
 2. X'' = Ch h (W \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
assume "x \<in> X''"
[PROOF STATE]
proof (state)
this:
x \<in> X''

goal (3 subgoals):
 1. X'' \<noteq> Ch h W
 2. X'' = Ch h (W \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
note Pbos = Pds'.blocking_on_allocation[OF \<open>Pds'.blocking_on ds W h X''\<close>]
                        Pds'.blocking_on_CD_on'[OF \<open>Pds'.blocking_on ds W h X''\<close> \<open>x \<in> X''\<close>]
                        Pds'.blocking_on_Field[OF \<open>Pds'.blocking_on ds W h X''\<close>, where d=d]
[PROOF STATE]
proof (state)
this:
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)

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

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
from \<open>allocation Y\<close> III \<open>d \<in> ds''\<close>  \<open>Xd x = d\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd Y
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
Xd x = d
[PROOF STEP]
have "dX Y (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd Y
\<forall>d\<in>ds''. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Pdds'.dX (cop ds) d)
d \<in> ds''
Xd x = d

goal (1 subgoal):
 1. Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by clarsimp (metis AboveS_Pd_Xd AboveS_Field dX_range' inj_on_eq_iff)
[PROOF STATE]
proof (state)
this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
with \<open>d \<notin> ds'\<close> \<open>Xd x = d\<close> Pbos
[PROOF STATE]
proof (chain)
picking this:
d \<notin> ds'
Xd x = d
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
have "dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
using this:
d \<notin> ds'
Xd x = d
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))

goal (1 subgoal):
 1. Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
[PROOF STEP]
by (clarsimp simp: Pd_shuffle_to_top_simps)
[PROOF STATE]
proof (state)
this:
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
note \<open>allocation Y\<close> \<open>d \<notin> ds'\<close> \<open>y \<notin> W\<close> \<open>Xd y = d\<close> \<open>x \<in> X''\<close> Pbos
[PROOF STATE]
proof (state)
this:
inj_on Xd Y
d \<notin> ds'
y \<notin> W
Xd y = d
x \<in> X''
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)

goal (2 subgoals):
 1. Xd x = d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
 2. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
inj_on Xd Y
d \<notin> ds'
y \<notin> W
Xd y = d
x \<in> X''
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Pdds'.dX Y (Xd x) \<subseteq> Field (Pd (Xd x))
Pdds'.dX X'' (Xd x) \<subseteq> Field (Pd (Xd x))
inj_on Xd Y
d \<notin> ds'
y \<notin> W
Xd y = d
x \<in> X''
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)

goal (1 subgoal):
 1. x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
by (clarsimp simp: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_Above Pdds'.Cd_Above
                                   Int_Un_distrib2)
                   (clarsimp simp: Pd_shuffle_to_top_simps shuffle_to_top_Field dX_singular dX_Int_Field_Pd Un_absorb2,
                    force simp: \<open>y \<in> Y\<close> shuffle_to_top_def dX_def Above_def dest: inj_onD intro: FieldI1)
[PROOF STATE]
proof (state)
this:
x \<in> Pdds'.CD_on ds (W \<union> X'')

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

goal (1 subgoal):
 1. Xd x \<noteq> d \<Longrightarrow> x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
from Pbos \<open>Xd x \<noteq> d\<close>
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)
Xd x \<noteq> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X''
x \<in> Pds'.CD_on ds (W \<union> X'')
Pdds'.dX X'' d \<subseteq> Field (Pd_shuffle_to_top ds' Y d)
Xd x \<noteq> d

goal (1 subgoal):
 1. x \<in> Pdds'.CD_on ds (W \<union> X'')
[PROOF STEP]
by (simp add: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_greatest Pdds'.Cd_greatest)
                   (simp add: Pd_shuffle_to_top_simps)
[PROOF STATE]
proof (state)
this:
x \<in> Pdds'.CD_on ds (W \<union> X'')

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

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

goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
with \<open>Pdds'.stable_on ds W\<close>
[PROOF STATE]
proof (chain)
picking this:
Pdds'.stable_on ds W
Pdds'.blocking_on ds W h X''
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
Pdds'.stable_on ds W
Pdds'.blocking_on ds W h X''

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

goal (1 subgoal):
 1. \<not> Pds'.stable_no_blocking_on ds W \<Longrightarrow> \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Pds'.cop ds. (w, z) \<in> Pd_shuffle_to_top (insert d ds') Y (Xd w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Pds'.cop ds = Pdds'.cop ds

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>finite F; a \<in> ds''; F \<subseteq> ds''; a \<notin> F; cop ds = Pdds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top F Y) Ch ds)\<rbrakk> \<Longrightarrow> cop ds = Pdds'.CH (Contracts.fp_cop_F (Pd_shuffle_to_top (insert a F) Y) Ch ds)
[PROOF STEP]
from \<open>?Z = CH (Pdds'.fp_cop_F ds)\<close> IH
[PROOF STATE]
proof (chain)
picking this:
Pds'.cop ds = Pdds'.cop ds
cop ds = Pds'.cop ds
[PROOF STEP]
show "cop ds = Pdds'.cop ds"
[PROOF STATE]
proof (prove)
using this:
Pds'.cop ds = Pdds'.cop ds
cop ds = Pds'.cop ds

goal (1 subgoal):
 1. cop ds = Pdds'.cop ds
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cop ds = Pdds'.cop ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem fp_cop_F_group_strategy_proof:
  shows "group_strategy_proof ds Contracts.cop"
        (is "group_strategy_proof _ ?\<phi>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group_strategy_proof ds (\<lambda>Pd Ch ds. Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds))
[PROOF STEP]
proof(rule group_strategy_proofI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix Pd Pds' Ch ds'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume XXX: "mechanism_domain Pd Ch" "mechanism_domain (override_on Pd Pds' ds') Ch"
     and YYY: "ds' \<subseteq> ds" "ds' \<noteq> {}"
     and ZZZ: "\<forall>d\<in>ds'. \<exists>y\<in>?\<phi> (override_on Pd Pds' ds') Ch ds. y \<in> AboveS (Pd d) (dX (?\<phi> Pd Ch ds) d)"
[PROOF STATE]
proof (state)
this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pds' ds') Ch
ds' \<subseteq> ds
ds' \<noteq> {}
\<forall>d\<in>ds'. \<exists>y\<in>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pds' ds') Ch ds). y \<in> AboveS (Pd d) (dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from XXX(1)
[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 ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (TruePref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from XXX(2)
[PROOF STATE]
proof (chain)
picking this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pds' ds') Ch
[PROOF STEP]
interpret
    ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "override_on Pd Pds' ds'" Ch
[PROOF STATE]
proof (prove)
using this:
ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pds' ds') Ch

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (override_on Pd Pds' ds') Ch
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?Y = "ManiPref.cop ds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?Z = "TruePref.cop ds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?Pd_shuffle_to_top = "TruePref.Pd_shuffle_to_top ds' ?Y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
interpret ManiPref': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd_shuffle_to_top Ch
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds)) Ch
[PROOF STEP]
using TruePref.Ch_unilateral_substitutes TruePref.Ch_irc TruePref.Ch_lad TruePref.Ch_range TruePref.Ch_singular
          TruePref.Pd_shuffle_to_top_linear ManiPref.stable_on_allocation[OF ManiPref.Theorem_1[of ds]]
          TruePref.Pd_shuffle_to_top_range ManiPref.dX_range
[PROOF STATE]
proof (prove)
using this:
\<forall>h. ManiPref.unilateral_substitutes_on UNIV (Ch h)
\<forall>h. irc (Ch h)
\<forall>h. lad (Ch h)
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
\<forall>h X. inj_on Xd (Ch h X)
inj_on Xd ?Y \<Longrightarrow> Linear_order (TruePref.Pd_shuffle_to_top ?ds' ?Y ?d)
inj_on Xd (ManiPref.cop ds)
Field (TruePref.Pd_shuffle_to_top ?ds' ?Y ?d) \<subseteq> {x. Xd x = ?d}
\<forall>d. ManiPref.dX ?X d \<subseteq> {x. Xd x = d}

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds)) Ch
[PROOF STEP]
by unfold_locales simp_all
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
let ?Y' = "ManiPref'.cop ds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "ManiPref'.stable_on ds ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ManiPref'.stable_on ds (ManiPref.cop ds)
[PROOF STEP]
proof(rule ManiPref'.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ManiPref'.individually_rational_on ds (ManiPref.cop ds)
 2. ManiPref'.stable_no_blocking_on ds (ManiPref.cop ds)
[PROOF STEP]
show "ManiPref'.individually_rational_on ds ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ManiPref'.individually_rational_on ds (ManiPref.cop ds)
[PROOF STEP]
proof(rule ManiPref'.individually_rational_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ManiPref'.CD_on ds (ManiPref.cop ds) = ManiPref.cop ds
 2. ManiPref'.CH (ManiPref.cop ds) = ManiPref.cop ds
[PROOF STEP]
show "ManiPref'.CD_on ds ?Y = ?Y" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ManiPref'.CD_on ds (ManiPref.cop ds) = ManiPref.cop ds
[PROOF STEP]
proof(rule set_elem_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds) \<Longrightarrow> x \<in> ManiPref.cop ds
 2. \<And>x. x \<in> ManiPref.cop ds \<Longrightarrow> x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds) \<Longrightarrow> x \<in> ManiPref.cop ds
 2. \<And>x. x \<in> ManiPref.cop ds \<Longrightarrow> x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)
[PROOF STEP]
assume "x \<in> ?rhs"
[PROOF STATE]
proof (state)
this:
x \<in> ManiPref.cop ds

goal (2 subgoals):
 1. \<And>x. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds) \<Longrightarrow> x \<in> ManiPref.cop ds
 2. \<And>x. x \<in> ManiPref.cop ds \<Longrightarrow> x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> ManiPref.cop ds
[PROOF STEP]
have "Xd x \<in> ds \<and> (Xd x \<notin> ds' \<longrightarrow> x \<in> Field (Pd (Xd x)))"
[PROOF STATE]
proof (prove)
using this:
x \<in> ManiPref.cop ds

goal (1 subgoal):
 1. Xd x \<in> ds \<and> (Xd x \<notin> ds' \<longrightarrow> x \<in> Field (Pd (Xd x)))
[PROOF STEP]
by (metis ManiPref.fp_cop_F_range_inv' TruePref.CH_range' override_on_apply_notin)
[PROOF STATE]
proof (state)
this:
Xd x \<in> ds \<and> (Xd x \<notin> ds' \<longrightarrow> x \<in> Field (Pd (Xd x)))

goal (2 subgoals):
 1. \<And>x. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds) \<Longrightarrow> x \<in> ManiPref.cop ds
 2. \<And>x. x \<in> ManiPref.cop ds \<Longrightarrow> x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)
[PROOF STEP]
with ManiPref.Theorem_1[of ds] \<open>x \<in> ?rhs\<close>
[PROOF STATE]
proof (chain)
picking this:
ManiPref.stable_on ds (ManiPref.cop ds)
x \<in> ManiPref.cop ds
Xd x \<in> ds \<and> (Xd x \<notin> ds' \<longrightarrow> x \<in> Field (Pd (Xd x)))
[PROOF STEP]
show "x \<in> ?lhs"
[PROOF STATE]
proof (prove)
using this:
ManiPref.stable_on ds (ManiPref.cop ds)
x \<in> ManiPref.cop ds
Xd x \<in> ds \<and> (Xd x \<notin> ds' \<longrightarrow> x \<in> Field (Pd (Xd x)))

goal (1 subgoal):
 1. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)
[PROOF STEP]
by (fastforce dest: ManiPref.stable_on_allocation
                    simp: ManiPref'.Cd_single ManiPref'.mem_CD_on_Cd TruePref.Pd_shuffle_to_top_Field dX_def)
[PROOF STATE]
proof (state)
this:
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds)

goal (1 subgoal):
 1. \<And>x. x \<in> ManiPref'.CD_on ds (ManiPref.cop ds) \<Longrightarrow> x \<in> ManiPref.cop ds
[PROOF STEP]
qed (meson IntE ManiPref'.CD_on_range')
[PROOF STATE]
proof (state)
this:
ManiPref'.CD_on ds (ManiPref.cop ds) = ManiPref.cop ds

goal (1 subgoal):
 1. ManiPref'.CH (ManiPref.cop ds) = ManiPref.cop ds
[PROOF STEP]
show "ManiPref'.CH ?Y = ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ManiPref'.CH (ManiPref.cop ds) = ManiPref.cop ds
[PROOF STEP]
by (simp add: ManiPref'.CH_irc_idem)
[PROOF STATE]
proof (state)
this:
ManiPref'.CH (ManiPref.cop ds) = ManiPref.cop ds

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ManiPref'.individually_rational_on ds (ManiPref.cop ds)

goal (1 subgoal):
 1. ManiPref'.stable_no_blocking_on ds (ManiPref.cop ds)
[PROOF STEP]
show "ManiPref'.stable_no_blocking_on ds ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ManiPref'.stable_no_blocking_on ds (ManiPref.cop ds)
[PROOF STEP]
proof(rule ManiPref'.stable_no_blocking_onI2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. ManiPref'.blocking_on ds (ManiPref.cop ds) h X'' \<Longrightarrow> False
[PROOF STEP]
fix h X''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. ManiPref'.blocking_on ds (ManiPref.cop ds) h X'' \<Longrightarrow> False
[PROOF STEP]
assume "ManiPref'.blocking_on ds ?Y h X''"
[PROOF STATE]
proof (state)
this:
ManiPref'.blocking_on ds (ManiPref.cop ds) h X''

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

goal (3 subgoals):
 1. X'' \<noteq> Ch h (ManiPref.cop ds)
 2. X'' = Ch h (ManiPref.cop ds \<union> X'')
 3. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
note Pbos = ManiPref'.blocking_on_Field[OF \<open>ManiPref'.blocking_on ds ?Y h X''\<close>, where d="Xd x"]
                    ManiPref'.blocking_on_allocation[OF \<open>ManiPref'.blocking_on ds ?Y h X''\<close>]
                    ManiPref'.blocking_on_CD_on'[OF \<open>ManiPref'.blocking_on ds ?Y h X''\<close> \<open>x \<in> X''\<close>]
                    ManiPref'.blocking_on_Cd[OF \<open>ManiPref'.blocking_on ds ?Y h X''\<close>, where d="Xd x"]
[PROOF STATE]
proof (state)
this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')

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

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
from ManiPref.fp_cop_F_allocation[of ds] \<open>x \<in> X''\<close> \<open>Xd x \<in> ds'\<close> Pbos bspec[OF ZZZ \<open>Xd x \<in> ds'\<close>]
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd (ManiPref.cop ds)
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))
[PROOF STEP]
have "dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd (ManiPref.cop ds)
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))

goal (1 subgoal):
 1. ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))
[PROOF STEP]
by (clarsimp simp: dX_singular ManiPref'.mem_CD_on_Cd ManiPref'.Cd_Above TruePref.Pd_shuffle_to_top_Field)
               (fastforce simp: TruePref.Pd_shuffle_to_top_simps dX_singular dest: TruePref.AboveS_Pd_Xd
                          dest: ManiPref.fp_cop_F_range_inv' ManiPref.CH_range' TruePref.Above_shuffle_to_top)
[PROOF STATE]
proof (state)
this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
from ManiPref.stable_on_range'[OF ManiPref.Theorem_1] \<open>Xd x \<in> ds'\<close>
[PROOF STATE]
proof (chain)
picking this:
?x \<in> ManiPref.cop ?ds \<Longrightarrow> ?x \<in> Field (override_on Pd Pds' ds' (Xd ?x))
Xd x \<in> ds'
[PROOF STEP]
have "dX ?Y (Xd x) \<subseteq> Field (Pds' (Xd x))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> ManiPref.cop ?ds \<Longrightarrow> ?x \<in> Field (override_on Pd Pds' ds' (Xd ?x))
Xd x \<in> ds'

goal (1 subgoal):
 1. ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))
[PROOF STEP]
by (metis dX_range' override_on_apply_in subsetI)
[PROOF STATE]
proof (state)
this:
ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
note bspec[OF ZZZ \<open>Xd x \<in> ds'\<close>] \<open>x \<in> X''\<close> \<open>Xd x \<in> ds'\<close> Pbos
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')

goal (2 subgoals):
 1. Xd x \<in> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
 2. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))
ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))
ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')

goal (1 subgoal):
 1. x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
using ManiPref.Pd_linear'[of "Xd x"] ManiPref.fp_cop_F_allocation[of ds]
                  ManiPref'.fp_cop_F_allocation[of ds]
[PROOF STATE]
proof (prove)
using this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (Pds' (Xd x))
ManiPref'.dX (ManiPref.cop ds) (Xd x) \<subseteq> Field (Pds' (Xd x))
\<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd (Xd x)) (ManiPref'.dX (TruePref.cop ds) (Xd x))
x \<in> X''
Xd x \<in> ds'
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
Linear_order (override_on Pd Pds' ds' (Xd x))
inj_on Xd (ManiPref.cop ds)
inj_on Xd (ManiPref'.cop ds)

goal (1 subgoal):
 1. x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
by (clarsimp simp: ManiPref'.mem_CD_on_Cd ManiPref'.Cd_Above_dX ManiPref.mem_CD_on_Cd
                               ManiPref.Cd_Above_dX dX_union dX_singular
                               TruePref.Pd_shuffle_to_top_Field TruePref.AboveS_Pd_Xd)
               (force simp: TruePref.Pd_shuffle_to_top_simps insert_absorb elim: Above_Linear_singleton
                     dest!: TruePref.Above_shuffle_to_top)
[PROOF STATE]
proof (state)
this:
x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')

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

goal (1 subgoal):
 1. Xd x \<notin> ds' \<Longrightarrow> x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
with Pbos
[PROOF STATE]
proof (chain)
picking this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
Xd x \<notin> ds'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ManiPref'.dX X'' (Xd x) \<subseteq> Field (TruePref.Pd_shuffle_to_top ds' (ManiPref.cop ds) (Xd x))
inj_on Xd X''
x \<in> ManiPref'.CD_on ds (ManiPref.cop ds \<union> X'')
ManiPref'.dX X'' (Xd x) \<subseteq> ManiPref'.Cd (Xd x) (ManiPref.cop ds \<union> X'')
Xd x \<notin> ds'

goal (1 subgoal):
 1. x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')
[PROOF STEP]
by (fastforce simp: ManiPref'.mem_CD_on_Cd ManiPref'.Cd_greatest ManiPref.mem_CD_on_Cd
                                ManiPref.Cd_greatest TruePref.Pd_shuffle_to_top_simps)
[PROOF STATE]
proof (state)
this:
x \<in> ManiPref.CD_on ds (ManiPref.cop ds \<union> X'')

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ManiPref'.stable_no_blocking_on ds (ManiPref.cop ds)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ManiPref'.stable_on ds (ManiPref.cop ds)

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ManiPref'.stable_on_allocation
[PROOF STATE]
proof (chain)
picking this:
ManiPref'.stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
ManiPref'.stable_on ds (ManiPref.cop ds)
[PROOF STEP]
have "{x \<in> ?Y. Xd x \<in> ds'} \<subseteq> {x \<in> ?Y'. Xd x \<in> ds'}"
[PROOF STATE]
proof (prove)
using this:
ManiPref'.stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
ManiPref'.stable_on ds (ManiPref.cop ds)

goal (1 subgoal):
 1. {x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}
[PROOF STEP]
by (force dest: ManiPref'.Theorem_5[of ds]
              simp: TruePref.Pd_shuffle_to_top_simps TruePref.shuffle_to_top_def dX_def dest: inj_onD)
[PROOF STATE]
proof (state)
this:
{x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from ManiPref.stable_on_allocation[OF ManiPref.Theorem_1] ZZZ
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd (ManiPref.cop ?ds)
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd d) (ManiPref'.dX (TruePref.cop ds) d)
[PROOF STEP]
have "?Z = ?Y'"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd (ManiPref.cop ?ds)
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd d) (ManiPref'.dX (TruePref.cop ds) d)

goal (1 subgoal):
 1. TruePref.cop ds = ManiPref'.cop ds
[PROOF STEP]
by (rule TruePref.Lemma_1)
[PROOF STATE]
proof (state)
this:
TruePref.cop ds = ManiPref'.cop ds

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
TruePref.cop ds = ManiPref'.cop ds

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note YYY ZZZ
[PROOF STATE]
proof (state)
this:
ds' \<subseteq> ds
ds' \<noteq> {}
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd d) (ManiPref'.dX (TruePref.cop ds) d)

goal (1 subgoal):
 1. \<And>Pd Pd' Ch ds'. \<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>Contracts.CH Ch (Contracts.fp_cop_F (override_on Pd Pd' ds') Ch ds). y \<in> AboveS (Pd d) (ManiPref'.dX (Contracts.CH Ch (Contracts.fp_cop_F Pd Ch ds)) d)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}
TruePref.cop ds = ManiPref'.cop ds
ds' \<subseteq> ds
ds' \<noteq> {}
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd d) (ManiPref'.dX (TruePref.cop ds) d)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
{x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}
TruePref.cop ds = ManiPref'.cop ds
ds' \<subseteq> ds
ds' \<noteq> {}
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> AboveS (Pd d) (ManiPref'.dX (TruePref.cop ds) d)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding AboveS_def dX_def
[PROOF STATE]
proof (prove)
using this:
{x \<in> ManiPref.cop ds. Xd x \<in> ds'} \<subseteq> {x \<in> ManiPref'.cop ds. Xd x \<in> ds'}
TruePref.cop ds = ManiPref'.cop ds
ds' \<subseteq> ds
ds' \<noteq> {}
\<forall>d\<in>ds'. \<exists>y\<in>ManiPref.cop ds. y \<in> {b \<in> Field (Pd d). \<forall>a\<in>{x \<in> TruePref.cop ds. Xd x = d}. b \<noteq> a \<and> (a, b) \<in> Pd d}

goal (1 subgoal):
 1. False
[PROOF STEP]
by (fastforce simp: ex_in_conv[symmetric] dest: TruePref.Pd_range')
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Corollary_2:
  assumes "ds \<noteq> {}"
  shows "\<not>(\<exists>Y. individually_rational_on ds Y
        \<and> (\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>Y. individually_rational_on ds Y \<and> (\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d))
[PROOF STEP]
proof(unfold individually_rational_on_def, safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d); CD_on ds Y = Y; CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d); CD_on ds Y = Y; CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "CD_on ds Y = Y" "CH Y = Y"
           and Z: "\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d)"
[PROOF STATE]
proof (state)
this:
CD_on ds Y = Y
CH Y = Y
\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d); CD_on ds Y = Y; CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>CD_on ds Y = Y\<close>
[PROOF STATE]
proof (chain)
picking this:
CD_on ds Y = Y
[PROOF STEP]
have "allocation Y"
[PROOF STATE]
proof (prove)
using this:
CD_on ds Y = Y

goal (1 subgoal):
 1. inj_on Xd Y
[PROOF STEP]
by (metis CD_on_inj_on_Xd)
[PROOF STATE]
proof (state)
this:
inj_on Xd Y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (dX (cop ds) d); CD_on ds Y = Y; CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>CD_on ds Y = Y\<close>
[PROOF STATE]
proof (chain)
picking this:
CD_on ds Y = Y
[PROOF STEP]
interpret Y: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd_singletons_for_ds Y ds" Ch
[PROOF STATE]
proof (prove)
using this:
CD_on ds Y = Y

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_singletons_for_ds Y ds) Ch
[PROOF STEP]
using Ch_unilateral_substitutes Ch_irc Ch_lad Ch_range Ch_singular Pd_singletons_for_ds_range
          Pd_singletons_for_ds_linear[OF CD_on_inj_on_Xd]
[PROOF STATE]
proof (prove)
using this:
CD_on ds Y = Y
\<forall>h. unilateral_substitutes_on UNIV (Ch h)
\<forall>h. irc (Ch h)
\<forall>h. lad (Ch h)
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
\<forall>h X. inj_on Xd (Ch h X)
Field (Pd_singletons_for_ds ?X ?ds ?d) \<subseteq> {x. Xd x = ?d}
Linear_order (Pd_singletons_for_ds (CD_on ?ds1 ?X1) ?ds ?d)

goal (1 subgoal):
 1. ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh (Pd_singletons_for_ds Y ds) Ch
[PROOF STEP]
by unfold_locales (simp_all, metis)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d); CD_on ds Y = Y; Y.CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from Y.fp_cop_F_doctor_optimal_match Y.doctor_optimal_matchI
[PROOF STATE]
proof (chain)
picking this:
Y.doctor_optimal_match ?ds (Y.cop ?ds)
\<lbrakk>Y.stable_on ?ds ?Y; \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ?ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>?Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)\<rbrakk> \<Longrightarrow> Y.doctor_optimal_match ?ds ?Y
[PROOF STEP]
have "CH (Y.fp_cop_F ds) = Y"
[PROOF STATE]
proof (prove)
using this:
Y.doctor_optimal_match ?ds (Y.cop ?ds)
\<lbrakk>Y.stable_on ?ds ?Y; \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ?ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>?Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)\<rbrakk> \<Longrightarrow> Y.doctor_optimal_match ?ds ?Y

goal (1 subgoal):
 1. Y.cop ds = Y
[PROOF STEP]
proof(rule Y.doctor_optimal_match_unique)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y.stable_on ds Y
 2. \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
show "Y.stable_on ds Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y.stable_on ds Y
[PROOF STEP]
proof(rule Y.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y.individually_rational_on ds Y
 2. Y.stable_no_blocking_on ds Y
[PROOF STEP]
show "Y.individually_rational_on ds Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y.individually_rational_on ds Y
[PROOF STEP]
proof(rule Y.individually_rational_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y.CD_on ds Y = Y
 2. Y.CH Y = Y
[PROOF STEP]
from \<open>CD_on ds Y = Y\<close> CD_on_Xd[where A=Y and ds=ds]
[PROOF STATE]
proof (chain)
picking this:
CD_on ds Y = Y
?x \<in> CD_on ds Y \<Longrightarrow> Xd ?x \<in> ds
[PROOF STEP]
show "Y.CD_on ds Y = Y"
[PROOF STATE]
proof (prove)
using this:
CD_on ds Y = Y
?x \<in> CD_on ds Y \<Longrightarrow> Xd ?x \<in> ds

goal (1 subgoal):
 1. Y.CD_on ds Y = Y
[PROOF STEP]
unfolding Y.CD_on_def CD_on_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>d\<in>ds. Cd d Y) = Y
?x \<in> (\<Union>d\<in>ds. Cd d Y) \<Longrightarrow> Xd ?x \<in> ds

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Y.Cd d Y) = Y
[PROOF STEP]
by (force simp: Y.Cd_greatest Cd_greatest greatest_def Pd_singletons_for_ds_simps dX_def)
[PROOF STATE]
proof (state)
this:
Y.CD_on ds Y = Y

goal (1 subgoal):
 1. Y.CH Y = Y
[PROOF STEP]
from \<open>CH Y = Y\<close>
[PROOF STATE]
proof (chain)
picking this:
Y.CH Y = Y
[PROOF STEP]
show "Y.CH Y = Y"
[PROOF STATE]
proof (prove)
using this:
Y.CH Y = Y

goal (1 subgoal):
 1. Y.CH Y = Y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Y.CH Y = Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Y.individually_rational_on ds Y

goal (1 subgoal):
 1. Y.stable_no_blocking_on ds Y
[PROOF STEP]
show "Y.stable_no_blocking_on ds Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y.stable_no_blocking_on ds Y
[PROOF STEP]
by (rule Y.stable_no_blocking_onI,
            drule subset_trans[OF _ Y.CD_on_range],
            clarsimp simp: Pd_singletons_for_ds_def dX_def Un_absorb1 subset_eq sup_commute)
[PROOF STATE]
proof (state)
this:
Y.stable_no_blocking_on ds Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Y.stable_on ds Y

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
fix x X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
assume "x \<in> X" "Y.stable_on ds X"
[PROOF STATE]
proof (state)
this:
x \<in> X
Y.stable_on ds X

goal (1 subgoal):
 1. \<And>X x. \<lbrakk>x \<in> X; Y.stable_on ds X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
with Y.Theorem_5[of ds X x] Pd_singletons_for_ds_linear[OF \<open>allocation Y\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Y.stable_on ds X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y.cop ds. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
Linear_order (Pd_singletons_for_ds Y ?ds ?d)
x \<in> X
Y.stable_on ds X
[PROOF STEP]
show "\<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Y.stable_on ds X; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>y\<in>Y.cop ds. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
Linear_order (Pd_singletons_for_ds Y ?ds ?d)
x \<in> X
Y.stable_on ds X

goal (1 subgoal):
 1. \<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)
[PROOF STEP]
by (fastforce simp: Pd_singletons_for_ds_simps Y.stable_on_Xd dX_def)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>Y. (x, y) \<in> Pd_singletons_for_ds Y ds (Xd x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Y.cop ds = Y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d); CD_on ds Y = Y; Y.CH Y = Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from Z \<open>CH (Y.fp_cop_F ds) = Y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d)
Y.cop ds = Y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d)
Y.cop ds = Y

goal (1 subgoal):
 1. False
[PROOF STEP]
using group_strategy_proofD[OF
      fp_cop_F_group_strategy_proof
      ContractsWithUnilateralSubstitutesAndIRCAndLAD_axioms subset_refl
      \<open>ds \<noteq> {}\<close>
      Y.ContractsWithUnilateralSubstitutesAndIRCAndLAD_axioms[unfolded Pd_singletons_for_ds_def]]
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d)
Y.cop ds = Y
\<exists>d\<in>ds. \<forall>y\<in>Y.CH (Contracts.fp_cop_F (override_on Pd (\<lambda>d. Y.dX Y d \<times> Y.dX Y d) ds) Ch ds). y \<notin> AboveS (Pd d) (Y.dX (cop ds) d)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Pd_singletons_for_ds_def
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>ds. \<exists>y\<in>Y. y \<in> AboveS (Pd d) (Y.dX (cop ds) d)
Y.CH (Contracts.fp_cop_F (override_on Pd (\<lambda>d. Y.dX Y d \<times> Y.dX Y d) ds) Ch ds) = Y
\<exists>d\<in>ds. \<forall>y\<in>Y.CH (Contracts.fp_cop_F (override_on Pd (\<lambda>d. Y.dX Y d \<times> Y.dX Y d) ds) Ch ds). y \<notin> AboveS (Pd d) (Y.dX (cop ds) d)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_simps[simp]:
  "initial (product A B) = (initial A, initial B)"
  "states (product A B) = (states A) \<times> (states B)"
  "inputs (product A B) = inputs A \<union> inputs B"
  "outputs (product A B) = outputs A \<union> outputs B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial (Product_FSM.product A B) = (FSM.initial A, FSM.initial B) &&& FSM.states (Product_FSM.product A B) = FSM.states A \<times> FSM.states B) &&& FSM.inputs (Product_FSM.product A B) = FSM.inputs A \<union> FSM.inputs B &&& FSM.outputs (Product_FSM.product A B) = FSM.outputs A \<union> FSM.outputs B
[PROOF STEP]
by (transfer; simp)+


[STATEMENT]
lemma product_transitions_def :
  "transitions (product A B) = {((qA,qB),x,y,(qA',qB')) | qA qB x y qA' qB' . (qA,x,y,qA') \<in> transitions A \<and> (qB,x,y,qB') \<in> transitions B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.transitions (Product_FSM.product A B) = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions A \<and> (qB, x, y, qB') \<in> FSM.transitions B}
[PROOF STEP]
by (transfer; simp)+