theory Example_Valid_StateH

lemma mdb_prev_s0H:
  "p \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' =
     (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or>
     p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or>
     p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or>
     p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or>
     p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or>
     p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30)" apply (rule iffI) apply (simp add: mdb_prev_def) apply (elim exE conjE) apply (frule map_to_ctes_kh0H_SomeD) apply (elim disjE, simp_all)[1] apply clarsimp apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E s0_ptrs_aligned split: if_split_asm) apply clarsimp apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E ucast_shiftr_3 ucast_shiftr_2 s0_ptrs_aligned split: if_split_asm) apply clarsimp apply (clarsimp simp: kh0H_all_obj_def' to_bl_use_of_bl the_nat_to_bl_simps cte_level_bits_def ucast_shiftr_13E ucast_shiftr_3 ucast_shiftr_2 s0_ptrs_aligned split: if_split_asm) apply (clarsimp simp: mdb_prev_def map_to_ctes_kh0H_dom) apply (elim disjE, simp_all add: kh0H_all_obj_def') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' = (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> 0; map_to_ctes kh0H \<turnstile> p \<leftarrow> p'\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> 0; \<exists>z. map_to_ctes kh0H p' = Some z \<and> p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p \<noteq> 0; map_to_ctes kh0H p' = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p \<noteq> 0; map_to_ctes kh0H p' = Some z; p = mdbPrev (cteMDBNode z); p' = idle_tcb_ptr \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = idle_tcb_ptr + 0x10 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = idle_tcb_ptr + 0x20 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = idle_tcb_ptr + 0x30 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = idle_tcb_ptr + 0x40 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = Low_tcb_ptr \<and> z = CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB (Low_cnode_ptr + 0x20) 0 False False) \<or> p' = Low_tcb_ptr + 0x10 \<and> z = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB (Low_cnode_ptr + 0x30) 0 False False) \<or> p' = Low_tcb_ptr + 0x20 \<and> z = CTE (capability.ReplyCap Low_tcb_ptr True True) (MDB 0 0 True True) \<or> p' = Low_tcb_ptr + 0x30 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = Low_tcb_ptr + 0x40 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = High_tcb_ptr \<and> z = CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB (High_cnode_ptr + 0x20) 0 False False) \<or> p' = High_tcb_ptr + 0x10 \<and> z = CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB (High_cnode_ptr + 0x30) 0 False False) \<or> p' = High_tcb_ptr + 0x20 \<and> z = CTE (capability.ReplyCap High_tcb_ptr True True) (MDB 0 0 True True) \<or> p' = High_tcb_ptr + 0x30 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = High_tcb_ptr + 0x40 \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' = irq_cnode_ptr \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' \<in> irq_node_offs_range \<and> z = CTE capability.NullCap (MDB 0 0 False False) \<or> p' \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte_cte Silc_cnode_ptr p' \<noteq> None \<and> z = the (Silc_cte_cte Silc_cnode_ptr p') \<or> p' \<in> cnode_offs_range High_cnode_ptr \<and> High_cte_cte High_cnode_ptr p' \<noteq> None \<and> z = the (High_cte_cte High_cnode_ptr p') \<or> p' \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte_cte Low_cnode_ptr p' \<noteq> None \<and> z = the (Low_cte_cte Low_cnode_ptr p')\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Silc_cte_cte Silc_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))); p' \<in> cnode_offs_range Silc_cnode_ptr \<and> (\<exists>y. Silc_cte_cte Silc_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Silc_cte_cte Silc_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = High_cte_cte High_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))); p' \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Low_cte_cte Low_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))); p' \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 4. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>mdbPrev (cteMDBNode y) \<noteq> 0; map_to_ctes kh0H p' = Some y; p = mdbPrev (cteMDBNode y); p' \<in> cnode_offs_range Silc_cnode_ptr; Silc_cte_cte Silc_cnode_ptr p' = Some y; mdbPrev (cteMDBNode y) = Low_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> Silc_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Silc_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Low_tcb_ptr \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x20; mdbPrev (cteMDBNode y) = Low_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x30; mdbPrev (cteMDBNode y) = High_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode y) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20
 2. \<lbrakk>mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = High_cte_cte High_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))); p' \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Low_cte_cte Low_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))); p' \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 4. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = High_cte_cte High_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))); p' \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. High_cte_cte High_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (High_cte_cte High_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Low_cte_cte Low_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))); p' \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>mdbPrev (cteMDBNode y) \<noteq> 0; map_to_ctes kh0H p' = Some y; p = mdbPrev (cteMDBNode y); p' \<in> cnode_offs_range High_cnode_ptr; High_cte_cte High_cnode_ptr p' = Some y; mdbPrev (cteMDBNode y) = Low_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> Silc_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Silc_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Low_tcb_ptr \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x20; mdbPrev (cteMDBNode y) = Low_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x30; mdbPrev (cteMDBNode y) = High_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode y) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20
 2. \<lbrakk>mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Low_cte_cte Low_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))); p' \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) \<noteq> 0; map_to_ctes kh0H p' = Low_cte_cte Low_cnode_ptr p'; p = mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))); p' \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. Low_cte_cte Low_cnode_ptr p' = Some y)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> mdbPrev (cteMDBNode (the (Low_cte_cte Low_cnode_ptr p'))) = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>mdbPrev (cteMDBNode y) \<noteq> 0; map_to_ctes kh0H p' = Some y; p = mdbPrev (cteMDBNode y); p' \<in> cnode_offs_range Low_cnode_ptr; Low_cte_cte Low_cnode_ptr p' = Some y; mdbPrev (cteMDBNode y) = Low_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> Silc_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Silc_cnode_ptr + 0x13E0 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x13E0; mdbPrev (cteMDBNode y) = Low_tcb_ptr \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x20; mdbPrev (cteMDBNode y) = Low_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> Low_cnode_ptr + 0x30; mdbPrev (cteMDBNode y) = High_tcb_ptr + 0x10 \<longrightarrow> p' \<noteq> High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode y) = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20
 2. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leftarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> \<exists>z. map_to_ctes kh0H p' = Some z \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal:
No subgoals!