theory ArchKHeap_AI

lemma set_object_pt_not_vs_lookup_pages:
  "\<lbrace>\<lambda>s. \<not>(ref \<unrhd> p') s
    \<and> ((\<exists>\<unrhd>p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of
              Some ptr \<Rightarrow>
                obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and>
                ptr \<noteq> p'
            | None \<Rightarrow> True))\<rbrace>
   set_object p (ArchObj (PageTable pt))
   \<lbrace>\<lambda>_ s. \<not>(ref \<unrhd> p') s\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply (clarsimp simp: obj_at_def) apply (case_tac "(\<exists>\<unrhd>p) s") apply (erule notE) apply clarsimp apply (subst (asm) vs_lookup_pages_def) apply clarsimp apply (erule vs_lookup_pagesI) apply (erule converse_rtrancl_induct) apply simp apply (drule vs_lookup_pages1D) apply (clarsimp simp: obj_at_def split:if_split_asm) apply (case_tac "pa=p") apply (clarsimp simp: vs_refs_pages_def graph_of_def) apply (rename_tac slot pte) apply (erule_tac x=slot in allE) apply (drule_tac R="vs_lookup_pages1 s" in rtranclD) apply clarsimp apply (drule tranclD) apply clarsimp apply (drule vs_lookup_pages1D) apply (clarsimp simp: obj_at_def vs_refs_pages_def) apply clarsimp apply (erule rtrancl_trans[OF r_into_rtrancl, rotated]) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) apply clarsimp apply (erule notE) apply (subst (asm) vs_lookup_pages_def) apply clarsimp apply (rule vs_lookup_pagesI, assumption) apply (erule rtrancl_induct) apply simp apply (drule vs_lookup_pages1D) apply (clarsimp simp: obj_at_def split:if_split_asm) apply (case_tac "pa=p") apply (clarsimp simp: vs_refs_pages_def graph_of_def) apply (rename_tac vs slot pte) apply (erule_tac x=vs in allE) apply (clarsimp simp: vs_lookup_pages_def) apply (drule(1) ImageI, erule (1) notE) apply clarsimp apply (erule rtrancl_trans[OF _ r_into_rtrancl]) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ref, p') \<notin> vs_lookup_pages s \<and> ((\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'))\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_ s. (ref, p') \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ref, p') \<notin> vs_lookup_pages s \<and> ((\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'))\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type (ArchObj (PageTable pt)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)
od \<lbrace>\<lambda>_ s. (ref, p') \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ref, p') \<notin> vs_lookup_pages s \<and> ((\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p')) \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type (ArchObj (PageTable pt)) \<longrightarrow> (ref, p') \<notin> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>(\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); (refa \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>* `` vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>)); (refa \<unrhd> p) s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; ((a, b), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; ((a, b), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a b. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s\<rbrakk> \<Longrightarrow> ((ref, p'), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b ya z. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; (ya, z) \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); (z, ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (z, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ya, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b ya z. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; (ya, z) \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); (z, ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (z, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (ya, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b ya z. \<lbrakk>\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; (z, ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (z, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<exists>rs r pa p' ko. ya = (rs, pa) \<and> z = (r # rs, p') \<and> ko_at ko pa (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>) \<and> (r, p') \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> (ya, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko)\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa = p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a aa b. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) aa) (Some APageTable) # a, b), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((VSRef (UCAST(8 \<rightarrow> 32) aa) (Some APageTable) # a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt aa) = Some b\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; case pte_ref_pages (pt slot) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; case pte_ref_pages (pt slot) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; (VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte) = (ref, p') \<or> (VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte) \<noteq> (ref, p') \<and> ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>+\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>+; obj_at (\<lambda>ko. vs_refs_pages ko = {}) pte s; pte \<noteq> p'\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; obj_at (\<lambda>ko. vs_refs_pages ko = {}) pte s; pte \<noteq> p'; \<exists>z. ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), z) \<in> vs_lookup_pages1 s \<and> (z, ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte aa b. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; obj_at (\<lambda>ko. vs_refs_pages ko = {}) pte s; pte \<noteq> p'; ((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), aa, b) \<in> vs_lookup_pages1 s; ((aa, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s y refa a slot pte aa b. \<lbrakk>((VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pte_ref_pages (pt slot) = Some pte; obj_at (\<lambda>ko. vs_refs_pages ko = {}) pte s; pte \<noteq> p'; ((aa, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<exists>rs r p p' ko. (VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # a, pte) = (rs, p) \<and> (aa, b) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((a, p), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b aa ba rs r pa. \<lbrakk>((aa, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((aa, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; pa = p \<longrightarrow> a = rs \<and> b = p \<and> aa = r # rs \<and> (r, ba) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> a = rs \<and> b = pa \<and> aa = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, ba) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b ba r ko. \<lbrakk>((r # a, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((r # a, ba), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; b \<noteq> p; kheap s b = Some ko; (r, ba) \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y refa a b ba r ko. \<lbrakk>((r # a, ba), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; \<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (refa \<unrhd> p) s; b \<noteq> p; kheap s b = Some ko; (r, ba) \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((a, b), r # a, ba) \<in> vs_lookup_pages1 s
 2. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; (\<exists>\<unrhd> p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of None \<Rightarrow> True | Some ptr \<Rightarrow> obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> ptr \<noteq> p'); kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<not> (\<exists>\<unrhd> p) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>(ref, p') \<notin> vs_lookup_pages s; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref \<unrhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>* `` vs_asid_refs (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s y a b. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; ((a, b), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (ref \<unrhd> p') s proof (prove)
goal (1 subgoal):
 1. \<And>s y a b. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; ((a, b), ref, p') \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> ((a, b), ref, p') \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> ((a, b), a, b) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b ya z. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ya) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (ya, z) \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); ((a, b), ya) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((a, b), z) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b ya z. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ya) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; (ya, z) \<in> vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>); ((a, b), ya) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((a, b), z) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b ya z. \<lbrakk>kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ya) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), ya) \<in> (vs_lookup_pages1 s)\<^sup>*; \<exists>rs r pa p' ko. ya = (rs, pa) \<and> z = (r # rs, p') \<and> ko_at ko pa (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>) \<and> (r, p') \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((a, b), z) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko)\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa = p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b aa ab ba. \<lbrakk>((a, b), aa, p) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, p) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pte_ref_pages (pt ab) = Some ba\<rbrakk> \<Longrightarrow> ((a, b), VSRef (UCAST(8 \<rightarrow> 32) ab) (Some APageTable) # aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b vs slot pte. \<lbrakk>((a, b), vs, p) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), vs, p) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pte_ref_pages (pt slot) = Some pte\<rbrakk> \<Longrightarrow> ((a, b), VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # vs, pte) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b vs slot pte. \<lbrakk>((a, b), vs, p) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), vs, p) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (a, b) \<in> vs_asid_refs (asid_table s); pte_ref_pages (pt slot) = Some pte; (vs, p) \<notin> vs_lookup_pages s\<rbrakk> \<Longrightarrow> ((a, b), VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # vs, pte) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s y a b vs slot pte. \<lbrakk>((a, b), vs, p) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), vs, p) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); (a, b) \<in> vs_asid_refs (asid_table s); pte_ref_pages (pt slot) = Some pte; (vs, p) \<notin> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> ((a, b), VSRef (UCAST(8 \<rightarrow> 32) slot) (Some APageTable) # vs, pte) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b aa ba ab bb rs r pa. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); pa = p \<longrightarrow> aa = rs \<and> ba = p \<and> ab = r # rs \<and> (r, bb) \<in> vs_refs_pages (ArchObj (PageTable pt)); pa = p \<or> aa = rs \<and> ba = pa \<and> ab = r # rs \<and> (\<exists>ko. kheap s pa = Some ko \<and> (r, bb) \<in> vs_refs_pages ko); pa \<noteq> p\<rbrakk> \<Longrightarrow> ((a, b), ab, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b aa ba bb r ko. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; ((a, b), aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); ba \<noteq> p; kheap s ba = Some ko; (r, bb) \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((a, b), r # aa, bb) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s y a b aa ba bb r ko. \<lbrakk>((a, b), aa, ba) \<in> (vs_lookup_pages1 (s\<lparr>kheap := \<lambda>a. if a = p then Some (ArchObj (PageTable pt)) else kheap s a\<rparr>))\<^sup>*; kheap s p = Some y; a_type y = a_type (ArchObj (PageTable pt)); \<forall>ref. (ref, p) \<notin> vs_lookup_pages s; (a, b) \<in> vs_asid_refs (asid_table s); ba \<noteq> p; kheap s ba = Some ko; (r, bb) \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> ((aa, ba), r # aa, bb) \<in> vs_lookup_pages1 s proof (prove)
goal:
No subgoals!