theory CSpace_AI

lemma (in mdb_insert_abs_sib) descendants_inc:
  assumes dinc: "descendants_inc m cs"
  assumes src: "cs src = Some c"
  assumes d: "cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c"
  shows "descendants_inc n (cs(dest \<mapsto> cap))" using dinc src d apply (simp add:descendants_inc_def del:split_paired_All) apply (intro allI conjI) apply (intro impI allI) apply (simp add:descendants_child descendants split:if_splits del:split_paired_All) apply (drule spec)+ apply (erule(1) impE) apply simp apply blast apply simp apply (simp add:descendants_of_def) apply (intro impI allI) apply (rule conjI) apply (intro impI) apply (simp add:descendants_child descendants
     split:if_splits del:split_paired_All) apply (simp add: descendants_of_def) apply (simp add:descendants_of_def descendants) apply (intro impI) apply (simp add: descendants del:split_paired_All split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_inc n (cs(dest \<mapsto> cap)) proof (prove)
using this:
descendants_inc m cs
cs src = Some c
cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c

goal (1 subgoal):
 1. descendants_inc n (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> \<forall>p. (p = dest \<longrightarrow> (\<forall>p'. p' \<noteq> dest \<longrightarrow> dest \<in> descendants_of p' n \<longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))) \<and> (p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p'))))) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> (\<forall>p'. p' \<noteq> dest \<longrightarrow> dest \<in> descendants_of p' n \<longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p')))
 2. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p = dest; p' \<noteq> dest; dest \<in> descendants_of p' n\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<in> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 3. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; src \<in> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; ?p49 p p' \<in> descendants_of (?p'51 p p') m \<longrightarrow> cap_class (the (cs (?p49 p p'))) = cap_class (the (cs (?p'51 p p'))) \<and> cap_range (the (cs (?p49 p p'))) \<subseteq> cap_range (the (cs (?p'51 p p')))\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 3. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; src \<in> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; cap_class (the (cs src)) = cap_class (the (cs p')) \<and> cap_range (the (cs src)) \<subseteq> cap_range (the (cs p'))\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 3. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; src \<in> descendants_of p' m; cap_class cap = cap_class (the (cs p')); cap_range cap \<subseteq> cap_range c; cap_class c = cap_class (the (cs p')) \<and> cap_range c \<subseteq> cap_range (the (cs p'))\<rbrakk> \<Longrightarrow> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 3. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>a b aa ba. (a, b) \<in> descendants_of (aa, ba) m \<longrightarrow> cap_class (the (cs (a, b))) = cap_class (the (cs (aa, ba))) \<and> cap_range (the (cs (a, b))) \<subseteq> cap_range (the (cs (aa, ba))); cs src = Some c; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; dest \<in> descendants_of p' m\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 2. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (\<forall>p'. (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')))) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap) \<and> (p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p'))) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' = dest \<longrightarrow> p \<in> descendants_of dest n \<longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest; p' = dest; p \<in> descendants_of dest n\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (3 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p \<noteq> dest; p' = dest; src \<in> descendants_of dest m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> cap_class (the (cs dest)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p \<noteq> dest; p' = dest; src \<notin> descendants_of dest m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> cap_class (the (cs dest)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap
 3. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; p \<noteq> dest; p' = dest; src \<notin> descendants_of dest m; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p \<in> descendants_of dest m\<rbrakk> \<Longrightarrow> cap_class (the (cs dest)) = cap_class c \<and> cap_range (the (cs p)) \<subseteq> cap_range cap
 2. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> p \<in> descendants_of p' n \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' m \<longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')); cs src = Some c; cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c; p \<noteq> dest; p' \<noteq> dest; p \<in> descendants_of p' n\<rbrakk> \<Longrightarrow> cap_class (the (cs p)) = cap_class (the (cs p')) \<and> cap_range (the (cs p)) \<subseteq> cap_range (the (cs p')) proof (prove)
goal:
No subgoals!