theory ArchFinalise_AI

lemma vs_lookup_empty_table:
  "(rs \<rhd> 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 \<rhd> q) s \<or> (rs = [VSRef (ucast x) None] \<and> q = p)" apply (erule vs_lookupE) apply clarsimp apply (drule vs_asid_refs_updateD) apply (erule disjE) apply (drule rtranclD) apply (erule disjE) apply clarsimp apply (fastforce simp: vs_lookup_def) apply clarsimp apply (drule trancl_sub_lift [rotated]) prefer 2 apply (rule vs_lookup_trancl_step) prefer 2 apply assumption apply (fastforce simp: vs_lookup_def) apply (clarsimp simp: obj_at_def vs_lookup1_def vs_refs_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_lookup1D) apply (clarsimp simp: obj_at_def vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rs \<rhd> 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 \<rhd> q) s \<or> rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> q = p proof (prove)
goal (1 subgoal):
 1. \<And>ref' p'. \<lbrakk>(ref', p') \<in> 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>)); ((ref', p'), rs, q) \<in> (vs_lookup1 (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 \<rhd> q) s \<or> rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> q = p proof (prove)
goal (1 subgoal):
 1. \<And>ref' p'. \<lbrakk>(ref', p') \<in> vs_asid_refs ((asid_table s)(x \<mapsto> p)); ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s) \<or> ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); (ref', p') = (rs, q) \<or> (ref', p') \<noteq> (rs, q) \<and> ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); (ref', p') = (rs, q)\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); (ref', p') \<noteq> (rs, q) \<and> ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 3. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> 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 \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); (ref', p') \<noteq> (rs, q) \<and> ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 3. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); (ref', p') \<noteq> (rs, q) \<and> ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> ?r'26 ref' p'
 2. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 3. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s
 2. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> ?r'26 ref' p'
 3. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (4 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> ?r29 ref' p' \<in> vs_lookup s
 2. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> (?r29 ref' p', rs, q) \<in> (vs_lookup1 s)\<^sup>+
 3. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> ?r'26 ref' p'
 4. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (4 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> (?r29 ref' p', rs, q) \<in> (vs_lookup1 s)\<^sup>+
 2. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (?r'26 ref' p')\<^sup>+\<rbrakk> \<Longrightarrow> ?r29 ref' p' \<in> vs_lookup s
 3. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> ?r'26 ref' p'
 4. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (3 subgoals):
 1. \<And>ref' p'. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; ((ref', p'), rs, q) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (ref' \<rhd> p') s
 2. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> vs_lookup1 s
 3. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (2 subgoals):
 1. \<And>ref' p' pa p'a. \<lbrakk>rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; (ref', p') \<in> vs_asid_refs (asid_table s); ref' = rs \<longrightarrow> p' \<noteq> q; (pa, p'a) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>)\<rbrakk> \<Longrightarrow> (pa, p'a) \<in> vs_lookup1 s
 2. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (1 subgoal):
 1. \<And>ref' p'. \<lbrakk>((ref', p'), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p; ref' = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<and> p' = p\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(([VSRef (UCAST(7 \<rightarrow> 32) x) None], p), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*; rs = [VSRef (UCAST(7 \<rightarrow> 32) x) None] \<longrightarrow> q \<noteq> p\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> 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 \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>+\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>) \<and> (z, rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>); ((a, b), rs, q) \<in> (vs_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<rparr>))\<^sup>*\<rbrakk> \<Longrightarrow> (rs \<rhd> 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_lookup1 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool (\<lambda>x. None)))\<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)))\<rparr>) \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> (rs \<rhd> q) s proof (prove)
goal:
No subgoals!