theory CSpace1_R

lemma updateUntypedCap_descendants_of:
  "\<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk>
   \<Longrightarrow> descendants_of' slot (m(src \<mapsto> cteCap_update
           (\<lambda>_. (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))) cte)) =
       descendants_of' slot m" apply (rule set_eqI) apply (clarsimp simp:descendants_of'_def subtree_def) apply (rule_tac x = x in fun_cong) apply (rule_tac f = lfp in arg_cong) apply (rule ext)+ apply (cut_tac x  = xa in parentOf_preserve
  [where m = "m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)"
   and  m' = m and p = slot]) apply (clarsimp,rule iffI,fastforce+) apply (clarsimp simp:isCap_simps split:if_splits) apply (clarsimp simp:sameRegionAs_def isCap_simps split:if_splits) apply (rule ext) apply (clarsimp simp:sameRegionAs_def isCap_simps split:if_splits)+ apply (simp add:mdb_next_def split:if_splits) apply (simp del:fun_upd_apply) apply (subgoal_tac "\<And>p. m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> p \<leadsto> xa
     = m \<turnstile> p \<leadsto> xa") apply simp apply (clarsimp simp:mdb_next_rel_def mdb_next_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> descendants_of' slot (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) = descendants_of' slot m proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (x \<in> descendants_of' slot (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte))) = (x \<in> descendants_of' slot m) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> lfp (\<lambda>p x. m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x)) x = lfp (\<lambda>p x. m \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> lfp (\<lambda>p x. m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x)) = lfp (\<lambda>p x. m \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (\<lambda>p x. m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf x)) = (\<lambda>p x. m \<turnstile> slot \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> slot parentOf x)) proof (prove)
goal (1 subgoal):
 1. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (5 subgoals):
 1. \<And>x p xa xb. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (xb \<in> dom (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte))) = (xb \<in> dom m)
 2. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap ctea) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap ctea)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 3. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap ctea) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap ctea) \<longrightarrow> capNtfnBadge (cteCap ctea) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap ctea) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap ctea) \<longrightarrow> capEPBadge (cteCap ctea) = capEPBadge (cteCap cte')) \<and> cteMDBNode ctea = cteMDBNode cte'
 4. \<And>x p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) pa = mdb_next m pa
 5. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (4 subgoals):
 1. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap ctea) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap ctea)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap ctea) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap ctea) \<longrightarrow> capNtfnBadge (cteCap ctea) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap ctea) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap ctea) \<longrightarrow> capEPBadge (cteCap ctea) = capEPBadge (cteCap cte')) \<and> cteMDBNode ctea = cteMDBNode cte'
 3. \<And>x p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) pa = mdb_next m pa
 4. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (4 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>m src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d v0 v1 idx) = global.sameRegionAs (capability.UntypedCap d v0 v1 f) \<and> (\<lambda>x. global.sameRegionAs x (capability.UntypedCap d v0 v1 idx)) = (\<lambda>x. global.sameRegionAs x (capability.UntypedCap d v0 v1 f))
 2. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap ctea) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap ctea) \<longrightarrow> capNtfnBadge (cteCap ctea) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap ctea) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap ctea) \<longrightarrow> capEPBadge (cteCap ctea) = capEPBadge (cteCap cte')) \<and> cteMDBNode ctea = cteMDBNode cte'
 3. \<And>x p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) pa = mdb_next m pa
 4. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (4 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>m src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d v0 v1 idx) = global.sameRegionAs (capability.UntypedCap d v0 v1 f)
 2. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap ctea) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap ctea) \<longrightarrow> capNtfnBadge (cteCap ctea) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap ctea) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap ctea) \<longrightarrow> capEPBadge (cteCap ctea) = capEPBadge (cteCap cte')) \<and> cteMDBNode ctea = cteMDBNode cte'
 3. \<And>x p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) pa = mdb_next m pa
 4. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (4 subgoals):
 1. \<And>d v0 v1 f x. \<lbrakk>m src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d v0 v1 idx) x = global.sameRegionAs (capability.UntypedCap d v0 v1 f) x
 2. \<And>x p xa xb ctea cte'. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) xb = Some ctea; m xb = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap ctea) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap ctea) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap ctea) \<longrightarrow> capNtfnBadge (cteCap ctea) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap ctea) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap ctea) \<longrightarrow> capEPBadge (cteCap ctea) = capEPBadge (cteCap cte')) \<and> cteMDBNode ctea = cteMDBNode cte'
 3. \<And>x p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte)) pa = mdb_next m pa
 4. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (2 subgoals):
 1. \<And>pa d v0 v1 f. \<lbrakk>m src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> mdb_next (m(src \<mapsto> cteCap_update (\<lambda>_. capability.UntypedCap d v0 v1 idx) cte)) pa = mdb_next m pa
 2. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (1 subgoal):
 1. \<And>p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) proof (prove)
goal (2 subgoals):
 1. \<And>p xa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa; \<And>p. m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> p \<leadsto> xa = m \<turnstile> p \<leadsto> xa\<rbrakk> \<Longrightarrow> (m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa)) = (m \<turnstile> slot \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa \<or> (\<exists>c'. p c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> slot parentOf xa))
 2. \<And>p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> pa \<leadsto> xa = m \<turnstile> pa \<leadsto> xa proof (prove)
goal (1 subgoal):
 1. \<And>p xa pa. \<lbrakk>m src = Some cte; isUntypedCap (cteCap cte); m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> slot parentOf xa = m \<turnstile> slot parentOf xa\<rbrakk> \<Longrightarrow> m(src \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) cte) \<turnstile> pa \<leadsto> xa = m \<turnstile> pa \<leadsto> xa proof (prove)
goal:
No subgoals!