theory VSpacePre_AI

lemma arch_update_cap_valid_mdb:
  "\<lbrace>cte_wp_at (is_arch_update cap) p and valid_mdb\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_mdb\<rbrace>" apply (simp add: valid_mdb_def2 pred_conj_def) apply (rule hoare_lift_Pf2 [where f=cdt]) prefer 2 apply wp[1] apply (rule hoare_lift_Pf2 [where f=is_original_cap]) prefer 2 apply wp[1] apply (rule hoare_pre) apply wp apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule conjI) apply (clarsimp simp: mdb_cte_at_def is_arch_update_def) apply (fastforce simp: is_cap_simps) apply (rule conjI) apply (clarsimp simp: untyped_mdb_def is_arch_update_def) apply (rule conjI) apply (fastforce simp: is_cap_simps) apply clarsimp apply (drule master_cap_obj_refs) apply fastforce apply (rule conjI) apply (erule(1) descendants_inc_minor) apply (clarsimp simp:is_arch_update_def) apply (frule master_cap_class) apply (clarsimp dest!:master_cap_cap_range) apply (rule conjI) apply (clarsimp simp: untyped_inc_def is_arch_update_def) subgoal by (fastforce simp: is_cap_simps) apply (rule conjI) apply (clarsimp simp: ut_revocable_def) apply (clarsimp simp: is_arch_update_def is_cap_simps) apply (rule conjI) apply (clarsimp simp: irq_revocable_def is_arch_update_def is_cap_simps simp del: split_paired_All) apply (rule conjI) apply (clarsimp simp: reply_master_revocable_def is_arch_update_def is_cap_simps) apply (clarsimp simp: reply_mdb_def is_arch_update_def) apply (rule conjI) apply (clarsimp simp: reply_caps_mdb_def is_cap_simps cap_master_cap_def
               simp del: split_paired_Ex split_paired_All) apply (fastforce elim!: exEI) apply (rule conjI, fastforce simp: is_cap_simps cap_master_cap_def reply_masters_mdb_def) by (erule (2) valid_arch_mdb_same_master_cap[simplified fun_upd_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap) p and valid_mdb\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. cte_wp_at (is_arch_update cap) p x \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state x p = Some c \<and> NullCap \<noteq> c) (cdt x) \<and> untyped_mdb (cdt x) (caps_of_state x) \<and> descendants_inc (cdt x) (caps_of_state x) \<and> no_mloop (cdt x) \<and> untyped_inc (cdt x) (caps_of_state x) \<and> ut_revocable (is_original_cap x) (caps_of_state x) \<and> irq_revocable (is_original_cap x) (caps_of_state x) \<and> reply_master_revocable (is_original_cap x) (caps_of_state x) \<and> reply_mdb (cdt x) (caps_of_state x) \<and> valid_arch_mdb (is_original_cap x) (caps_of_state x)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. cte_wp_at (is_arch_update cap) p xa \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xa p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xa) \<and> descendants_inc x (caps_of_state xa) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xa) \<and> ut_revocable (is_original_cap xa) (caps_of_state xa) \<and> irq_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_master_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_mdb x (caps_of_state xa) \<and> valid_arch_mdb (is_original_cap xa) (caps_of_state xa)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable (is_original_cap a) (caps_of_state a) \<and> irq_revocable (is_original_cap a) (caps_of_state a) \<and> reply_master_revocable (is_original_cap a) (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb (is_original_cap a) (caps_of_state a)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (cdt x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (cdt x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>x. P (cdt x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (cdt x)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>xa. cte_wp_at (is_arch_update cap) p xa \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xa p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xa) \<and> descendants_inc x (caps_of_state xa) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xa) \<and> ut_revocable (is_original_cap xa) (caps_of_state xa) \<and> irq_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_master_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_mdb x (caps_of_state xa) \<and> valid_arch_mdb (is_original_cap xa) (caps_of_state xa)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable (is_original_cap a) (caps_of_state a) \<and> irq_revocable (is_original_cap a) (caps_of_state a) \<and> reply_master_revocable (is_original_cap a) (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb (is_original_cap a) (caps_of_state a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. cte_wp_at (is_arch_update cap) p xa \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xa p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xa) \<and> descendants_inc x (caps_of_state xa) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xa) \<and> ut_revocable (is_original_cap xa) (caps_of_state xa) \<and> irq_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_master_revocable (is_original_cap xa) (caps_of_state xa) \<and> reply_mdb x (caps_of_state xa) \<and> valid_arch_mdb (is_original_cap xa) (caps_of_state xa)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable (is_original_cap a) (caps_of_state a) \<and> irq_revocable (is_original_cap a) (caps_of_state a) \<and> reply_master_revocable (is_original_cap a) (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb (is_original_cap a) (caps_of_state a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>xb. cte_wp_at (is_arch_update cap) p xb \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xb p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xb) \<and> descendants_inc x (caps_of_state xb) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xb) \<and> ut_revocable xa (caps_of_state xb) \<and> irq_revocable xa (caps_of_state xb) \<and> reply_master_revocable xa (caps_of_state xb) \<and> reply_mdb x (caps_of_state xb) \<and> valid_arch_mdb xa (caps_of_state xb)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable xa (caps_of_state a) \<and> irq_revocable xa (caps_of_state a) \<and> reply_master_revocable xa (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb xa (caps_of_state a)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>x. P (is_original_cap x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (is_original_cap x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x P. \<lbrace>\<lambda>x. P (is_original_cap x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (is_original_cap x)\<rbrace>
 2. \<And>x xa. \<lbrace>\<lambda>xb. cte_wp_at (is_arch_update cap) p xb \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xb p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xb) \<and> descendants_inc x (caps_of_state xb) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xb) \<and> ut_revocable xa (caps_of_state xb) \<and> irq_revocable xa (caps_of_state xb) \<and> reply_master_revocable xa (caps_of_state xb) \<and> reply_mdb x (caps_of_state xb) \<and> valid_arch_mdb xa (caps_of_state xb)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable xa (caps_of_state a) \<and> irq_revocable xa (caps_of_state a) \<and> reply_master_revocable xa (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb xa (caps_of_state a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>xb. cte_wp_at (is_arch_update cap) p xb \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state xb p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state xb) \<and> descendants_inc x (caps_of_state xb) \<and> no_mloop x \<and> untyped_inc x (caps_of_state xb) \<and> ut_revocable xa (caps_of_state xb) \<and> irq_revocable xa (caps_of_state xb) \<and> reply_master_revocable xa (caps_of_state xb) \<and> reply_mdb x (caps_of_state xb) \<and> valid_arch_mdb xa (caps_of_state xb)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable xa (caps_of_state a) \<and> irq_revocable xa (caps_of_state a) \<and> reply_master_revocable xa (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb xa (caps_of_state a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>?Q52 x xa\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state a p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state a) \<and> descendants_inc x (caps_of_state a) \<and> no_mloop x \<and> untyped_inc x (caps_of_state a) \<and> ut_revocable xa (caps_of_state a) \<and> irq_revocable xa (caps_of_state a) \<and> reply_master_revocable xa (caps_of_state a) \<and> reply_mdb x (caps_of_state a) \<and> valid_arch_mdb xa (caps_of_state a)\<rbrace>
 2. \<And>x xa s. cte_wp_at (is_arch_update cap) p s \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state s) \<and> descendants_inc x (caps_of_state s) \<and> no_mloop x \<and> untyped_inc x (caps_of_state s) \<and> ut_revocable xa (caps_of_state s) \<and> irq_revocable xa (caps_of_state s) \<and> reply_master_revocable xa (caps_of_state s) \<and> reply_mdb x (caps_of_state s) \<and> valid_arch_mdb xa (caps_of_state s) \<Longrightarrow> ?Q52 x xa s proof (prove)
goal (1 subgoal):
 1. \<And>x xa s. cte_wp_at (is_arch_update cap) p s \<and> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x (caps_of_state s) \<and> descendants_inc x (caps_of_state s) \<and> no_mloop x \<and> untyped_inc x (caps_of_state s) \<and> ut_revocable xa (caps_of_state s) \<and> irq_revocable xa (caps_of_state s) \<and> reply_master_revocable xa (caps_of_state s) \<and> reply_mdb x (caps_of_state s) \<and> valid_arch_mdb xa (caps_of_state s) \<Longrightarrow> mdb_cte_at (\<lambda>pa. \<exists>c. ((caps_of_state s)(p \<mapsto> cap)) pa = Some c \<and> NullCap \<noteq> c) x \<and> untyped_mdb x ((caps_of_state s)(p \<mapsto> cap)) \<and> descendants_inc x ((caps_of_state s)(p \<mapsto> cap)) \<and> no_mloop x \<and> untyped_inc x ((caps_of_state s)(p \<mapsto> cap)) \<and> ut_revocable xa ((caps_of_state s)(p \<mapsto> cap)) \<and> irq_revocable xa ((caps_of_state s)(p \<mapsto> cap)) \<and> reply_master_revocable xa ((caps_of_state s)(p \<mapsto> cap)) \<and> reply_mdb x ((caps_of_state s)(p \<mapsto> cap)) \<and> valid_arch_mdb xa ((caps_of_state s)(p \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>pa. (pa = p \<longrightarrow> NullCap \<noteq> cap) \<and> (pa \<noteq> p \<longrightarrow> (\<exists>c. caps_of_state s pa = Some c \<and> NullCap \<noteq> c))) x \<and> untyped_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> mdb_cte_at (\<lambda>pa. (pa = p \<longrightarrow> NullCap \<noteq> cap) \<and> (pa \<noteq> p \<longrightarrow> (\<exists>c. caps_of_state s pa = Some c \<and> NullCap \<noteq> c))) x
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b aa ba. \<lbrakk>\<forall>a b aa ba. x (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> NullCap \<noteq> c); caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; x (aa, ba) = Some (a, b)\<rbrakk> \<Longrightarrow> ((a, b) = p \<longrightarrow> NullCap \<noteq> cap) \<and> ((aa, ba) = p \<longrightarrow> NullCap \<noteq> cap)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> ((a, b) = p \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>a b. ((a, b) = p \<longrightarrow> obj_refs cap \<inter> untyped_range cap \<noteq> {} \<longrightarrow> p \<in> descendants_of p x) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<forall>cap'. caps_of_state s (a, b) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (a, b) \<in> descendants_of p x)))) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<exists>a b. (a, b) = p) \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> obj_refs cap \<inter> untyped_range capa \<noteq> {} \<longrightarrow> p \<in> descendants_of (a, b) x))
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (3 subgoals):
 1. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> (a, b) = p \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>a b. ((a, b) = p \<longrightarrow> obj_refs cap \<inter> untyped_range cap \<noteq> {} \<longrightarrow> p \<in> descendants_of p x) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<forall>cap'. caps_of_state s (a, b) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (a, b) \<in> descendants_of p x)))
 2. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> p \<longrightarrow> (\<exists>a b. (a, b) = p) \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> obj_refs cap \<inter> untyped_range capa \<noteq> {} \<longrightarrow> p \<in> descendants_of (a, b) x)
 3. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> p \<longrightarrow> (\<exists>a b. (a, b) = p) \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> obj_refs cap \<inter> untyped_range capa \<noteq> {} \<longrightarrow> p \<in> descendants_of (a, b) x)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b aa ba capaa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s (aa, ba) = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; p = (aa, ba); a = aa \<longrightarrow> b \<noteq> ba; caps_of_state s (a, b) = Some capaa; is_untyped_cap capaa; obj_refs cap \<inter> untyped_range capaa \<noteq> {}\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) x
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b aa ba capaa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s (aa, ba) = Some capa; \<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; p = (aa, ba); a = aa \<longrightarrow> b \<noteq> ba; caps_of_state s (a, b) = Some capaa; is_untyped_cap capaa; obj_refs cap \<inter> untyped_range capaa \<noteq> {}; obj_refs cap = obj_refs capa\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) x
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (caps_of_state s). cap_class (the (if x = p then Some cap else caps_of_state s x)) = cap_class (the (caps_of_state s x)) \<and> cap_range (the (if x = p then Some cap else caps_of_state s x)) = cap_range (the (caps_of_state s x))
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; untyped_mdb x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; caps_of_state s p = Some capa\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap = cap_range capa
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; untyped_mdb x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; caps_of_state s p = Some capa; cap_class cap = cap_class capa\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap = cap_range capa
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> untyped_inc x (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; \<forall>a b aa ba c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) x \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) x \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba)); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> ((a, b) = p \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>aa ba. ((aa, ba) = p \<longrightarrow> p \<in> descendants_of p x \<and> usable_untyped_range cap = {} \<or> a = aa \<and> b = ba) \<and> ((aa, ba) \<noteq> p \<longrightarrow> (\<forall>c'. caps_of_state s (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range cap \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range c' = {}) \<and> (untyped_range cap \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of (aa, ba) x \<and> untyped_range cap \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> (aa, ba) \<in> descendants_of p x \<and> untyped_range c' \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of p x \<and> usable_untyped_range cap = {} \<or> p \<in> descendants_of (aa, ba) x \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba))))) \<and> ((a, b) \<noteq> p \<longrightarrow> (\<forall>aa ba. (aa, ba) = p \<longrightarrow> (\<forall>c. caps_of_state s (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range cap = {}) \<and> (untyped_range c \<subset> untyped_range cap \<longrightarrow> (a, b) \<in> descendants_of p x \<and> untyped_range c \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of (a, b) x \<and> untyped_range cap \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> p \<in> descendants_of (a, b) x \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of p x \<and> usable_untyped_range cap = {} \<or> a = aa \<and> b = ba))))
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s_ p = Some c \<and> NullCap \<noteq> c) x_; caps_of_state s_ p = Some capa_; untyped_mdb x_ (caps_of_state s_); descendants_inc x_ (caps_of_state s_); no_mloop x_; \<forall>a b aa ba c. caps_of_state s_ (a, b) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (\<forall>c'. caps_of_state s_ (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> (a, b) \<in> descendants_of (aa, ba) x_ \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x_ \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) x_ \<and> usable_untyped_range c = {} \<or> (a, b) \<in> descendants_of (aa, ba) x_ \<and> usable_untyped_range c' = {} \<or> a = aa \<and> b = ba)); ut_revocable xa_ (caps_of_state s_); irq_revocable xa_ (caps_of_state s_); reply_master_revocable xa_ (caps_of_state s_); reply_mdb x_ (caps_of_state s_); valid_arch_mdb xa_ (caps_of_state s_); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa_\<rbrakk> \<Longrightarrow> ((a_, b_) = p \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>aa ba. ((aa, ba) = p \<longrightarrow> p \<in> descendants_of p x_ \<and> usable_untyped_range cap = {} \<or> a_ = aa \<and> b_ = ba) \<and> ((aa, ba) \<noteq> p \<longrightarrow> (\<forall>c'. caps_of_state s_ (aa, ba) = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range cap \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range c' = {}) \<and> (untyped_range cap \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of (aa, ba) x_ \<and> untyped_range cap \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> (aa, ba) \<in> descendants_of p x_ \<and> untyped_range c' \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> (aa, ba) \<in> descendants_of p x_ \<and> usable_untyped_range cap = {} \<or> p \<in> descendants_of (aa, ba) x_ \<and> usable_untyped_range c' = {} \<or> a_ = aa \<and> b_ = ba))))) \<and> ((a_, b_) \<noteq> p \<longrightarrow> (\<forall>aa ba. (aa, ba) = p \<longrightarrow> (\<forall>c. caps_of_state s_ (a_, b_) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap cap \<longrightarrow> (untyped_range c \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range cap = {}) \<and> (untyped_range c \<subset> untyped_range cap \<longrightarrow> (a_, b_) \<in> descendants_of p x_ \<and> untyped_range c \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap \<subset> untyped_range c \<longrightarrow> p \<in> descendants_of (a_, b_) x_ \<and> untyped_range cap \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range cap \<longrightarrow> p \<in> descendants_of (a_, b_) x_ \<and> usable_untyped_range c = {} \<or> (a_, b_) \<in> descendants_of p x_ \<and> usable_untyped_range cap = {} \<or> a_ = aa \<and> b_ = ba)))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> ut_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a b. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s (a, b) = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> xa (a, b); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s); p = (a, b); is_untyped_cap cap\<rbrakk> \<Longrightarrow> xa (a, b)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> irq_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_master_revocable xa (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; is_arch_update cap capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); reply_mdb x (caps_of_state s); valid_arch_mdb xa (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_caps_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> reply_masters_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_caps_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a)
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_masters_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xa s capa a aa b t rights. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); ArchObjectCap (cap_master_arch_cap a) = (case capa of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap x \<Rightarrow> ThreadCap x | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (cap_master_arch_cap acap) | _ \<Rightarrow> capa); \<forall>ptr t. (\<exists>rights. caps_of_state s ptr = Some (ReplyCap t False rights)) \<longrightarrow> (\<exists>ptr'. x ptr = Some ptr' \<and> (\<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t True rights'))); reply_masters_mdb x (caps_of_state s); cap = ArchObjectCap a; (aa, b) \<noteq> p; caps_of_state s (aa, b) = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> p \<and> (ptr' \<noteq> p \<longrightarrow> x (aa, b) = Some ptr' \<and> (\<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t True rights')))
 2. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_masters_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> reply_masters_mdb x (\<lambda>a. if a = p then Some cap else caps_of_state s a) \<and> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s capa. \<lbrakk>mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) x; caps_of_state s p = Some capa; untyped_mdb x (caps_of_state s); descendants_inc x (caps_of_state s); no_mloop x; untyped_inc x (caps_of_state s); ut_revocable xa (caps_of_state s); irq_revocable xa (caps_of_state s); reply_master_revocable xa (caps_of_state s); valid_arch_mdb xa (caps_of_state s); is_arch_cap cap; cap_master_cap cap = cap_master_cap capa; reply_caps_mdb x (caps_of_state s); reply_masters_mdb x (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_arch_mdb xa (\<lambda>a. if a = p then Some cap else caps_of_state s a)