theory Confine_S

lemma remove_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysRemove e c\<^sub>1 c\<^sub>2) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (x, y) \<in> directly_tgs_connected s" 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_remove, simp) prefer 5 apply (drule shares_caps_remove, simp) apply(auto dest!: caps_of_remove) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step (SysRemove e c\<^sub>1 c\<^sub>2) 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\<^sub>1 \<in> caps_of s e; s' = s \<or> s' = removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_cap x \<in>cap caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) y \<or> grant_cap y \<in>cap caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y \<or> take_cap y \<in>cap caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<or> grant_cap x \<in>cap caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) y \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y; is_entity s e; c\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 s) y. x = target c' \<and> rights (extra_rights (take_cap x)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y; is_entity s e; c\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 s) y. x = target c' \<and> rights (extra_rights (take_cap x)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) y. x = target c' \<and> rights (extra_rights (grant_cap x)) \<subseteq> rights (extra_rights c')) \<or> shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y; is_entity s e; c\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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\<^sub>1 \<in> caps_of s e; s' = removeOperation e c\<^sub>1 c\<^sub>2 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 (removeOperation e c\<^sub>1 c\<^sub>2 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!