theory Confine_S

lemma store_connected_generalOp:
  "\<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s)\<rbrakk> \<Longrightarrow>
   (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)" apply (unfold store_connected_def) apply (erule rtrancl_induct) apply clarsimp apply (clarsimp) apply (fold store_connected_def) apply (subgoal_tac "(y, z) \<in> store_connected_direct s") apply (clarsimp simp: store_connected_def) apply (erule disjE) apply fastforce apply clarsimp apply (erule notE) apply fastforce apply (frule store_connected_direct_generalOp) apply (clarsimp simp: store_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<Longrightarrow> (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 proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>* \<Longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. (x, x) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, x) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (x, y) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (x, y) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<and> (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> (target c, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (x, y) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<longrightarrow> (target c, z) \<notin> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (x, y) \<in> (store_connected_direct s)\<^sup>* \<or> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<longrightarrow> (target c, z) \<notin> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (3 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<longrightarrow> (target c, z) \<notin> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<longrightarrow> (target c, z) \<notin> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s; (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 3. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<longrightarrow> (target c, z) \<notin> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s; (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>* \<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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (target c, z) \<notin> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s; (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>*; (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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s))\<^sup>*; (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct s; (x, e\<^sub>1) \<in> (store_connected_direct s)\<^sup>*; (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_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (target c, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, z) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s); (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; (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<longrightarrow> (x, e\<^sub>1) \<in> store_connected s \<longrightarrow> (target c, z) \<notin> store_connected s; (y, z) \<in> store_connected_direct s \<or> y = e\<^sub>1 \<and> z = target c \<and> Store \<in> rights (extra_rights c)\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal:
No subgoals!