theory Confine_S

lemma store_connected_generalOp2:
  "\<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s);
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk> \<Longrightarrow>
   s \<turnstile> x \<leftrightarrow>* y" apply (drule store_connected_generalOp) apply (erule disjE) apply (simp add: tgs_connected_def) apply (drule store_connected_directly_tgs_connected, simp) apply clarsimp apply (drule store_connected_directly_tgs_connected [where x=x and y=e\<^sub>1]) apply (drule store_connected_directly_tgs_connected [where x="target c" and y=y]) apply (drule (1) store_connected_generalOp_not_new) apply (erule disjE) apply (drule store_connected_direct_in_store_connected) apply (drule store_connected_directly_tgs_connected [where x=e\<^sub>1 and y="target c"]) apply (simp add: tgs_connected_def) apply (drule directly_tgs_connected_comm [where x="e\<^sub>0" and y="e\<^sub>1"]) apply (erule disjE) apply (drule store_connected_directly_tgs_connected [where x=e\<^sub>0 and y="target c"]) apply (simp add: tgs_connected_def) apply (drule (1) create_caps_directly_tgs_connected) apply (simp add: tgs_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, y) \<in> store_connected s \<or> (x, e\<^sub>1) \<in> store_connected s \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>1) \<in> store_connected s \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (x, y) \<in> (directly_tgs_connected s)\<^sup>*
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>1) \<in> store_connected s \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>1) \<in> store_connected s \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>1) \<in> store_connected s; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (target c, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (target c, y) \<in> store_connected s; s \<turnstile> x \<leftrightarrow> e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>1, target c) \<in> store_connected_direct s \<or> (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>1, target c) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>1, target c) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> target c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; (e\<^sub>0, target c) \<in> store_connected s \<or> Create \<in> rights c; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; (e\<^sub>0, target c) \<in> store_connected s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> target c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leftrightarrow> e\<^sub>1; s \<turnstile> target c \<leftrightarrow> y; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0; Create \<in> rights c; s \<turnstile> e\<^sub>0 \<leftrightarrow> target c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!