theory Deterministic_AI

lemma cte_at_next_slot':
  "\<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s)\<rbrakk>
    \<Longrightarrow> next_slot p (cdt_list s) (cdt s) = Some n \<Longrightarrow> cte_at n s" apply(simp add: next_slot_def) apply(simp split: if_split_asm) apply(drule next_childD, simp) apply(rule_tac x=p in descendants_of_cte_at, simp add: child_descendant, simp) apply(rule next_not_child_pinduct2[where t="cdt_list s" and p=p
                                             and m="cdt s"]) apply(rule_tac p=a in descendants_of_cte_at2) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(simp) apply(assumption) apply(simp add: next_not_child_termination valid_mdb_def valid_list_2_def
               split: if_split_asm) apply(case_tac "cdt s p") apply(simp) apply(simp) apply(rule descendants_of_cte_at) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(simp add: valid_mdb_def) apply(drule next_sibD) apply(case_tac "cdt s p") apply(simp) apply(rule descendants_of_cte_at) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(simp add: valid_mdb_def) apply(intro allI impI, drule next_sibD) apply(simp) apply(elim exE conjE) apply(drule_tac after_in_list_in_list) apply(simp add: valid_list_2_def) apply(rule_tac x="(aa, b)" in descendants_of_cte_at, simp add: child_descendant, simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); next_slot p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); (if cdt_list s p \<noteq> [] then next_child p (cdt_list s) else next_not_child p (cdt_list s) (cdt s)) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; next_child p (cdt_list s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p \<noteq> []; (\<exists>xs. cdt_list s p = n # xs) \<and> cdt s n = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) n s proof (prove)
goal (5 subgoals):
 1. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_sib a (cdt_list s) (cdt s) = None; cdt s a = Some slot; cte_wp_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child p (cdt_list s) (cdt s) = Some n
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 5. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (6 subgoals):
 1. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_sib a (cdt_list s) (cdt s) = None; cdt s a = Some slot; cte_wp_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> a \<in> descendants_of slot (cdt s)
 2. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_sib a (cdt_list s) (cdt s) = None; cdt s a = Some slot; cte_wp_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child p (cdt_list s) (cdt s) = Some n
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 5. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 6. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; next_sib a (cdt_list s) (cdt s) = None; cdt s a = Some slot; cte_wp_at (\<lambda>_. True) a s\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child p (cdt_list s) (cdt s) = Some n
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 5. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> next_not_child p (cdt_list s) (cdt s) = Some n
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s)) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s)) = Some n; cdt s p = None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 5. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (if next_sib a (cdt_list s) (cdt s) = None then case cdt s a of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib a (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (if next_sib a (cdt_list s) (cdt s) = None then case cdt s a of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib a (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> p \<in> descendants_of (?x129 a) (cdt s)
 2. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (if next_sib a (cdt_list s) (cdt s) = None then case cdt s a of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib a (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 5. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; next_sib p (cdt_list s) (cdt s) = None; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); (if next_sib a (cdt_list s) (cdt s) = None then case cdt s a of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> if next_sib p (cdt_list s) (cdt s) = None then case cdt s p of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib p (cdt_list s) (cdt s) else next_sib a (cdt_list s) (cdt s)) = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); next_sib p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = None\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> p \<in> descendants_of (?x140 a) (cdt s)
 2. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 4. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>finite_depth (cdt s); cdt_list s p = []; \<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}; \<forall>a b. distinct (cdt_list s (a, b)); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>pa. cdt s p = Some pa \<and> after_in_list (cdt_list s pa) p = Some n; cdt s p = Some a\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 3. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> \<forall>a slot. next_sib a (cdt_list s) (cdt s) = Some slot \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; \<exists>p. cdt s a = Some p \<and> after_in_list (cdt_list s p) a = Some slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a slot. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; \<exists>aa b. cdt s a = Some (aa, b) \<and> after_in_list (cdt_list s (aa, b)) a = Some slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a slot aa b. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; cdt s a = Some (aa, b); after_in_list (cdt_list s (aa, b)) a = Some slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a slot aa b. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; cdt s a = Some (aa, b); slot \<in> set (cdt_list s (aa, b))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>a slot aa b. \<lbrakk>(\<forall>a b. set (cdt_list s (a, b)) = {c. cdt s c = Some (a, b)}) \<and> (\<forall>a b. distinct (cdt_list s (a, b))); valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n; cdt s a = Some (aa, b); cdt s slot = Some (aa, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list s; valid_mdb s; finite_depth (cdt s); cdt_list s p = []; next_not_child p (cdt_list s) (cdt s) = Some n\<rbrakk> \<Longrightarrow> finite_depth (cdt s) proof (prove)
goal:
No subgoals!