theory Tcb_R

lemma checkCapAt_cteInsert_corres:
  "cap_relation new_cap newCap \<Longrightarrow>
   corres dc (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
               and cte_at slot and K (is_cnode_or_valid_arch new_cap
                                        \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap
                                               \<longrightarrow> cap_asid new_cap \<noteq> None))
               and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
                                \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
                                    pt_pd_asid c = pt_pd_asid new_cap) src_slot)
             (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) (cte_map (target, ref))
               and valid_cap' newCap)
     (check_cap_at new_cap src_slot
      (check_cap_at (cap.ThreadCap target) slot
       (cap_insert new_cap src_slot (target, ref))))
     (checkCapAt newCap (cte_map src_slot)
      (checkCapAt (ThreadCap target) (cte_map slot)
       (assertDerived (cte_map src_slot) newCap (cteInsert newCap (cte_map src_slot) (cte_map (target, ref))))))" apply (rule corres_guard_imp) apply (rule_tac P="cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and
                           cte_at slot and
                           cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
                                   \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot
                           and einvs and K (is_cnode_or_valid_arch new_cap
                                            \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap
                                                 \<longrightarrow> cap_asid new_cap \<noteq> None))"
                        and
                        P'="cte_wp_at' (\<lambda>c. cteCap c = NullCap) (cte_map (target, ref))
                            and invs' and valid_cap' newCap"
                       in checkCapAt_corres, assumption) apply (rule checkCapAt_weak_corres, simp) apply (unfold assertDerived_def)[1] apply (rule corres_stateAssert_implied [where P'=\<top>]) apply simp apply (erule cteInsert_corres [OF _ refl refl]) apply clarsimp apply (drule cte_wp_at_norm [where p=src_slot]) apply (case_tac src_slot) apply (clarsimp simp: state_relation_def) apply (drule (1) pspace_relation_cte_wp_at) apply fastforce apply fastforce apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule (2) is_derived_eq [THEN iffD1]) apply (erule cte_wp_at_weakenE, rule TrueI) apply assumption apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def
                            is_cap_simps is_valid_vtable_root_def
                     dest!: cap_master_cap_eqDs) apply (erule(1) checked_insert_is_derived) apply simp apply simp apply fastforce apply (clarsimp simp: cte_wp_at_caps_of_state) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) (check_cap_at new_cap src_slot (check_cap_at (cap.ThreadCap target) slot (cap_insert new_cap src_slot (target, ref)))) (checkCapAt newCap (cte_map src_slot) (checkCapAt (capability.ThreadCap target) (cte_map slot) (assertDerived (cte_map src_slot) newCap (cteInsert newCap (cte_map src_slot) (cte_map (target, ref)))))) proof (prove)
goal (3 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?Q ?Q' (check_cap_at new_cap src_slot (check_cap_at (cap.ThreadCap target) slot (cap_insert new_cap src_slot (target, ref)))) (checkCapAt newCap (cte_map src_slot) (checkCapAt (capability.ThreadCap target) (cte_map slot) (assertDerived (cte_map src_slot) newCap (cteInsert newCap (cte_map src_slot) (cte_map (target, ref))))))
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?Q4 ?Q'4 (check_cap_at (cap.ThreadCap target) slot (cap_insert new_cap src_slot (target, ref))) (checkCapAt (capability.ThreadCap target) (cte_map slot) (assertDerived (cte_map src_slot) newCap (cteInsert newCap (cte_map src_slot) (cte_map (target, ref)))))
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> ?Q'4 s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?P5 ?P'5 (cap_insert new_cap src_slot (target, ref)) (assertDerived (cte_map src_slot) newCap (cteInsert newCap (cte_map src_slot) (cte_map (target, ref))))
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (?P5 and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (?P'5 and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?P5 ?P'5 (cap_insert new_cap src_slot (target, ref)) (do stateAssert (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s) [];
cteInsert newCap (cte_map src_slot) (cte_map (target, ref))
od)
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (?P5 and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (?P'5 and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (6 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?P10 ?P'5 (cap_insert new_cap src_slot (target, ref)) (K_bind (cteInsert newCap (cte_map src_slot) (cte_map (target, ref))) ())
 2. \<And>s s'. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; ?P10 s; True; ?P'5 s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (?P10 and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (?P'5 and pspace_aligned' and pspace_distinct') s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 6. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (6 subgoals):
 1. cap_relation new_cap newCap \<Longrightarrow> corres dc ?P10 ?P'5 (cap_insert new_cap src_slot (target, ref)) (cteInsert newCap (cte_map src_slot) (cte_map (target, ref)))
 2. \<And>s s'. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; ?P10 s; True; ?P'5 s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (?P10 and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (?P'5 and pspace_aligned' and pspace_distinct') s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 6. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s)) s; True; (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref))) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; src_slot \<noteq> (target, ref); cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; src_slot \<noteq> (target, ref); cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; \<exists>c. cte_wp_at ((=) c) src_slot s \<and> is_derived (cdt s) src_slot new_cap c\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b. \<lbrakk>cap_relation new_cap newCap; (s, s') \<in> state_relation; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; src_slot \<noteq> (target, ref); cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; \<exists>c. cte_wp_at ((=) c) src_slot s \<and> is_derived (cdt s) src_slot new_cap c; src_slot = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map src_slot) newCap \<circ> cteCap) (cte_map src_slot) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); pspace_relation (kheap s) (ksPSpace s'); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map (a, b)) newCap \<circ> cteCap) (cte_map (a, b)) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (7 subgoals):
 1. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 3. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map (a, b)) newCap \<circ> cteCap) (cte_map (a, b)) s'
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 6. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 7. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (6 subgoals):
 1. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map (a, b)) newCap \<circ> cteCap) (cte_map (a, b)) s'
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 6. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b c. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_wp_at' (\<lambda>cte. cap_relation c (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (is_derived' (ctes_of s') (cte_map (a, b)) newCap \<circ> cteCap) (cte_map (a, b)) s'
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b c cte ctea. \<lbrakk>cap_relation new_cap newCap; valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; ctes_of s' (cte_map (target, ref)) = Some cte; cteCap cte = capability.NullCap; ctes_of s' (cte_map (a, b)) = Some ctea; cap_relation c (cteCap ctea)\<rbrakk> \<Longrightarrow> is_derived' (ctes_of s') (cte_map (a, b)) newCap (cteCap ctea)
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (6 subgoals):
 1. \<And>s s' a b c cte ctea. \<lbrakk>valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; ctes_of s' (cte_map (target, ref)) = Some cte; cteCap cte = capability.NullCap; ctes_of s' (cte_map (a, b)) = Some ctea; cap_relation c (cteCap ctea)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s
 2. \<And>s s' a b c cte ctea. \<lbrakk>valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; ctes_of s' (cte_map (target, ref)) = Some cte; cteCap cte = capability.NullCap; ctes_of s' (cte_map (a, b)) = Some ctea; cap_relation c (cteCap ctea)\<rbrakk> \<Longrightarrow> is_derived (cdt s) (a, b) new_cap c
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 6. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s s' a b c cte ctea. \<lbrakk>valid_objs s; pspace_distinct' s'; pspace_distinct s; pspace_aligned' s'; pspace_aligned s; valid_mdb' s'; valid_mdb s; valid_cap' newCap s'; valid_list s; a = target \<longrightarrow> b \<noteq> ref; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; src_slot = (a, b); cte_wp_at ((=) c) (a, b) s; is_derived (cdt s) (a, b) new_cap c; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; ctes_of s' (cte_map (target, ref)) = Some cte; cteCap cte = capability.NullCap; ctes_of s' (cte_map (a, b)) = Some ctea; cap_relation c (cteCap ctea)\<rbrakk> \<Longrightarrow> is_derived (cdt s) (a, b) new_cap c
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None))) s \<and> cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src_slot \<noteq> (target, ref)) and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and (\<lambda>s. cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) slot and invs) s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; cte_wp_at (\<lambda>_. True) slot s; cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot s; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_mdb s \<and> src_slot \<noteq> (target, ref) \<and> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; cte_wp_at (\<lambda>_. True) slot s; cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot s; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); cte_wp_at (same_object_as new_cap) src_slot s\<rbrakk> \<Longrightarrow> src_slot \<noteq> (target, ref) \<and> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s a b. \<lbrakk>cap_relation new_cap newCap; cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) s; cte_wp_at (\<lambda>_. True) slot s; cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot s; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); cte_wp_at (same_object_as new_cap) src_slot s; src_slot = (a, b)\<rbrakk> \<Longrightarrow> src_slot \<noteq> (target, ref) \<and> cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa\<rbrakk> \<Longrightarrow> (a = target \<longrightarrow> b \<noteq> ref) \<and> is_derived (cdt s) (a, b) new_cap capa
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa\<rbrakk> \<Longrightarrow> a = target \<longrightarrow> b \<noteq> ref
 2. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa\<rbrakk> \<Longrightarrow> is_derived (cdt s) (a, b) new_cap capa
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (5 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa; cap_master_cap new_cap = cap_master_cap capa\<rbrakk> \<Longrightarrow> a = target \<longrightarrow> b \<noteq> ref
 2. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa\<rbrakk> \<Longrightarrow> is_derived (cdt s) (a, b) new_cap capa
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 5. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa; same_object_as new_cap capa\<rbrakk> \<Longrightarrow> is_derived (cdt s) (a, b) new_cap capa
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (4 subgoals):
 1. \<And>s a b cap capa. \<lbrakk>cap_relation new_cap newCap; caps_of_state s (target, ref) = Some cap.NullCap; invs s; valid_list s; valid_sched s; is_cnode_or_valid_arch new_cap; is_pt_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); is_pd_cap new_cap \<longrightarrow> (\<exists>y. cap_asid new_cap = Some y); src_slot = (a, b); caps_of_state s slot = Some cap; obj_refs capa = obj_refs new_cap \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> obj_refs new_cap = obj_refs capa \<longrightarrow> table_cap_ref capa = table_cap_ref new_cap \<and> pt_pd_asid capa = pt_pd_asid new_cap
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 4. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap) s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' newCap and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and pspace_aligned' and pspace_distinct') s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) s \<and> invs' s \<and> valid_cap' newCap s \<and> cte_wp_at' (global.sameObjectAs newCap \<circ> cteCap) (cte_map src_slot) s\<rbrakk> \<Longrightarrow> pspace_distinct' s \<and> pspace_aligned' s \<and> valid_mdb' s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 3. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; (einvs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref) and cte_wp_at (\<lambda>_. True) slot and cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap \<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and> pt_pd_asid c = pt_pd_asid new_cap) src_slot and einvs and K (is_cnode_or_valid_arch new_cap \<and> (is_pt_cap new_cap \<or> is_pd_cap new_cap \<longrightarrow> cap_asid new_cap \<noteq> None)) and cte_wp_at (\<lambda>_. True) src_slot and invs) s
 2. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) and valid_cap' newCap) s\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) (cte_map (target, ref)) and invs' and valid_cap' newCap and pspace_aligned' and pspace_distinct') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_relation new_cap newCap; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (target, ref)) s; valid_cap' newCap s\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s proof (prove)
goal:
No subgoals!