theory PolicySystemSAC

lemma abd_affects_bw : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` abd_affects_set \<subseteq> subjectAffects SACAuthGraph (partition_label x)" apply (simp only:abd_affects_set_def) apply (rule subsetI) 
  (* refl cases *)
   apply (case_tac "partition_label x = xa") apply (simp add: affects_lrefl) 
  (* non-refl cases *)
   apply (simp only: image_insert) apply (erule_tac a = xa in insertE) apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) apply (simp, simp, simp, simp) apply (erule_tac a = xa in insertE) apply (simp only:) apply (rule_tac ep = "partition_label x" and l' = "partition_label RM" in affects_recv) apply (simp) apply (auto)[1] apply (erule_tac a = xa in insertE) apply (simp only:) apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) apply (simp, simp, simp, simp) apply (erule_tac a = xa in insertE) apply (simp only:) apply (clarify) apply (erule notE) apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) apply (simp, simp, simp, simp) apply (erule_tac a = xa in insertE) apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) apply (simp, simp, simp, simp) apply (erule_tac a = xa in insertE) apply (rule_tac ep = "xa" and l = "partition_label x" in affects_ep_bound_trans) apply (rule_tac x = "partition_label RM" in exI) apply (rule_tac x = "partition_label x" in exI) apply (intro conjI) apply (simp,simp,simp) apply (erule_tac a = xa in insertE) apply (rule_tac ep = "xa" and l = "partition_label x" in affects_ep_bound_trans) apply (rule_tac x = "partition_label RM" in exI) apply (rule_tac x = "partition_label x" in exI) apply (intro conjI) apply (simp,simp,simp,simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` abd_affects_set \<subseteq> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2} \<subseteq> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}; partition_label x = xa\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> partition_label ` {NicB, RM, R, NicA, NicD, EP, NTFN2}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> insert (partition_label NicB) (insert (partition_label RM) (insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))))); partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicB\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label RM) (insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicB\<rbrakk> \<Longrightarrow> (partition_label x, SyncSend, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicB\<rbrakk> \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicB\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicB\<rbrakk> \<Longrightarrow> (partition_label RM, Write, xa) \<in> SACAuthGraph
 5. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label RM) (insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label RM) (insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label RM\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label RM; xa = partition_label RM\<rbrakk> \<Longrightarrow> partition_label RM \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label RM; xa = partition_label RM\<rbrakk> \<Longrightarrow> (partition_label x, Receive, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label RM; xa = partition_label RM\<rbrakk> \<Longrightarrow> (partition_label RM, SyncSend, partition_label x) \<in> SACAuthGraph
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label RM; xa = partition_label RM\<rbrakk> \<Longrightarrow> (partition_label RM, SyncSend, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label R) (insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label R\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label R; xa = partition_label R\<rbrakk> \<Longrightarrow> partition_label R \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label R; xa = partition_label R\<rbrakk> \<Longrightarrow> (partition_label x, SyncSend, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label R; xa = partition_label R\<rbrakk> \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label R; xa = partition_label R\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label R; xa = partition_label R\<rbrakk> \<Longrightarrow> (partition_label RM, Write, partition_label R) \<in> SACAuthGraph
 5. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicA) (insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicA\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> partition_label NicA; xa = partition_label NicA\<rbrakk> \<Longrightarrow> partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>partition_label NicA \<notin> subjectAffects SACAuthGraph (partition_label x); x \<in> {NicB, NicD}\<rbrakk> \<Longrightarrow> x = NicA
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. x \<in> {NicB, NicD} \<Longrightarrow> partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. \<And>xa. x \<in> {NicB, NicD} \<Longrightarrow> (partition_label x, SyncSend, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. x \<in> {NicB, NicD} \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. \<And>xa. x \<in> {NicB, NicD} \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. x \<in> {NicB, NicD} \<Longrightarrow> (partition_label RM, Write, partition_label NicA) \<in> SACAuthGraph
 5. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NicD) (insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {})))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicD\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicD\<rbrakk> \<Longrightarrow> (partition_label x, SyncSend, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicD\<rbrakk> \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicD\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NicD\<rbrakk> \<Longrightarrow> (partition_label RM, Write, xa) \<in> SACAuthGraph
 5. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label EP) (insert (partition_label NTFN2) (partition_label ` {}))\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, ntfn) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> \<exists>ntfn. (partition_label RM, Receive, ntfn) \<in> SACAuthGraph \<and> (partition_label RM, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, ntfn) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph \<and> (partition_label RM, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, xa) \<in> SACAuthGraph
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label EP\<rbrakk> \<Longrightarrow> (partition_label x, Notify, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> insert (partition_label NTFN2) (partition_label ` {})\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> partition_label ` {}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, ntfn) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> partition_label ` {}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> \<exists>ntfn. (partition_label RM, Receive, ntfn) \<in> SACAuthGraph \<and> (partition_label RM, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, ntfn) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> partition_label ` {}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph \<and> (partition_label RM, Receive, xa) \<in> SACAuthGraph \<and> (partition_label x, Notify, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> partition_label ` {}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, partition_label x) \<in> SACAuthGraph
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> (partition_label RM, Receive, xa) \<in> SACAuthGraph
 3. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa = partition_label NTFN2\<rbrakk> \<Longrightarrow> (partition_label x, Notify, partition_label x) \<in> SACAuthGraph
 4. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<in> partition_label ` {}\<rbrakk> \<Longrightarrow> xa \<in> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!