theory Noninterference_Base

lemma Noninfluence_gen:
  "\<lbrakk> confidentiality_u; integrity_u \<rbrakk> \<Longrightarrow> Noninfluence_gen" apply (subst Noninfluence_gen_def) apply (intro allI) proof - assume conf: "confidentiality_u" assume integ: "integrity_u" fix u as s ts show "reachable s \<and> Ball ts reachable
        \<longrightarrow> Ball ts (sameFor_dom s (sources as s u))
        \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t)
        \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)" proof(induct as arbitrary: s ts) case Nil show ?case apply (clarsimp simp: sameFor_dom_def ipurge_Nil sources_Nil uwr_equiv_def) apply (clarsimp simp: execution_Run) done next case (Cons a as) show ?case apply (clarsimp simp: ipurge_Cons | safe)+ apply (rule uwr_equiv_Cons_bothI) apply assumption apply blast apply (clarify) apply (rename_tac ta tb s' tb') apply (rule Cons.hyps[rule_format]) apply (blast intro: reachable_Step) apply (clarsimp) apply (rename_tac tc' tc) using conf apply (rule_tac s=s and t=tc and a=a in sources_unwinding_step, simp+)[1] apply (clarsimp, rename_tac tc' tc) apply (rule sched_equiv_preserved[OF conf], (auto simp: sources_refl))[1] apply blast apply (rename_tac ta) apply (rule uwr_equiv_Cons_leftI, blast) apply (clarsimp, rename_tac s') apply (case_tac "dom a s = schedDomain") apply (cut_tac s=s and a=a and as=as and u=u in schedDomain_in_sources_Cons, assumption+) apply (metis schedIncludesCurrentDom sources_eq[OF conf]) apply (rule Cons.hyps[rule_format]) apply (blast intro: reachable_Step) apply (rename_tac tb) apply (rule_tac a=a in sources_equiv_preserved_left[OF integ conf], simp+) apply (fastforce simp: schedIncludesCurrentDom sources_eq[OF conf]) apply blast apply assumption apply assumption apply (rule_tac s=s and a=a in sched_equiv_preserved_left[OF integ], simp+) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> Noninfluence_gen proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> \<forall>u as s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (prove)
goal (1 subgoal):
 1. \<And>u as s ts. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (state)
goal (1 subgoal):
 1. \<And>u as s ts. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (state)
this:
confidentiality_u

goal (1 subgoal):
 1. \<And>u as s ts. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (state)
this:
integrity_u

goal (1 subgoal):
 1. \<And>u as s ts. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (state)
goal (1 subgoal):
 1. \<And>u as s ts. \<lbrakk>confidentiality_u; integrity_u\<rbrakk> \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (prove)
goal (1 subgoal):
 1. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u) proof (state)
goal (2 subgoals):
 1. \<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources [] s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s [] t (ipurge u [] ts) u)
 2. \<And>a as s ts. (\<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)) \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources (a # as) s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (state)
this:


goal (2 subgoals):
 1. \<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources [] s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s [] t (ipurge u [] ts) u)
 2. \<And>a as s ts. (\<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)) \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources (a # as) s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (prove)
goal (1 subgoal):
 1. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>a\<in>ts. s \<approx>sources [] s u\<approx> a) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s [] t (ipurge u [] ts) u) proof (prove)
goal (1 subgoal):
 1. \<And>t s' t'. \<lbrakk>reachable s; Ball ts reachable; \<forall>x\<in>ts. s \<sim>u\<sim> x; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts; s' \<in> execution A s []; t' \<in> execution A t []\<rbrakk> \<Longrightarrow> s' \<sim>u\<sim> t' proof (prove)
goal:
No subgoals! proof (state)
this:
reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>a\<in>ts. s \<approx>sources [] s u\<approx> a) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s [] t (ipurge u [] ts) u)

goal (1 subgoal):
 1. \<And>a as s ts. (\<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)) \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources (a # as) s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (state)
goal (1 subgoal):
 1. \<And>a as s ts. (\<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)) \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources (a # as) s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (state)
this:
reachable ?s \<and> Ball ?ts reachable \<longrightarrow> (\<forall>a\<in>?ts. ?s \<approx>sources as ?s u\<approx> a) \<longrightarrow> (\<forall>t\<in>?ts. ?s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>?ts. uwr_equiv ?s as t (ipurge u as ?ts) u)

goal (1 subgoal):
 1. \<And>a as s ts. (\<And>s ts. reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)) \<Longrightarrow> reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources (a # as) s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (prove)
goal (1 subgoal):
 1. reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (a # ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 2. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (4 subgoals):
 1. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> reachable s
 2. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> reachable t
 3. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' as t' (ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 4. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' as t' (ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 3. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> \<forall>s' t'. (s, s') \<in> local.Step a \<and> (t, t') \<in> local.Step a \<longrightarrow> uwr_equiv s' as t' (ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 2. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>s t s' t'. \<lbrakk>s \<in> ts; dom a s \<in> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts; (s, s') \<in> local.Step a; (t, t') \<in> local.Step a\<rbrakk> \<Longrightarrow> uwr_equiv s' as t' (ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 2. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> uwr_equiv s' as tb' (ipurge u as (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})) u
 2. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (5 subgoals):
 1. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> reachable s' \<and> Ball (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a}) reachable
 2. \<And>ta tb s' tb' x. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; x \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> x
 3. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 4. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 5. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (4 subgoals):
 1. \<And>ta tb s' tb' x. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; x \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> x
 2. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (4 subgoals):
 1. \<And>ta tb s' tb' x xa. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; xa \<in> ts; (xa, x) \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> x
 2. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (4 subgoals):
 1. \<And>ta tb s' tb' tc' tc. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; tc \<in> ts; (tc, tc') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> tc'
 2. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
using this:
confidentiality_u

goal (4 subgoals):
 1. \<And>ta tb s' tb' tc' tc. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; tc \<in> ts; (tc, tc') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> tc'
 2. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 4. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (3 subgoals):
 1. \<And>ta tb s' tb' t. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; t \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 2. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 3. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (3 subgoals):
 1. \<And>ta tb s' tb' tc' tc. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a; tc \<in> ts; (tc, tc') \<in> local.Step a\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> tc'
 2. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 3. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>ta tb s' tb'. \<lbrakk>ta \<in> ts; dom a ta \<in> sources (a # as) ta u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; tb \<in> ts; (s, s') \<in> local.Step a; (tb, tb') \<in> local.Step a\<rbrakk> \<Longrightarrow> tb' \<in> (\<Union>s\<in>ts. {s'. (s, s') \<in> local.Step a})
 2. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; t \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) t (ipurge u as ts) u proof (prove)
goal (1 subgoal):
 1. \<And>ta. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts\<rbrakk> \<Longrightarrow> uwr_equiv s (a # as) ta (ipurge u as ts) u proof (prove)
goal (1 subgoal):
 1. \<And>ta. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts\<rbrakk> \<Longrightarrow> \<forall>s'. (s, s') \<in> local.Step a \<longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u proof (prove)
goal (1 subgoal):
 1. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s = schedDomain\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u
 2. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u proof (prove)
goal (2 subgoals):
 1. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s = schedDomain; dom a s \<in> sources (a # as) s u\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u
 2. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u proof (prove)
goal (1 subgoal):
 1. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> uwr_equiv s' as ta (ipurge u as ts) u proof (prove)
goal (4 subgoals):
 1. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> reachable s' \<and> Ball ts reachable
 2. \<And>ta s' x. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; x \<in> ts\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> x
 3. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 4. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (3 subgoals):
 1. \<And>ta s' x. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; x \<in> ts\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> x
 2. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (3 subgoals):
 1. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> s' \<approx>sources as s' u\<approx> tb
 2. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (6 subgoals):
 1. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> dom a s \<notin> sources (a # as) s u
 2. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> s \<approx>sources (a # as) s u\<approx> tb
 3. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a
 4. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> dom a s \<noteq> schedDomain
 5. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 6. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (5 subgoals):
 1. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> s \<approx>sources (a # as) s u\<approx> tb
 2. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a
 3. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> dom a s \<noteq> schedDomain
 4. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 5. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (4 subgoals):
 1. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> (s, s') \<in> local.Step a
 2. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> dom a s \<noteq> schedDomain
 3. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 4. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (3 subgoals):
 1. \<And>ta s' tb. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; tb \<in> ts\<rbrakk> \<Longrightarrow> dom a s \<noteq> schedDomain
 2. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 3. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal (2 subgoals):
 1. \<And>ta s' t. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain; t \<in> ts\<rbrakk> \<Longrightarrow> s' \<sim>schedDomain\<sim> t
 2. \<And>ta s'. \<lbrakk>\<forall>s\<in>ts. dom a s \<notin> sources (a # as) s u; reachable s; Ball ts reachable; \<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b; \<forall>t\<in>ts. s \<sim>schedDomain\<sim> t; ta \<in> ts; (s, s') \<in> local.Step a; dom a s \<noteq> schedDomain\<rbrakk> \<Longrightarrow> ta \<in> ts proof (prove)
goal:
No subgoals! proof (state)
this:
reachable s \<and> Ball ts reachable \<longrightarrow> (\<forall>b\<in>ts. s \<approx>sources (a # as) s u\<approx> b) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s (a # as) t (ipurge u (a # as) ts) u)

goal:
No subgoals! proof (state)
this:
reachable s \<and> Ball ts reachable \<longrightarrow> Ball ts (sameFor_dom s (sources as s u)) \<longrightarrow> (\<forall>t\<in>ts. s \<sim>schedDomain\<sim> t) \<longrightarrow> (\<forall>t\<in>ts. uwr_equiv s as t (ipurge u as ts) u)

goal:
No subgoals!