theory ArchCSpaceInvPre_AI

lemma set_cap_unique_table_caps:
  "\<lbrace>\<lambda>s. unique_table_caps (caps_of_state s)
      \<and> ((is_pt_cap cap \<or> is_pd_cap cap)
             \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow>
                  (is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap)
                    \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None)
                    \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)
             \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap
                                              \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap')
                                              \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. unique_table_caps (caps_of_state s)\<rbrace>" apply wp apply (simp only: unique_table_caps_def) apply (elim conjE) apply (erule impCE) apply clarsimp apply (erule impCE) prefer 2 apply (simp del: imp_disjL) apply (thin_tac "\<forall>a b. P a b" for P) apply (auto simp: cte_wp_at_caps_of_state)[1] apply (clarsimp simp del: imp_disjL del: allI) apply (case_tac "cap_asid cap \<noteq> None") apply (clarsimp del: allI) apply (elim allEI | rule impI)+ apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] apply (elim allEI) apply (intro conjI impI) apply (elim allEI) apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] apply (elim allEI) apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unique_table_caps (caps_of_state s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. unique_table_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. unique_table_caps (caps_of_state s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)) \<Longrightarrow> unique_table_caps ((caps_of_state s)(ptr \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)) \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (is_pt_cap cap \<or> is_pd_cap cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); \<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b))))
 2. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b))))
 2. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); \<not> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)\<rbrakk> \<Longrightarrow> \<forall>p p' capa cap'. ((caps_of_state s)(ptr \<mapsto> cap)) p = Some capa \<longrightarrow> ((caps_of_state s)(ptr \<mapsto> cap)) p' = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (2 subgoals):
 1. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; cap_asid cap \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b))))
 2. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (2 subgoals):
 1. \<And>s oldcap y. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; obj_refs oldcap = obj_refs cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> \<forall>a b. (a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))
 2. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (2 subgoals):
 1. \<And>s oldcap y a b aa ba capa. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; obj_refs oldcap = obj_refs cap; cap_asid cap = Some y; (a, b) \<noteq> ptr; (aa, ba) = ptr; caps_of_state s (a, b) = Some capa \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s (a, b) = Some capa; cap_asid capa = None; obj_refs cap = obj_refs capa\<rbrakk> \<Longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)
 2. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (1 subgoal):
 1. \<And>s oldcap. \<lbrakk>\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>a b. ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (1 subgoal):
 1. \<And>s oldcap a b. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; \<forall>aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))\<rbrakk> \<Longrightarrow> ((a, b) = ptr \<longrightarrow> (\<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))))) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (\<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)))) proof (prove)
goal (2 subgoals):
 1. \<And>s oldcap a b. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; \<forall>aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); (a, b) = ptr\<rbrakk> \<Longrightarrow> \<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)))
 2. \<And>s oldcap a b. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; \<forall>aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); (a, b) \<noteq> ptr\<rbrakk> \<Longrightarrow> \<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) proof (prove)
goal (2 subgoals):
 1. \<And>s oldcap a b aa ba. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; (a, b) = ptr; \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))\<rbrakk> \<Longrightarrow> ((aa, ba) = ptr \<longrightarrow> cap_asid cap = None \<longrightarrow> (is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)))
 2. \<And>s oldcap a b. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; \<forall>aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); (a, b) \<noteq> ptr\<rbrakk> \<Longrightarrow> \<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) proof (prove)
goal (1 subgoal):
 1. \<And>s oldcap a b. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; \<forall>aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b)); (a, b) \<noteq> ptr\<rbrakk> \<Longrightarrow> \<forall>aa ba. (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) proof (prove)
goal (1 subgoal):
 1. \<And>s oldcap a b aa ba. \<lbrakk>caps_of_state s ptr = Some oldcap; is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap; cap_asid cap = None \<longrightarrow> cap_asid oldcap = None; obj_refs oldcap = obj_refs cap; \<not> cap_asid cap \<noteq> None; (a, b) \<noteq> ptr; \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> aa = a \<and> ba = b))\<rbrakk> \<Longrightarrow> (aa, ba) = ptr \<longrightarrow> (\<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> cap_asid capa = None \<longrightarrow> obj_refs cap = obj_refs capa \<longrightarrow> (is_pd_cap capa \<longrightarrow> is_pd_cap cap \<longrightarrow> aa = a \<and> ba = b) \<and> (is_pt_cap capa \<longrightarrow> is_pt_cap cap \<longrightarrow> aa = a \<and> ba = b)) proof (prove)
goal:
No subgoals!