[STATEMENT]
theorem Theorem_1:
  shows "\<not>(mechanism_stable ds \<phi> \<and> nonbossy ds \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (Bossy''.mechanism_stable ds \<phi> \<and> Bossy''.nonbossy ds \<phi>)
[PROOF STEP]
proof(rule notI, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume S: "Bossy.mechanism_stable ds \<phi>"
[PROOF STATE]
proof (state)
this:
Bossy''.mechanism_stable ds \<phi>

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume NB: "Bossy.nonbossy ds \<phi>"
[PROOF STATE]
proof (state)
this:
Bossy''.nonbossy ds \<phi>

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from S Bossy'_stable BPd'_BCh_mechanism_domain
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh
[PROOF STEP]
consider (A) "\<phi> BPd' BCh ds = {d1h3, d3h1}" | (B) "\<phi> BPd' BCh ds = {d1h1, d3h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh

goal (1 subgoal):
 1. \<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh

goal (1 subgoal):
 1. \<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
case A
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh ds = {d1h3, d3h1}

goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
from S BPd_BCh_mechanism_domain Bossy_stable
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})
[PROOF STEP]
have "\<phi> BPd BCh ds = {d1h1, d3h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})

goal (1 subgoal):
 1. \<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})

goal (1 subgoal):
 1. \<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> BPd BCh ds = {d1h1, d3h3}

goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
with Xd_xs ds xs dset A
[PROOF STATE]
proof (chain)
picking this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}

goal (1 subgoal):
 1. False
[PROOF STEP]
using nonbossy_Pd[OF NB BPd_BCh_mechanism_domain BPd'_BCh_mechanism_domain[unfolded BPd'_def]]
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
\<lbrakk>Bossy''.dX (\<phi> BPd BCh ds) (Xd d2h1) = Bossy''.dX (\<phi> (BPd(Xd d2h1 := {})) BCh ds) (Xd d2h1); Xd d2h1 \<in> ds\<rbrakk> \<Longrightarrow> \<phi> BPd BCh ds = \<phi> (BPd(Xd d2h1 := {})) BCh ds

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding BPd'_def[symmetric] dX_def
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
\<lbrakk>{x \<in> \<phi> BPd BCh ds. Xd x = Xd d2h1} = {x \<in> \<phi> BPd' BCh ds. Xd x = Xd d2h1}; Xd d2h1 \<in> ds\<rbrakk> \<Longrightarrow> \<phi> BPd BCh ds = \<phi> BPd' BCh ds

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

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
case B
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh ds = {d1h1, d3h3}

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
from S BPd'_BCh'_mechanism_domain Bossy''_stable
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})
[PROOF STEP]
have "\<phi> BPd' BCh' ds = {d3h1, d1h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})

goal (1 subgoal):
 1. \<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})

goal (1 subgoal):
 1. \<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh' ds = {d3h1, d1h3}

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
with Xh_xs hs xs dset B
[PROOF STATE]
proof (chain)
picking this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}

goal (1 subgoal):
 1. False
[PROOF STEP]
using nonbossy_Ch[OF NB BPd'_BCh_mechanism_domain BPd'_BCh'_mechanism_domain[unfolded BCh'_def]]
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
Bossy''.hX (\<phi> BPd' BCh ds) (Xh d1h2) = Bossy''.hX (\<phi> BPd' (BCh(Xh d1h2 := \<lambda>X. set_option (find (\<lambda>x. x \<in> X) [d1h2, d2h2, d3h2]))) ds) (Xh d1h2) \<Longrightarrow> \<phi> BPd' BCh ds = \<phi> BPd' (BCh(Xh d1h2 := \<lambda>X. set_option (find (\<lambda>x. x \<in> X) [d1h2, d2h2, d3h2]))) ds

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding BCh'_def[symmetric] hX_def
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
{x \<in> \<phi> BPd' BCh ds. Xh x = Xh d1h2} = {x \<in> \<phi> BPd' BCh' ds. Xh x = Xh d1h2} \<Longrightarrow> \<phi> BPd' BCh ds = \<phi> BPd' BCh' ds

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

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

goal:
No subgoals!
[PROOF STEP]
qed