theory ArchVSpace_AI

lemma vs_refs_add_one':
  "p \<notin> kernel_mapping_slots \<Longrightarrow>
   vs_refs (ArchObj (PageDirectory (pd (p := pde)))) =
   vs_refs (ArchObj (PageDirectory pd))
       - Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
       \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" apply (simp add: vs_refs_def) apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (clarsimp del: disjCI dest!: graph_ofD split: if_split_asm) apply (rule disjI1) apply (rule conjI) apply (rule_tac x="(aa,ba)" in image_eqI) apply simp apply (simp add: graph_of_def) apply clarsimp apply (erule disjE) apply (clarsimp dest!: graph_ofD) apply (rule_tac x="(aa,ba)" in image_eqI) apply simp apply (clarsimp simp: graph_of_def split:if_split_asm) apply clarsimp apply (rule_tac x="(p,x)" in image_eqI) apply simp apply (clarsimp simp: graph_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<notin> kernel_mapping_slots \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) proof (prove)
goal (1 subgoal):
 1. p \<notin> kernel_mapping_slots \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) proof (prove)
goal (1 subgoal):
 1. \<And>x. p \<notin> kernel_mapping_slots \<Longrightarrow> (x \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))) = (x \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. p \<notin> kernel_mapping_slots \<Longrightarrow> ((a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))) = ((a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 2. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 3. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (4 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) = (case (aa, ba) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 3. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 4. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 2. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 3. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; aa \<notin> kernel_mapping_slots; aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); (if aa \<in> kernel_mapping_slots then None else pde_ref (pd aa)) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); (if aa \<in> kernel_mapping_slots then None else pde_ref (pd aa)) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) = (case (aa, ba) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); (if aa \<in> kernel_mapping_slots then None else pde_ref (pd aa)) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))
 3. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>p \<notin> kernel_mapping_slots; (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); (if aa \<in> kernel_mapping_slots then None else pde_ref (pd aa)) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x))
 2. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p \<notin> kernel_mapping_slots; (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<notin> kernel_mapping_slots; pde_ref pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory), x) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>p \<notin> kernel_mapping_slots; pde_ref pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory), x) = (case (p, x) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>x. \<lbrakk>p \<notin> kernel_mapping_slots; pde_ref pde = Some x\<rbrakk> \<Longrightarrow> (p, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<notin> kernel_mapping_slots; pde_ref pde = Some x\<rbrakk> \<Longrightarrow> (p, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(p := pde)) x)) proof (prove)
goal:
No subgoals!