theory Deterministic_AI

lemma finite_depth:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "valid_mdb s \<Longrightarrow> finite_depth (cdt s)" apply(simp add: finite_depth_def) apply(intro allI) apply(subgoal_tac "{x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s}") prefer 2 apply(fastforce simp: descendants_of_cte_at2) apply(drule finite_subset) apply(simp add: cte_wp_at_set_finite) apply(case_tac "cdt s slot") apply(fastforce) apply(rule ccontr) apply(simp) apply(frule_tac f="\<lambda>x. THE y. cdt s x = Some y" in inj_on_iff_eq_card) apply(subgoal_tac "inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}") prefer 2 apply(simp(no_asm) add: inj_on_def) apply(intro allI impI) apply(rule ccontr) apply(frule_tac b=x and c=y in descendants_linear) apply(simp) apply(simp) apply(case_tac "cdt s x") apply(fastforce) apply(case_tac "cdt s y") apply(fastforce) apply(fastforce simp: valid_mdb_def sib_not_desc) apply(simp) apply(subgoal_tac "((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)})
                      \<subset> {x. slot \<in> descendants_of x (cdt s)}") prefer 2 apply(rule psubsetI) apply(rule subsetI) apply(simp) apply(erule imageE) apply(case_tac "cdt s xa") apply(fastforce) apply(rule_tac b=xa in descendants_trans) apply(simp) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(rule_tac x=a in set_neqI[symmetric]) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(rule notI) apply(erule imageE) apply(case_tac "cdt s x") apply(fastforce) apply(fastforce simp: sib_not_desc valid_mdb_def) apply(drule psubset_card_mono) apply(assumption) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> \<forall>slot. \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. valid_mdb s \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>valid_mdb s; {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s}\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None
 2. \<And>slot. valid_mdb s \<Longrightarrow> {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s} proof (prove)
goal (2 subgoals):
 1. \<And>slot. valid_mdb s \<Longrightarrow> {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s}
 2. \<And>slot. \<lbrakk>valid_mdb s; {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s}\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>valid_mdb s; {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. cte_wp_at (\<lambda>_. True) x s}\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. valid_mdb s \<Longrightarrow> finite {x. cte_wp_at (\<lambda>_. True) x s}
 2. \<And>slot. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<nexists>p. (slot \<in> descendants_of p (cdt s) \<or> p = slot) \<and> cdt s p = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)})\<rbrakk> \<Longrightarrow> inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)})\<rbrakk> \<Longrightarrow> inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)})\<rbrakk> \<Longrightarrow> \<forall>x. slot \<in> descendants_of x (cdt s) \<longrightarrow> (\<forall>y. slot \<in> descendants_of y (cdt s) \<longrightarrow> (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya) \<longrightarrow> x = y)
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y\<rbrakk> \<Longrightarrow> slot \<in> descendants_of y (cdt s)
 2. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y\<rbrakk> \<Longrightarrow> x \<noteq> y
 3. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y\<rbrakk> \<Longrightarrow> x \<noteq> y
 2. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x y. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = None\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a x y aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = Some aa\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x y aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = Some aa\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x y aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = Some aa; cdt s y = None\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a x y aa ab. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = Some aa; cdt s y = Some ab\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x y aa ab. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); slot \<in> descendants_of x (cdt s); slot \<in> descendants_of y (cdt s); (THE y. cdt s x = Some y) = (THE ya. cdt s y = Some ya); x \<noteq> y; x \<in> descendants_of y (cdt s) \<or> y \<in> descendants_of x (cdt s); cdt s x = Some aa; cdt s y = Some ab\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)} = (card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}); inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)} proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subseteq> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x \<in> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> x \<in> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x \<in> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> slot \<in> descendants_of x (cdt s)
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x xa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> slot \<in> descendants_of x (cdt s)
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>slot a x xa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = None\<rbrakk> \<Longrightarrow> slot \<in> descendants_of x (cdt s)
 2. \<And>slot a x xa aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = Some aa\<rbrakk> \<Longrightarrow> slot \<in> descendants_of x (cdt s)
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 4. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x xa aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = Some aa\<rbrakk> \<Longrightarrow> slot \<in> descendants_of x (cdt s)
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>slot a x xa aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = Some aa\<rbrakk> \<Longrightarrow> slot \<in> descendants_of xa (cdt s)
 2. \<And>slot a x xa aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = Some aa\<rbrakk> \<Longrightarrow> xa \<in> descendants_of x (cdt s)
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 4. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x xa aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; x = (THE y. cdt s xa = Some y); xa \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s xa = Some aa\<rbrakk> \<Longrightarrow> xa \<in> descendants_of x (cdt s)
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<noteq> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> a \<in> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> a \<notin> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> a \<notin> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; a \<in> (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; a = (THE y. cdt s x = Some y); x \<in> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>slot a x. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; a = (THE y. cdt s x = Some y); x \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s x = None\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a x aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; a = (THE y. cdt s x = Some y); x \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s x = Some aa\<rbrakk> \<Longrightarrow> False
 3. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a x aa. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; a = (THE y. cdt s x = Some y); x \<in> {x. slot \<in> descendants_of x (cdt s)}; cdt s x = Some aa\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; finite {x. slot \<in> descendants_of x (cdt s)}; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_mdb s; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> ?A193 slot a \<subset> {x. slot \<in> descendants_of x (cdt s)}
 2. \<And>slot a. \<lbrakk>valid_mdb s; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}; card (?A193 slot a) < card {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>valid_mdb s; cdt s slot = Some a; \<forall>p. slot \<notin> descendants_of p (cdt s) \<and> p \<noteq> slot \<or> (\<exists>y. cdt s p = Some y); card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) = card {x. slot \<in> descendants_of x (cdt s)}; inj_on (\<lambda>x. THE y. cdt s x = Some y) {x. slot \<in> descendants_of x (cdt s)}; (\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)} \<subset> {x. slot \<in> descendants_of x (cdt s)}; card ((\<lambda>x. THE y. cdt s x = Some y) ` {x. slot \<in> descendants_of x (cdt s)}) < card {x. slot \<in> descendants_of x (cdt s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!