theory CSpace_R

lemma mdb_chunked_prev_update:
  "mdb_chunked (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = mdb_chunked m" apply (simp add: mdb_chunked_def trancl_prev_update rtrancl_prev_update is_chunk_def) apply (rule iffI) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=cap in allE) apply (simp add: modify_map_if split: if_split_asm) apply (erule impE, blast) apply (erule allE, erule impE, blast) apply clarsimp apply blast apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=cap in allE) apply (simp add: modify_map_if split: if_split_asm) apply (erule impE, blast) apply clarsimp apply blast apply (erule allE, erule impE, blast) apply clarsimp apply blast apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = mdb_chunked m proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))) = (\<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))) proof (prove)
goal (2 subgoals):
 1. \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>\<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))); m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>(\<exists>na. (x = p \<longrightarrow> mdbPrev_update f n = na) \<and> (x = p \<or> na = n)) \<longrightarrow> (\<forall>cap'a. (\<exists>n'a. (x = p' \<longrightarrow> cap' = cap'a \<and> mdbPrev_update f n' = n'a) \<and> (x = p' \<or> cap'a = cap' \<and> n'a = n')) \<longrightarrow> global.sameRegionAs cap cap'a \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap'a cap'')))); m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap'a. (\<exists>n'a. (x = p' \<longrightarrow> cap' = cap'a \<and> mdbPrev_update f n' = n'a) \<and> (x = p' \<or> cap'a = cap' \<and> n'a = n')) \<longrightarrow> global.sameRegionAs cap cap'a \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap'a cap'')))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p = Some (CTE cap n); m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x = p'' \<or> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))
 2. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (1 subgoal):
 1. \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) \<Longrightarrow> \<forall>p p' cap. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>\<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE cap n); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x = p; \<exists>node. m p = Some (CTE cap node) \<and> mdbPrev_update f node = n\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); m p = Some (CTE cap n); x = p'; \<exists>node. m p' = Some (CTE cap' node) \<and> mdbPrev_update f node = n'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 3. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'; x = p; \<exists>node. m p = Some (CTE cap node) \<and> mdbPrev_update f node = n; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); m p = Some (CTE cap n); x = p'; \<exists>node. m p' = Some (CTE cap' node) \<and> mdbPrev_update f node = n'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 3. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (3 subgoals):
 1. \<And>p' cap cap' n' node. \<lbrakk>m p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; x \<noteq> p'; m \<turnstile> x \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ x; m x = Some (CTE cap node); m \<turnstile> x \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ x \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* x \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))\<rbrakk> \<Longrightarrow> (m \<turnstile> x \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ x \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* x \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); m p = Some (CTE cap n); x = p'; \<exists>node. m p' = Some (CTE cap' node) \<and> mdbPrev_update f node = n'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 3. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); m p = Some (CTE cap n); x = p'; \<exists>node. m p' = Some (CTE cap' node) \<and> mdbPrev_update f node = n'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; m p = Some (CTE cap n); x = p'; \<exists>node. m p' = Some (CTE cap' node) \<and> mdbPrev_update f node = n'; global.sameRegionAs cap cap' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (p' = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (p' \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (2 subgoals):
 1. \<And>p cap n cap' node. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> x; m p = Some (CTE cap n); m \<turnstile> p \<leadsto>\<^sup>+ x \<or> m \<turnstile> x \<leadsto>\<^sup>+ p; m x = Some (CTE cap' node); m \<turnstile> p \<leadsto>\<^sup>+ x \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* x \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')); m \<turnstile> x \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ x \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* x \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> x \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap'')))
 2. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))); x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; x \<noteq> p; m p = Some (CTE cap n); x \<noteq> p'; m p' = Some (CTE cap' n'); m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')); m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap''))\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. (x = p'' \<longrightarrow> (\<exists>node. m p'' = Some (CTE cap'' node) \<and> mdbPrev_update f node = n'')) \<and> (x \<noteq> p'' \<longrightarrow> m p'' = Some (CTE cap'' n''))) \<and> global.sameRegionAs cap' cap''))) proof (prove)
goal:
No subgoals!