theory Noninterference_Base

lemma ipurge_eq'_helper:
  "\<lbrakk> s \<in> ss; dom a s \<in> sources (a # as) s u; \<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u;
     (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t);
     t \<in> ts; confidentiality_u \<rbrakk>
     \<Longrightarrow> False" apply (cut_tac s=s and t=t and as=as and u=u in sources_eq, simp+) apply (clarsimp  simp: sources_Cons | safe)+ apply (rename_tac s') apply (drule_tac x=t in bspec, simp) apply clarsimp apply (cut_tac s=t in enabled_Step, simp) apply (erule exE, rename_tac t') apply (drule_tac x="sources as t' u" in spec) apply (cut_tac s=s' and t=t' and u=u in sources_eq, simp+) apply (fastforce elim: sched_equiv_preserved) apply (fastforce intro: reachable_Step) apply (fastforce intro: reachable_Step) apply (fastforce simp: schedIncludesCurrentDom) apply (drule_tac x=t in bspec, simp) apply clarsimp apply (rename_tac v s') apply (drule_tac x=v in spec, erule impE, fastforce simp: schedIncludesCurrentDom) apply (cut_tac s=t in enabled_Step[where a=a], simp, clarsimp, rename_tac t') apply (cut_tac s=s' and t=t' and u=u in sources_eq, simp+) apply (fastforce elim: sched_equiv_preserved) apply (fastforce intro: reachable_Step) apply (fastforce intro: reachable_Step) apply (fastforce simp: schedIncludesCurrentDom) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> ss; dom a s \<in> sources (a # as) s u; \<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> ss; dom a s \<in> sources (a # as) s u; \<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x) \<and> (\<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u))\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); \<exists>s'a. (t, s'a) \<in> local.Step (?a31 s')\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s')\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s'); (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s'); (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s'); (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> reachable s'
 3. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s'); (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> reachable t'
 4. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step (?a31 s'); (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u; sources (?as37 s' t') s' u = sources (?as37 s' t') t' u\<rbrakk> \<Longrightarrow> False
 5. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> reachable s'
 2. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> reachable t'
 3. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u; sources (?as37 s' t') s' u = sources (?as37 s' t') t' u\<rbrakk> \<Longrightarrow> False
 4. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u\<rbrakk> \<Longrightarrow> reachable t'
 2. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u; sources (?as37 s' t') s' u = sources (?as37 s' t') t' u\<rbrakk> \<Longrightarrow> False
 3. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<in> sources as s' u; (s, s') \<in> local.Step a; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u); (t, t') \<in> local.Step a; (\<forall>s'. sources as t' u = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> sources as t' u; sources (?as37 s' t') s' u = sources (?as37 s' t') t' u\<rbrakk> \<Longrightarrow> False
 2. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s\<in>ts. (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (s, s') \<notin> local.Step a) \<or> dom a s \<notin> x) \<and> (\<forall>v. dom a s \<leadsto> v \<longrightarrow> (\<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)); \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; (\<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x) \<and> (\<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>v. dom a t \<leadsto> v \<longrightarrow> (\<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t'
 2. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable s'
 3. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable t'
 4. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a; sources (?as164 v s' t') s' u = sources (?as164 v s' t') t' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable s'
 2. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable t'
 3. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a; sources (?as164 v s' t') s' u = sources (?as164 v s' t') t' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable t'
 2. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a; sources (?as164 v s' t') s' u = sources (?as164 v s' t') t' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v s' t'. \<lbrakk>s \<in> ss; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; t \<in> ts; confidentiality_u; sources as s u = sources as t u; dom a s \<leadsto> v; (s, s') \<in> local.Step a; v \<in> sources as s' u; \<forall>x. (\<forall>s'. x = sources as s' u \<longrightarrow> (t, s') \<notin> local.Step a) \<or> dom a t \<notin> x; \<forall>s'. (t, s') \<in> local.Step a \<longrightarrow> v \<notin> sources as s' u; (t, t') \<in> local.Step a; sources (?as164 v s' t') s' u = sources (?as164 v s' t') t' u\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!