theory CSpace1_R

lemma mdb_untyped'_preserve_oneway:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
  isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
  \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte')
  \<and> isNotificationCap (cteCap cte)  = isNotificationCap (cteCap cte')
  \<and> (isNotificationCap (cteCap cte) \<longrightarrow> (capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')))
  \<and> (isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte'))
  \<and> (isEndpointCap (cteCap cte) \<longrightarrow> (capEPBadge (cteCap cte) = capEPBadge (cteCap cte')))
  \<and> capRange (cteCap cte) = capRange (cteCap cte')
  \<and> cteMDBNode cte = cteMDBNode cte'"
  assumes sameRegion:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> cteMDBNode cte = cteMDBNode cte'
  \<and> sameRegionAs (cteCap cte) = sameRegionAs (cteCap cte')
  \<and> (\<lambda>x. sameRegionAs x (cteCap cte)) = (\<lambda>x. sameRegionAs x (cteCap cte'))"
  assumes mdb_next:"\<And>p. mdb_next m p = mdb_next m' p"
  shows
  "untyped_mdb' m \<Longrightarrow> untyped_mdb' m'" apply (clarsimp simp:untyped_mdb'_def) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply (frule iffD2[OF dom,OF domI],rotate_tac) apply clarsimp apply (case_tac y,case_tac ya) apply (frule misc) apply fastforce apply clarsimp apply (frule_tac x = p' in misc) apply fastforce apply (frule_tac x = p in misc) apply assumption apply clarsimp apply (clarsimp simp: descendants_of'_def Invariants_H.subtree_def) apply (erule_tac f1 = "\<lambda>x. lfp x y" for y in iffD1[OF arg_cong,rotated]) apply (rule ext)+ apply (subgoal_tac "\<And>p p'. (m \<turnstile> p \<leadsto> p') = (m' \<turnstile> p \<leadsto> p')") apply (thin_tac "P" for P)+ apply (subgoal_tac "(m \<turnstile> p parentOf x) = (m' \<turnstile> p parentOf x)") apply fastforce apply (rule parentOf_preserve[OF dom]) apply (simp add:misc sameRegion mdb_next mdb_next_rel_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' m \<Longrightarrow> untyped_mdb' m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p = Some (CTE c n); isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c; m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); p \<in> dom m; m' p = Some (CTE c n)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); p \<in> dom m; m' p = Some (CTE c n); p' \<in> dom m; isUntypedCap c\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' y ya. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' y ya x1 x2 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' y ya x1 x2 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a\<rbrakk> \<Longrightarrow> m' p = Some (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)
 2. \<And>p p' c n c' n' y ya x1 x2 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)) \<and> isNotificationCap (cteCap y) = isNotificationCap (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)) \<and> (isNotificationCap (cteCap y) \<longrightarrow> capNtfnBadge (cteCap y) = capNtfnBadge (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a))) \<and> isEndpointCap (cteCap y) = isEndpointCap (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)) \<and> (isEndpointCap (cteCap y) \<longrightarrow> capEPBadge (cteCap y) = capEPBadge (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a))) \<and> capRange (cteCap y) = capRange (cteCap (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)) \<and> cteMDBNode y = cteMDBNode (?cte'38 p p' c n c' n' y ya x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' y ya x1 x2 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. y = CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. ya = CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m' p = Some (CTE c n); isUntypedCap c; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> isNotificationCap (cteCap y) = isNotificationCap (cteCap (CTE c n)) \<and> (isNotificationCap (cteCap y) \<longrightarrow> capNtfnBadge (cteCap y) = capNtfnBadge (cteCap (CTE c n))) \<and> isEndpointCap (cteCap y) = isEndpointCap (cteCap (CTE c n)) \<and> (isEndpointCap (cteCap y) \<longrightarrow> capEPBadge (cteCap y) = capEPBadge (cteCap (CTE c n))) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c\<rbrakk> \<Longrightarrow> m' p' = Some (?cte'73 p p' c n c' n' x1 x1a x2a)
 2. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; isUntypedCap (cteCap (CTE x1a x2a)) = isUntypedCap (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a)) \<and> untypedRange (cteCap (CTE x1a x2a)) = untypedRange (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a)) \<and> isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a)) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a)) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a))) \<and> capRange (cteCap (CTE x1a x2a)) = capRange (cteCap (?cte'73 p p' c n c' n' x1 x1a x2a)) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (?cte'73 p p' c n c' n' x1 x1a x2a)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; isUntypedCap (cteCap (CTE x1a x2a)) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap (CTE x1a x2a)) = untypedRange (cteCap (CTE c' n')) \<and> isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (CTE c' n'))) \<and> capRange (cteCap (CTE x1a x2a)) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; isUntypedCap (cteCap (CTE x1a x2a)) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap (CTE x1a x2a)) = untypedRange (cteCap (CTE c' n')) \<and> isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (CTE c' n'))) \<and> capRange (cteCap (CTE x1a x2a)) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> m' p = Some (?cte'176 p p' c n c' n' x1 x1a x2a)
 2. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; isUntypedCap (cteCap (CTE x1a x2a)) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap (CTE x1a x2a)) = untypedRange (cteCap (CTE c' n')) \<and> isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (CTE c' n'))) \<and> capRange (cteCap (CTE x1a x2a)) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (CTE c' n'); isUntypedCap (cteCap (CTE x1 n)) = isUntypedCap (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a)) \<and> untypedRange (cteCap (CTE x1 n)) = untypedRange (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a)) \<and> isNotificationCap (cteCap (CTE x1 n)) = isNotificationCap (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a)) \<and> (isNotificationCap (cteCap (CTE x1 n)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 n)) = capNtfnBadge (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a))) \<and> isEndpointCap (cteCap (CTE x1 n)) = isEndpointCap (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a)) \<and> (isEndpointCap (cteCap (CTE x1 n)) \<longrightarrow> capEPBadge (cteCap (CTE x1 n)) = capEPBadge (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a))) \<and> capRange (cteCap (CTE x1 n)) = capRange (cteCap (?cte'176 p p' c n c' n' x1 x1a x2a)) \<and> cteMDBNode (CTE x1 n) = cteMDBNode (?cte'176 p p' c n c' n' x1 x1a x2a)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a x2a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap x1a \<longrightarrow> capRange x1a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a x2a); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; isUntypedCap (cteCap (CTE x1a x2a)) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap (CTE x1a x2a)) = untypedRange (cteCap (CTE c' n')) \<and> isNotificationCap (cteCap (CTE x1a x2a)) = isNotificationCap (cteCap (CTE c' n')) \<and> (isNotificationCap (cteCap (CTE x1a x2a)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1a x2a)) = capNtfnBadge (cteCap (CTE c' n'))) \<and> isEndpointCap (cteCap (CTE x1a x2a)) = isEndpointCap (cteCap (CTE c' n')) \<and> (isEndpointCap (cteCap (CTE x1a x2a)) \<longrightarrow> capEPBadge (cteCap (CTE x1a x2a)) = capEPBadge (cteCap (CTE c' n'))) \<and> capRange (cteCap (CTE x1a x2a)) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode (CTE x1a x2a) = cteMDBNode (CTE c' n'); isUntypedCap (cteCap (CTE x1 n)) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap (CTE x1 n)) = untypedRange (cteCap (CTE c n)) \<and> isNotificationCap (cteCap (CTE x1 n)) = isNotificationCap (cteCap (CTE c n)) \<and> (isNotificationCap (cteCap (CTE x1 n)) \<longrightarrow> capNtfnBadge (cteCap (CTE x1 n)) = capNtfnBadge (cteCap (CTE c n))) \<and> isEndpointCap (cteCap (CTE x1 n)) = isEndpointCap (cteCap (CTE c n)) \<and> (isEndpointCap (cteCap (CTE x1 n)) \<longrightarrow> capEPBadge (cteCap (CTE x1 n)) = capEPBadge (cteCap (CTE c n))) \<and> capRange (cteCap (CTE x1 n)) = capRange (cteCap (CTE c n)) \<and> cteMDBNode (CTE x1 n) = cteMDBNode (CTE c n)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p' \<in> descendants_of' p m; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; lfp (\<lambda>pa x. m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) p'; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> lfp (\<lambda>pa x. m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x)) p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> (\<lambda>pa x. m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (\<lambda>pa x. m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x)) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x1 x1a pa x. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x)) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x1a pa x. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'; \<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x))
 2. \<And>p p' c n c' n' x1 x1a pa x pb p'a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> m \<turnstile> pb \<leadsto> p'a = m' \<turnstile> pb \<leadsto> p'a proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x1a pa x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x))
 2. \<And>p p' c n c' n' x1 x1a pa x pb p'a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> m \<turnstile> pb \<leadsto> p'a = m' \<turnstile> pb \<leadsto> p'a proof (prove)
goal (3 subgoals):
 1. \<And>p p' c n c' n' x1 x1a pa x. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m \<turnstile> p parentOf x = m' \<turnstile> p parentOf x\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x))
 2. \<And>p p' c n c' n' x1 x1a pa x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> p parentOf x = m' \<turnstile> p parentOf x
 3. \<And>p p' c n c' n' x1 x1a pa x pb p'a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> m \<turnstile> pb \<leadsto> p'a = m' \<turnstile> pb \<leadsto> p'a proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x1 x1a pa x. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> p parentOf x = m' \<turnstile> p parentOf x
 2. \<And>p p' c n c' n' x1 x1a pa x pb p'a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> m \<turnstile> pb \<leadsto> p'a = m' \<turnstile> pb \<leadsto> p'a proof (prove)
goal (4 subgoals):
 1. \<And>p p' c n c' n' x1 x1a pa x xa cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p p' c n c' n' x1 x1a pa x xa cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m xa = Some cte; m' xa = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> cteMDBNode cte = cteMDBNode cte'
 3. \<And>p p' c n c' n' x1 x1a pa x pb. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> mdb_next m pb = mdb_next m' pb
 4. \<And>p p' c n c' n' x1 x1a pa x pb p'a. \<lbrakk>m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; m' p = Some (CTE c n); isUntypedCap c; m p = Some (CTE x1 n); m p' = Some (CTE x1a n'); isUntypedCap x1; untypedRange x1 = untypedRange c; isNotificationCap x1 = isNotificationCap c; isNotificationCap c \<longrightarrow> capNtfnBadge x1 = capNtfnBadge c; isEndpointCap x1 = isEndpointCap c; isEndpointCap c \<longrightarrow> capEPBadge x1 = capEPBadge c; capRange x1 = capRange c; \<not> isUntypedCap x1a; untypedRange x1a = untypedRange c'; isNotificationCap x1a = isNotificationCap c'; isNotificationCap c' \<longrightarrow> capNtfnBadge x1a = capNtfnBadge c'; isEndpointCap x1a = isEndpointCap c'; isEndpointCap c' \<longrightarrow> capEPBadge x1a = capEPBadge c'; capRange x1a = capRange c'\<rbrakk> \<Longrightarrow> m \<turnstile> pb \<leadsto> p'a = m' \<turnstile> pb \<leadsto> p'a proof (prove)
goal:
No subgoals!