theory Confine_S

lemma removeSet_connected:
  " \<lbrakk>s' \<in> step (SysRemoveSet e c C) s; s' \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y" apply(simp add: step_def split: if_split_asm) apply(erule disjE, simp) apply(simp add: directly_tgs_connected_def leak_def) apply(simp add: cap_in_caps_def) apply(clarsimp) apply safe prefer 3 apply (drule shares_caps_removeSet, simp) prefer 5 apply (drule shares_caps_removeSet, simp) apply (auto dest!: caps_of_removeSet) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step (SysRemoveSet e c C) s; s' \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; is_entity s e; c \<in> caps_of s e; s' = s \<or> s' = removeSetOperation e c C s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_cap x \<in>cap caps_of (removeSetOperation e c C s) y \<or> grant_cap y \<in>cap caps_of (removeSetOperation e c C s) x \<or> shares_caps (removeSetOperation e c C s) x y \<or> take_cap y \<in>cap caps_of (removeSetOperation e c C s) x \<or> grant_cap x \<in>cap caps_of (removeSetOperation e c C s) y \<or> shares_caps (removeSetOperation e c C s) x y; is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>c'\<in>caps_of (removeSetOperation e c C s) y. x = target c' \<and> rights (extra_rights (take_cap x)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeSetOperation e c C s) x y \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeSetOperation e c C s) x y; is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s\<rbrakk> \<Longrightarrow> (\<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (take_cap x)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) \<or> shares_caps s x y \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')) \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>c'\<in>caps_of (removeSetOperation e c C s) y. x = target c' \<and> rights (extra_rights (take_cap x)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeSetOperation e c C s) x y \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeSetOperation e c C s) y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeSetOperation e c C s) x y; is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c') proof (prove)
goal (6 subgoals):
 1. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 2. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 3. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 4. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 5. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 6. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c') proof (prove)
goal (6 subgoals):
 1. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 2. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 3. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 4. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 5. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 6. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c') proof (prove)
goal (5 subgoals):
 1. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 2. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 3. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 4. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 5. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s y. x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s x. y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s x y; shares_caps (removeSetOperation e c C s) x y\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 2. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 3. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 4. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 5. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a) proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)
 2. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 3. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'\<in>caps_of s (target c'). x = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'a\<in>caps_of s x. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<not> shares_caps s x (target c'); c' \<in> caps_of (removeSetOperation e c C s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s (target c'). x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')
 4. \<And>c'. \<lbrakk>is_entity s e; c \<in> caps_of s e; s' = removeSetOperation e c C s; \<forall>c'a\<in>caps_of s y. target c' = target c'a \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'a))) \<subseteq> rights (extra_rights c'a); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); \<forall>c'\<in>caps_of s (target c'). y = target c' \<longrightarrow> \<not> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); \<not> shares_caps s (target c') y; c' \<in> caps_of (removeSetOperation e c C s) y; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); x = target c'\<rbrakk> \<Longrightarrow> \<exists>c'a\<in>caps_of s y. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a) proof (prove)
goal:
No subgoals!