[STATEMENT]
theorem type_preservation:
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>T t : T \<Longrightarrow> t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>T s : T"
  "\<Gamma>, \<Delta> \<turnstile>\<^sub>C c \<Longrightarrow> c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma>, \<Delta> \<turnstile>\<^sub>C d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T) &&& (\<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>C c; c \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d)
[PROOF STEP]
proof(induct arbitrary: s and d rule: typing_trm_typing_cmd.inducts)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s sa. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>sa. s \<longlonglongrightarrow> sa \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T sa : T1; t \<degree> s \<longlonglongrightarrow> sa\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T sa : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 5. \<And>\<Gamma> \<Delta> t T x d. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T; \<Delta> x = T; <x>t \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
case (app \<Gamma> \<Delta> t T1 T2 s s')
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1 \<rightarrow> T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1
s \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1
t \<degree> s \<longlonglongrightarrow> s'

goal (5 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> \<Delta> t T1 T2 s sa. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>sa. s \<longlonglongrightarrow> sa \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T sa : T1; t \<degree> s \<longlonglongrightarrow> sa\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T sa : T2
 3. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 4. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 5. \<And>\<Gamma> \<Delta> t T x d. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T; \<Delta> x = T; <x>t \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1 \<rightarrow> T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1
s \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1
t \<degree> s \<longlonglongrightarrow> s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1 \<rightarrow> T2
\<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1
s \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T1
t \<degree> s \<longlonglongrightarrow> s'

goal (1 subgoal):
 1. \<Gamma> , \<Delta> \<turnstile>\<^sub>T s' : T2
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t \<degree> s \<longlonglongrightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s' : T2
[PROOF STEP]
apply (erule redE; clarsimp simp: subst_type(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C
 2. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = u \<degree> s; t \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T u \<degree> s : T2
 3. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = t \<degree> u; s \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t \<degree> u : T2
[PROOF STEP]
apply (subgoal_tac "\<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>(T1\<rightarrow>T2) : c) : T2")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c; \<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>T1 \<rightarrow> T2:c) : T2\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C
 2. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>T1 \<rightarrow> T2:c) : T2
 3. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = u \<degree> s; t \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T u \<degree> s : T2
 4. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = t \<degree> u; s \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t \<degree> u : T2
[PROOF STEP]
apply (drule typing_ctxt_correct1, clarsimp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C
 2. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>T1 \<rightarrow> T2:c) : T2
 3. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = u \<degree> s; t \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T u \<degree> s : T2
 4. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = t \<degree> u; s \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t \<degree> u : T2
[PROOF STEP]
apply (subgoal_tac "\<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 (liftM_ctxt (\<diamond> \<^sup>\<bullet> s) 0)]\<^sup>C")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c; \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 liftM_ctxt (\<diamond> \<^sup>\<bullet> s) 0]\<^sup>C\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C
 2. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T2\<rangle> \<turnstile>\<^sub>C c[0=0 liftM_ctxt (\<diamond> \<^sup>\<bullet> s) 0]\<^sup>C
 3. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>T1 \<rightarrow> T2:c) : T2
 4. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = u \<degree> s; t \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T u \<degree> s : T2
 5. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = t \<degree> u; s \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t \<degree> u : T2
[PROOF STEP]
apply (clarsimp, rule struct_subst_type_command)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>1.44 c T1a \<turnstile>\<^sub>C c
 2. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> \<^sup>\<bullet> s : T2 \<Leftarrow> ?T1.44 c T1a
 3. \<And>c T1a. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta> \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t \<diamond> : T1a \<rightarrow> T2 \<Leftarrow> T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1a; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> ?\<Delta>1.44 c T1a = \<Delta>\<langle>0:?T1.44 c T1a\<rangle>
 4. \<And>c. \<lbrakk>\<And>s. \<mu>T1 \<rightarrow> T2:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; t = \<mu>T1 \<rightarrow> T2:c; s' = \<mu>T2:c[0=0 \<diamond> \<^sup>\<bullet> liftM_trm s 0]\<^sup>C; \<Gamma> , \<Delta>\<langle>0:T1 \<rightarrow> T2\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ctxt_subst (\<diamond> \<^sup>\<bullet> s) (\<mu>T1 \<rightarrow> T2:c) : T2
 5. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = u \<degree> s; t \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T u \<degree> s : T2
 6. \<And>u. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T1 \<rightarrow> T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2; \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; \<And>s. s \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1; s' = t \<degree> u; s \<longlonglongrightarrow> u\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T t \<degree> u : T2
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T s' : T2

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 3. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 4. \<And>\<Gamma> \<Delta> t T x d. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T; \<Delta> x = T; <x>t \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 3. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 4. \<And>\<Gamma> \<Delta> t T x d. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T; \<Delta> x = T; <x>t \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
case (passivate \<Gamma> \<Delta> t T x)
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T
\<Delta> x = T
<x>t \<^sub>C\<longlonglongrightarrow> d

goal (4 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 3. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 4. \<And>\<Gamma> \<Delta> t T x d. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T; \<Delta> x = T; <x>t \<^sub>C\<longlonglongrightarrow> d\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T
\<Delta> x = T
<x>t \<^sub>C\<longlonglongrightarrow> d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : T
t \<longlonglongrightarrow> ?s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T ?s : T
\<Delta> x = T
<x>t \<^sub>C\<longlonglongrightarrow> d

goal (1 subgoal):
 1. \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : \<Delta> x; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; <x>t \<^sub>C\<longlonglongrightarrow> d; T = \<Delta> x\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
apply (erule redE, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>\<And>s. \<mu>\<Delta> x:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; t = \<mu>\<Delta> x:c; d = dropM_cmd (c[0=x \<diamond>]\<^sup>C) x; \<Gamma> , \<Delta>\<langle>0:\<Delta> x\<rangle> \<turnstile>\<^sub>C c\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd (c[0=x \<diamond>]\<^sup>C) x
 2. \<And>s. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : \<Delta> x; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; d = <x>s; t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
apply (drule struct_subst_type_command [where \<beta> = x])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c. \<lbrakk>\<And>s. \<mu>\<Delta> x:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; t = \<mu>\<Delta> x:c; d = dropM_cmd (c[0=x \<diamond>]\<^sup>C) x\<rbrakk> \<Longrightarrow> \<Gamma> , ?\<Delta>15 c \<turnstile>\<^sub>c\<^sub>t\<^sub>x\<^sub>t ?E15 c : ?U15 c \<Leftarrow> ?T1.15 c
 2. \<And>c. \<lbrakk>\<And>s. \<mu>\<Delta> x:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; t = \<mu>\<Delta> x:c; d = dropM_cmd (c[0=x \<diamond>]\<^sup>C) x\<rbrakk> \<Longrightarrow> \<Delta>\<langle>0:\<Delta> x\<rangle> = ?\<Delta>15 c\<langle>?\<alpha>15 c:?T1.15 c\<rangle>
 3. \<And>c. \<lbrakk>\<And>s. \<mu>\<Delta> x:c \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; t = \<mu>\<Delta> x:c; d = dropM_cmd (c[0=x \<diamond>]\<^sup>C) x; \<Gamma> , ?\<Delta>15 c\<langle>x:?U15 c\<rangle> \<turnstile>\<^sub>C c[?\<alpha>15 c=x liftM_ctxt (?E15 c) x]\<^sup>C\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C dropM_cmd (c[0=x \<diamond>]\<^sup>C) x
 4. \<And>s. \<lbrakk>\<Gamma> , \<Delta> \<turnstile>\<^sub>T t : \<Delta> x; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : \<Delta> x; T = \<Delta> x; d = <x>s; t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>C d
[PROOF STEP]
apply (fastforce simp: dropM_env(2))+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma> , \<Delta> \<turnstile>\<^sub>C d

goal (3 subgoals):
 1. \<And>\<Gamma> x T \<Delta> s. \<lbrakk>\<Gamma> x = T; `x \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
 2. \<And>\<Gamma> T1 \<Delta> t T2 s. \<lbrakk>\<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T t : T2; \<And>s. t \<longlonglongrightarrow> s \<Longrightarrow> \<Gamma>\<langle>0:T1\<rangle> , \<Delta> \<turnstile>\<^sub>T s : T2; \<lambda>T1:t \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T1 \<rightarrow> T2
 3. \<And>\<Gamma> \<Delta> T c s. \<lbrakk>\<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C c; \<And>d. c \<^sub>C\<longlonglongrightarrow> d \<Longrightarrow> \<Gamma> , \<Delta>\<langle>0:T\<rangle> \<turnstile>\<^sub>C d; \<mu>T:c \<longlonglongrightarrow> s\<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile>\<^sub>T s : T
[PROOF STEP]
qed (force simp: dropM_type)+


[STATEMENT]
lemma Pd_refl:
  assumes "x \<in> Field (Pd d)"
  shows "(x, x) \<in> Pd d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, x) \<in> Pd d
[PROOF STEP]
using assms Pd_linear'
[PROOF STATE]
proof (prove)
using this:
x \<in> Field (Pd d)
Linear_order (Pd ?d)

goal (1 subgoal):
 1. (x, x) \<in> Pd d
[PROOF STEP]
by (meson subset_refl underS_incl_iff)


[STATEMENT]
lemma Pd_Xd:
  assumes "(x, y) \<in> Pd d"
  shows "Xd x = d \<and> Xd y = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x = d \<and> Xd y = d
[PROOF STEP]
using assms Pd_range contra_subsetD
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> Pd d
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?c \<notin> ?A

goal (1 subgoal):
 1. Xd x = d \<and> Xd y = d
[PROOF STEP]
unfolding Field_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> Pd d
\<forall>d. Domain (Pd d) \<union> Range (Pd d) \<subseteq> {x. Xd x = d}
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?c \<notin> ?A

goal (1 subgoal):
 1. Xd x = d \<and> Xd y = d
[PROOF STEP]
by blast


[STATEMENT]
lemma Above_Pd_Xd:
  assumes "x \<in> Above (Pd d) X"
  shows "Xd x = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Above (Pd d) X

goal (1 subgoal):
 1. Xd x = d
[PROOF STEP]
by (blast dest: Above_Field Pd_range')


[STATEMENT]
lemma AboveS_Pd_Xd:
  assumes "x \<in> AboveS (Pd d) X"
  shows "Xd x = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> AboveS (Pd d) X

goal (1 subgoal):
 1. Xd x = d
[PROOF STEP]
by (blast dest: AboveS_Field Pd_range')


[STATEMENT]
lemma Cd_Xd:
  shows "x \<in> Cd d X \<Longrightarrow> Xd x = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Cd d X \<Longrightarrow> Xd x = d
[PROOF STEP]
using Pd_range Cd_range
[PROOF STATE]
proof (prove)
using this:
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)

goal (1 subgoal):
 1. x \<in> Cd d X \<Longrightarrow> Xd x = d
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Cd_inj_on_Xd:
  shows "inj_on Xd (Cd d X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd (Cd d X)
[PROOF STEP]
by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton)


[STATEMENT]
lemma Cd_range_disjoint:
  assumes "d \<noteq> d'"
  shows "Cd d A \<inter> Cd d' A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d A \<inter> Cd d' A = {}
[PROOF STEP]
using assms Cd_range Pd_range
[PROOF STATE]
proof (prove)
using this:
d \<noteq> d'
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}

goal (1 subgoal):
 1. Cd d A \<inter> Cd d' A = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma Cd_single:
  assumes "x \<in> X"
  assumes "inj_on Xd X"
  assumes "x \<in> Field (Pd d)"
  shows "x \<in> Cd d X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Cd d X
[PROOF STEP]
using assms Pd_linear
[PROOF STATE]
proof (prove)
using this:
x \<in> X
inj_on Xd X
x \<in> Field (Pd d)
\<forall>d. Linear_order (Pd d)

goal (1 subgoal):
 1. x \<in> Cd d X
[PROOF STEP]
unfolding Cd_greatest greatest_def
[PROOF STATE]
proof (prove)
using this:
x \<in> X
inj_on Xd X
x \<in> Field (Pd d)
\<forall>d. Linear_order (Pd d)

goal (1 subgoal):
 1. x \<in> {x \<in> X \<inter> Field (Pd d). \<forall>y\<in>X \<inter> Field (Pd d). (y, x) \<in> Pd d}
[PROOF STEP]
by clarsimp (metis Pd_Xd inj_on_eq_iff subset_refl underS_incl_iff)


[STATEMENT]
lemma Cd_Above:
  shows "Cd d X = Above (Pd d) (X \<inter> Field (Pd d)) \<inter> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d X = Above (Pd d) (X \<inter> Field (Pd d)) \<inter> X
[PROOF STEP]
unfolding Cd_greatest greatest_Above Above_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b \<in> Field (Pd d). \<forall>a\<in>X \<inter> Field (Pd d). (a, b) \<in> Pd d} \<inter> (X \<inter> Field (Pd d)) = {b \<in> Field (Pd d). \<forall>a\<in>X \<inter> Field (Pd d). (a, b) \<in> Pd d} \<inter> X
[PROOF STEP]
by blast


[STATEMENT]
lemma MaxR_maxR:
  shows "MaxR.maxR (Pd d) = maxR d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MaxR.maxR (Pd d) = maxR d
[PROOF STEP]
by (simp add: fun_eq_iff maxR_def Cd.maxR_code)


[STATEMENT]
lemma MaxR_MaxR_f:
  shows "MaxR.MaxR_f (Pd d) = MaxR_f d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MaxR.MaxR_f (Pd d) = MaxR_f d
[PROOF STEP]
by (simp add: fun_eq_iff Cd.MaxR_f_code MaxR_f_def MaxR_maxR cong: option.case_cong)


[STATEMENT]
lemma Cd_simps[simp, nitpick_simp]:
  shows "Cd d {} = {}"
        "Cd d (insert x A) = (if x \<in> Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y \<in> Cd d A} else Cd d A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d {} = {} &&& Cd d (insert x A) = (if x \<in> Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y \<in> Cd d A} else Cd d A)
[PROOF STEP]
unfolding Cd.simps MaxR_maxR
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = {} &&& (if x \<in> Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y \<in> Cd d A} else Cd d A) = (if x \<in> Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y \<in> Cd d A} else Cd d A)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma CD_on_def2:
  shows "CD_on ds A = (\<Union>d\<in>ds. Cd d (A \<inter> Field (Pd d)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds A = (\<Union>d\<in>ds. Cd d (A \<inter> Field (Pd d)))
[PROOF STEP]
using Cd_domain
[PROOF STATE]
proof (prove)
using this:
Cd ?d (?X \<inter> Field (Pd ?d)) = Cd ?d ?X

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

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d A) = (\<Union>d\<in>ds. Cd d (A \<inter> Field (Pd d)))
[PROOF STEP]
by blast


[STATEMENT]
lemma CD_on_Xd:
  assumes "x \<in> CD_on ds A"
  shows "Xd x \<in> ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
using assms Cd_Xd
[PROOF STATE]
proof (prove)
using this:
x \<in> CD_on ds A
?x \<in> Cd ?d ?X \<Longrightarrow> Xd ?x = ?d

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

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


[STATEMENT]
lemma mem_CD_on_Cd:
  shows "x \<in> CD_on ds X \<longleftrightarrow> (x \<in> Cd (Xd x) X \<and> Xd x \<in> ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> CD_on ds X) = (x \<in> Cd (Xd x) X \<and> Xd x \<in> ds)
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> (\<Union>d\<in>ds. Cd d X)) = (x \<in> Cd (Xd x) X \<and> Xd x \<in> ds)
[PROOF STEP]
using Cd_range Cd_Xd
[PROOF STATE]
proof (prove)
using this:
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)
?x \<in> Cd ?d ?X \<Longrightarrow> Xd ?x = ?d

goal (1 subgoal):
 1. (x \<in> (\<Union>d\<in>ds. Cd d X)) = (x \<in> Cd (Xd x) X \<and> Xd x \<in> ds)
[PROOF STEP]
by blast


[STATEMENT]
lemma CD_on_domain:
  assumes "d \<in> ds"
  shows "CD_on ds A \<inter> Field (Pd d) = Cd d (A \<inter> Field (Pd d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds A \<inter> Field (Pd d) = Cd d (A \<inter> Field (Pd d))
[PROOF STEP]
unfolding CD_on_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d (A \<inter> Field (Pd d))) \<inter> Field (Pd d) = Cd d (A \<inter> Field (Pd d))
[PROOF STEP]
using assms Cd_range
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d (A \<inter> Field (Pd d))) \<inter> Field (Pd d) = Cd d (A \<inter> Field (Pd d))
[PROOF STEP]
by (force dest: Pd_range')


[STATEMENT]
lemma CD_on_range:
  shows "CD_on ds A \<subseteq> A \<inter> (\<Union>d\<in>ds. Field (Pd d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds A \<subseteq> A \<inter> (\<Union>d\<in>ds. Field (Pd d))
[PROOF STEP]
using Cd_range
[PROOF STATE]
proof (prove)
using this:
Cd ?d ?X \<subseteq> ?X \<inter> Field (Pd ?d)

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

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d A) \<subseteq> A \<inter> (\<Union>d\<in>ds. Field (Pd d))
[PROOF STEP]
by blast


[STATEMENT]
lemma CD_on_f_range_on:
  shows "f_range_on A (CD_on ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_range_on A (CD_on ds)
[PROOF STEP]
by (rule f_range_onI) (meson CD_on_range Int_subset_iff)


[STATEMENT]
lemma RD_on_mono:
  shows "mono (RD_on ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (Rf (CD_on ds))
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>X. X - (\<Union>d\<in>ds. Cd d X))
[PROOF STEP]
by (rule monoI) (auto dest: monoD[OF Rf_Cd_mono])


[STATEMENT]
lemma CD_on_Chernoff:
  shows "Chernoff (CD_on ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Chernoff (CD_on ds)
[PROOF STEP]
using mono_on_mono RD_on_mono[of ds] Rf_mono_on_iia_on[of UNIV] Chernoff_on_iia_on
[PROOF STATE]
proof (prove)
using this:
Basis.mono_on UNIV = mono
mono (Rf (CD_on ds))
Basis.mono_on (Pow UNIV) (Rf ?f) = iia ?f
Chernoff_on ?A ?f = iia_on ?A ?f

goal (1 subgoal):
 1. Chernoff (CD_on ds)
[PROOF STEP]
by (simp add: fun_eq_iff) blast


[STATEMENT]
lemma CD_on_irc:
  shows "irc (CD_on ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irc (CD_on ds)
[PROOF STEP]
by (rule ircI) (fastforce simp: CD_on_def ircD[OF Cd_irc] simp del: Cd_simps cong: SUP_cong)


[STATEMENT]
lemma CD_on_path_independent:
  shows "path_independent (\<lambda>X. CD_on ds X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_independent (CD_on ds)
[PROOF STEP]
using CD_on_f_range_on CD_on_Chernoff CD_on_consistency
[PROOF STATE]
proof (prove)
using this:
f_range_on ?A (CD_on ?ds)
Chernoff (CD_on ?ds)
consistency (CD_on ?ds)

goal (1 subgoal):
 1. path_independent (CD_on ds)
[PROOF STEP]
by (blast intro: path_independent_onI2)


[STATEMENT]
lemma CD_on_simps:
  shows "CD_on ds {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds {} = {}
[PROOF STEP]
using CD_on_range
[PROOF STATE]
proof (prove)
using this:
CD_on ?ds ?A \<subseteq> ?A \<inter> (\<Union>d\<in>?ds. Field (Pd d))

goal (1 subgoal):
 1. CD_on ds {} = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma CD_on_inj_on_Xd:
  shows "inj_on Xd (CD_on ds X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd (CD_on ds X)
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd (\<Union>d\<in>ds. Cd d X)
[PROOF STEP]
by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton)


[STATEMENT]
lemma CD_on_card:
  shows "card (CD_on ds X) = (\<Sum>d\<in>ds. card (Cd d X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (CD_on ds X) = (\<Sum>d\<in>ds. card (Cd d X))
[PROOF STEP]
unfolding CD_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>d\<in>ds. Cd d X) = (\<Sum>d\<in>ds. card (Cd d X))
[PROOF STEP]
by (simp add: card_UN_disjoint Cd_range_disjoint)


[STATEMENT]
lemma CD_on_closed:
  assumes "inj_on Xd X"
  assumes "X \<subseteq> (\<Union>d\<in>ds. Field (Pd d))"
  shows "CD_on ds X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds X = X
[PROOF STEP]
using assms Cd_domain Cd_single[OF _ assms(1)]
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X
X \<subseteq> (\<Union>d\<in>ds. Field (Pd d))
Cd ?d (?X \<inter> Field (Pd ?d)) = Cd ?d ?X
\<lbrakk>?x \<in> X; ?x \<in> Field (Pd ?d)\<rbrakk> \<Longrightarrow> ?x \<in> Cd ?d X

goal (1 subgoal):
 1. CD_on ds X = X
[PROOF STEP]
unfolding CD_on_def2
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X
X \<subseteq> (\<Union>d\<in>ds. Field (Pd d))
Cd ?d (?X \<inter> Field (Pd ?d)) = Cd ?d ?X
\<lbrakk>?x \<in> X; ?x \<in> Field (Pd ?d)\<rbrakk> \<Longrightarrow> ?x \<in> Cd ?d X

goal (1 subgoal):
 1. (\<Union>d\<in>ds. Cd d (X \<inter> Field (Pd d))) = X
[PROOF STEP]
by (force dest: Cd_range')


[STATEMENT]
lemma Ch_simps:
  shows "Ch h {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch 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. Ch h {} = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma Ch_range_disjoint:
  assumes "h \<noteq> h'"
  shows "Ch h A \<inter> Ch h' A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ch h A \<inter> Ch h' A = {}
[PROOF STEP]
using assms Ch_range
[PROOF STATE]
proof (prove)
using this:
h \<noteq> h'
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}

goal (1 subgoal):
 1. Ch h A \<inter> Ch h' A = {}
[PROOF STEP]
by blast


[STATEMENT]
lemma Ch_f_range:
  shows "f_range (Ch h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_range (Ch 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. f_range (Ch h)
[PROOF STEP]
unfolding f_range_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h X. Ch h X \<subseteq> {x \<in> X. Xh x = h}

goal (1 subgoal):
 1. \<forall>B\<subseteq>UNIV. Ch h B \<subseteq> B
[PROOF STEP]
by blast


[STATEMENT]
lemma CH_card:
  shows "card (CH X) = (\<Sum>h\<in>UNIV. card (Ch h X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (CH X) = (\<Sum>h\<in>UNIV. card (Ch h X))
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (\<Union>h. Ch h X) = (\<Sum>h\<in>UNIV. card (Ch h X))
[PROOF STEP]
by (simp add: card_UN_disjoint Ch_range_disjoint)


[STATEMENT]
lemma CH_simps:
  shows "CH {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH {} = {}
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h. Ch h {}) = {}
[PROOF STEP]
by (simp add: Ch_simps)


[STATEMENT]
lemma CH_range:
  shows "CH A \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH A \<subseteq> A
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h. Ch h A) \<subseteq> A
[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) \<subseteq> A
[PROOF STEP]
by blast


[STATEMENT]
lemma mem_CH_Ch:
  shows "x \<in> CH X \<longleftrightarrow> x \<in> Ch (Xh x) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> CH X) = (x \<in> Ch (Xh x) X)
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> (\<Union>h. Ch h X)) = (x \<in> Ch (Xh x) X)
[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. (x \<in> (\<Union>h. Ch h X)) = (x \<in> Ch (Xh x) X)
[PROOF STEP]
by blast


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

goal (1 subgoal):
 1. x \<in> (\<Union>h. Ch h X)
[PROOF STEP]
by blast


[STATEMENT]
lemma dX_union:
  shows "dX (X \<union> Y) d = dX X d \<union> dX Y d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dX (X \<union> Y) d = dX X d \<union> dX Y d
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> X \<union> Y. Xd x = d} = {x \<in> X. Xd x = d} \<union> {x \<in> Y. Xd x = d}
[PROOF STEP]
by auto


[STATEMENT]
lemma dX_range:
  shows "\<forall>d. dX X d \<subseteq> {x. Xd x = d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. dX X d \<subseteq> {x. Xd x = d}
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. {x \<in> X. Xd x = d} \<subseteq> {x. Xd x = d}
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma dX_range':
  assumes "x \<in> dX X d"
  shows "x \<in> X \<and> Xd x = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X \<and> Xd x = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> dX X d

goal (1 subgoal):
 1. x \<in> X \<and> Xd x = d
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> X. Xd x = d}

goal (1 subgoal):
 1. x \<in> X \<and> Xd x = d
[PROOF STEP]
by simp


[STATEMENT]
lemma dX_empty_or_singleton:
  assumes "allocation X"
  shows "\<forall>d. dX X d = {} \<or> (\<exists>x. dX X d = {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. dX X d = {} \<or> (\<exists>x. dX X d = {x})
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. {x \<in> X. Xd x = d} = {} \<or> (\<exists>x. {x \<in> X. Xd x = d} = {x})
[PROOF STEP]
using \<open>allocation X\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X

goal (1 subgoal):
 1. \<forall>d. {x \<in> X. Xd x = d} = {} \<or> (\<exists>x. {x \<in> X. Xd x = d} = {x})
[PROOF STEP]
by (fastforce dest: inj_onD)


[STATEMENT]
lemma dX_linear:
  assumes "allocation X"
  shows "Linear_order (dX X d \<times> dX X d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linear_order (dX X d \<times> dX X d)
[PROOF STEP]
using spec[OF dX_empty_or_singleton[OF \<open>allocation X\<close>], where x=d]
[PROOF STATE]
proof (prove)
using this:
dX X d = {} \<or> (\<exists>x. dX X d = {x})

goal (1 subgoal):
 1. Linear_order (dX X d \<times> dX X d)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dX_singular:
  assumes "allocation X"
  assumes "x \<in> X"
  assumes "d = Xd x"
  shows "dX X d = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dX X d = {x}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X
x \<in> X
d = Xd x

goal (1 subgoal):
 1. dX X d = {x}
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
using this:
inj_on Xd X
x \<in> X
d = Xd x

goal (1 subgoal):
 1. {x \<in> X. Xd x = d} = {x}
[PROOF STEP]
by (fastforce dest: inj_onD)


[STATEMENT]
lemma dX_Int_Field_Pd:
  assumes "dX X d \<subseteq> Field (Pd d)"
  shows "X \<inter> Field (Pd d) = dX X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<inter> Field (Pd d) = dX X d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dX X d \<subseteq> Field (Pd d)

goal (1 subgoal):
 1. X \<inter> Field (Pd d) = dX X d
[PROOF STEP]
unfolding dX_def
[PROOF STATE]
proof (prove)
using this:
{x \<in> X. Xd x = d} \<subseteq> Field (Pd d)

goal (1 subgoal):
 1. X \<inter> Field (Pd d) = {x \<in> X. Xd x = d}
[PROOF STEP]
by (fastforce dest: Pd_range')


[STATEMENT]
lemma Cd_Above_dX:
  assumes "dX X d \<subseteq> Field (Pd d)"
  shows "Cd d X = Above (Pd d) (dX X d) \<inter> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d X = Above (Pd d) (dX X d) \<inter> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dX X d \<subseteq> Field (Pd d)

goal (1 subgoal):
 1. Cd d X = Above (Pd d) (dX X d) \<inter> X
[PROOF STEP]
unfolding Cd_greatest greatest_Above Above_def dX_def
[PROOF STATE]
proof (prove)
using this:
{x \<in> X. Xd x = d} \<subseteq> Field (Pd d)

goal (1 subgoal):
 1. {b \<in> Field (Pd d). \<forall>a\<in>X \<inter> Field (Pd d). (a, b) \<in> Pd d} \<inter> (X \<inter> Field (Pd d)) = {b \<in> Field (Pd d). \<forall>a\<in>{x \<in> X. Xd x = d}. (a, b) \<in> Pd d} \<inter> X
[PROOF STEP]
by (auto dest: Pd_range')


[STATEMENT]
lemma stable_onI:
  assumes "individually_rational_on ds X"
  assumes "stable_no_blocking_on ds X"
  shows "stable_on ds X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_on ds X
[PROOF STEP]
unfolding stable_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. individually_rational_on ds X \<and> stable_no_blocking_on ds X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
individually_rational_on ds X
stable_no_blocking_on ds X

goal (1 subgoal):
 1. individually_rational_on ds X \<and> stable_no_blocking_on ds X
[PROOF STEP]
by blast


[STATEMENT]
lemma individually_rational_onI:
  assumes "CD_on ds X = X"
  assumes "CH X = X"
  shows "individually_rational_on ds X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. individually_rational_on ds X
[PROOF STEP]
unfolding individually_rational_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds X = X \<and> CH X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CD_on ds X = X
CH X = X

goal (1 subgoal):
 1. CD_on ds X = X \<and> CH X = X
[PROOF STEP]
by blast


[STATEMENT]
lemma individually_rational_on_CD_on:
  assumes "individually_rational_on ds X"
  shows "CD_on ds X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
individually_rational_on ds X

goal (1 subgoal):
 1. CD_on ds X = X
[PROOF STEP]
unfolding individually_rational_on_def
[PROOF STATE]
proof (prove)
using this:
CD_on ds X = X \<and> CH X = X

goal (1 subgoal):
 1. CD_on ds X = X
[PROOF STEP]
by blast


[STATEMENT]
lemma individually_rational_on_Cd:
  assumes "individually_rational_on ds X"
  shows "Cd d X = dX X d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d X = dX X d
[PROOF STEP]
using individually_rational_on_CD_on[OF assms]
[PROOF STATE]
proof (prove)
using this:
CD_on ds X = X

goal (1 subgoal):
 1. Cd d X = dX X d
[PROOF STEP]
by (auto simp: dX_def mem_CD_on_Cd dest: Cd_range' Cd_Xd)


[STATEMENT]
lemma individually_rational_on_empty:
  shows "individually_rational_on ds {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. individually_rational_on ds {}
[PROOF STEP]
by (simp add: CD_on_simps CH_simps individually_rational_onI)


[STATEMENT]
lemma blocking_onI:
  assumes "X'' \<noteq> Ch h X"
  assumes "X'' = Ch h (X \<union> X'')"
  assumes "\<And>x. x \<in> X'' \<Longrightarrow> x \<in> CD_on ds (X \<union> X'')"
  shows "blocking_on ds X h X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blocking_on ds X h X''
[PROOF STEP]
unfolding blocking_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X'' \<noteq> Ch h X \<and> X'' = Ch h (X \<union> X'') \<and> X'' \<subseteq> CD_on ds (X \<union> X'')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
X'' \<noteq> Ch h X
X'' = Ch h (X \<union> X'')
?x \<in> X'' \<Longrightarrow> ?x \<in> CD_on ds (X \<union> X'')

goal (1 subgoal):
 1. X'' \<noteq> Ch h X \<and> X'' = Ch h (X \<union> X'') \<and> X'' \<subseteq> CD_on ds (X \<union> X'')
[PROOF STEP]
by blast


[STATEMENT]
lemma blocking_on_imp_not_stable:
  assumes "blocking_on ds X h X''"
  shows "\<not>stable_on ds X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> stable_on ds X
[PROOF STEP]
unfolding stable_on_def stable_no_blocking_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (individually_rational_on ds X \<and> (\<forall>h X'. \<not> blocking_on ds X h X'))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''

goal (1 subgoal):
 1. \<not> (individually_rational_on ds X \<and> (\<forall>h X'. \<not> blocking_on ds X h X'))
[PROOF STEP]
by blast


[STATEMENT]
lemma blocking_on_allocation:
  assumes "blocking_on ds X h X''"
  shows "allocation X''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd X''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''

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

goal (1 subgoal):
 1. inj_on Xd X''
[PROOF STEP]
by (metis Ch_singular')


[STATEMENT]
lemma blocking_on_Field:
  assumes "blocking_on ds X h X''"
  shows "dX X'' d \<subseteq> Field (Pd d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dX X'' d \<subseteq> Field (Pd d)
[PROOF STEP]
using assms blocking_on_allocation[OF assms]
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''
inj_on Xd X''

goal (1 subgoal):
 1. dX X'' d \<subseteq> Field (Pd d)
[PROOF STEP]
unfolding blocking_on_def dX_def
[PROOF STATE]
proof (prove)
using this:
X'' \<noteq> Ch h X \<and> X'' = Ch h (X \<union> X'') \<and> X'' \<subseteq> CD_on ds (X \<union> X'')
inj_on Xd X''

goal (1 subgoal):
 1. {x \<in> X''. Xd x = d} \<subseteq> Field (Pd d)
[PROOF STEP]
by (force simp: Pd_range' dest: CD_on_range')


[STATEMENT]
lemma blocking_on_CD_on:
  assumes "blocking_on ds X h X''"
  shows "X'' \<subseteq> CD_on ds (X \<union> X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (X \<union> X'')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''

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

goal (1 subgoal):
 1. X'' \<subseteq> CD_on ds (X \<union> X'')
[PROOF STEP]
by blast


[STATEMENT]
lemma blocking_on_CD_on':
  assumes "blocking_on ds X h X''"
  assumes "x \<in> X''"
  shows "x \<in> CD_on ds (X \<union> X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''
x \<in> X''

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

goal (1 subgoal):
 1. x \<in> CD_on ds (X \<union> X'')
[PROOF STEP]
by blast


[STATEMENT]
lemma blocking_on_Cd:
  assumes "blocking_on ds X h X''"
  shows "dX X'' d \<subseteq> Cd d (X \<union> X'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dX X'' d \<subseteq> Cd d (X \<union> X'')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X h X''

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

goal (1 subgoal):
 1. dX X'' d \<subseteq> Cd d (X \<union> X'')
[PROOF STEP]
by (force dest: dX_range' simp: mem_CD_on_Cd)


[STATEMENT]
lemma stable_no_blocking_onI:
  assumes "\<And>h X''. \<lbrakk>X'' = Ch h (X \<union> X''); X'' \<noteq> Ch h X; X'' \<subseteq> CD_on ds (X \<union> X'')\<rbrakk> \<Longrightarrow> False"
  shows "stable_no_blocking_on ds X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds X
[PROOF STEP]
unfolding stable_no_blocking_on_def blocking_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h X'. \<not> (X' \<noteq> Ch h X \<and> X' = Ch h (X \<union> X') \<and> X' \<subseteq> CD_on ds (X \<union> X'))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X'' = Ch ?h (X \<union> ?X''); ?X'' \<noteq> Ch ?h X; ?X'' \<subseteq> CD_on ds (X \<union> ?X'')\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>h X'. \<not> (X' \<noteq> Ch h X \<and> X' = Ch h (X \<union> X') \<and> X' \<subseteq> CD_on ds (X \<union> X'))
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_no_blocking_onI2:
  assumes "\<And>h X''. blocking_on ds X h X'' \<Longrightarrow> False"
  shows "stable_no_blocking_on ds X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds X
[PROOF STEP]
unfolding stable_no_blocking_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h X'. \<not> blocking_on ds X h X'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
blocking_on ds X ?h ?X'' \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>h X'. \<not> blocking_on ds X h X'
[PROOF STEP]
by blast


[STATEMENT]
lemma "stable_no_blocking_on ds UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds UNIV
[PROOF STEP]
using stable_no_blocking_onI
[PROOF STATE]
proof (prove)
using this:
(\<And>h X''. \<lbrakk>X'' = Ch h (?X \<union> X''); X'' \<noteq> Ch h ?X; X'' \<subseteq> CD_on ?ds (?X \<union> X'')\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> stable_no_blocking_on ?ds ?X

goal (1 subgoal):
 1. stable_no_blocking_on ds UNIV
[PROOF STEP]
by fastforce


[STATEMENT]
lemma stable_on_allocation:
  assumes "stable_on ds X"
  shows "allocation X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stable_on ds X

goal (1 subgoal):
 1. inj_on Xd X
[PROOF STEP]
unfolding stable_on_def individually_rational_on_def
[PROOF STATE]
proof (prove)
using this:
(CD_on ds X = X \<and> CH X = X) \<and> stable_no_blocking_on ds X

goal (1 subgoal):
 1. inj_on Xd X
[PROOF STEP]
by (metis CD_on_inj_on_Xd)


[STATEMENT]
lemma stable_on_blocking_onD:
  assumes "stable_on ds X"
  shows "\<lbrakk>X'' = Ch h (X \<union> X''); X'' \<subseteq> CD_on ds (X \<union> X'')\<rbrakk> \<Longrightarrow> X'' = Ch h X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X'' = Ch h (X \<union> X''); X'' \<subseteq> CD_on ds (X \<union> X'')\<rbrakk> \<Longrightarrow> X'' = Ch h X
[PROOF STEP]
using \<open>stable_on ds X\<close>
[PROOF STATE]
proof (prove)
using this:
stable_on ds X

goal (1 subgoal):
 1. \<lbrakk>X'' = Ch h (X \<union> X''); X'' \<subseteq> CD_on ds (X \<union> X'')\<rbrakk> \<Longrightarrow> X'' = Ch h X
[PROOF STEP]
unfolding stable_on_def individually_rational_on_def stable_no_blocking_on_def blocking_on_def
[PROOF STATE]
proof (prove)
using this:
(CD_on ds X = X \<and> CH X = X) \<and> (\<forall>h X'. \<not> (X' \<noteq> Ch h X \<and> X' = Ch h (X \<union> X') \<and> X' \<subseteq> CD_on ds (X \<union> X')))

goal (1 subgoal):
 1. \<lbrakk>X'' = Ch h (X \<union> X''); X'' \<subseteq> CD_on ds (X \<union> X'')\<rbrakk> \<Longrightarrow> X'' = Ch h X
[PROOF STEP]
by blast


[STATEMENT]
lemma not_stable_on_cases[consumes 1, case_names not_individually_rational not_no_blocking]:
  assumes "\<not> stable_on ds X"
  assumes "\<not> individually_rational_on ds X \<Longrightarrow> P"
  assumes "\<not> stable_no_blocking_on ds X \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> stable_on ds X
\<not> individually_rational_on ds X \<Longrightarrow> P
\<not> stable_no_blocking_on ds X \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
unfolding stable_on_def
[PROOF STATE]
proof (prove)
using this:
\<not> (individually_rational_on ds X \<and> stable_no_blocking_on ds X)
\<not> individually_rational_on ds X \<Longrightarrow> P
\<not> stable_no_blocking_on ds X \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_CD_on:
  assumes "stable_pair_on ds XD_XH"
  shows "match XD_XH = CD_on ds (fst XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match XD_XH = CD_on ds (fst XD_XH)
[PROOF STEP]
using %invisible assms CD_on_range
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
CD_on ?ds ?A \<subseteq> ?A \<inter> (\<Union>d\<in>?ds. Field (Pd d))

goal (1 subgoal):
 1. match XD_XH = CD_on ds (fst XD_XH)
[PROOF STEP]
unfolding stable_pair_on_def split_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH)
CD_on ?ds ?A \<subseteq> ?A \<inter> (\<Union>d\<in>?ds. Field (Pd d))

goal (1 subgoal):
 1. match XD_XH = CD_on ds (fst XD_XH)
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_CH:
  assumes "stable_pair_on ds XD_XH"
  shows "match XD_XH = CH (snd XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match XD_XH = CH (snd XD_XH)
[PROOF STEP]
using %invisible assms CH_range
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
CH ?A \<subseteq> ?A

goal (1 subgoal):
 1. match XD_XH = CH (snd XD_XH)
[PROOF STEP]
unfolding stable_pair_on_def split_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH)
CH ?A \<subseteq> ?A

goal (1 subgoal):
 1. match XD_XH = CH (snd XD_XH)
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_CD_on_CH:
  assumes "stable_pair_on ds XD_XH"
  shows "CD_on ds (fst XD_XH) = CH (snd XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CD_on ds (fst XD_XH) = CH (snd XD_XH)
[PROOF STEP]
using %invisible assms stable_pair_on_CD_on stable_pair_on_CH
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
stable_pair_on ?ds ?XD_XH \<Longrightarrow> match ?XD_XH = CD_on ?ds (fst ?XD_XH)
stable_pair_on ?ds ?XD_XH \<Longrightarrow> match ?XD_XH = CH (snd ?XD_XH)

goal (1 subgoal):
 1. CD_on ds (fst XD_XH) = CH (snd XD_XH)
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_allocation:
  assumes "stable_pair_on ds XD_XH"
  shows "allocation (match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd (match XD_XH)
[PROOF STEP]
unfolding %invisible stable_pair_on_CD_on[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on Xd (CD_on ds (fst XD_XH))
[PROOF STEP]
by (rule CD_on_inj_on_Xd)


[STATEMENT]
lemma stable_pair_onI:
  assumes "fst XD_XH = - RH (snd XD_XH)"
  assumes "snd XD_XH = - RD_on ds (fst XD_XH)"
  shows "stable_pair_on ds XD_XH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_pair_on ds XD_XH
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fst XD_XH = - Rf CH (snd XD_XH)
snd XD_XH = - Rf (CD_on ds) (fst XD_XH)

goal (1 subgoal):
 1. stable_pair_on ds XD_XH
[PROOF STEP]
unfolding stable_pair_on_def split_def
[PROOF STATE]
proof (prove)
using this:
fst XD_XH = - Rf CH (snd XD_XH)
snd XD_XH = - Rf (CD_on ds) (fst XD_XH)

goal (1 subgoal):
 1. fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH)
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_onE:
  shows "\<lbrakk>stable_pair_on ds XD_XH; \<lbrakk>- RH (snd XD_XH) = fst XD_XH; - RD_on ds (fst XD_XH) = snd XD_XH\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stable_pair_on ds XD_XH; \<lbrakk>- Rf CH (snd XD_XH) = fst XD_XH; - Rf (CD_on ds) (fst XD_XH) = snd XD_XH\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
unfolding stable_pair_on_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH); \<lbrakk>- Rf CH (snd XD_XH) = fst XD_XH; - Rf (CD_on ds) (fst XD_XH) = snd XD_XH\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by blast


[STATEMENT]
lemma stable_pair_on_Cd:
  assumes "stable_pair_on ds XD_XH"
  assumes "d \<in> ds"
  shows "Cd d (fst XD_XH) = match XD_XH \<inter> Field (Pd d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d (fst XD_XH) = match XD_XH \<inter> Field (Pd d)
[PROOF STEP]
using stable_pair_on_CD_on[OF \<open>stable_pair_on ds XD_XH\<close>] CD_on_domain Cd_domain \<open>d \<in> ds\<close>
[PROOF STATE]
proof (prove)
using this:
match XD_XH = CD_on ds (fst XD_XH)
?d \<in> ?ds \<Longrightarrow> CD_on ?ds ?A \<inter> Field (Pd ?d) = Cd ?d (?A \<inter> Field (Pd ?d))
Cd ?d (?X \<inter> Field (Pd ?d)) = Cd ?d ?X
d \<in> ds

goal (1 subgoal):
 1. Cd d (fst XD_XH) = match XD_XH \<inter> Field (Pd d)
[PROOF STEP]
by simp


[STATEMENT]
lemma stable_pair_on_Cd_match:
  assumes "stable_pair_on ds XD_XH"
  assumes "d \<in> ds"
  shows "Cd d (match XD_XH) = Cd d (fst XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cd d (match XD_XH) = Cd d (fst XD_XH)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
d \<in> ds

goal (1 subgoal):
 1. Cd d (match XD_XH) = Cd d (fst XD_XH)
[PROOF STEP]
by (metis Cd_domain Cd_idem stable_pair_on_Cd)


[STATEMENT]
lemma stable_pair_on_Xd:
  assumes "stable_pair_on ds XD_XH"
  assumes "x \<in> match XD_XH"
  shows "Xd x \<in> ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
using assms CD_on_Xd
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
x \<in> match XD_XH
?x \<in> CD_on ?ds ?A \<Longrightarrow> Xd ?x \<in> ?ds

goal (1 subgoal):
 1. Xd x \<in> ds
[PROOF STEP]
unfolding stable_pair_on_def split_def
[PROOF STATE]
proof (prove)
using this:
fst XD_XH = - Rf CH (snd XD_XH) \<and> snd XD_XH = - Rf (CD_on ds) (fst XD_XH)
x \<in> match XD_XH
?x \<in> CD_on ?ds ?A \<Longrightarrow> Xd ?x \<in> ?ds

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


[STATEMENT]
lemma stable_pair_on_match_Cd:
  assumes "stable_pair_on ds XD_XH"
  assumes "x \<in> match XD_XH"
  shows "x \<in> Cd (Xd x) (match XD_XH)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Cd (Xd x) (match XD_XH)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stable_pair_on ds XD_XH
x \<in> match XD_XH

goal (1 subgoal):
 1. x \<in> Cd (Xd x) (match XD_XH)
[PROOF STEP]
by (metis (full_types) CD_on_def Cd_Xd UN_iff stable_pair_on_CD_on stable_pair_on_Cd_match)


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

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


[STATEMENT]
lemma D2_ALL:
  shows "(\<forall>d. P d) = (\<forall>d\<in>{D1, D2}. P d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>d. P d) = (\<forall>d\<in>{D1, D2}. P d)
[PROOF STEP]
using D2_UNIV
[PROOF STATE]
proof (prove)
using this:
UNIV = set [D1, D2]

goal (1 subgoal):
 1. (\<forall>d. P d) = (\<forall>d\<in>{D1, D2}. P d)
[PROOF STEP]
by auto


[STATEMENT]
lemma D2_UNION:
  shows "(\<Union>d. P d) = (\<Union>d\<in>{D1, D2}. P d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range P) = \<Union> (P ` {D1, D2})
[PROOF STEP]
using D2_UNIV
[PROOF STATE]
proof (prove)
using this:
UNIV = set [D1, D2]

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


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

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


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

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


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


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


[STATEMENT]
lemma CX4h_range:
  shows "CX4h h X \<subseteq> {x \<in> X. H = h}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CX4h h X \<subseteq> {x \<in> X. H = h}
[PROOF STEP]
by (cases "(h, X)" rule: CX4h.cases) (auto simp: spec[OF H1.nchotomy, of h])


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


[STATEMENT]
lemma Xd1_Xd2_stable:
  shows "StableNoDecomp.stable {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_on UNIV {Xd1, Xd2}
[PROOF STEP]
proof(rule StableNoDecomp.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. StableNoDecomp.individually_rational_on UNIV {Xd1, Xd2}
 2. StableNoDecomp.stable_no_blocking_on UNIV {Xd1, Xd2}
[PROOF STEP]
show "StableNoDecomp.individually_rational {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.individually_rational_on UNIV {Xd1, Xd2}
[PROOF STEP]
by (simp add: StableNoDecomp.individually_rational_on_def StableNoDecomp.CD_on_def
      StableNoDecomp.CH_def insert_commute D2_UNION cong add: SUP_cong_simp)
[PROOF STATE]
proof (state)
this:
StableNoDecomp.individually_rational_on UNIV {Xd1, Xd2}

goal (1 subgoal):
 1. StableNoDecomp.stable_no_blocking_on UNIV {Xd1, Xd2}
[PROOF STEP]
show "StableNoDecomp.stable_no_blocking {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_no_blocking_on UNIV {Xd1, Xd2}
[PROOF STEP]
apply (rule StableNoDecomp.stable_no_blocking_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule_tac x="(H, X'')" in CX4h.cases)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>h X'' uu_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (uu_, {Xd1})\<rbrakk> \<Longrightarrow> False
 2. \<And>h X'' uv_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (uv_, {Xd1'})\<rbrakk> \<Longrightarrow> False
 3. \<And>h X'' uw_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (uw_, {Xd2})\<rbrakk> \<Longrightarrow> False
 4. \<And>h X'' ux_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (ux_, {Xd2'})\<rbrakk> \<Longrightarrow> False
 5. \<And>h X'' uy_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (uy_, {Xd1, Xd1'})\<rbrakk> \<Longrightarrow> False
 6. \<And>h X'' uz_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (uz_, {Xd1, Xd2})\<rbrakk> \<Longrightarrow> False
 7. \<And>h X'' va_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (va_, {Xd1, Xd2'})\<rbrakk> \<Longrightarrow> False
 8. \<And>h X'' vb_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (vb_, {Xd1', Xd2})\<rbrakk> \<Longrightarrow> False
 9. \<And>h X'' vc_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (vc_, {Xd1', Xd2'})\<rbrakk> \<Longrightarrow> False
 10. \<And>h X'' vd_. \<lbrakk>X'' = CX4h h ({Xd1, Xd2} \<union> X''); X'' \<noteq> CX4h h {Xd1, Xd2}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1, Xd2} \<union> X''); (H, X'') = (vd_, {Xd2, Xd2'})\<rbrakk> \<Longrightarrow> False
A total of 16 subgoals...
[PROOF STEP]
apply (simp_all add: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_no_blocking_on UNIV {Xd1, Xd2}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Xd1'_Xd2'_stable:
  shows "StableNoDecomp.stable {Xd1', Xd2'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_on UNIV {Xd1', Xd2'}
[PROOF STEP]
proof(rule StableNoDecomp.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. StableNoDecomp.individually_rational_on UNIV {Xd1', Xd2'}
 2. StableNoDecomp.stable_no_blocking_on UNIV {Xd1', Xd2'}
[PROOF STEP]
show "StableNoDecomp.individually_rational {Xd1', Xd2'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.individually_rational_on UNIV {Xd1', Xd2'}
[PROOF STEP]
by (simp add: StableNoDecomp.individually_rational_on_def StableNoDecomp.CD_on_def
      StableNoDecomp.CH_def insert_commute D2_UNION cong add: SUP_cong_simp)
[PROOF STATE]
proof (state)
this:
StableNoDecomp.individually_rational_on UNIV {Xd1', Xd2'}

goal (1 subgoal):
 1. StableNoDecomp.stable_no_blocking_on UNIV {Xd1', Xd2'}
[PROOF STEP]
show "StableNoDecomp.stable_no_blocking {Xd1', Xd2'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_no_blocking_on UNIV {Xd1', Xd2'}
[PROOF STEP]
apply (rule StableNoDecomp.stable_no_blocking_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule_tac x="(H, X'')" in CX4h.cases)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>h X'' uu_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (uu_, {Xd1})\<rbrakk> \<Longrightarrow> False
 2. \<And>h X'' uv_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (uv_, {Xd1'})\<rbrakk> \<Longrightarrow> False
 3. \<And>h X'' uw_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (uw_, {Xd2})\<rbrakk> \<Longrightarrow> False
 4. \<And>h X'' ux_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (ux_, {Xd2'})\<rbrakk> \<Longrightarrow> False
 5. \<And>h X'' uy_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (uy_, {Xd1, Xd1'})\<rbrakk> \<Longrightarrow> False
 6. \<And>h X'' uz_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (uz_, {Xd1, Xd2})\<rbrakk> \<Longrightarrow> False
 7. \<And>h X'' va_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (va_, {Xd1, Xd2'})\<rbrakk> \<Longrightarrow> False
 8. \<And>h X'' vb_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (vb_, {Xd1', Xd2})\<rbrakk> \<Longrightarrow> False
 9. \<And>h X'' vc_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (vc_, {Xd1', Xd2'})\<rbrakk> \<Longrightarrow> False
 10. \<And>h X'' vd_. \<lbrakk>X'' = CX4h h ({Xd1', Xd2'} \<union> X''); X'' \<noteq> CX4h h {Xd1', Xd2'}; X'' \<subseteq> StableNoDecomp.CD_on UNIV ({Xd1', Xd2'} \<union> X''); (H, X'') = (vd_, {Xd2, Xd2'})\<rbrakk> \<Longrightarrow> False
A total of 16 subgoals...
[PROOF STEP]
apply (simp_all add: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_no_blocking_on UNIV {Xd1', Xd2'}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stable:
  shows "StableNoDecomp.stable X \<longleftrightarrow> X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}"
(*<*)
(is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_on UNIV X = (X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'})
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. StableNoDecomp.stable_on UNIV X \<Longrightarrow> X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
 2. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'} \<Longrightarrow> StableNoDecomp.stable_on UNIV X
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_on UNIV X

goal (2 subgoals):
 1. StableNoDecomp.stable_on UNIV X \<Longrightarrow> X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
 2. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'} \<Longrightarrow> StableNoDecomp.stable_on UNIV X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
StableNoDecomp.stable_on UNIV X
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
StableNoDecomp.stable_on UNIV X

goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
[PROOF STEP]
using X4_pow[where X=X]
[PROOF STATE]
proof (prove)
using this:
StableNoDecomp.stable_on UNIV X
X \<in> set ` set (subseqs [Xd1, Xd1', Xd2, Xd2'])

goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
[PROOF STEP]
unfolding StableNoDecomp.stable_on_def StableNoDecomp.individually_rational_on_def
              StableNoDecomp.stable_no_blocking_on_def StableNoDecomp.blocking_on_def
              StableNoDecomp.CD_on_def StableNoDecomp.CH_def
[PROOF STATE]
proof (prove)
using this:
((\<Union>d. StableNoDecomp.Cd d X) = X \<and> (\<Union>h. CX4h h X) = X) \<and> (\<forall>h X'. \<not> (X' \<noteq> CX4h h X \<and> X' = CX4h h (X \<union> X') \<and> X' \<subseteq> (\<Union>d. StableNoDecomp.Cd d (X \<union> X'))))
X \<in> set ` set (subseqs [Xd1, Xd1', Xd2, Xd2'])

goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
[PROOF STEP]
by simp (elim disjE, simp_all add: D2_UNION X4_ALL insert_commute StableNoDecomp.maxR_def cong add: SUP_cong_simp)
[PROOF STATE]
proof (state)
this:
X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}

goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'} \<Longrightarrow> StableNoDecomp.stable_on UNIV X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'} \<Longrightarrow> StableNoDecomp.stable_on UNIV X
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}

goal (1 subgoal):
 1. X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'} \<Longrightarrow> StableNoDecomp.stable_on UNIV X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}

goal (1 subgoal):
 1. StableNoDecomp.stable_on UNIV X
[PROOF STEP]
using Xd1_Xd2_stable Xd1'_Xd2'_stable
[PROOF STATE]
proof (prove)
using this:
X = {Xd1, Xd2} \<or> X = {Xd1', Xd2'}
StableNoDecomp.stable_on UNIV {Xd1, Xd2}
StableNoDecomp.stable_on UNIV {Xd1', Xd2'}

goal (1 subgoal):
 1. StableNoDecomp.stable_on UNIV X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_on UNIV X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma StableNoDecomp_XD_XH:
  shows "StableNoDecomp.stable_pair (XD, XH) \<longleftrightarrow> (XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'})"
(*<*)
(is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StableNoDecomp.stable_pair_on UNIV (XD, XH) = (XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'})
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. StableNoDecomp.stable_pair_on UNIV (XD, XH) \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[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. StableNoDecomp.stable_pair_on UNIV (XD, XH) \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[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. StableNoDecomp.stable_pair_on UNIV (XD, XH) \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[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. StableNoDecomp.stable_pair_on UNIV (XD, XH) \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)

goal (2 subgoals):
 1. StableNoDecomp.stable_pair_on UNIV (XD, XH) \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)

goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
(* Expand the Cartesian product and check. *)
[PROOF STATE]
proof (prove)
using this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)

goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
using X4_pow [of XD] X4_pow [of XH]
[PROOF STATE]
proof (prove)
using this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)
XD \<in> set ` set (subseqs [Xd1, Xd1', Xd2, Xd2'])
XH \<in> set ` set (subseqs [Xd1, Xd1', Xd2, Xd2'])

goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>StableNoDecomp.stable_pair_on UNIV (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'} \<or> XD = {Xd1, Xd1', Xd2} \<or> XD = {Xd1, Xd1', Xd2'} \<or> XD = {Xd1, Xd1'} \<or> XD = {Xd1, Xd2, Xd2'} \<or> XD = {Xd1, Xd2} \<or> XD = {Xd1, Xd2'} \<or> XD = {Xd1} \<or> XD = {Xd1', Xd2, Xd2'} \<or> XD = {Xd1', Xd2} \<or> XD = {Xd1', Xd2'} \<or> XD = {Xd1'} \<or> XD = {Xd2, Xd2'} \<or> XD = {Xd2} \<or> XD = {Xd2'} \<or> XD = {}; XH = {Xd1, Xd1', Xd2, Xd2'} \<or> XH = {Xd1, Xd1', Xd2} \<or> XH = {Xd1, Xd1', Xd2'} \<or> XH = {Xd1, Xd1'} \<or> XH = {Xd1, Xd2, Xd2'} \<or> XH = {Xd1, Xd2} \<or> XH = {Xd1, Xd2'} \<or> XH = {Xd1} \<or> XH = {Xd1', Xd2, Xd2'} \<or> XH = {Xd1', Xd2} \<or> XH = {Xd1', Xd2'} \<or> XH = {Xd1'} \<or> XH = {Xd2, Xd2'} \<or> XH = {Xd2} \<or> XH = {Xd2'} \<or> XH = {}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
apply (erule StableNoDecomp.stable_pair_onE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>XD = {Xd1, Xd1', Xd2, Xd2'} \<or> XD = {Xd1, Xd1', Xd2} \<or> XD = {Xd1, Xd1', Xd2'} \<or> XD = {Xd1, Xd1'} \<or> XD = {Xd1, Xd2, Xd2'} \<or> XD = {Xd1, Xd2} \<or> XD = {Xd1, Xd2'} \<or> XD = {Xd1} \<or> XD = {Xd1', Xd2, Xd2'} \<or> XD = {Xd1', Xd2} \<or> XD = {Xd1', Xd2'} \<or> XD = {Xd1'} \<or> XD = {Xd2, Xd2'} \<or> XD = {Xd2} \<or> XD = {Xd2'} \<or> XD = {}; XH = {Xd1, Xd1', Xd2, Xd2'} \<or> XH = {Xd1, Xd1', Xd2} \<or> XH = {Xd1, Xd1', Xd2'} \<or> XH = {Xd1, Xd1'} \<or> XH = {Xd1, Xd2, Xd2'} \<or> XH = {Xd1, Xd2} \<or> XH = {Xd1, Xd2'} \<or> XH = {Xd1} \<or> XH = {Xd1', Xd2, Xd2'} \<or> XH = {Xd1', Xd2} \<or> XH = {Xd1', Xd2'} \<or> XH = {Xd1'} \<or> XH = {Xd2, Xd2'} \<or> XH = {Xd2} \<or> XH = {Xd2'} \<or> XH = {}; - Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH)\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (256 subgoals):
 1. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 2. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 3. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 4. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 5. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2, Xd2'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 6. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 7. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 8. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 9. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
 10. \<lbrakk>- Rf StableNoDecomp.CH (snd (XD, XH)) = fst (XD, XH); - Rf (StableNoDecomp.CD_on UNIV) (fst (XD, XH)) = snd (XD, XH); XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2}\<rbrakk> \<Longrightarrow> XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
A total of 256 subgoals...
[PROOF STEP]
apply (simp_all add: StableNoDecomp.CD_on_def StableNoDecomp.CH_def)
[PROOF STATE]
proof (prove)
goal (244 subgoals):
 1. \<lbrakk>- {Xd1, Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; insert Xd1 (insert Xd1' (insert Xd2 (insert Xd2' (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'})))) = {Xd1, Xd1', Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>- {Xd1, Xd1', Xd2} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1', Xd2}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>- {Xd1, Xd1', Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1', Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2'}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>- {Xd1'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1'}\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>- {Xd1, Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>UNIV = {Xd1, Xd1', Xd2, Xd2'}; (\<Union>d. StableNoDecomp.Cd d UNIV) = {Xd1, Xd2}; XD = UNIV; XH = {Xd1, Xd2}\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>insert Xd2' (- {Xd1, Xd2'}) = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2'}\<rbrakk> \<Longrightarrow> False
 8. \<lbrakk>UNIV = {Xd1, Xd1', Xd2, Xd2'}; (\<Union>d. StableNoDecomp.Cd d UNIV) = {Xd1}; XD = UNIV; XH = {Xd1}\<rbrakk> \<Longrightarrow> False
 9. \<lbrakk>- {Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1', Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 10. \<lbrakk>- {Xd2} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1', Xd2}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2}\<rbrakk> \<Longrightarrow> False
A total of 244 subgoals...
[PROOF STEP]
unfolding X4_UNIV [simplified]
[PROOF STATE]
proof (prove)
goal (244 subgoals):
 1. \<lbrakk>- {Xd1, Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; insert Xd1 (insert Xd1' (insert Xd2 (insert Xd2' (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'})))) = {Xd1, Xd1', Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>- {Xd1, Xd1', Xd2} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1', Xd2}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>- {Xd1, Xd1', Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1', Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1', Xd2'}\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>- {Xd1'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd1'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd1'}\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>- {Xd1, Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>{Xd1, Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; (\<Union>d. StableNoDecomp.Cd d {Xd1, Xd1', Xd2, Xd2'}) = {Xd1, Xd2}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2}\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>insert Xd2' (- {Xd1, Xd2'}) = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1, Xd2'}\<rbrakk> \<Longrightarrow> False
 8. \<lbrakk>{Xd1, Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; (\<Union>d. StableNoDecomp.Cd d {Xd1, Xd1', Xd2, Xd2'}) = {Xd1}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1}\<rbrakk> \<Longrightarrow> False
 9. \<lbrakk>- {Xd1', Xd2, Xd2'} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1', Xd2, Xd2'}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2, Xd2'}\<rbrakk> \<Longrightarrow> False
 10. \<lbrakk>- {Xd2} = {Xd1, Xd1', Xd2, Xd2'}; - {Xd1, Xd1', Xd2, Xd2'} \<union> (\<Union>x. if Xd1 \<in> Field (PX4d x) then if StableNoDecomp.Cd x {Xd1', Xd2, Xd2'} = {} then {Xd1} else {StableNoDecomp.maxR x Xd1 y |y. y \<in> StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}} else StableNoDecomp.Cd x {Xd1', Xd2, Xd2'}) = {Xd1', Xd2}; XD = {Xd1, Xd1', Xd2, Xd2'}; XH = {Xd1', Xd2}\<rbrakk> \<Longrightarrow> False
A total of 244 subgoals...
[PROOF STEP]
apply (auto simp: D2_ALL D2_UNION X4_ALL insert_commute StableNoDecomp.maxR_def linord_of_list_linord_of_listP)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}

goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}

goal (1 subgoal):
 1. XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'} \<Longrightarrow> StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}

goal (1 subgoal):
 1. StableNoDecomp.stable_pair_on UNIV (XD, XH)
[PROOF STEP]
unfolding StableNoDecomp.stable_pair_on_def
[PROOF STATE]
proof (prove)
using this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}

goal (1 subgoal):
 1. case (XD, XH) of (XD, XH) \<Rightarrow> XD = - Rf StableNoDecomp.CH XH \<and> XH = - Rf (StableNoDecomp.CD_on UNIV) XD
[PROOF STEP]
using X4.exhaust
[PROOF STATE]
proof (prove)
using this:
XD = {} \<and> XH = {Xd1, Xd1', Xd2, Xd2'}
\<lbrakk>?y = Xd1 \<Longrightarrow> ?P; ?y = Xd1' \<Longrightarrow> ?P; ?y = Xd2 \<Longrightarrow> ?P; ?y = Xd2' \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. case (XD, XH) of (XD, XH) \<Rightarrow> XD = - Rf StableNoDecomp.CH XH \<and> XH = - Rf (StableNoDecomp.CD_on UNIV) XD
[PROOF STEP]
by (auto simp: StableNoDecomp.CH_def)
[PROOF STATE]
proof (state)
this:
StableNoDecomp.stable_pair_on UNIV (XD, XH)

goal:
No subgoals!
[PROOF STEP]
qed