theory ArchFinalise_AI

lemma vs_lookup_pages_empty_table:
  "(rs \<unrhd> q)
  (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool Map.empty)),
     arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow>
   (rs \<unrhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)" apply (subst (asm) vs_lookup_pages_def) apply (clarsimp simp: Image_def) apply (drule vs_asid_refs_updateD) apply (erule disjE) apply (drule rtranclD) apply (erule disjE) apply clarsimp apply (fastforce simp: vs_lookup_pages_def) apply clarsimp apply (drule trancl_sub_lift [rotated]) prefer 2 apply (rule vs_lookup_pages_trancl_step) prefer 2 apply assumption apply (fastforce simp: vs_lookup_pages_def) apply (clarsimp simp: obj_at_def vs_lookup_pages1_def vs_refs_pages_def
                  split: if_split_asm) apply clarsimp apply (drule rtranclD) apply (erule disjE) apply clarsimp apply clarsimp apply (drule tranclD) apply clarsimp apply (drule vs_lookup_pages1D) apply (clarsimp simp: obj_at_def vs_refs_pages_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rs \<unrhd> q) (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>) \<Longrightarrow> (rs \<unrhd> q) s \<or> rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> q = p proof (prove)
goal (1 subgoal):
 1. (rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>* `` vs_asid_refs (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)) \<Longrightarrow> (rs \<unrhd> q) s \<or> rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> q = p proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs ((asid_table s)(x \<mapsto> p)); ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s) \<or> a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); (a, b) = (rs, q) \<or> (a, b) \<noteq> (rs, q) \<and> ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); (a, b) = (rs, q)\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); (a, b) \<noteq> (rs, q) \<and> ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 3. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (rs, q) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); (a, b) \<noteq> (rs, q) \<and> ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 3. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); (a, b) \<noteq> (rs, q) \<and> ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> ?r'26 a b
 2. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 3. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> ?r'26 a b
 3. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> ?r29 a b \<in> vs_lookup_pages s
 2. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> (?r29 a b, rs, q) \<in> (vs_lookup_pages1 s)\<^sup>+
 3. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> ?r'26 a b
 4. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> (?r29 a b, rs, q) \<in> (vs_lookup_pages1 s)\<^sup>+
 2. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (?r'26 a b)\<^sup>+\<rbrakk> \<Longrightarrow> ?r29 a b \<in> vs_lookup_pages s
 3. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> ?r'26 a b
 4. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; ((a, b), rs, q) \<in> (vs_lookup_pages1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (a \<unrhd> b) s
 2. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> vs_lookup_pages1 s
 3. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>a b pa p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (a, b) \<in> vs_asid_refs (asid_table s); a = rs \<longrightarrow> b \<noteq> q; (pa, p') \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p') \<in> vs_lookup_pages1 s
 2. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; a = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> b = p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) = (rs, q) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) \<noteq> (rs, q) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) = (rs, q)\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s
 2. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) \<noteq> (rs, q) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) \<noteq> (rs, q) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; [VSRef (UCAST(7 \<rightarrow> 32) x) None] = rs \<longrightarrow> p \<noteq> q; (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; [VSRef (UCAST(7 \<rightarrow> 32) x) None] = rs \<longrightarrow> p \<noteq> q; \<exists>z. (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), z) \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>) \<and> (z, rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; [VSRef (UCAST(7 \<rightarrow> 32) x) None] = rs \<longrightarrow> p \<noteq> q; (([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), a, b) \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>); ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; [VSRef (UCAST(7 \<rightarrow> 32) x) None] = rs \<longrightarrow> p \<noteq> q; ((a, b), rs, q) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>))\<^sup>*; \<exists>rs r pa p' ko. ([VSRef (UCAST(7 \<rightarrow> 32) x) None], p) = (rs, pa) \<and> (a, b) = (r # rs, p') \<and> ko_at ko pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None))), arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(x \<mapsto> p)\<rparr>\<rparr>) \<and> (r, p') \<in> vs_refs_pages ko\<rbrakk> \<Longrightarrow> (rs \<unrhd> q) s proof (prove)
goal:
No subgoals!