[STATEMENT]
lemma Ch_domain:
  shows "Ch h (A \<inter> {x. Xh x = h}) = Ch h A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch h (A \<inter> {x. Xh x = h}) = Ch h A
[PROOF STEP]
using %invisible irc_on_discard[OF spec[OF Ch_irc, of h], where B="A \<inter> {x. Xh x = h}" and C="A - {x. Xh x = h}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (A - {x. Xh x = h}); A \<inter> {x. Xh x = h} \<union> (A - {x. Xh x = h}) \<subseteq> UNIV; Ch h (A \<inter> {x. Xh x = h} \<union> (A - {x. Xh x = h})) \<inter> (A - {x. Xh x = h}) = {}\<rbrakk> \<Longrightarrow> Ch h (A \<inter> {x. Xh x = h} \<union> (A - {x. Xh x = h})) = Ch h (A \<inter> {x. Xh x = h})

goal (1 subgoal):
 1. Ch h (A \<inter> {x. Xh x = h}) = Ch h A
[PROOF STEP]
by (fastforce simp: Un_Diff_Int ac_simps dest: Ch_range')


[STATEMENT]
lemma %invisible CH_domain:
  shows "CH A \<inter> {x. Xh x = h} = Ch h (A \<inter> {x. Xh x = h})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH A \<inter> {x. Xh x = h} = Ch h (A \<inter> {x. Xh x = h})
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h. Ch h A) \<inter> {x. Xh x = h} = Ch h (A \<inter> {x. Xh x = h})
[PROOF STEP]
using Ch_range
[PROOF STATE]
proof (prove)
using this:
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}

goal (1 subgoal):
 1. (\<Union>h. Ch h A) \<inter> {x. Xh x = h} = Ch h (A \<inter> {x. Xh x = h})
[PROOF STEP]
by (auto simp: Ch_domain)


[STATEMENT]
lemma %invisible stable_pair_on_Ch:
  assumes "stable_pair_on ds XD_XH"
  shows "Ch h (snd XD_XH) = match XD_XH \<inter> {x. Xh x = h}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch h (snd XD_XH) = match XD_XH \<inter> {x. Xh x = h}
[PROOF STEP]
using stable_pair_on_CH[OF assms] CH_domain Ch_domain
[PROOF STATE]
proof (prove)
using this:
match XD_XH = CH (snd XD_XH)
CH ?A \<inter> {x. Xh x = ?h} = Ch ?h (?A \<inter> {x. Xh x = ?h})
Ch ?h (?A \<inter> {x. Xh x = ?h}) = Ch ?h ?A

goal (1 subgoal):
 1. Ch h (snd XD_XH) = match XD_XH \<inter> {x. Xh x = h}
[PROOF STEP]
by simp


[STATEMENT]
lemma CH_irc_idem:
  shows "CH (CH A) = CH A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH (CH A) = CH A
[PROOF STEP]
unfolding %invisible CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h. Ch h (\<Union>h. Ch h A)) = (\<Union>h. Ch h A)
[PROOF STEP]
by (metis CH_def CH_domain Ch_domain Ch_irc_idem)


[STATEMENT]
lemma Ch_CH_irc_idem:
  shows "Ch h (CH A) = Ch h A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch h (CH A) = Ch h A
[PROOF STEP]
using %invisible CH_domain CH_irc_idem Ch_domain
[PROOF STATE]
proof (prove)
using this:
CH ?A \<inter> {x. Xh x = ?h} = Ch ?h (?A \<inter> {x. Xh x = ?h})
CH (CH ?A) = CH ?A
Ch ?h (?A \<inter> {x. Xh x = ?h}) = Ch ?h ?A

goal (1 subgoal):
 1. Ch h (CH A) = Ch h A
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_individually_rational:
  assumes "stable_pair_on ds XD_XH"
  shows "individually_rational_on ds (match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. individually_rational_on ds (match XD_XH)
[PROOF STEP]
by %invisible (metis CD_on_idem CH_irc_idem stable_pair_on_CD_on stable_pair_on_CD_on_CH assms individually_rational_onI)


[STATEMENT]
lemma stable_pair_on_stable_no_blocking_on:
  assumes "stable_pair_on ds XD_XH"
  shows "stable_no_blocking_on ds (match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds (match XD_XH)
[PROOF STEP]
proof(rule stable_no_blocking_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix h X''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume C: "X'' = Ch h (match XD_XH \<union> X'')"
[PROOF STATE]
proof (state)
this:
X'' = Ch h (match XD_XH \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume NE: "X'' \<noteq> Ch h (match XD_XH)"
[PROOF STATE]
proof (state)
this:
X'' \<noteq> Ch h (match XD_XH)

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume CD: "X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')"
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "X'' \<subseteq> snd XD_XH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
from CD
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')
[PROOF STEP]
have "X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')"
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')
[PROOF STEP]
by (simp only: stable_pair_on_CD_on[OF assms])
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')
[PROOF STEP]
have "X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')"
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
[PROOF STEP]
using CD_on_path_independent
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')
path_independent (CD_on ?ds)

goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
[PROOF STEP]
unfolding path_independent_def
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (CD_on ds (fst XD_XH) \<union> X'')
\<forall>B C. CD_on ?ds (B \<union> C) = CD_on ?ds (B \<union> CD_on ?ds C)

goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
[PROOF STEP]
by (simp add: Un_commute)
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
have "fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
[PROOF STEP]
using CD_on_Chernoff
[PROOF STATE]
proof (prove)
using this:
Chernoff (CD_on ?ds)

goal (1 subgoal):
 1. fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
[PROOF STEP]
unfolding Chernoff_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>B\<subseteq>UNIV. \<forall>C\<subseteq>B. CD_on ?ds B \<inter> C \<subseteq> CD_on ?ds C

goal (1 subgoal):
 1. fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
[PROOF STEP]
by (simp add: inf_commute)
[PROOF STATE]
proof (state)
this:
fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
stable_pair_on ds XD_XH

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
unfolding stable_pair_on_def split_def
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (fst XD_XH \<union> X'')
fst XD_XH \<inter> CD_on ds (fst XD_XH \<union> X'') \<subseteq> CD_on ds (fst XD_XH)
fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH)

goal (1 subgoal):
 1. X'' \<subseteq> snd XD_XH
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> snd XD_XH

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X'' \<subseteq> snd XD_XH

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> snd XD_XH
[PROOF STEP]
have "Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')"
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> snd XD_XH

goal (1 subgoal):
 1. Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')
[PROOF STEP]
by (force intro!: consistencyD[OF Ch_consistency] dest: Ch_range')
[PROOF STATE]
proof (state)
this:
Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from NE
[PROOF STATE]
proof (chain)
picking this:
X'' \<noteq> Ch h (match XD_XH)
[PROOF STEP]
have "X'' \<noteq> Ch h (snd XD_XH)"
[PROOF STATE]
proof (prove)
using this:
X'' \<noteq> Ch h (match XD_XH)

goal (1 subgoal):
 1. X'' \<noteq> Ch h (snd XD_XH)
[PROOF STEP]
using stable_pair_on_CH[OF assms] CH_domain[of _ h] Ch_domain[of h]
[PROOF STATE]
proof (prove)
using this:
X'' \<noteq> Ch h (match XD_XH)
match XD_XH = CH (snd XD_XH)
CH ?A \<inter> {x. Xh x = h} = Ch h (?A \<inter> {x. Xh x = h})
Ch h (?A \<inter> {x. Xh x = h}) = Ch h ?A

goal (1 subgoal):
 1. X'' \<noteq> Ch h (snd XD_XH)
[PROOF STEP]
by (metis Ch_irc_idem)
[PROOF STATE]
proof (state)
this:
X'' \<noteq> Ch h (snd XD_XH)

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')
X'' \<noteq> Ch h (snd XD_XH)
[PROOF STEP]
have "X'' \<noteq> Ch h (match XD_XH \<union> X'')"
[PROOF STATE]
proof (prove)
using this:
Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')
X'' \<noteq> Ch h (snd XD_XH)

goal (1 subgoal):
 1. X'' \<noteq> Ch h (match XD_XH \<union> X'')
[PROOF STEP]
using stable_pair_on_CH[OF assms] CH_domain[of _ h] Ch_domain[of h]
[PROOF STATE]
proof (prove)
using this:
Ch h (snd XD_XH) = Ch h (Ch h (snd XD_XH) \<union> X'')
X'' \<noteq> Ch h (snd XD_XH)
match XD_XH = CH (snd XD_XH)
CH ?A \<inter> {x. Xh x = h} = Ch h (?A \<inter> {x. Xh x = h})
Ch h (?A \<inter> {x. Xh x = h}) = Ch h ?A

goal (1 subgoal):
 1. X'' \<noteq> Ch h (match XD_XH \<union> X'')
[PROOF STEP]
by (metis (no_types, lifting) inf.right_idem inf_sup_distrib2)
[PROOF STATE]
proof (state)
this:
X'' \<noteq> Ch h (match XD_XH \<union> X'')

goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = Ch h (match XD_XH \<union> X''); X'' \<noteq> Ch h (match XD_XH); X'' \<subseteq> CD_on ds (match XD_XH \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with C
[PROOF STATE]
proof (chain)
picking this:
X'' = Ch h (match XD_XH \<union> X'')
X'' \<noteq> Ch h (match XD_XH \<union> X'')
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
X'' = Ch h (match XD_XH \<union> X'')
X'' \<noteq> Ch h (match XD_XH \<union> X'')

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem stable_pair_on_stable_on:
  assumes "stable_pair_on ds XD_XH"
  shows "stable_on ds (match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_on ds (match XD_XH)
[PROOF STEP]
using %invisible assms stable_pair_on_allocation stable_pair_on_individually_rational stable_pair_on_stable_no_blocking_on
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
stable_pair_on ?ds ?XD_XH \<Longrightarrow> inj_on Xd (match ?XD_XH)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> individually_rational_on ?ds (match ?XD_XH)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> stable_no_blocking_on ?ds (match ?XD_XH)

goal (1 subgoal):
 1. stable_on ds (match XD_XH)
[PROOF STEP]
by (blast intro: stable_onI)


[STATEMENT]
lemma Ch_XH_largest_Field:
  assumes "x \<in> Ch h XH_largest"
  shows "x \<in> Field (Pd (Xd x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Field (Pd (Xd x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h XH_largest

goal (1 subgoal):
 1. x \<in> Field (Pd (Xd x))
[PROOF STEP]
unfolding XH_largest_def
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h {y. Xd y \<in> ds \<and> y \<in> Field (Pd (Xd y)) \<and> (\<forall>x\<in>dX X (Xd y). (x, y) \<in> Pd (Xd y))}

goal (1 subgoal):
 1. x \<in> Field (Pd (Xd x))
[PROOF STEP]
by (blast dest: Ch_range')


[STATEMENT]
lemma Ch_XH_largest_Xd:
  assumes "x \<in> Ch h XH_largest"
  shows "Xd x \<in> ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h XH_largest

goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
unfolding XH_largest_def
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h {y. Xd y \<in> ds \<and> y \<in> Field (Pd (Xd y)) \<and> (\<forall>x\<in>dX X (Xd y). (x, y) \<in> Pd (Xd y))}

goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
by (blast dest: Ch_range')


[STATEMENT]
lemma X_subseteq_XH_largest:
  shows "X \<subseteq> XH_largest"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> XH_largest
[PROOF STEP]
proof(rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> XH_largest
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> XH_largest
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> XH_largest
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
obtain d where "d \<in> ds" "x \<in> Cd d X"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>d \<in> ds; x \<in> Cd d X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using stable_on_CD_on[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (prove)
using this:
x \<in> X
CD_on ds X = X

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>d \<in> ds; x \<in> Cd d X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
using this:
x \<in> X
(\<Union>d\<in>ds. Cd d X) = X

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>d \<in> ds; x \<in> Cd d X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d \<in> ds
x \<in> Cd d X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> XH_largest
[PROOF STEP]
with \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
d \<in> ds
x \<in> Cd d X
[PROOF STEP]
show "x \<in> XH_largest"
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
d \<in> ds
x \<in> Cd d X

goal (1 subgoal):
 1. x \<in> XH_largest
[PROOF STEP]
using Pd_linear' Pd_range' Cd_range subset_Image1_Image1_iff[of "Pd d"] stable_on_allocation[of ds X]
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
d \<in> ds
x \<in> Cd d X
Linear_order (Pd ?d)
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)
\<lbrakk>Preorder (Pd d); ?a \<in> Field (Pd d); ?b \<in> Field (Pd d)\<rbrakk> \<Longrightarrow> (Pd d `` {?a} \<subseteq> Pd d `` {?b}) = ((?b, ?a) \<in> Pd d)
stable_on ds X \<Longrightarrow> inj_on Xd X

goal (1 subgoal):
 1. x \<in> XH_largest
[PROOF STEP]
unfolding XH_largest_def linear_order_on_def partial_order_on_def stable_on_def inj_on_def dX_def
[PROOF STATE]
proof (prove)
using this:
individually_rational_on ds X \<and> stable_no_blocking_on ds X
d \<in> ds
x \<in> Cd d X
(Preorder (Pd ?d) \<and> antisym (Pd ?d)) \<and> Total (Pd ?d)
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)
\<lbrakk>Preorder (Pd d); ?a \<in> Field (Pd d); ?b \<in> Field (Pd d)\<rbrakk> \<Longrightarrow> (Pd d `` {?a} \<subseteq> Pd d `` {?b}) = ((?b, ?a) \<in> Pd d)
individually_rational_on ds X \<and> stable_no_blocking_on ds X \<Longrightarrow> \<forall>x\<in>X. \<forall>y\<in>X. Xd x = Xd y \<longrightarrow> x = y

goal (1 subgoal):
 1. x \<in> {y. Xd y \<in> ds \<and> y \<in> Field (Pd (Xd y)) \<and> (\<forall>x\<in>{x \<in> X. Xd x = Xd y}. (x, y) \<in> Pd (Xd y))}
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
x \<in> XH_largest

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma X_subseteq_XD_smallest:
  shows "X \<subseteq> XD_smallest"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> XD_smallest
[PROOF STEP]
unfolding XD_smallest_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> - (XH_largest - X)
[PROOF STEP]
by blast


[STATEMENT]
lemma X_XD_smallest_XH_largest:
  shows "X = XD_smallest \<inter> XH_largest"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = XD_smallest \<inter> XH_largest
[PROOF STEP]
using X_subseteq_XH_largest
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> XH_largest

goal (1 subgoal):
 1. X = XD_smallest \<inter> XH_largest
[PROOF STEP]
unfolding XD_smallest_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> XH_largest

goal (1 subgoal):
 1. X = - (XH_largest - X) \<inter> XH_largest
[PROOF STEP]
by blast


[STATEMENT]
lemma XH_largestCdXXH_largest:
  assumes "x \<in> Ch h XH_largest"
  shows "x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> Ch h XH_largest
[PROOF STEP]
have "(y, x) \<in> Pd (Xd x)" if "Xd y = Xd x" and "y \<in> X" for y
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h XH_largest

goal (1 subgoal):
 1. (y, x) \<in> Pd (Xd x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h XH_largest
Xd y = Xd x
y \<in> X

goal (1 subgoal):
 1. (y, x) \<in> Pd (Xd x)
[PROOF STEP]
by (fastforce simp: XH_largest_def dX_def dest: Ch_range')
[PROOF STATE]
proof (state)
this:
\<lbrakk>Xd ?y = Xd x; ?y \<in> X\<rbrakk> \<Longrightarrow> (?y, x) \<in> Pd (Xd x)

goal (1 subgoal):
 1. x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)
[PROOF STEP]
with Ch_XH_largest_Field[OF assms] Pd_linear Pd_range
[PROOF STATE]
proof (chain)
picking this:
x \<in> Field (Pd (Xd x))
\<forall>d. Linear_order (Pd d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<lbrakk>Xd ?y = Xd x; ?y \<in> X\<rbrakk> \<Longrightarrow> (?y, x) \<in> Pd (Xd x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> Field (Pd (Xd x))
\<forall>d. Linear_order (Pd d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<lbrakk>Xd ?y = Xd x; ?y \<in> X\<rbrakk> \<Longrightarrow> (?y, x) \<in> Pd (Xd x)

goal (1 subgoal):
 1. x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)
[PROOF STEP]
using assms Ch_XH_largest_Field[OF assms]
[PROOF STATE]
proof (prove)
using this:
x \<in> Field (Pd (Xd x))
\<forall>d. Linear_order (Pd d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<lbrakk>Xd ?y = Xd x; ?y \<in> X\<rbrakk> \<Longrightarrow> (?y, x) \<in> Pd (Xd x)
x \<in> Ch h XH_largest
x \<in> Field (Pd (Xd x))

goal (1 subgoal):
 1. x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)
[PROOF STEP]
by (clarsimp simp: Cd_greatest greatest_def)
       (metis Ch_singular Pd_range' inj_onD subset_refl underS_incl_iff)
[PROOF STATE]
proof (state)
this:
x \<in> Cd (Xd x) (X \<union> Ch h XH_largest)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CH_XH_largest:
  shows "CH XH_largest = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH XH_largest = X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CH XH_largest = X
[PROOF STEP]
have "Ch h XH_largest \<subseteq> CD_on ds (X \<union> Ch h XH_largest)" for h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch h XH_largest \<subseteq> CD_on ds (X \<union> Ch h XH_largest)
[PROOF STEP]
using XH_largestCdXXH_largest Ch_XH_largest_Xd Ch_XH_largest_Field
[PROOF STATE]
proof (prove)
using this:
?x \<in> Ch ?h XH_largest \<Longrightarrow> ?x \<in> Cd (Xd ?x) (X \<union> Ch ?h XH_largest)
?x \<in> Ch ?h XH_largest \<Longrightarrow> Xd ?x \<in> ds
?x \<in> Ch ?h XH_largest \<Longrightarrow> ?x \<in> Field (Pd (Xd ?x))

goal (1 subgoal):
 1. Ch h XH_largest \<subseteq> CD_on ds (X \<union> Ch h XH_largest)
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> Ch ?h XH_largest \<Longrightarrow> ?x \<in> Cd (Xd ?x) (X \<union> Ch ?h XH_largest)
?x \<in> Ch ?h XH_largest \<Longrightarrow> Xd ?x \<in> ds
?x \<in> Ch ?h XH_largest \<Longrightarrow> ?x \<in> Field (Pd (Xd ?x))

goal (1 subgoal):
 1. Ch h XH_largest \<subseteq> (\<Union>d\<in>ds. Cd d (X \<union> Ch h XH_largest))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ch ?h XH_largest \<subseteq> CD_on ds (X \<union> Ch ?h XH_largest)

goal (1 subgoal):
 1. CH XH_largest = X
[PROOF STEP]
from \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
[PROOF STEP]
have "Ch h XH_largest = Ch h X" for h
[PROOF STATE]
proof (prove)
using this:
stable_on ds X

goal (1 subgoal):
 1. Ch h XH_largest = Ch h X
[PROOF STEP]
using \<open>Ch h XH_largest \<subseteq> CD_on ds (X \<union> Ch h XH_largest)\<close> X_subseteq_XH_largest
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
Ch h XH_largest \<subseteq> CD_on ds (X \<union> Ch h XH_largest)
X \<subseteq> XH_largest

goal (1 subgoal):
 1. Ch h XH_largest = Ch h X
[PROOF STEP]
by - (erule stable_on_blocking_onD[where h=h and X''="Ch h XH_largest"];
          force intro!: consistencyD[OF Ch_consistency] dest: Ch_range')
[PROOF STATE]
proof (state)
this:
Ch ?h XH_largest = Ch ?h X

goal (1 subgoal):
 1. CH XH_largest = X
[PROOF STEP]
with stable_on_CH[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (chain)
picking this:
CH X = X
Ch ?h XH_largest = Ch ?h X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CH X = X
Ch ?h XH_largest = Ch ?h X

goal (1 subgoal):
 1. CH XH_largest = X
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>h. Ch h X) = X
Ch ?h XH_largest = Ch ?h X

goal (1 subgoal):
 1. (\<Union>h. Ch h XH_largest) = X
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CH XH_largest = X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cd_XD_smallest:
  assumes "d \<in> ds"
  shows "Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
proof(cases "X \<inter> Field (Pd d) = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X \<inter> Field (Pd d) = {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
 2. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
X \<inter> Field (Pd d) = {}

goal (2 subgoals):
 1. X \<inter> Field (Pd d) = {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
 2. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
with Pd_range' Cd_range'[where X=X] stable_on_CD_on[OF \<open>stable_on ds X\<close>] mem_CD_on_Cd assms
[PROOF STATE]
proof (chain)
picking this:
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
?x \<in> Cd ?d X \<Longrightarrow> ?x \<in> X \<inter> Field (Pd ?d)
CD_on ds X = X
(?x \<in> CD_on ?ds ?X) = (?x \<in> Cd (Xd ?x) ?X \<and> Xd ?x \<in> ?ds)
d \<in> ds
X \<inter> Field (Pd d) = {}
[PROOF STEP]
have "- XH_largest \<inter> Field (Pd d) = {}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
?x \<in> Cd ?d X \<Longrightarrow> ?x \<in> X \<inter> Field (Pd ?d)
CD_on ds X = X
(?x \<in> CD_on ?ds ?X) = (?x \<in> Cd (Xd ?x) ?X \<and> Xd ?x \<in> ?ds)
d \<in> ds
X \<inter> Field (Pd d) = {}

goal (1 subgoal):
 1. - XH_largest \<inter> Field (Pd d) = {}
[PROOF STEP]
unfolding XH_largest_def dX_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> Field (Pd ?d) \<Longrightarrow> Xd ?x = ?d
?x \<in> Cd ?d X \<Longrightarrow> ?x \<in> X \<inter> Field (Pd ?d)
CD_on ds X = X
(?x \<in> CD_on ?ds ?X) = (?x \<in> Cd (Xd ?x) ?X \<and> Xd ?x \<in> ?ds)
d \<in> ds
X \<inter> Field (Pd d) = {}

goal (1 subgoal):
 1. - {y. Xd y \<in> ds \<and> y \<in> Field (Pd (Xd y)) \<and> (\<forall>x\<in>{x \<in> X. Xd x = Xd y}. (x, y) \<in> Pd (Xd y))} \<inter> Field (Pd d) = {}
[PROOF STEP]
by auto blast
[PROOF STATE]
proof (state)
this:
- XH_largest \<inter> Field (Pd d) = {}

goal (2 subgoals):
 1. X \<inter> Field (Pd d) = {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
 2. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- XH_largest \<inter> Field (Pd d) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- XH_largest \<inter> Field (Pd d) = {}

goal (1 subgoal):
 1. Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
unfolding XD_smallest_def
[PROOF STATE]
proof (prove)
using this:
- XH_largest \<inter> Field (Pd d) = {}

goal (1 subgoal):
 1. Cd d (- (XH_largest - X) \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
by (simp add: Int_Un_distrib2)
[PROOF STATE]
proof (state)
this:
Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))

goal (1 subgoal):
 1. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
X \<inter> Field (Pd d) \<noteq> {}

goal (1 subgoal):
 1. X \<inter> Field (Pd d) \<noteq> {} \<Longrightarrow> Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
with Pd_linear'[of d] \<open>stable_on ds X\<close> stable_on_CD_on stable_on_allocation assms
[PROOF STATE]
proof (chain)
picking this:
Linear_order (Pd d)
stable_on ds X
stable_on ?ds ?X \<Longrightarrow> CD_on ?ds ?X = ?X
stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
d \<in> ds
X \<inter> Field (Pd d) \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd d)
stable_on ds X
stable_on ?ds ?X \<Longrightarrow> CD_on ?ds ?X = ?X
stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
d \<in> ds
X \<inter> Field (Pd d) \<noteq> {}

goal (1 subgoal):
 1. Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
unfolding XD_smallest_def order_on_defs total_on_def
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd d) \<and> trans (Pd d)) \<and> antisym (Pd d)) \<and> (\<forall>x\<in>Field (Pd d). \<forall>y\<in>Field (Pd d). x \<noteq> y \<longrightarrow> (x, y) \<in> Pd d \<or> (y, x) \<in> Pd d)
stable_on ds X
stable_on ?ds ?X \<Longrightarrow> CD_on ?ds ?X = ?X
stable_on ?ds ?X \<Longrightarrow> inj_on Xd ?X
d \<in> ds
X \<inter> Field (Pd d) \<noteq> {}

goal (1 subgoal):
 1. Cd d (- (XH_largest - X) \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))
[PROOF STEP]
by (auto 0 0 simp: Int_Un_distrib2 Cd_greatest greatest_def XH_largest_def dX_def)
       (metis (mono_tags, lifting) IntI Pd_range' UnCI inj_onD)+
[PROOF STATE]
proof (state)
this:
Cd d (XD_smallest \<inter> Field (Pd d)) = Cd d (X \<inter> Field (Pd d))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CD_on_XD_smallest:
  shows "CD_on ds XD_smallest = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds XD_smallest = X
[PROOF STEP]
using stable_on_CD_on[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (prove)
using this:
CD_on ds X = X

goal (1 subgoal):
 1. CD_on ds XD_smallest = X
[PROOF STEP]
unfolding CD_on_def2
[PROOF STATE]
proof (prove)
using this:
(\<Union>d\<in>ds. Cd d (X \<inter> Field (Pd d))) = X

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d (XD_smallest \<inter> Field (Pd d))) = X
[PROOF STEP]
by (simp add: Cd_XD_smallest)


[STATEMENT]
theorem stable_on_stable_pair_on:
  shows "stable_pair_on ds (XD_smallest, XH_largest)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_pair_on ds (XD_smallest, XH_largest)
[PROOF STEP]
proof(rule stable_pair_onI, simp_all only: prod.sel)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. XD_smallest = - Rf CH XH_largest
 2. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
from CH_XH_largest
[PROOF STATE]
proof (chain)
picking this:
CH XH_largest = X
[PROOF STEP]
have "- RH XH_largest = - (XH_largest - X)"
[PROOF STATE]
proof (prove)
using this:
CH XH_largest = X

goal (1 subgoal):
 1. - Rf CH XH_largest = - (XH_largest - X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- Rf CH XH_largest = - (XH_largest - X)

goal (2 subgoals):
 1. XD_smallest = - Rf CH XH_largest
 2. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Rf CH XH_largest = - (XH_largest - X)

goal (2 subgoals):
 1. XD_smallest = - Rf CH XH_largest
 2. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
from X_XD_smallest_XH_largest
[PROOF STATE]
proof (chain)
picking this:
X = XD_smallest \<inter> XH_largest
[PROOF STEP]
have "\<dots> = XD_smallest"
[PROOF STATE]
proof (prove)
using this:
X = XD_smallest \<inter> XH_largest

goal (1 subgoal):
 1. - (XH_largest - X) = XD_smallest
[PROOF STEP]
unfolding XD_smallest_def
[PROOF STATE]
proof (prove)
using this:
X = - (XH_largest - X) \<inter> XH_largest

goal (1 subgoal):
 1. - (XH_largest - X) = - (XH_largest - X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- (XH_largest - X) = XD_smallest

goal (2 subgoals):
 1. XD_smallest = - Rf CH XH_largest
 2. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- Rf CH XH_largest = XD_smallest
[PROOF STEP]
show "XD_smallest = -RH XH_largest"
[PROOF STATE]
proof (prove)
using this:
- Rf CH XH_largest = XD_smallest

goal (1 subgoal):
 1. XD_smallest = - Rf CH XH_largest
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
XD_smallest = - Rf CH XH_largest

goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
from CD_on_XD_smallest
[PROOF STATE]
proof (chain)
picking this:
CD_on ds XD_smallest = X
[PROOF STEP]
have "-RD_on ds XD_smallest = -(XD_smallest - X)"
[PROOF STATE]
proof (prove)
using this:
CD_on ds XD_smallest = X

goal (1 subgoal):
 1. - Rf (CD_on ds) XD_smallest = - (XD_smallest - X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- Rf (CD_on ds) XD_smallest = - (XD_smallest - X)

goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Rf (CD_on ds) XD_smallest = - (XD_smallest - X)

goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
have "\<dots> = XH_largest"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (XD_smallest - X) = XH_largest
[PROOF STEP]
unfolding XD_smallest_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- (XH_largest - X) - X) = XH_largest
[PROOF STEP]
using X_subseteq_XH_largest
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> XH_largest

goal (1 subgoal):
 1. - (- (XH_largest - X) - X) = XH_largest
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- (XD_smallest - X) = XH_largest

goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- Rf (CD_on ds) XD_smallest = XH_largest
[PROOF STEP]
show "XH_largest = -RD_on ds XD_smallest"
[PROOF STATE]
proof (prove)
using this:
- Rf (CD_on ds) XD_smallest = XH_largest

goal (1 subgoal):
 1. XH_largest = - Rf (CD_on ds) XD_smallest
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
XH_largest = - Rf (CD_on ds) XD_smallest

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem T1:
  shows "stable_on ds X \<longleftrightarrow> (\<exists>XD_XH. stable_pair_on ds XD_XH \<and> X = match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_on ds X = (\<exists>XD_XH. stable_pair_on ds XD_XH \<and> X = match XD_XH)
[PROOF STEP]
using stable_pair_on_stable_on stable_on_stable_pair_on X_XD_smallest_XH_largest
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ?ds ?XD_XH \<Longrightarrow> stable_on ?ds (match ?XD_XH)
stable_on ?ds ?X \<Longrightarrow> stable_pair_on ?ds (XD_smallest ?ds ?X, XH_largest ?ds ?X)
stable_on ?ds ?X \<Longrightarrow> ?X = XD_smallest ?ds ?X \<inter> XH_largest ?ds ?X

goal (1 subgoal):
 1. stable_on ds X = (\<exists>XD_XH. stable_pair_on ds XD_XH \<and> X = match XD_XH)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fix_F_stable_pair_on:
  assumes "X = F ds X"
  shows "stable_pair_on ds (map_prod id undual X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_pair_on ds (map_prod id undual X)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
X = F ds X

goal (1 subgoal):
 1. stable_pair_on ds (map_prod id undual X)
[PROOF STEP]
by (cases X) (simp add: F_def F1_def F2_def stable_pair_on_def dual_eq_iff)


[STATEMENT]
lemma stable_pair_on_fix_F:
  assumes "stable_pair_on ds X"
  shows "map_prod id dual X = F ds (map_prod id dual X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_prod id dual X = F ds (map_prod id dual X)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds X

goal (1 subgoal):
 1. map_prod id dual X = F ds (map_prod id dual X)
[PROOF STEP]
unfolding F_def F1_def F2_def stable_pair_on_def split_def
[PROOF STATE]
proof (prove)
using this:
fst X = - Rf CH (snd X) \<and> snd X = - Rf (CD_on ds) (fst X)

goal (1 subgoal):
 1. map_prod id dual X = (- Rf CH (undual (snd (map_prod id dual X))), dual (- Rf (CD_on ds) (- Rf CH (undual (snd (map_prod id dual X))))))
[PROOF STEP]
by (metis fst_map_prod id_apply prod.collapse snd_map_prod undual_dual)


[STATEMENT]
lemma Rh_mono:
  shows "mono (Rh h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (Rf (Ch h))
[PROOF STEP]
using %invisible substitutes_on_Rf_mono_on[OF spec[OF Ch_substitutes]] mono_on_mono
[PROOF STATE]
proof (prove)
using this:
finite UNIV \<Longrightarrow> Basis.mono_on (Pow UNIV) (Rf (Ch ?x1))
Basis.mono_on UNIV = mono

goal (1 subgoal):
 1. mono (Rf (Ch h))
[PROOF STEP]
by (simp add: fun_eq_iff) blast


[STATEMENT]
lemma RH_mono:
  shows "mono RH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (Rf CH)
[PROOF STEP]
unfolding %invisible CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>X. X - (\<Union>h. Ch h X))
[PROOF STEP]
by (rule monoI) (auto dest: monoD[OF Rh_mono])


[STATEMENT]
lemma F1_antimono:
  shows "antimono F1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<subseteq>) (\<lambda>x y. y \<subseteq> x) F1
[PROOF STEP]
by %invisible (rule antimonoI) (auto simp: F1_def dest: Diff_mono[OF _ monoD[OF RH_mono]])


[STATEMENT]
lemma F2_antimono:
  shows "antimono (F2 ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<subseteq>) (\<lambda>x y. y \<subseteq> x) (F2 ds)
[PROOF STEP]
by %invisible (rule antimonoI) (auto simp: F2_def dest: Diff_mono[OF _ monoD[OF RD_on_mono]])


[STATEMENT]
lemma F_mono:
  shows "mono (F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (F ds)
[PROOF STEP]
unfolding %invisible F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>(XD, XH). (F1 (undual XH), dual (F2 ds (F1 (undual XH)))))
[PROOF STEP]
using antimonoD[OF F1_antimono] antimonoD[OF F2_antimono]
[PROOF STATE]
proof (prove)
using this:
?x \<subseteq> ?y \<Longrightarrow> F1 ?y \<subseteq> F1 ?x
?x \<subseteq> ?y \<Longrightarrow> F2 ?ds1 ?y \<subseteq> F2 ?ds1 ?x

goal (1 subgoal):
 1. mono (\<lambda>(XD, XH). (F1 (undual XH), dual (F2 ds (F1 (undual XH)))))
[PROOF STEP]
by (auto intro: monoI simp: less_eq_dual_def)


[STATEMENT]
lemma F2_o_F1_mono:
  shows "mono (F2 ds \<circ> F1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (F2 ds \<circ> F1)
[PROOF STEP]
by %invisible (metis F2_antimono F1_antimono antimono_def comp_apply monoI)


[STATEMENT]
lemma gfp_F_lfp_F:
  shows "gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
let ?F' = "dual \<circ> F2 ds \<circ> F1 \<circ> undual"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
have "gfp (F ds) = (F1 (undual (gfp ?F')), gfp ?F')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp (F ds) = (F1 (undual (gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))), gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))
[PROOF STEP]
by (subst gfp_prod[OF F_mono]) (simp add: F_def o_def gfp_const)
[PROOF STATE]
proof (state)
this:
gfp (F ds) = (F1 (undual (gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))), gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))

goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gfp (F ds) = (F1 (undual (gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))), gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual))

goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
have "gfp ?F' = dual (lfp (F2 ds \<circ> F1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual) = dual (lfp (F2 ds \<circ> F1))
[PROOF STEP]
by (simp add: lfp_dual_gfp[OF F2_o_F1_mono, simplified o_assoc])
[PROOF STATE]
proof (state)
this:
gfp (dual \<circ> F2 ds \<circ> F1 \<circ> undual) = dual (lfp (F2 ds \<circ> F1))

goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gfp (F ds) = (F1 (undual (dual (lfp (F2 ds \<circ> F1)))), dual (lfp (F2 ds \<circ> F1)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gfp (F ds) = (F1 (undual (dual (lfp (F2 ds \<circ> F1)))), dual (lfp (F2 ds \<circ> F1)))

goal (1 subgoal):
 1. gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
unfolding gfp_F_def
[PROOF STATE]
proof (prove)
using this:
gfp (F ds) = (F1 (undual (dual (lfp (F2 ds \<circ> F1)))), dual (lfp (F2 ds \<circ> F1)))

goal (1 subgoal):
 1. map_prod id undual (gfp (F ds)) = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gfp_F ds = (F1 (lfp (F2 ds \<circ> F1)), lfp (F2 ds \<circ> F1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gfp_F_code[code]:
  shows "gfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) top)
[PROOF STEP]
using %invisible gfp_F_def gfp_while_lattice[OF F_mono]
[PROOF STATE]
proof (prove)
using this:
gfp_F ?ds = map_prod id undual (gfp (F ?ds))
finite UNIV \<Longrightarrow> gfp (F ?ds1) = while (\<lambda>A. F ?ds1 A \<noteq> A) (F ?ds1) top

goal (1 subgoal):
 1. gfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) top)
[PROOF STEP]
by simp


[STATEMENT]
lemma lfp_F_code[code]:
  shows "lfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) bot)
[PROOF STEP]
using %invisible lfp_F_def lfp_while_lattice[OF F_mono]
[PROOF STATE]
proof (prove)
using this:
lfp_F ?ds = map_prod id undual (lfp (F ?ds))
finite UNIV \<Longrightarrow> lfp (F ?ds1) = while (\<lambda>A. F ?ds1 A \<noteq> A) (F ?ds1) bot

goal (1 subgoal):
 1. lfp_F ds = map_prod id undual (while (\<lambda>A. F ds A \<noteq> A) (F ds) bot)
[PROOF STEP]
by simp


[STATEMENT]
lemma H2_UNIV:
  shows "UNIV = set [H1, H2]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = set [H1, H2]
[PROOF STEP]
using H2.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = H1 \<Longrightarrow> ?P; ?y = H2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. UNIV = set [H1, H2]
[PROOF STEP]
by auto


[STATEMENT]
lemma H2_ALL [simp]:
  shows "(\<forall>h. P h) = (\<forall>h\<in>{H1, H2}. P h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h. P h) = (\<forall>h\<in>{H1, H2}. P h)
[PROOF STEP]
using H2_UNIV
[PROOF STATE]
proof (prove)
using this:
UNIV = set [H1, H2]

goal (1 subgoal):
 1. (\<forall>h. P h) = (\<forall>h\<in>{H1, H2}. P h)
[PROOF STEP]
by auto


[STATEMENT]
lemma H2_UNION:
  shows "(\<Union>h. P h) = (\<Union>h\<in>{H1, H2}. P h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range P) = \<Union> (P ` {H1, H2})
[PROOF STEP]
using H2_UNIV
[PROOF STATE]
proof (prove)
using this:
UNIV = set [H1, H2]

goal (1 subgoal):
 1. \<Union> (range P) = \<Union> (P ` {H1, H2})
[PROOF STEP]
by auto


[STATEMENT]
lemma P_D2_H2_d_linear:
  shows "Linear_order (P_D2_H2_d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (P_D2_H2_d d)
[PROOF STEP]
by (cases d) (simp_all add: linord_of_list_Linear_order)


[STATEMENT]
lemma P_D2_H2_d_range:
  shows "Field (P_D2_H2_d d) \<subseteq> {x. fst x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (P_D2_H2_d d) \<subseteq> {x. fst x = d}
[PROOF STEP]
by (cases d) simp_all


[STATEMENT]
lemma P_D2_H2_h_substitutes:
  shows "substitutes (P_D2_H2_h h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. substitutes (P_D2_H2_h h)
[PROOF STEP]
by %invisible (cases h) (auto intro!: substitutes_onI simp: P_D2_H2_H1_def P_D2_H2_H2_def split: if_splits)


[STATEMENT]
lemma P920_example_gfp_F_value:
  shows "P920_example_gfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P920_example_gfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})
[PROOF STEP]
by eval


[STATEMENT]
lemma P920_example_gfp_F_match_value:
  shows "P920_example.match (P920_example_gfp_F UNIV) = {(D1, H1), (D2, H2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P920_example.match (P920_example_gfp_F UNIV) = {(D1, H1), (D2, H2)}
[PROOF STEP]
unfolding P920_example_gfp_F_value
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P920_example.match ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)}) = {(D1, H1), (D2, H2)}
[PROOF STEP]
by simp


[STATEMENT]
lemma P920_example_lfp_F_value:
  shows "P920_example_lfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P920_example_lfp_F UNIV = ({(D1, H1), (D1, H2), (D2, H2)}, {(D1, H1), (D2, H1), (D2, H2)})
[PROOF STEP]
by eval


[STATEMENT]
lemma doctor_optimal_match_unique:
  assumes "doctor_optimal_match ds X"
  assumes "doctor_optimal_match ds Y"
  shows "X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = Y
[PROOF STEP]
proof(rule iffD2[OF set_eq_iff, rule_format])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> X) = (x \<in> Y)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> X) = (x \<in> Y)
[PROOF STEP]
from Pd_linear'[where d="Xd x"] Pd_Xd[where d="Xd x"]
       stable_on_allocation[OF doctor_optimal_match_stable_on[OF assms(1)]]
       stable_on_allocation[OF doctor_optimal_match_stable_on[OF assms(2)]]
       assms
[PROOF STATE]
proof (chain)
picking this:
Linear_order (Pd (Xd x))
(?x, ?y) \<in> Pd (Xd x) \<Longrightarrow> Xd ?x = Xd x \<and> Xd ?y = Xd x
inj_on Xd X
inj_on Xd Y
doctor_optimal_match ds X
doctor_optimal_match ds Y
[PROOF STEP]
show "x \<in> X \<longleftrightarrow> x \<in> Y"
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd (Xd x))
(?x, ?y) \<in> Pd (Xd x) \<Longrightarrow> Xd ?x = Xd x \<and> Xd ?y = Xd x
inj_on Xd X
inj_on Xd Y
doctor_optimal_match ds X
doctor_optimal_match ds Y

goal (1 subgoal):
 1. (x \<in> X) = (x \<in> Y)
[PROOF STEP]
unfolding doctor_optimal_match_def order_on_defs
[PROOF STATE]
proof (prove)
using this:
((Refl (Pd (Xd x)) \<and> trans (Pd (Xd x))) \<and> antisym (Pd (Xd x))) \<and> Total (Pd (Xd x))
(?x, ?y) \<in> Pd (Xd x) \<Longrightarrow> Xd ?x = Xd x \<and> Xd ?y = Xd x
inj_on Xd X
inj_on Xd Y
stable_on ds X \<and> (\<forall>Xa. \<forall>x\<in>Xa. stable_on ds Xa \<longrightarrow> (\<exists>y\<in>X. (x, y) \<in> Pd (Xd x)))
stable_on ds Y \<and> (\<forall>X. \<forall>x\<in>X. stable_on ds X \<longrightarrow> (\<exists>y\<in>Y. (x, y) \<in> Pd (Xd x)))

goal (1 subgoal):
 1. (x \<in> X) = (x \<in> Y)
[PROOF STEP]
by - (rule iffI; metis antisymD inj_on_eq_iff)
[PROOF STATE]
proof (state)
this:
(x \<in> X) = (x \<in> Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gfp_F_upperbound:
  shows "(fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)
[PROOF STEP]
have "(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
using stable_pair_on_fix_F[OF \<open>stable_pair_on ds XD_XH\<close>]
[PROOF STATE]
proof (prove)
using this:
map_prod id dual XD_XH = F ds (map_prod id dual XD_XH)

goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
by (metis id_apply map_prod_simp prod.collapse)
[PROOF STATE]
proof (state)
this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)
[PROOF STEP]
by (fastforce intro: gfp_upperbound)
[PROOF STATE]
proof (state)
this:
(fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma XD_XH_gfp_F:
  shows "fst XD_XH \<subseteq> fst (gfp_F ds)"
    and "snd (gfp_F ds) \<subseteq> snd XD_XH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst XD_XH \<subseteq> fst (gfp_F ds) &&& snd (gfp_F ds) \<subseteq> snd XD_XH
[PROOF STEP]
using %invisible gfp_F_upperbound
[PROOF STATE]
proof (prove)
using this:
(fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)

goal (1 subgoal):
 1. fst XD_XH \<subseteq> fst (gfp_F ds) &&& snd (gfp_F ds) \<subseteq> snd XD_XH
[PROOF STEP]
unfolding gfp_F_def
[PROOF STATE]
proof (prove)
using this:
(fst XD_XH, dual (snd XD_XH)) \<le> gfp (F ds)

goal (1 subgoal):
 1. fst XD_XH \<subseteq> fst (map_prod id undual (gfp (F ds))) &&& snd (map_prod id undual (gfp (F ds))) \<subseteq> snd XD_XH
[PROOF STEP]
by (simp_all add: less_eq_dual_def less_eq_prod_def)


[STATEMENT]
lemma lfp_F_upperbound:
  shows "lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
have "(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
using stable_pair_on_fix_F[OF \<open>stable_pair_on ds XD_XH\<close>]
[PROOF STATE]
proof (prove)
using this:
map_prod id dual XD_XH = F ds (map_prod id dual XD_XH)

goal (1 subgoal):
 1. (fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
by (metis id_apply map_prod_simp prod.collapse)
[PROOF STATE]
proof (state)
this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(fst XD_XH, dual (snd XD_XH)) = F ds (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))
[PROOF STEP]
by (fastforce intro: lfp_lowerbound)
[PROOF STATE]
proof (state)
this:
lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma XD_XH_lfp_F:
  shows "fst (lfp_F ds) \<subseteq> fst XD_XH"
    and "snd XD_XH \<subseteq> snd (lfp_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (lfp_F ds) \<subseteq> fst XD_XH &&& snd XD_XH \<subseteq> snd (lfp_F ds)
[PROOF STEP]
using %invisible lfp_F_upperbound
[PROOF STATE]
proof (prove)
using this:
lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. fst (lfp_F ds) \<subseteq> fst XD_XH &&& snd XD_XH \<subseteq> snd (lfp_F ds)
[PROOF STEP]
unfolding lfp_F_def
[PROOF STATE]
proof (prove)
using this:
lfp (F ds) \<le> (fst XD_XH, dual (snd XD_XH))

goal (1 subgoal):
 1. fst (map_prod id undual (lfp (F ds))) \<subseteq> fst XD_XH &&& snd XD_XH \<subseteq> snd (map_prod id undual (lfp (F ds)))
[PROOF STEP]
by (simp_all add: less_eq_dual_def less_eq_prod_def)


[STATEMENT]
theorem gfp_f_doctor_optimal:
  assumes "x \<in> match XD_XH"
  shows "\<exists>y \<in> match (gfp_F ds). (x, y) \<in> Pd (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>match (gfp_F ds). (x, y) \<in> Pd (Xd x)
[PROOF STEP]
using %invisible assms gfp_F_stable_pair_on[where ds=ds] \<open>stable_pair_on ds XD_XH\<close>
      stable_pair_on_CD_on stable_pair_on_Xd Cd_Xd mem_CD_on_Cd
      XD_XH_gfp_F(1) Cd_mono[where d="Xd x" and x=x and X="fst XD_XH" and Y="fst (gfp_F ds)"]
[PROOF STATE]
proof (prove)
using this:
x \<in> match XD_XH
stable_pair_on ds (gfp_F ds)
stable_pair_on ds XD_XH
stable_pair_on ?ds ?XD_XH \<Longrightarrow> match ?XD_XH = CD_on ?ds (fst ?XD_XH)
\<lbrakk>stable_pair_on ?ds ?XD_XH; ?x \<in> match ?XD_XH\<rbrakk> \<Longrightarrow> Xd ?x \<in> ?ds
?x \<in> Cd ?d ?X \<Longrightarrow> Xd ?x = ?d
(?x \<in> CD_on ?ds ?X) = (?x \<in> Cd (Xd ?x) ?X \<and> Xd ?x \<in> ?ds)
fst XD_XH \<subseteq> fst (gfp_F ds)
x \<in> Cd (Xd x) (fst XD_XH) \<Longrightarrow> \<exists>y\<in>Cd (Xd x) (fst XD_XH \<union> fst (gfp_F ds)). (x, y) \<in> Pd (Xd x)

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


[STATEMENT]
theorem lfp_f_doctor_pessimal:
  assumes "x \<in> match (lfp_F ds)"
  shows "\<exists>y \<in> match XD_XH. (x, y) \<in> Pd (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>match XD_XH. (x, y) \<in> Pd (Xd x)
[PROOF STEP]
using %invisible assms lfp_F_stable_pair_on[where ds=ds] \<open>stable_pair_on ds XD_XH\<close>
      stable_pair_on_CD_on stable_pair_on_Xd Cd_Xd mem_CD_on_Cd
      XD_XH_lfp_F(1) Cd_mono[where d="Xd x" and x=x and X="fst (lfp_F ds)" and Y="fst XD_XH"]
[PROOF STATE]
proof (prove)
using this:
x \<in> match (lfp_F ds)
stable_pair_on ds (lfp_F ds)
stable_pair_on ds XD_XH
stable_pair_on ?ds ?XD_XH \<Longrightarrow> match ?XD_XH = CD_on ?ds (fst ?XD_XH)
\<lbrakk>stable_pair_on ?ds ?XD_XH; ?x \<in> match ?XD_XH\<rbrakk> \<Longrightarrow> Xd ?x \<in> ?ds
?x \<in> Cd ?d ?X \<Longrightarrow> Xd ?x = ?d
(?x \<in> CD_on ?ds ?X) = (?x \<in> Cd (Xd ?x) ?X \<and> Xd ?x \<in> ?ds)
fst (lfp_F ds) \<subseteq> fst XD_XH
x \<in> Cd (Xd x) (fst (lfp_F ds)) \<Longrightarrow> \<exists>y\<in>Cd (Xd x) (fst (lfp_F ds) \<union> fst XD_XH). (x, y) \<in> Pd (Xd x)

goal (1 subgoal):
 1. \<exists>y\<in>match XD_XH. (x, y) \<in> Pd (Xd x)
[PROOF STEP]
by (metis sup.absorb_iff2)


[STATEMENT]
theorem (in ContractsWithSubstitutesAndIRC) gfp_F_doctor_optimal_match:
  shows "doctor_optimal_match ds (match (gfp_F ds))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doctor_optimal_match ds (match (gfp_F ds))
[PROOF STEP]
by %invisible (rule doctor_optimal_matchI[OF gfp_F_stable_on]) (auto simp: T1 elim: gfp_f_doctor_optimal)


[STATEMENT]
theorem lfp_f_hospital_optimal:
  assumes "stable_pair_on ds XD_XH"
  assumes "x \<in> Ch h (match (lfp_F ds))"
  shows "x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)
[PROOF STEP]
from \<open>stable_pair_on ds XD_XH\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_pair_on ds XD_XH
[PROOF STEP]
have "match (lfp_F ds) \<union> match XD_XH \<subseteq> snd (lfp_F ds)"
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH

goal (1 subgoal):
 1. match (lfp_F ds) \<union> match XD_XH \<subseteq> snd (lfp_F ds)
[PROOF STEP]
by (simp add: XD_XH_lfp_F(2) le_infI2)
[PROOF STATE]
proof (state)
this:
match (lfp_F ds) \<union> match XD_XH \<subseteq> snd (lfp_F ds)

goal (1 subgoal):
 1. x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)
[PROOF STEP]
with \<open>x \<in> Ch h (match (lfp_F ds))\<close> lfp_F_stable_pair_on stable_pair_on_Ch Ch_range
[PROOF STATE]
proof (chain)
picking this:
x \<in> Ch h (match (lfp_F ds))
stable_pair_on ?ds (lfp_F ?ds)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> Ch ?h (snd ?XD_XH) = match ?XD_XH \<inter> {x. Xh x = ?h}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
match (lfp_F ds) \<union> match XD_XH \<subseteq> snd (lfp_F ds)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h (match (lfp_F ds))
stable_pair_on ?ds (lfp_F ?ds)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> Ch ?h (snd ?XD_XH) = match ?XD_XH \<inter> {x. Xh x = ?h}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
match (lfp_F ds) \<union> match XD_XH \<subseteq> snd (lfp_F ds)

goal (1 subgoal):
 1. x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)
[PROOF STEP]
by - (rule iia_onD[OF Ch_iia[where h=h], where B="snd (lfp_F ds)", simplified]; blast)
[PROOF STATE]
proof (state)
this:
x \<in> Ch h (match (lfp_F ds) \<union> match XD_XH)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem gfp_f_hospital_pessimal:
  assumes "stable_pair_on ds XD_XH"
  assumes "x \<in> Ch h (match XD_XH)"
  shows "x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)
[PROOF STEP]
from \<open>stable_pair_on ds XD_XH\<close>
[PROOF STATE]
proof (chain)
picking this:
stable_pair_on ds XD_XH
[PROOF STEP]
have "match (gfp_F ds) \<union> match XD_XH \<subseteq> snd XD_XH"
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH

goal (1 subgoal):
 1. match (gfp_F ds) \<union> match XD_XH \<subseteq> snd XD_XH
[PROOF STEP]
by (simp add: XD_XH_gfp_F(2) le_infI2)
[PROOF STATE]
proof (state)
this:
match (gfp_F ds) \<union> match XD_XH \<subseteq> snd XD_XH

goal (1 subgoal):
 1. x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)
[PROOF STEP]
with assms lfp_F_stable_pair_on stable_pair_on_Ch Ch_range
[PROOF STATE]
proof (chain)
picking this:
stable_pair_on ds XD_XH
x \<in> Ch h (match XD_XH)
stable_pair_on ?ds (lfp_F ?ds)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> Ch ?h (snd ?XD_XH) = match ?XD_XH \<inter> {x. Xh x = ?h}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
match (gfp_F ds) \<union> match XD_XH \<subseteq> snd XD_XH
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
x \<in> Ch h (match XD_XH)
stable_pair_on ?ds (lfp_F ?ds)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> Ch ?h (snd ?XD_XH) = match ?XD_XH \<inter> {x. Xh x = ?h}
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
match (gfp_F ds) \<union> match XD_XH \<subseteq> snd XD_XH

goal (1 subgoal):
 1. x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)
[PROOF STEP]
by - (rule iia_onD[OF Ch_iia[where h=h], where B="snd XD_XH", simplified]; blast+)
[PROOF STATE]
proof (state)
this:
x \<in> Ch h (match (gfp_F ds) \<union> match XD_XH)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma F'_apply:
  "F' (XD, XH) = (- RH (undual XH), dual (- RD_on (ds - {d'}) XD))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F' (XD, XH) = (- Rf CH (undual XH), dual (- Rf (CD_on (ds - {d'})) XD))
[PROOF STEP]
by (simp add: F'_def)


[STATEMENT]
lemma %invisible F1'_antimono:
  shows "antimono (\<lambda>XH. - RH XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<subseteq>) (\<lambda>x y. y \<subseteq> x) (\<lambda>XH. - Rf CH XH)
[PROOF STEP]
by %invisible (rule antimonoI) (auto simp: F1_def dest: Diff_mono[OF _ monoD[OF RH_mono]])


[STATEMENT]
lemma %invisible F2'_antimono:
  shows "antimono (\<lambda>XD. - RD_on (ds-{d'}) XD)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<subseteq>) (\<lambda>x y. y \<subseteq> x) (\<lambda>XD. - Rf (CD_on (ds - {d'})) XD)
[PROOF STEP]
by %invisible (rule antimonoI) (auto simp: F2_def dest: Diff_mono[OF _ monoD[OF RD_on_mono]])


[STATEMENT]
lemma F'_mono:
  shows "mono F'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono F'
[PROOF STEP]
unfolding %invisible F'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>(XD, XH). (- Rf CH (undual XH), dual (- Rf (CD_on (ds - {d'})) XD)))
[PROOF STEP]
using antimonoD[OF F1'_antimono] antimonoD[OF F2'_antimono]
[PROOF STATE]
proof (prove)
using this:
?x \<subseteq> ?y \<Longrightarrow> - Rf CH ?y \<subseteq> - Rf CH ?x
?x \<subseteq> ?y \<Longrightarrow> - Rf (CD_on (ds - {d'})) ?y \<subseteq> - Rf (CD_on (ds - {d'})) ?x

goal (1 subgoal):
 1. mono (\<lambda>(XD, XH). (- Rf CH (undual XH), dual (- Rf (CD_on (ds - {d'})) XD)))
[PROOF STEP]
by (auto intro: monoI simp: less_eq_dual_def)


[STATEMENT]
lemma fix_F'_stable_pair_on:
  "stable_pair_on (ds - {d'}) (map_prod id undual A)"
  if "A = F' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
obtain x y where "A = (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. A = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases A)
[PROOF STATE]
proof (state)
this:
A = (x, y)

goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
A = F' A
A = (x, y)
[PROOF STEP]
have "F' (x, y) = (x, y)"
[PROOF STATE]
proof (prove)
using this:
A = F' A
A = (x, y)

goal (1 subgoal):
 1. F' (x, y) = (x, y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F' (x, y) = (x, y)

goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F' (x, y) = (x, y)
[PROOF STEP]
have "- Rf CH (undual y) = x" and
    "dual (- Rf (CD_on (ds - {d'})) x) = y"
[PROOF STATE]
proof (prove)
using this:
F' (x, y) = (x, y)

goal (1 subgoal):
 1. - Rf CH (undual y) = x &&& dual (- Rf (CD_on (ds - {d'})) x) = y
[PROOF STEP]
by (simp_all only: F'_apply prod_eq_iff fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
- Rf CH (undual y) = x
dual (- Rf (CD_on (ds - {d'})) x) = y

goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
with \<open>A = (x, y)\<close>
[PROOF STATE]
proof (chain)
picking this:
A = (x, y)
- Rf CH (undual y) = x
dual (- Rf (CD_on (ds - {d'})) x) = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = (x, y)
- Rf CH (undual y) = x
dual (- Rf (CD_on (ds - {d'})) x) = y

goal (1 subgoal):
 1. stable_pair_on (ds - {d'}) (map_prod id undual A)
[PROOF STEP]
by (simp add: stable_pair_on_def dual_eq_iff)
[PROOF STATE]
proof (state)
this:
stable_pair_on (ds - {d'}) (map_prod id undual A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma F_start:
  shows "F ds (XD_smallest ds X, dual (XH_largest ds X)) = (XD_smallest ds X, dual (XH_largest ds X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F ds (XD_smallest ds X, dual (XH_largest ds X)) = (XD_smallest ds X, dual (XH_largest ds X))
[PROOF STEP]
using %invisible CH_XH_largest[OF \<open>stable_on ds X\<close>] CD_on_XD_smallest[OF \<open>stable_on ds X\<close>] X_subseteq_XH_largest[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (prove)
using this:
CH (XH_largest ds X) = X
CD_on ds (XD_smallest ds X) = X
X \<subseteq> XH_largest ds X

goal (1 subgoal):
 1. F ds (XD_smallest ds X, dual (XH_largest ds X)) = (XD_smallest ds X, dual (XH_largest ds X))
[PROOF STEP]
unfolding F_def F1_def F2_def XD_smallest_def
[PROOF STATE]
proof (prove)
using this:
CH (XH_largest ds X) = X
CD_on ds (- (XH_largest ds X - X)) = X
X \<subseteq> XH_largest ds X

goal (1 subgoal):
 1. (case (- (XH_largest ds X - X), dual (XH_largest ds X)) of (XD, XH) \<Rightarrow> (- Rf CH (undual XH), dual (- Rf (CD_on ds) (- Rf CH (undual XH))))) = (- (XH_largest ds X - X), dual (XH_largest ds X))
[PROOF STEP]
by (auto simp add: dual_eq_iff)


[STATEMENT]
lemma F'_start:
  shows "(XD_smallest ds X, dual (XH_largest ds X)) \<le> F' (XD_smallest ds X, dual (XH_largest ds X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (XD_smallest ds X, dual (XH_largest ds X)) \<le> F' (XD_smallest ds X, dual (XH_largest ds X))
[PROOF STEP]
using %invisible F_start
[PROOF STATE]
proof (prove)
using this:
F ds (XD_smallest ds X, dual (XH_largest ds X)) = (XD_smallest ds X, dual (XH_largest ds X))

goal (1 subgoal):
 1. (XD_smallest ds X, dual (XH_largest ds X)) \<le> F' (XD_smallest ds X, dual (XH_largest ds X))
[PROOF STEP]
unfolding F_def F1_def F2_def F'_def
[PROOF STATE]
proof (prove)
using this:
(case (XD_smallest ds X, dual (XH_largest ds X)) of (XD, XH) \<Rightarrow> (- Rf CH (undual XH), dual (- Rf (CD_on ds) (- Rf CH (undual XH))))) = (XD_smallest ds X, dual (XH_largest ds X))

goal (1 subgoal):
 1. (XD_smallest ds X, dual (XH_largest ds X)) \<le> (case (XD_smallest ds X, dual (XH_largest ds X)) of (XD, XH) \<Rightarrow> (- Rf CH (undual XH), dual (- Rf (CD_on (ds - {d'})) XD)))
[PROOF STEP]
unfolding CD_on_def XD_smallest_def
[PROOF STATE]
proof (prove)
using this:
(case (- (XH_largest ds X - X), dual (XH_largest ds X)) of (XD, XH) \<Rightarrow> (- Rf CH (undual XH), dual (- (- Rf CH (undual XH) - (\<Union>d\<in>ds. Cd d (- Rf CH (undual XH))))))) = (- (XH_largest ds X - X), dual (XH_largest ds X))

goal (1 subgoal):
 1. (- (XH_largest ds X - X), dual (XH_largest ds X)) \<le> (case (- (XH_largest ds X - X), dual (XH_largest ds X)) of (XD, XH) \<Rightarrow> (- Rf CH (undual XH), dual (- (XD - (\<Union>d\<in>ds - {d'}. Cd d XD)))))
[PROOF STEP]
by (auto simp add: dual_eq_iff dual_less_eq_iff)


[STATEMENT]
lemma F'_iter_match_stable_on:
  shows "stable_on (ds-{d'}) F'_iter_match"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_on (ds - {d'}) (match (map_prod id undual F'_iter))
[PROOF STEP]
by %invisible (rule stable_pair_on_stable_on) (metis F'_iter_stable_pair_on)


[STATEMENT]
theorem F'_iter_match_doctors_weakly_better_off:
  assumes "x \<in> Cd d X"
  assumes "d \<noteq> d'"
  shows "\<exists>y \<in> Cd d F'_iter_match. (x, y) \<in> Pd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
from \<open>stable_on ds X\<close> assms
[PROOF STATE]
proof (chain)
picking this:
stable_on ds X
x \<in> Cd d X
d \<noteq> d'
[PROOF STEP]
have "d \<in> ds"
[PROOF STATE]
proof (prove)
using this:
stable_on ds X
x \<in> Cd d X
d \<noteq> d'

goal (1 subgoal):
 1. d \<in> ds
[PROOF STEP]
by (blast dest: Cd_Xd Cd_range' stable_on_Xd)
[PROOF STATE]
proof (state)
this:
d \<in> ds

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
with assms \<open>stable_on ds X\<close> stable_on_stable_pair_on[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (chain)
picking this:
x \<in> Cd d X
d \<noteq> d'
stable_on ds X
stable_pair_on ds (XD_smallest ds X, XH_largest ds X)
d \<in> ds
[PROOF STEP]
have "\<exists>y\<in>Cd d (XD_smallest ds X \<union> fst F'_iter). (x, y) \<in> Pd d"
[PROOF STATE]
proof (prove)
using this:
x \<in> Cd d X
d \<noteq> d'
stable_on ds X
stable_pair_on ds (XD_smallest ds X, XH_largest ds X)
d \<in> ds

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (XD_smallest ds X \<union> fst F'_iter). (x, y) \<in> Pd d
[PROOF STEP]
by - (rule Cd_mono; fastforce dest: X_XD_smallest_XH_largest stable_pair_on_Cd_match)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>Cd d (XD_smallest ds X \<union> fst F'_iter). (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
with F'_iter_stable_pair_on F'_start_le_F'_iter
[PROOF STATE]
proof (chain)
picking this:
stable_pair_on (ds - {d'}) (map_prod id undual F'_iter)
(XD_smallest ds X, dual (XH_largest ds X)) \<le> F'_iter
\<exists>y\<in>Cd d (XD_smallest ds X \<union> fst F'_iter). (x, y) \<in> Pd d
[PROOF STEP]
have "\<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d"
[PROOF STATE]
proof (prove)
using this:
stable_pair_on (ds - {d'}) (map_prod id undual F'_iter)
(XD_smallest ds X, dual (XH_largest ds X)) \<le> F'_iter
\<exists>y\<in>Cd d (XD_smallest ds X \<union> fst F'_iter). (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d
[PROOF STEP]
by (metis Pair_le Un_absorb1 prod.collapse)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
with \<open>d \<noteq> d'\<close> \<open>d \<in> ds\<close>
[PROOF STATE]
proof (chain)
picking this:
d \<noteq> d'
d \<in> ds
\<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d \<noteq> d'
d \<in> ds
\<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
using stable_pair_on_Cd[OF F'_iter_stable_pair_on, symmetric, of d]
[PROOF STATE]
proof (prove)
using this:
d \<noteq> d'
d \<in> ds
\<exists>y\<in>Cd d (fst F'_iter). (x, y) \<in> Pd d
d \<in> ds - {d'} \<Longrightarrow> match (map_prod id undual F'_iter) \<inter> Field (Pd d) = Cd d (fst (map_prod id undual F'_iter))

goal (1 subgoal):
 1. \<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d
[PROOF STEP]
by (subst Cd_domain[symmetric]) (simp add: Cd_idem)
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>Cd d (match (map_prod id undual F'_iter)). (x, y) \<in> Pd d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem F'_iter_match_hospitals_weakly_worse_off:
  assumes "x \<in> Ch h X"
  shows "x \<in> Ch h (F'_iter_match \<union> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Ch h (match (map_prod id undual F'_iter) \<union> X)
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> Ch h (match (map_prod id undual F'_iter) \<union> X)
[PROOF STEP]
from F'_iter_stable_pair_on F'_start_le_F'_iter stable_on_stable_pair_on[OF \<open>stable_on ds X\<close>] X_subseteq_XH_largest[OF \<open>stable_on ds X\<close>]
[PROOF STATE]
proof (chain)
picking this:
stable_pair_on (ds - {d'}) (map_prod id undual F'_iter)
(XD_smallest ds X, dual (XH_largest ds X)) \<le> F'_iter
stable_pair_on ds (XD_smallest ds X, XH_largest ds X)
X \<subseteq> XH_largest ds X
[PROOF STEP]
have "F'_iter_match \<union> X \<subseteq> XH_largest ds X"
[PROOF STATE]
proof (prove)
using this:
stable_pair_on (ds - {d'}) (map_prod id undual F'_iter)
(XD_smallest ds X, dual (XH_largest ds X)) \<le> F'_iter
stable_pair_on ds (XD_smallest ds X, XH_largest ds X)
X \<subseteq> XH_largest ds X

goal (1 subgoal):
 1. match (map_prod id undual F'_iter) \<union> X \<subseteq> XH_largest ds X
[PROOF STEP]
by (simp add: less_eq_prod_def le_infI2 less_eq_dual_def)
[PROOF STATE]
proof (state)
this:
match (map_prod id undual F'_iter) \<union> X \<subseteq> XH_largest ds X

goal (1 subgoal):
 1. x \<in> Ch h (match (map_prod id undual F'_iter) \<union> X)
[PROOF STEP]
with assms Ch_range \<open>stable_on ds X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> Ch h X
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
stable_on ds X
match (map_prod id undual F'_iter) \<union> X \<subseteq> XH_largest ds X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> Ch h X
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}
stable_on ds X
match (map_prod id undual F'_iter) \<union> X \<subseteq> XH_largest ds X

goal (1 subgoal):
 1. x \<in> Ch h (match (map_prod id undual F'_iter) \<union> X)
[PROOF STEP]
by - (rule iia_onD[OF Ch_iia, where B="XH_largest ds X"], auto, metis Ch_CH_irc_idem CH_XH_largest)
[PROOF STATE]
proof (state)
this:
x \<in> Ch h (match (map_prod id undual F'_iter) \<union> X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cd_XD_gfp_F_card:
  assumes "d \<in> ds"
  shows "card (Cd d (fst XD_XH)) \<le> card (Cd d (fst (gfp_F ds)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (Cd d (fst XD_XH)) \<le> card (Cd d (fst (gfp_F ds)))
[PROOF STEP]
using %invisible assms Cd_lad XD_XH_gfp_F(1)[OF \<open>stable_pair_on ds XD_XH\<close>]
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
lad_on ?X (Cd ?d)
fst XD_XH \<subseteq> fst (gfp_F ds)

goal (1 subgoal):
 1. card (Cd d (fst XD_XH)) \<le> card (Cd d (fst (gfp_F ds)))
[PROOF STEP]
unfolding lad_on_def
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
\<forall>B\<subseteq>?X. \<forall>C\<subseteq>B. card (Cd ?d C) \<le> card (Cd ?d B)
fst XD_XH \<subseteq> fst (gfp_F ds)

goal (1 subgoal):
 1. card (Cd d (fst XD_XH)) \<le> card (Cd d (fst (gfp_F ds)))
[PROOF STEP]
by blast


[STATEMENT]
lemma Ch_gfp_F_XH_card:
  shows "card (Ch h (snd (gfp_F ds))) \<le> card (Ch h (snd XD_XH))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (Ch h (snd (gfp_F ds))) \<le> card (Ch h (snd XD_XH))
[PROOF STEP]
using %invisible Ch_lad XD_XH_gfp_F(2)[OF \<open>stable_pair_on ds XD_XH\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>h. lad (Ch h)
snd (gfp_F ds) \<subseteq> snd XD_XH

goal (1 subgoal):
 1. card (Ch h (snd (gfp_F ds))) \<le> card (Ch h (snd XD_XH))
[PROOF STEP]
unfolding lad_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h B. B \<subseteq> UNIV \<longrightarrow> (\<forall>C\<subseteq>B. card (Ch h C) \<le> card (Ch h B))
snd (gfp_F ds) \<subseteq> snd XD_XH

goal (1 subgoal):
 1. card (Ch h (snd (gfp_F ds))) \<le> card (Ch h (snd XD_XH))
[PROOF STEP]
by blast


[STATEMENT]
theorem Theorem_8:
  shows "d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))"
    and "card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))) &&& card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
proof %invisible -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
let ?Sum_Cd_gfp = "\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
let ?Sum_Ch_gfp = "\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
let ?Sum_Cd_XD = "\<Sum>d\<in>ds. card (Cd d (fst XD_XH))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
let ?Sum_Ch_XH = "\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "?Sum_Cd_gfp = ?Sum_Ch_gfp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
[PROOF STEP]
using stable_pair_on_CD_on_CH[OF gfp_F_stable_pair_on] CD_on_card[symmetric] CH_card[symmetric]
[PROOF STATE]
proof (prove)
using this:
CD_on ?ds (fst (gfp_F ?ds)) = CH (snd (gfp_F ?ds))
(\<Sum>d\<in>?ds. card (Cd d ?X)) = card (CD_on ?ds ?X)
(\<Sum>h\<in>UNIV. card (Ch h ?X)) = card (CH ?X)

goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "\<dots> \<le> ?Sum_Ch_XH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))
[PROOF STEP]
using Ch_gfp_F_XH_card
[PROOF STATE]
proof (prove)
using this:
card (Ch ?h (snd (gfp_F ds))) \<le> card (Ch ?h (snd XD_XH))

goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))
[PROOF STEP]
by (simp add: sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "\<dots> = ?Sum_Cd_XD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
[PROOF STEP]
using stable_pair_on_CD_on_CH[OF \<open>stable_pair_on ds XD_XH\<close>] CD_on_card[symmetric] CH_card[symmetric]
[PROOF STATE]
proof (prove)
using this:
CD_on ds (fst XD_XH) = CH (snd XD_XH)
(\<Sum>d\<in>?ds. card (Cd d ?X)) = card (CD_on ?ds ?X)
(\<Sum>h\<in>UNIV. card (Ch h ?X)) = card (CH ?X)

goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
[PROOF STEP]
have "?Sum_Cd_XD = ?Sum_Cd_gfp"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))

goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))
[PROOF STEP]
using Cd_XD_gfp_F_card
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
?d \<in> ds \<Longrightarrow> card (Cd ?d (fst XD_XH)) \<le> card (Cd ?d (fst (gfp_F ds)))

goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))
[PROOF STEP]
by (simp add: eq_iff sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))

goal (2 subgoals):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
 2. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
with Cd_XD_gfp_F_card
[PROOF STATE]
proof (chain)
picking this:
?d \<in> ds \<Longrightarrow> card (Cd ?d (fst XD_XH)) \<le> card (Cd ?d (fst (gfp_F ds)))
(\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))
[PROOF STEP]
show "d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))"
[PROOF STATE]
proof (prove)
using this:
?d \<in> ds \<Longrightarrow> card (Cd ?d (fst XD_XH)) \<le> card (Cd ?d (fst (gfp_F ds)))
(\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))

goal (1 subgoal):
 1. d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))
[PROOF STEP]
by (fastforce elim: sum_mono_inv)
[PROOF STATE]
proof (state)
this:
d \<in> ds \<Longrightarrow> card (Cd d (fst XD_XH)) = card (Cd d (fst (gfp_F ds)))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "?Sum_Ch_XH = ?Sum_Cd_XD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
[PROOF STEP]
using stable_pair_on_CD_on_CH[OF \<open>stable_pair_on ds XD_XH\<close>] CD_on_card[symmetric] CH_card[symmetric]
[PROOF STATE]
proof (prove)
using this:
CD_on ds (fst XD_XH) = CH (snd XD_XH)
(\<Sum>d\<in>?ds. card (Cd d ?X)) = card (CD_on ?ds ?X)
(\<Sum>h\<in>UNIV. card (Ch h ?X)) = card (CH ?X)

goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) = (\<Sum>d\<in>ds. card (Cd d (fst XD_XH)))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "\<dots> \<le> ?Sum_Cd_gfp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))
[PROOF STEP]
using Cd_XD_gfp_F_card
[PROOF STATE]
proof (prove)
using this:
?d \<in> ds \<Longrightarrow> card (Cd ?d (fst XD_XH)) \<le> card (Cd ?d (fst (gfp_F ds)))

goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))
[PROOF STEP]
by (simp add: sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst XD_XH))) \<le> (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds))))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
have "\<dots> = ?Sum_Ch_gfp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
[PROOF STEP]
using stable_pair_on_CD_on_CH[OF gfp_F_stable_pair_on] CD_on_card[symmetric] CH_card[symmetric]
[PROOF STATE]
proof (prove)
using this:
CD_on ?ds (fst (gfp_F ?ds)) = CH (snd (gfp_F ?ds))
(\<Sum>d\<in>?ds. card (Cd d ?X)) = card (CD_on ?ds ?X)
(\<Sum>h\<in>UNIV. card (Ch h ?X)) = card (CH ?X)

goal (1 subgoal):
 1. (\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>ds. card (Cd d (fst (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
[PROOF STEP]
have "?Sum_Ch_gfp = ?Sum_Ch_XH"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))

goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))
[PROOF STEP]
using Ch_gfp_F_XH_card
[PROOF STATE]
proof (prove)
using this:
(\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH))) \<le> (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds))))
card (Ch ?h (snd (gfp_F ds))) \<le> card (Ch ?h (snd XD_XH))

goal (1 subgoal):
 1. (\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))
[PROOF STEP]
by (simp add: eq_iff sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
with Ch_gfp_F_XH_card
[PROOF STATE]
proof (chain)
picking this:
card (Ch ?h (snd (gfp_F ds))) \<le> card (Ch ?h (snd XD_XH))
(\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))
[PROOF STEP]
show "card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))"
[PROOF STATE]
proof (prove)
using this:
card (Ch ?h (snd (gfp_F ds))) \<le> card (Ch ?h (snd XD_XH))
(\<Sum>h\<in>UNIV. card (Ch h (snd (gfp_F ds)))) = (\<Sum>h\<in>UNIV. card (Ch h (snd XD_XH)))

goal (1 subgoal):
 1. card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))
[PROOF STEP]
by (fastforce elim: sym[OF sum_mono_inv])
[PROOF STATE]
proof (state)
this:
card (Ch h (snd XD_XH)) = card (Ch h (snd (gfp_F ds)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ContractsWithSubstitutesAndIRC) Theorem_9_counterexample:
  assumes "stable_on ds Y"
  assumes "stable_on ds Z"
  shows "card (Ch h Y) = card (Ch h Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (Ch h Y) = card (Ch h Z)
[PROOF STEP]
oops


[STATEMENT]
lemma X3_UNIV:
  shows "UNIV = set [Xd1, Xd1', Xd2]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = set [X3.Xd1, X3.Xd1', X3.Xd2]
[PROOF STEP]
using X3.exhaust
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y = X3.Xd1 \<Longrightarrow> ?P; ?y = X3.Xd1' \<Longrightarrow> ?P; ?y = X3.Xd2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. UNIV = set [X3.Xd1, X3.Xd1', X3.Xd2]
[PROOF STEP]
by auto


[STATEMENT]
lemma X3_all_pow:
  shows "(\<forall>X''. P X'') \<longleftrightarrow> (\<forall>X''\<in>set ` set (subseqs [Xd1, Xd1', Xd2]). P X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>X''. P X'') = (\<forall>X''\<in>set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]). P X'')
[PROOF STEP]
using X3_pow
[PROOF STATE]
proof (prove)
using this:
?X \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2])

goal (1 subgoal):
 1. (\<forall>X''. P X'') = (\<forall>X''\<in>set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]). P X'')
[PROOF STEP]
by blast


[STATEMENT]
lemma PX3d_linear:
  shows "Linear_order (PX3d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (PX3d d)
[PROOF STEP]
by (cases d) (simp_all add: linord_of_list_Linear_order)


[STATEMENT]
lemma PX3d_range:
  shows "Field (PX3d d) \<subseteq> {x. X3d x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (PX3d d) \<subseteq> {x. X3d x = d}
[PROOF STEP]
by (cases d) simp_all


[STATEMENT]
lemma CX3h_range:
  shows "CX3h h X \<subseteq> {x\<in>X. X3h x = h}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CX3h h X \<subseteq> {x \<in> X. H = h}
[PROOF STEP]
by (cases "(h, X)" rule: CX3h.cases; simp; metis (mono_tags) H1.exhaust)


[STATEMENT]
lemma CX3h_singular:
  shows "inj_on X3d (CX3h h X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on X3d (CX3h h X)
[PROOF STEP]
by (cases "(h, X)" rule: CX3h.cases) auto


[STATEMENT]
lemma CX3h_substitutes:
  shows "substitutes (CX3h h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. substitutes (CX3h h)
[PROOF STEP]
apply (rule substitutes_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B)\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
[PROOF STEP]
apply (cut_tac X=B in X3_pow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2])\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
[PROOF STEP]
apply (case_tac b)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 2. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1'\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 3. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd2\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
[PROOF STEP]
apply (case_tac [!] a)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1; a = X3.Xd1\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 2. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1; a = X3.Xd1'\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 3. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1; a = X3.Xd2\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 4. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1'; a = X3.Xd1\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 5. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1'; a = X3.Xd1'\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 6. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd1'; a = X3.Xd2\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 7. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd2; a = X3.Xd1\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 8. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd2; a = X3.Xd1'\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
 9. \<And>B a b. \<lbrakk>B \<subseteq> UNIV; a \<in> UNIV; b \<in> UNIV; b \<notin> CX3h h (insert b B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); b = X3.Xd2; a = X3.Xd2\<rbrakk> \<Longrightarrow> b \<notin> CX3h h (insert a (insert b B))
[PROOF STEP]
apply (auto simp: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma CX3h_irc:
  shows "irc (CX3h h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irc (CX3h h)
[PROOF STEP]
apply (rule ircI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a. a \<notin> CX3h h (insert a B) \<Longrightarrow> CX3h h (insert a B) = CX3h h B
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a. \<lbrakk>a \<notin> CX3h h (insert a B); h = H\<rbrakk> \<Longrightarrow> CX3h h (insert a B) = CX3h h B
[PROOF STEP]
apply (cut_tac X=B in X3_pow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B a. \<lbrakk>a \<notin> CX3h h (insert a B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2])\<rbrakk> \<Longrightarrow> CX3h h (insert a B) = CX3h h B
[PROOF STEP]
apply (case_tac a)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>B a. \<lbrakk>a \<notin> CX3h h (insert a B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); a = X3.Xd1\<rbrakk> \<Longrightarrow> CX3h h (insert a B) = CX3h h B
 2. \<And>B a. \<lbrakk>a \<notin> CX3h h (insert a B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); a = X3.Xd1'\<rbrakk> \<Longrightarrow> CX3h h (insert a B) = CX3h h B
 3. \<And>B a. \<lbrakk>a \<notin> CX3h h (insert a B); h = H; B \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2]); a = X3.Xd2\<rbrakk> \<Longrightarrow> CX3h h (insert a B) = CX3h h B
[PROOF STEP]
apply (auto simp: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Theorem_9_stable_Xd1':
  shows "Theorem_9.stable_on UNIV {Xd1'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.stable_on UNIV {X3.Xd1'}
[PROOF STEP]
proof %invisible (rule Theorem_9.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1'}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
note image_cong_simp [cong del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N =simp=> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1'}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
note INF_cong_simp [cong]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B =simp=> ?C x = ?D x\<rbrakk> \<Longrightarrow> Inf (?C ` ?A) = Inf (?D ` ?B)

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1'}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
note SUP_cong_simp [cong]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B =simp=> ?C x = ?D x\<rbrakk> \<Longrightarrow> Sup (?C ` ?A) = Sup (?D ` ?B)

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1'}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
show "Theorem_9.individually_rational_on UNIV {Xd1'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1'}
[PROOF STEP]
by (rule Theorem_9.individually_rational_onI)
       (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.CH_def)
[PROOF STATE]
proof (state)
this:
Theorem_9.individually_rational_on UNIV {X3.Xd1'}

goal (1 subgoal):
 1. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
show "Theorem_9.stable_no_blocking_on UNIV {Xd1'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}
[PROOF STEP]
apply (rule Theorem_9.stable_no_blocking_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1'} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1'}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1'} \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1'} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1'}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1'} \<union> X''); h = H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac X=X'' in X3_pow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1'} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1'}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1'} \<union> X''); h = H; X'' \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h H (insert X3.Xd1' X''); X'' \<noteq> {X3.Xd1'}; X'' \<subseteq> Theorem_9.CD_on UNIV (insert X3.Xd1' X''); h = H; X'' = {X3.Xd1, X3.Xd1', X3.Xd2} \<or> X'' = {X3.Xd1, X3.Xd1'} \<or> X'' = {X3.Xd1, X3.Xd2} \<or> X'' = {X3.Xd1} \<or> X'' = {X3.Xd1', X3.Xd2} \<or> X'' = {X3.Xd2} \<or> X'' = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd1', X3.Xd2}; {X3.Xd1, X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd1', X3.Xd2}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd1'
 2. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd1', X3.Xd2}; {X3.Xd1, X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd1', X3.Xd2}; \<not> False; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1'
 3. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1'} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd1'}; {X3.Xd1, X3.Xd1'} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd1'}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd1'
 4. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd2}; {X3.Xd1, X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd2}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd1'
 5. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd2}; {X3.Xd1, X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd2}; \<not> False; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1'
 6. \<And>h X'' x. \<lbrakk>{X3.Xd1} = CX3h H {X3.Xd1', X3.Xd1}; {X3.Xd1} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd1'
 7. \<And>h X'' x. \<lbrakk>{X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1', X3.Xd2}; {X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1', X3.Xd2}; \<not> False; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1'
 8. \<And>h X'' x. \<lbrakk>{X3.Xd2} = CX3h H {X3.Xd1', X3.Xd2}; {X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd2}; \<not> False; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1'
 9. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd2} = CX3h H {X3.Xd1', X3.Xd1, X3.Xd2}; {X3.Xd1, X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1, X3.Xd2}; \<not> False; X3.Xd1' \<noteq> X3.Xd1; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd2
 10. \<And>h X'' x. \<lbrakk>{X3.Xd1} = CX3h H {X3.Xd1', X3.Xd1}; {X3.Xd1} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1', X3.Xd1}; \<not> False; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd1
A total of 12 subgoals...
[PROOF STEP]
apply (simp_all add: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Theorem_9.stable_no_blocking_on UNIV {X3.Xd1'}

goal:
No subgoals!
[PROOF STEP]
qed