theory Ipc_DR

lemma remove_parent_dummy_when_pending_wp:
  "\<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap) ) s) (cdt s); tcb_at y s\<rbrakk>
  \<Longrightarrow>\<lbrace>(=) (transform s)\<rbrace> remove_parent (y, tcb_pending_op_slot) \<lbrace>\<lambda>r. (=) (transform s)\<rbrace>" apply (clarsimp simp:remove_parent_def valid_def simpler_modify_def transform_def) apply (rule ext) apply (clarsimp simp:transform_cdt_def| rule conjI)+ apply (clarsimp simp: map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at split:if_splits) apply (frule_tac slot'="(aa,bb)" in mdb_cte_at_cte_wp_at') apply simp apply (drule_tac ad = aa in  invalid_cte_wp_at_pending_slot) apply fastforce+ apply (clarsimp simp: map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at split:if_splits) apply (drule_tac ad = ab in invalid_cte_wp_at_pending_slot) apply fastforce+ apply (erule mdb_cte_at_cte_wp_at') apply simp+ apply (clarsimp simp: map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at | rule conjI)+ apply (drule_tac ad = ac in invalid_cte_wp_at_pending_slot) apply fastforce+ apply (erule mdb_cte_at_cte_wp_at) apply simp+ apply clarsimp apply (drule_tac ad = aa in invalid_cte_wp_at_pending_slot) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> remove_parent (y, tcb_pending_op_slot) \<lbrace>\<lambda>r. (=) (transform s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> transform_cdt s = (\<lambda>x. if x = (y, tcb_pending_op_slot) then None else if cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x = Some (y, tcb_pending_op_slot) then cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> (y, tcb_pending_op_slot) else cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> transform_cdt s x = (if x = (y, tcb_pending_op_slot) then None else if cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x = Some (y, tcb_pending_op_slot) then cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> (y, tcb_pending_op_slot) else cdl_cdt \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cdt s (?slot57 a b aa ab ba bb) = Some (aa, bb)
 2. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) s\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 4. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (5 subgoals):
 1. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) s\<rbrakk> \<Longrightarrow> transform_cslot_ptr (aa, ?bd59 a b aa ab ba bb) = (y, tcb_pending_op_slot)
 2. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (aa, ?bd59 a b aa ab ba bb) s
 3. \<And>a b aa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot); cdt s (a, b) = Some (ab, ba); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (aa, bb); transform_cslot_ptr (aa, bb) = (y, tcb_pending_op_slot); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) s; False\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 5. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; map_lift_over transform_cslot_ptr (cdt s) (a, b) = Some (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot)
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> ((\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_option transform_cslot_ptr (cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)))) \<and> ((\<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot)
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, ?bd93 a b aa ba ab ac bb bc) = (y, tcb_pending_op_slot)
 2. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (ab, ?bd93 a b aa ba ab ac bb bc) s
 3. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> ((\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_option transform_cslot_ptr (cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)))) \<and> ((\<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot)
 4. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (ab, bc) s
 2. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> ((\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_option transform_cslot_ptr (cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)))) \<and> ((\<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot)
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab ac bb bc. \<lbrakk>transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cdt s (?slot97 a b aa ba ab ac bb bc) = Some (ab, bc)
 2. \<And>a b aa ba ab ac bb bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (a, b); cdt s (aa, ba) = Some (ac, bb); cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (a, b)) = Some (ab, bc); transform_cslot_ptr (ab, bc) = (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> ((\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> (a = y \<longrightarrow> b \<noteq> tcb_pending_op_slot) \<longrightarrow> Some (y, tcb_pending_op_slot) = map_option transform_cslot_ptr (cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)))) \<and> ((\<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot)
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (a, b) \<noteq> Some (y, tcb_pending_op_slot) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s) (y, tcb_pending_op_slot) = None proof (prove)
goal (2 subgoals):
 1. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None
 2. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> (\<forall>aa ba. transform_cslot_ptr (aa, ba) = (a, b) \<longrightarrow> (aa, ba) \<notin> dom (cdt s)) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (4 subgoals):
 1. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ac, ?bd131 aa ba ab bb ac bc ad bd) = (y, tcb_pending_op_slot)
 2. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (ac, ?bd131 aa ba ab bb ac bc ad bd) s
 3. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None
 4. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> (\<forall>aa ba. transform_cslot_ptr (aa, ba) = (a, b) \<longrightarrow> (aa, ba) \<notin> dom (cdt s)) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (3 subgoals):
 1. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (ac, bc) s
 2. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> (\<forall>aa ba. transform_cslot_ptr (aa, ba) = (a, b) \<longrightarrow> (aa, ba) \<notin> dom (cdt s)) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (3 subgoals):
 1. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot)\<rbrakk> \<Longrightarrow> cdt s (ac, bc) = Some (?slot'135 aa ba ab bb ac bc ad bd)
 2. \<And>aa ba ab bb ac bc ad bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); transform_cslot_ptr (ac, bc) = (y, tcb_pending_op_slot); cdt s (ac, bc) = Some (ad, bd); \<forall>a b. cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = Some (a, b) \<longrightarrow> transform_cslot_ptr (a, b) \<noteq> (y, tcb_pending_op_slot); False\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None
 3. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> (\<forall>aa ba. transform_cslot_ptr (aa, ba) = (a, b) \<longrightarrow> (aa, ba) \<notin> dom (cdt s)) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s\<rbrakk> \<Longrightarrow> (\<forall>aa ba. transform_cslot_ptr (aa, ba) = (a, b) \<longrightarrow> (aa, ba) \<notin> dom (cdt s)) \<longrightarrow> (\<exists>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<and> (a, b) \<in> dom (cdt s)) \<longrightarrow> a = y \<and> b = tcb_pending_op_slot \<longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (1 subgoal):
 1. \<And>aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); tcb_at y s; \<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb)\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal (3 subgoals):
 1. \<And>aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (aa, ?bd150 aa ba ab bb) = (y, tcb_pending_op_slot)
 2. \<And>aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (aa, ?bd150 aa ba ab bb) s
 3. \<And>aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>a b. transform_cslot_ptr (a, b) = (y, tcb_pending_op_slot) \<longrightarrow> (a, b) \<notin> dom (cdt s); transform_cslot_ptr (aa, ba) = (y, tcb_pending_op_slot); cdt s (aa, ba) = Some (ab, bb); False\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) transform_cslot_ptr (y, tcb_pending_op_slot)) = None proof (prove)
goal:
No subgoals!