theory CSpace_AI

lemma untyped_mdb_update_free_index:
  "\<lbrakk>m src = Some capa;m' = m (src\<mapsto> capa\<lparr>free_index :=x\<rparr>) \<rbrakk> \<Longrightarrow>
   untyped_mdb c (m') = untyped_mdb c (m)" apply (rule iffI) apply (clarsimp simp:untyped_mdb_def) apply (drule_tac x = a in spec) apply (drule_tac x = b in spec) apply (drule_tac x = aa in spec) apply (drule_tac x = ba in spec) apply (case_tac "src = (a,b)") apply (case_tac "src = (aa,ba)") apply (clarsimp simp:is_cap_simps free_index_update_def) apply (drule_tac x = "capa\<lparr>free_index :=x\<rparr>" in spec) apply (clarsimp simp:is_cap_simps free_index_update_def) apply (drule_tac x = cap' in spec) apply (clarsimp split:if_split_asm)+ apply (clarsimp simp:untyped_mdb_def) apply (case_tac "src = (a,b)") apply (clarsimp simp:is_cap_simps free_index_update_def split:cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa)\<rbrakk> \<Longrightarrow> untyped_mdb c m' = untyped_mdb c m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m'\<rbrakk> \<Longrightarrow> untyped_mdb c m
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); \<forall>a b aa ba cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>b aa ba cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>aa ba cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>ba cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src = (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src = (a, b); src = (aa, ba)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src = (a, b); src \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 4. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src = (a, b); src \<noteq> (aa, ba)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; src = (a, b); src \<noteq> (aa, ba); (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some (free_index_update (\<lambda>_. x) capa) \<longrightarrow> is_untyped_cap (free_index_update (\<lambda>_. x) capa) \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range (free_index_update (\<lambda>_. x) capa) \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap' dev r bits f. \<lbrakk>m' = m((a, b) \<mapsto> UntypedCap dev r bits x); m (a, b) = Some (UntypedCap dev r bits f); m (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src = (a, b); a = aa \<longrightarrow> b \<noteq> ba; \<forall>cap'. (if aa = a \<and> ba = b then Some (free_index_update (\<lambda>_. x) (UntypedCap dev r bits f)) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c; capa = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba cap' dev r bits f. \<lbrakk>m' = m((a, b) \<mapsto> UntypedCap dev r bits x); m (a, b) = Some (UntypedCap dev r bits f); m (aa, ba) = Some cap'; obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; src = (a, b); a = aa \<longrightarrow> b \<noteq> ba; capa = UntypedCap dev r bits f; (if aa = a \<and> ba = b then Some (free_index_update (\<lambda>_. x) (UntypedCap dev r bits f)) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 2. \<And>a b aa ba cap cap'. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); m (a, b) = Some cap; is_untyped_cap cap; m (aa, ba) = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>cap. (if (a, b) = src then Some (free_index_update (\<lambda>_. x) capa) else m (a, b)) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. (if (aa, ba) = src then Some (free_index_update (\<lambda>_. x) capa) else m (aa, ba)) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (aa, ba) \<in> descendants_of (a, b) c
 3. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); untyped_mdb c m\<rbrakk> \<Longrightarrow> untyped_mdb c (m(src \<mapsto> free_index_update (\<lambda>_. x) capa)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); \<forall>a b aa ba cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. m (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c)\<rbrakk> \<Longrightarrow> ((a, b) = src \<longrightarrow> is_untyped_cap capa \<longrightarrow> (\<forall>a b. ((a, b) = src \<longrightarrow> obj_refs capa \<inter> untyped_range capa \<noteq> {} \<longrightarrow> src \<in> descendants_of src c) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<forall>cap'. m (a, b) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> (a, b) \<in> descendants_of src c)))) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<exists>a b. (a, b) = src) \<longrightarrow> (\<forall>cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> obj_refs capa \<inter> untyped_range cap \<noteq> {} \<longrightarrow> src \<in> descendants_of (a, b) c)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); \<forall>a b aa ba cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. m (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src = (a, b)\<rbrakk> \<Longrightarrow> ((a, b) = src \<longrightarrow> is_untyped_cap capa \<longrightarrow> (\<forall>a b. ((a, b) = src \<longrightarrow> obj_refs capa \<inter> untyped_range capa \<noteq> {} \<longrightarrow> src \<in> descendants_of src c) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<forall>cap'. m (a, b) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> (a, b) \<in> descendants_of src c)))) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<exists>a b. (a, b) = src) \<longrightarrow> (\<forall>cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> obj_refs capa \<inter> untyped_range cap \<noteq> {} \<longrightarrow> src \<in> descendants_of (a, b) c))
 2. \<And>a b. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa); \<forall>a b aa ba cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. m (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) c); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> ((a, b) = src \<longrightarrow> is_untyped_cap capa \<longrightarrow> (\<forall>a b. ((a, b) = src \<longrightarrow> obj_refs capa \<inter> untyped_range capa \<noteq> {} \<longrightarrow> src \<in> descendants_of src c) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<forall>cap'. m (a, b) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> (a, b) \<in> descendants_of src c)))) \<and> ((a, b) \<noteq> src \<longrightarrow> (\<exists>a b. (a, b) = src) \<longrightarrow> (\<forall>cap. m (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> obj_refs capa \<inter> untyped_range cap \<noteq> {} \<longrightarrow> src \<in> descendants_of (a, b) c)) proof (prove)
goal:
No subgoals!