theory Noninterference_Base

lemma ipurge_eq':
  "(\<forall>s t. s\<in>ss \<and> t\<in>ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and>
   (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u
   \<longrightarrow> ipurge u as ss = ipurge u as ts" proof (induct as arbitrary: ss ts) case Nil show ?case apply (simp add: ipurge_def) done next case (Cons a as) show ?case apply (clarsimp simp: ipurge_Cons schedIncludesCurrentDom) apply (intro conjI impI) apply (rule "Cons.hyps"[rule_format]) apply clarsimp apply (metis sched_equiv_preserved reachable_Step enabled_Step) apply clarsimp apply (drule ipurge_eq'_helper, simp+)[1] apply clarsimp apply (drule ipurge_eq'_helper, (simp add: uwr_sym)+)[1] apply (rule "Cons.hyps"[rule_format], auto) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts proof (state)
goal (2 subgoals):
 1. \<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u [] ss = ipurge u [] ts
 2. \<And>a as ss ts. (\<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts) \<Longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (state)
this:


goal (2 subgoals):
 1. \<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u [] ss = ipurge u [] ts
 2. \<And>a as ss ts. (\<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts) \<Longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (prove)
goal (1 subgoal):
 1. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u [] ss = ipurge u [] ts proof (prove)
goal:
No subgoals! proof (state)
this:
(\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u [] ss = ipurge u [] ts

goal (1 subgoal):
 1. \<And>a as ss ts. (\<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts) \<Longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (state)
goal (1 subgoal):
 1. \<And>a as ss ts. (\<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts) \<Longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (state)
this:
(\<forall>s t. s \<in> ?ss \<and> t \<in> ?ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ?ss) \<and> (\<exists>t. t \<in> ?ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ?ss = ipurge u as ?ts

goal (1 subgoal):
 1. \<And>a as ss ts. (\<And>ss ts. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts) \<Longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (prove)
goal (1 subgoal):
 1. (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts proof (prove)
goal (1 subgoal):
 1. ((\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u) \<longrightarrow> ((\<exists>s\<in>ts. dom a s \<in> sources (a # as) s u) \<longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) \<and> ((\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u) \<longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts)) \<and> ((\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u) \<longrightarrow> ((\<exists>s\<in>ts. dom a s \<in> sources (a # as) s u) \<longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) \<and> ((\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u) \<longrightarrow> (\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u as ss = ipurge u as ts)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 2. \<lbrakk>\<exists>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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts
 3. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<exists>s\<in>ss. dom a s \<in> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> (\<forall>s t. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) \<and> t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a}) \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a})) \<and> (\<exists>t. t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) \<and> confidentiality_u
 2. \<lbrakk>\<exists>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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts
 3. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (4 subgoals):
 1. \<And>s sa sb t. \<lbrakk>s \<in> ss; dom a s \<in> sources (a # as) s u; sa \<in> ts; dom a sa \<in> sources (a # as) sa u; \<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t; sb \<in> ss; confidentiality_u; t \<in> ts\<rbrakk> \<Longrightarrow> (\<forall>s t. (\<exists>x\<in>ss. (x, s) \<in> local.Step a) \<and> (\<exists>x\<in>ts. (x, t) \<in> local.Step a) \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. \<exists>x\<in>ss. (x, s) \<in> local.Step a) \<and> (\<exists>t. \<exists>x\<in>ts. (x, t) \<in> local.Step a)
 2. \<lbrakk>\<exists>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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts
 3. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<exists>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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts
 2. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 3. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (3 subgoals):
 1. \<And>s sa t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; s \<in> ss; dom a s \<in> 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; sa \<in> ss; confidentiality_u; t \<in> ts\<rbrakk> \<Longrightarrow> a # ipurge u as (\<Union>s\<in>ss. {s'. (s, s') \<in> local.Step a}) = ipurge u as ts
 2. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 3. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; \<exists>s\<in>ts. dom a s \<in> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 2. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> sources (a # as) s u; s \<in> ts; dom a s \<in> 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; sa \<in> ss; confidentiality_u; t \<in> ts\<rbrakk> \<Longrightarrow> ipurge u as ss = a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 2. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s\<in>ss. dom a s \<notin> 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) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u\<rbrakk> \<Longrightarrow> ipurge u as ss = ipurge u as ts proof (prove)
goal:
No subgoals! proof (state)
this:
(\<forall>s t. s \<in> ss \<and> t \<in> ts \<longrightarrow> s \<sim>schedDomain\<sim> t \<and> reachable s \<and> reachable t) \<and> (\<exists>s. s \<in> ss) \<and> (\<exists>t. t \<in> ts) \<and> confidentiality_u \<longrightarrow> ipurge u (a # as) ss = ipurge u (a # as) ts

goal:
No subgoals!