theory Untyped_AI

lemma not_waiting_reply_slot_no_descendants:
  "\<lbrakk> st_tcb_at (Not \<circ> awaiting_reply) t s;
     valid_reply_caps s; valid_objs s; valid_mdb s \<rbrakk>
       \<Longrightarrow> descendants_of (t, tcb_cnode_index 2) (cdt s) = {}" apply (rule ccontr, erule nonemptyE) apply (clarsimp simp: valid_mdb_def reply_mdb_def reply_masters_mdb_def) apply (frule_tac ref="tcb_cnode_index 2" in tcb_at_cte_at[OF st_tcb_at_tcb_at]) apply (simp add: domI) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule(1) tcb_cap_valid_caps_of_stateD) apply (clarsimp simp: tcb_cap_valid_def st_tcb_at_tcb_at) apply (clarsimp simp: st_tcb_def2) apply (erule disjE) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply (elim allE impE) apply fastforce apply (clarsimp) apply (drule(1) bspec) apply (subgoal_tac "has_reply_cap t s") apply (erule notE[rotated], strengthen reply_cap_doesnt_exist_strg) apply (simp add: st_tcb_def2) apply (erule exE) apply (drule caps_of_state_cteD)+ apply (fastforce simp add:has_reply_cap_def is_reply_cap_to_def elim:cte_wp_at_lift
                    intro:  caps_of_state_cteD) apply clarsimp apply (frule mdb_Null_descendants[OF caps_of_state_cteD]) apply (simp add: valid_mdb_def reply_mdb_def reply_masters_mdb_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of (t, tcb_cnode_index 2) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; valid_mdb s; x \<in> descendants_of (t, tcb_cnode_index 2) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> tcb_cnode_index 2 \<in> dom tcb_cap_cases
 2. \<And>a b. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_cap_valid cap (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>st_tcb_at (Not \<circ> awaiting_reply) t s; valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; st_tcb_at (\<lambda>st. is_master_reply_cap cap \<and> obj_ref_of cap = t \<and> AllowGrant \<in> cap_rights cap \<or> halted st \<and> cap = NullCap) t s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; is_master_reply_cap cap \<and> obj_ref_of cap = t \<and> AllowGrant \<in> cap_rights cap \<or> halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; is_master_reply_cap cap \<and> obj_ref_of cap = t \<and> AllowGrant \<in> cap_rights cap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R\<rbrakk> \<Longrightarrow> \<exists>rights. caps_of_state s (?a40 a b tcb R, ?b41 a b tcb R) = Some (ReplyCap (?t42 a b tcb R) True rights)
 2. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (?a40 a b tcb R, ?b41 a b tcb R) = None \<and> (\<forall>ptr'\<in>descendants_of (?a40 a b tcb R, ?b41 a b tcb R) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap (?t42 a b tcb R) False rights'))\<rbrakk> \<Longrightarrow> False
 3. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None \<and> (\<forall>ptr'\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<forall>ptr'\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> False
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights'); has_reply_cap t s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> has_reply_cap t s
 3. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s
 2. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> has_reply_cap t s
 3. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; \<exists>rights'. caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> has_reply_cap t s
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R rights'. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some (ReplyCap t True R); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; caps_of_state s (a, b) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> has_reply_cap t s
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb R rights'. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; AllowGrant \<in> R; cdt s (t, tcb_cnode_index 2) = None; cte_wp_at ((=) (ReplyCap t True R)) (t, tcb_cnode_index 2) s; cte_wp_at ((=) (ReplyCap t False rights')) (a, b) s\<rbrakk> \<Longrightarrow> has_reply_cap t s
 2. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some cap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some NullCap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some NullCap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>a b tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some NullCap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb); descendants_of (t, tcb_cnode_index 2) (cdt s) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb. \<lbrakk>valid_reply_caps s; valid_objs s; (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s); 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_caps_mdb (cdt s) (caps_of_state s); \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')); valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s (t, tcb_cnode_index 2) = Some NullCap; tcb_state tcb \<noteq> BlockedOnReply; get_tcb t s = Some tcb; halted (tcb_state tcb); descendants_of (t, tcb_cnode_index 2) (cdt s) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!