theory CSpace_AI

lemma descendants_inc:
  assumes dinc: "descendants_inc m cs"
  assumes src: "cs src = Some c"
  assumes type: "cap_class cap = cap_class c \<and> cap_range cap \<subseteq> cap_range c"
  shows "descendants_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" using dinc src type apply (simp add:descendants_inc_def del:split_paired_All) apply (intro allI conjI) apply (intro impI allI) apply (simp add:descendants_child split:if_splits del:split_paired_All) apply (erule disjE) 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
     split:if_splits del:split_paired_All) apply (simp add: descendants_of_def) apply (cut_tac p = p in dest_no_parent_trancl,simp) apply (simp add:descendants_of_def) apply (intro impI) apply (simp add:descendants_child split:if_splits del:split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_inc (m(dest \<mapsto> src)) (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 (m(dest \<mapsto> src)) (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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src))\<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 \<or> p' = src; 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 \<and> p' \<noteq> src; 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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (4 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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; src \<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 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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p' = src\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 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; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m \<and> p' \<noteq> src; 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'))
 4. \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (4 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; src \<in> descendants_of p' m; ?p52 p p' \<in> descendants_of (?p'54 p p') m \<longrightarrow> cap_class (the (cs (?p52 p p'))) = cap_class (the (cs (?p'54 p p'))) \<and> cap_range (the (cs (?p52 p p'))) \<subseteq> cap_range (the (cs (?p'54 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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p' = src\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 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; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m \<and> p' \<noteq> src; 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'))
 4. \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (4 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; src \<in> descendants_of p' m; 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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p' = src\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 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; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m \<and> p' \<noteq> src; 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'))
 4. \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (4 subgoals):
 1. \<And>p p'. \<lbrakk>cs src = Some c; p = dest; p' \<noteq> dest; cap_class cap = cap_class (the (cs p')); cap_range cap \<subseteq> cap_range c; src \<in> descendants_of p' m; 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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p' = src\<rbrakk> \<Longrightarrow> cap_class c = cap_class (the (cs p')) \<and> cap_range cap \<subseteq> cap_range (the (cs p'))
 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; p = dest; p' \<noteq> dest; src \<notin> descendants_of p' m \<and> p' \<noteq> src; 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'))
 4. \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; p' = src\<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 \<and> p' \<noteq> src; 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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 \<and> p' \<noteq> src; 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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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 (m(dest \<mapsto> src))\<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' (m(dest \<mapsto> src)) \<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 \<or> dest = src; 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 \<and> dest \<noteq> src; 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' (m(dest \<mapsto> src)) \<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>a b aa ba. m \<Turnstile> (aa, ba) \<rightarrow> (a, b) \<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 \<noteq> src; p' = src; dest = src; cap_class cap = cap_class c; cap_range cap \<subseteq> cap_range c; m \<Turnstile> src \<rightarrow> p\<rbrakk> \<Longrightarrow> 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 \<and> dest \<noteq> src; 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' (m(dest \<mapsto> src)) \<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 \<and> dest \<noteq> src; 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' (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src)) \<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' (m(dest \<mapsto> src))\<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!