theory ArchArch_IF

lemma get_pt_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag \<top>\<top> \<top> (get_pt ptr)" unfolding get_pt_def apply (rule equiv_valid_rv_bind) apply (rule get_object_revrv) apply (simp) apply (case_tac rv) apply (simp | rule fail_ev2_l)+ apply (case_tac rv') apply (simp | rule fail_ev2_r)+ apply (rename_tac arch_kernel_obj arch_kernel_obj') apply (case_tac arch_kernel_obj) apply (simp | rule fail_ev2_l)+ apply (case_tac arch_kernel_obj') apply (simp | rule fail_ev2_r | rule return_ev2)+ apply (case_tac arch_kernel_obj') apply (simp | rule fail_ev2_l)+ apply (rule get_object_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) (get_pt ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) (do kobj <- get_object ptr;
case kobj of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W (\<lambda>_. True) (get_object ptr)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable pt) \<Rightarrow> return pt | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' x11 x12. rv = CNode x11 x12 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>rv rv' x2. rv = TCB x2 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<And>rv rv' x3. rv = Endpoint x3 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 4. \<And>rv rv' x4. rv = Notification x4 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 5. \<And>rv rv' x5. rv = ArchObj x5 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q rv) (?Q rv') (case rv of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' x5. rv = ArchObj x5 \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' x5 x11 x12. \<lbrakk>rv = ArchObj x5; rv' = CNode x11 x12\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. \<And>rv rv' x5 x2. \<lbrakk>rv = ArchObj x5; rv' = TCB x2\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 3. \<And>rv rv' x5 x3. \<lbrakk>rv = ArchObj x5; rv' = Endpoint x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 4. \<And>rv rv' x5 x4. \<lbrakk>rv = ArchObj x5; rv' = Notification x4\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 5. \<And>rv rv' x5 x5a. \<lbrakk>rv = ArchObj x5; rv' = ArchObj x5a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q rv') (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case rv' of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' x5 x5a. \<lbrakk>rv = ArchObj x5; rv' = ArchObj x5a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj x5)) (?Q (ArchObj x5a)) (case x5 of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case x5a of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj'. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x1. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = ASIDPool x1\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 4. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 5. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2. \<lbrakk>rv = ArchObj (PageTable x2); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageTable x2))) (?Q (ArchObj arch_kernel_obj')) (return x2) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 4. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2 x1. \<lbrakk>rv = ArchObj (PageTable x2); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2; arch_kernel_obj' = ASIDPool x1\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageTable x2))) (?Q (ArchObj arch_kernel_obj')) (return x2) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2 x2a. \<lbrakk>rv = ArchObj (PageTable x2); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2; arch_kernel_obj' = PageTable x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageTable x2))) (?Q (ArchObj arch_kernel_obj')) (return x2) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2 x3. \<lbrakk>rv = ArchObj (PageTable x2); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2; arch_kernel_obj' = PageDirectory x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageTable x2))) (?Q (ArchObj arch_kernel_obj')) (return x2) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 4. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x2 x41 x42. \<lbrakk>rv = ArchObj (PageTable x2); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageTable x2; arch_kernel_obj' = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageTable x2))) (?Q (ArchObj arch_kernel_obj')) (return x2) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 5. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 6. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 7. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3. \<lbrakk>rv = ArchObj (PageDirectory x3); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageDirectory x3))) (?Q (ArchObj arch_kernel_obj')) fail (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3 x1. \<lbrakk>rv = ArchObj (PageDirectory x3); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3; arch_kernel_obj' = ASIDPool x1\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageDirectory x3))) (?Q (ArchObj arch_kernel_obj')) fail (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 2. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3 x2. \<lbrakk>rv = ArchObj (PageDirectory x3); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3; arch_kernel_obj' = PageTable x2\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageDirectory x3))) (?Q (ArchObj arch_kernel_obj')) fail (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 3. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3 x3a. \<lbrakk>rv = ArchObj (PageDirectory x3); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3; arch_kernel_obj' = PageDirectory x3a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageDirectory x3))) (?Q (ArchObj arch_kernel_obj')) fail (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 4. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x3 x41 x42. \<lbrakk>rv = ArchObj (PageDirectory x3); rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = PageDirectory x3; arch_kernel_obj' = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj (PageDirectory x3))) (?Q (ArchObj arch_kernel_obj')) fail (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 5. \<And>rv rv' arch_kernel_obj arch_kernel_obj' x41 x42. \<lbrakk>rv = ArchObj arch_kernel_obj; rv' = ArchObj arch_kernel_obj'; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>_ _. True) (?Q (ArchObj arch_kernel_obj)) (?Q (ArchObj arch_kernel_obj')) (case arch_kernel_obj of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail) (case arch_kernel_obj' of PageTable x \<Rightarrow> return x | _ \<Rightarrow> fail)
 6. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_object ptr \<lbrace>?Q\<rbrace> proof (prove)
goal:
No subgoals!