theory Noninterference_Base_Alternatives

lemma ipurgx_xpurge':
  "confidentiality_u
   \<Longrightarrow> (\<forall>s\<in>ss. reachable s) \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s\<in>ss \<and> s'\<in>ss \<longrightarrow> s\<sim>schedDomain\<sim>s')
       \<longrightarrow> ipurgx u as ss = xpurge u as ss" apply (induct as arbitrary: ss) apply (simp add: ipurgx_Nil xpurge_Nil) apply (clarsimp simp: xpurge_Cons ipurgx_Cons | safe)+ apply (drule_tac x="\<Union>s\<in>ss. {s'. (s,s') \<in> Step a}" in meta_spec) apply (erule impE) apply (rule conjI) apply (fastforce intro: reachable_Step) apply (rule conjI) apply (drule bspec, assumption, frule_tac a=a in enabled_Step) apply blast apply clarsimp apply (match conclusion in \<open>s' \<sim>schedDomain\<sim> t'\<close> for s' t' \<Rightarrow>
             \<open>match premises in \<open>(s,s') \<in> Step a\<close> and \<open>(t,t') \<in> Step a\<close> for a s t \<Rightarrow>
                \<open>rule sched_equiv_preserved[of s t]\<close>\<close>) apply assumption apply blast apply blast apply blast apply assumption apply assumption apply assumption apply (simp add: xources_sources) apply (simp add: xources_sources) apply (erule notE) apply (frule_tac s=s and t=sa in sources_eq, simp+) apply (erule ssubst) apply (subst schedIncludesCurrentDom) prefer 2 apply assumption apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. confidentiality_u \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss proof (prove)
goal (2 subgoals):
 1. \<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u [] ss = xpurge u [] ss
 2. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u (a # as) ss = xpurge u (a # as) ss proof (prove)
goal (1 subgoal):
 1. \<And>a as ss. \<lbrakk>\<And>ss. confidentiality_u \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u\<rbrakk> \<Longrightarrow> Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u (a # as) ss = xpurge u (a # as) ss proof (prove)
goal (3 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 3. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (3 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; Ball (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) reachable \<and> (\<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) \<and> (\<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 3. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (4 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> Ball (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) reachable \<and> (\<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) \<and> (\<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s')
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 4. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (5 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> Ball (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) reachable
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> (\<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) \<and> (\<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s')
 3. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 4. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 5. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (4 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> (\<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) \<and> (\<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s')
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 4. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (5 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> \<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> \<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s'
 3. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 4. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 5. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (5 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; reachable s; \<exists>s'. (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> \<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> \<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s'
 3. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 4. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 5. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (4 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss\<rbrakk> \<Longrightarrow> \<forall>s s'. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> s' \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> s'
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 4. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (4 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> sb \<sim>schedDomain\<sim> s'
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 4. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (9 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> confidentiality_u
 2. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable x
 3. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable xa
 4. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> x \<sim>schedDomain\<sim> xa
 5. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (x, sb) \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 6. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 7. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 8. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 9. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (8 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable x
 2. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable xa
 3. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> x \<sim>schedDomain\<sim> xa
 4. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (x, sb) \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 5. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 6. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 7. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 8. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (7 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable xa
 2. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> x \<sim>schedDomain\<sim> xa
 3. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (x, sb) \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 4. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 5. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 6. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 7. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (6 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> x \<sim>schedDomain\<sim> xa
 2. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (x, sb) \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 3. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 4. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 5. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 6. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (5 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (x, sb) \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 2. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step (?a87 a as ss s sa sb s' x xa)
 3. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 4. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 5. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (4 subgoals):
 1. \<And>a as ss s sa sb s' x xa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; x \<in> ss; (x, sb) \<in> local.Step a; xa \<in> ss; (xa, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> (xa, s') \<in> local.Step a
 2. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 3. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 4. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (3 subgoals):
 1. \<And>a as ss s sa. \<lbrakk>confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; s \<in> ss; dom a s \<in> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sa \<in> ss; ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})
 2. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 3. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (2 subgoals):
 1. \<And>a as ss s. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; \<forall>s\<in>ss. dom a s \<in> sources (a # as) s u; \<forall>s\<in>ss. dom a s \<notin> xources (a # as) s u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; s \<in> ss\<rbrakk> \<Longrightarrow> a # ipurgx u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = xpurge u as ss
 2. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> xources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; dom a s \<notin> sources (a # as) s u; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> xpurge u as ss = a # xpurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> dom a s \<in> sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss; sources (?as120 a as ss s sa sb) s (?u120 a as ss s sa sb) = sources (?as120 a as ss s sa sb) sa (?u120 a as ss s sa sb)\<rbrakk> \<Longrightarrow> dom a s \<in> sources (a # as) s u proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> dom a s \<in> sources (a # as) sa u proof (prove)
goal (2 subgoals):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> ?t124 a as ss s sa sb
 2. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> dom a (?t124 a as ss s sa sb) \<in> sources (a # as) sa u proof (prove)
goal (2 subgoals):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> dom a (?t124 a as ss s sa sb) \<in> sources (a # as) sa u
 2. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> ?t124 a as ss s sa sb proof (prove)
goal (1 subgoal):
 1. \<And>a as ss s sa sb. \<lbrakk>\<And>ss. Ball ss reachable \<and> (\<exists>s. s \<in> ss) \<and> (\<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s') \<longrightarrow> ipurgx u as ss = xpurge u as ss; confidentiality_u; s \<in> ss; sa \<in> ss; dom a sa \<in> sources (a # as) sa u; Ball ss reachable; \<forall>s s'. s \<in> ss \<and> s' \<in> ss \<longrightarrow> s \<sim>schedDomain\<sim> s'; sb \<in> ss\<rbrakk> \<Longrightarrow> s \<sim>schedDomain\<sim> sa proof (prove)
goal:
No subgoals!