theory Noninterference_Base_Alternatives

lemma xources_sources:
  "confidentiality_u \<Longrightarrow> reachable s \<longrightarrow> (xources as s u = sources as s u)" apply (induct as arbitrary: s) apply (simp add: xources_Nil sources_Nil) apply (simp add: sources_Cons xources_Cons) apply (rule impI) apply (rule un_eq) apply (rule sym) apply (simp only: Union_eq, simp only: UNION_eq[symmetric]) apply (simp only: Inter_eq, simp only: INTER_eq[symmetric]) apply (rule Un_eq_Int) apply (clarsimp simp: Step_def) apply (erule reachable_enabled) apply (clarsimp simp: Step_def) apply (erule reachable_enabled) apply clarsimp apply (drule_tac x=s'a in meta_spec, clarsimp simp: reachable_Step) apply (rule sources_eq) apply assumption apply (fastforce intro: sched_equiv_preserved uwr_refl) apply (fastforce intro: reachable_Step) apply (fastforce intro: reachable_Step) apply (rule Collect_cong) apply (rule conj_cong, rule refl) apply safe apply (cut_tac s=s and a=a in enabled_Step) apply assumption apply clarsimp apply (drule_tac x=s' in spec) apply clarsimp apply (rule_tac x=v in exI) apply clarsimp apply (rule_tac x=s' in exI) apply (drule_tac x=s' in meta_spec) apply (fastforce intro: reachable_Step) apply (rule_tac x=v in exI, clarsimp) apply (drule_tac x=s' in meta_spec) apply (clarsimp simp: reachable_Step) apply (rule subst[OF sources_eq]) apply assumption prefer 4 apply assumption apply (fastforce intro: sched_equiv_preserved uwr_refl) by (auto intro: reachable_Step)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> reachable s \<longrightarrow> xources as s u = sources as s u proof (prove)
goal (2 subgoals):
 1. \<And>s. confidentiality_u \<Longrightarrow> reachable s \<longrightarrow> xources [] s u = sources [] s u
 2. \<And>a as s. \<lbrakk>\<And>s. confidentiality_u \<Longrightarrow> reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u\<rbrakk> \<Longrightarrow> reachable s \<longrightarrow> xources (a # as) s u = sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. confidentiality_u \<Longrightarrow> reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u\<rbrakk> \<Longrightarrow> reachable s \<longrightarrow> xources (a # as) s u = sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u\<rbrakk> \<Longrightarrow> reachable s \<longrightarrow> \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = \<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = \<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} \<union> {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a} = \<Union> {sources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<Union> {sources as s' u |s'. (s, s') \<in> local.Step a} = \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>{sources as s' u |s'. (s, s') \<in> local.Step a}. x) = \<Inter> {xources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>{sources as s' u |s'. (s, s') \<in> local.Step a}. x) = (\<Inter>x\<in>{xources as s' u |s'. (s, s') \<in> local.Step a}. x)
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (4 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}
 3. \<And>a as s x y. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}; y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}\<rbrakk> \<Longrightarrow> x = y
 4. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (4 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s [a]
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}
 3. \<And>a as s x y. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}; y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}\<rbrakk> \<Longrightarrow> x = y
 4. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (3 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>y. y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}
 2. \<And>a as s x y. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}; y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (3 subgoals):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s [a]
 2. \<And>a as s x y. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}; y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}\<rbrakk> \<Longrightarrow> x = y
 3. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s x y. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; x \<in> {sources as s' u |s'. (s, s') \<in> local.Step a}; y \<in> {xources as s' u |s'. (s, s') \<in> local.Step a}\<rbrakk> \<Longrightarrow> x = y
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a\<rbrakk> \<Longrightarrow> sources as s' u = xources as s'a u
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> sources as s' u = sources as s'a u
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (5 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> confidentiality_u
 2. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> s'a
 3. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'
 4. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'a
 5. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (4 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> s'a
 2. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'
 3. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'a
 4. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (3 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'
 2. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'a
 3. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' s'a. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s'a) \<in> local.Step a; xources as s'a u = sources as s'a u\<rbrakk> \<Longrightarrow> reachable s'a
 2. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> {w. w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))} = {w. w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))} proof (prove)
goal (1 subgoal):
 1. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s\<rbrakk> \<Longrightarrow> (w = dom a s \<and> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u))) = (w = dom a s \<and> (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u))) proof (prove)
goal (1 subgoal):
 1. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; w = dom a s\<rbrakk> \<Longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)) = (\<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)) proof (prove)
goal (2 subgoals):
 1. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (3 subgoals):
 1. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)\<rbrakk> \<Longrightarrow> reachable s
 2. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u); \<exists>s'. (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 3. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s w. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u); \<exists>s'. (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s'. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u); (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s'. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; (s, s') \<in> local.Step a \<longrightarrow> (\<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' v. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<leadsto> v; v \<in> xources as s' u\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' v. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<leadsto> v; v \<in> xources as s' u\<rbrakk> \<Longrightarrow> dom a s \<leadsto> v \<and> (\<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u)
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' v. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<leadsto> v; v \<in> xources as s' u\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> local.Step a \<and> v \<in> sources as s' u
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' v. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<leadsto> v; v \<in> xources as s' u\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a \<and> v \<in> sources as s' u
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (2 subgoals):
 1. \<And>a as s s' v. \<lbrakk>confidentiality_u; reachable s; (s, s') \<in> local.Step a; dom a s \<leadsto> v; v \<in> xources as s' u; reachable s' \<longrightarrow> xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a \<and> v \<in> sources as s' u
 2. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (1 subgoal):
 1. \<And>a as s w v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>v. dom a s \<leadsto> v \<and> v \<in> xources as s' u proof (prove)
goal (1 subgoal):
 1. \<And>a as s v s' s'a. \<lbrakk>\<And>s. reachable s \<longrightarrow> xources as s u = sources as s u; confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> v \<in> xources as s' u proof (prove)
goal (1 subgoal):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; reachable s' \<longrightarrow> xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> v \<in> xources as s' u proof (prove)
goal (1 subgoal):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> v \<in> sources as s' u proof (prove)
goal (5 subgoals):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> confidentiality_u
 2. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> ?s92 a as s v s' s'a \<sim>schedDomain\<sim> s'
 3. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable (?s92 a as s v s' s'a)
 4. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s'
 5. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> v \<in> sources as (?s92 a as s v s' s'a) u proof (prove)
goal (4 subgoals):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> ?s92 a as s v s' s'a \<sim>schedDomain\<sim> s'
 2. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable (?s92 a as s v s' s'a)
 3. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s'
 4. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> v \<in> sources as (?s92 a as s v s' s'a) u proof (prove)
goal (4 subgoals):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> v \<in> sources as (?s92 a as s v s' s'a) u
 2. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> ?s92 a as s v s' s'a \<sim>schedDomain\<sim> s'
 3. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable (?s92 a as s v s' s'a)
 4. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s' proof (prove)
goal (3 subgoals):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> s'a \<sim>schedDomain\<sim> s'
 2. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s'a
 3. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s' proof (prove)
goal (2 subgoals):
 1. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s'a
 2. \<And>a as s v s' s'a. \<lbrakk>confidentiality_u; reachable s; dom a s \<leadsto> v; (s, s'a) \<in> local.Step a; v \<in> sources as s'a u; (s, s') \<in> local.Step a; xources as s' u = sources as s' u\<rbrakk> \<Longrightarrow> reachable s'