kings-crown/FVELER_Isabelle huggingface dataset:
theory PolicySystemSAC

lemma c_affects_self_only : "x \<in> {partition_label NicC} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC)" apply (erule insertE) apply (simp only:, rule affects_lrefl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label NicC} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC) proof (prove)
goal (2 subgoals):
 1. x = partition_label NicC \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC)
 2. x \<in> {} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC) proof (prove)
goal (1 subgoal):
 1. x \<in> {} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_reads_bd : "x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label R)" apply (rule reads_read) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> (partition_label R, Read, x) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label R)" apply (rule_tac a="partition_label SC" and auth'="SyncSend" and ep="partition_label EP" and t="partition_label RM" and auth="Receive" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp, rule reads_Control_rev, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal (5 subgoals):
 1. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph
 2. SyncSend \<in> {Notify, SyncSend, Reset}
 3. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 4. Receive \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label R)" apply (rule_tac ep="partition_label EP" and b="partition_label SC" in read_sync_ep_read_senders) apply (rule r_reads_ep, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label R)
 2. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_reads_a : "partition_label NicA \<in> subjectReads SACAuthGraph (partition_label R)" apply (rule_tac a="partition_label NicA" and auth'="Reset" and ep="partition_label NicA" and t="partition_label RM" and auth="Receive" in reads_read_queued_thread_read_ep) apply (simp_all add:reads_Control_rev[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicA \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal (5 subgoals):
 1. (partition_label NicA, Reset, partition_label NicA) \<in> SACAuthGraph
 2. Reset \<in> {Notify, SyncSend, Reset}
 3. (partition_label RM, Receive, partition_label NicA) \<in> SACAuthGraph
 4. Receive \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label R)" apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) apply (rule r_reads_sc, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicC \<in> subjectReads SACAuthGraph (partition_label R) proof (prove)
goal (2 subgoals):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label R)
 2. (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_affects_bd : "x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac auth="Write" in affects_write) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (2 subgoals):
 1. x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> (partition_label R, Write, x) \<in> SACAuthGraph
 2. x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> Write \<in> {Control, Write} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac l="partition_label R" and ep="partition_label R" in affects_recv) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (2 subgoals):
 1. (partition_label R, Receive, partition_label R) \<in> SACAuthGraph
 2. (partition_label RM, SyncSend, partition_label R) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_affects_a : "partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac l="partition_label R" and ep="partition_label R" and l'="partition_label RM" and auth="Receive" in affects_reset) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (4 subgoals):
 1. (partition_label R, Reset, partition_label R) \<in> SACAuthGraph
 2. (partition_label RM, Receive, partition_label R) \<in> SACAuthGraph
 3. Receive \<in> {SyncSend, Receive}
 4. (partition_label RM, Write, partition_label NicA) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_affects_ntfn3 : "partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac l="partition_label R" and auth="Receive" in affects_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (2 subgoals):
 1. (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph
 2. Receive \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma r_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac l="partition_label R" in affects_ep_bound_trans) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label NTFN2) \<in> SACAuthGraph \<and> (partition_label R, Notify, ntfn) \<in> SACAuthGraph
theory PolicySystemSAC

lemma r_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label R)" apply (rule_tac l="partition_label R" in affects_ep_bound_trans) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects SACAuthGraph (partition_label R) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label EP) \<in> SACAuthGraph \<and> (partition_label R, Notify, ntfn) \<in> SACAuthGraph
theory PolicySystemSAC

lemma rm_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label RM)" apply (rule_tac ep="partition_label EP" in read_sync_ep_read_senders) apply (simp_all add:reads_ep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label RM)
 2. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label RM)" apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) apply (rule rm_reads_sc, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicC \<in> subjectReads SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label RM)
 2. (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_affects_via_control : "x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label RM)" apply (rule_tac l="partition_label RM" and auth="Control" in affects_write) apply (simp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> (partition_label RM, Control, x) \<in> SACAuthGraph
 2. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> Control \<in> {Control, Write} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label RM)" apply (rule_tac auth="Receive" in affects_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 2. Receive \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label RM)" apply (rule_tac l="partition_label RM" and ep="partition_label EP" in affects_recv) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectAffects SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 2. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label RM)" apply (rule_tac l="partition_label RM" and auth="Receive" in affects_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. (partition_label RM, Receive, partition_label NTFN2) \<in> SACAuthGraph
 2. Receive \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma rm_affects_ntfn3 : "partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label RM)" apply (rule_tac l="partition_label RM" in affects_ep_bound_trans) apply clarsimp by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label RM) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label NTFN3) \<in> SACAuthGraph \<and> (partition_label RM, Notify, ntfn) \<in> SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb = partition_label RM \<and> ntfn = partition_label EP \<or> tcb = partition_label SC \<and> ntfn = partition_label NTFN1 \<or> tcb = partition_label RM \<and> ntfn = partition_label NTFN2 \<or> tcb = partition_label R \<and> ntfn = partition_label NTFN3 \<or> ntfn = tcb \<or> tcb = partition_label RM \<and> ntfn = partition_label R \<or> tcb = partition_label RM \<and> ntfn = partition_label NicA \<or> tcb = partition_label RM \<and> ntfn = partition_label NicB \<or> tcb = partition_label RM \<and> ntfn = partition_label NicD \<or> (\<exists>z. (tcb = partition_label RM \<and> z = partition_label R \<or> tcb = partition_label RM \<and> z = partition_label NicA \<or> tcb = partition_label RM \<and> z = partition_label NicB \<or> tcb = partition_label RM \<and> z = partition_label NicD) \<and> (z = partition_label RM \<and> ntfn = partition_label R \<or> z = partition_label RM \<and> ntfn = partition_label NicA \<or> z = partition_label RM \<and> ntfn = partition_label NicB \<or> z = partition_label RM \<and> ntfn = partition_label NicD))) \<and> (tcb = partition_label R \<or> partition_label NTFN3 = tcb) \<and> (ntfn = partition_label RM \<or> ntfn = partition_label R \<or> ntfn = partition_label NicA \<or> ntfn = partition_label NicB \<or> ntfn = partition_label NicD \<or> (\<exists>z. (z = partition_label R \<or> z = partition_label NicA \<or> z = partition_label NicB \<or> z = partition_label NicD) \<and> (z = partition_label RM \<and> ntfn = partition_label R \<or> z = partition_label RM \<and> ntfn = partition_label NicA \<or> z = partition_label RM \<and> ntfn = partition_label NicB \<or> z = partition_label RM \<and> ntfn = partition_label NicD)))
theory PolicySystemSAC

lemma ep_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label EP)" apply (rule_tac ep="partition_label EP" in read_sync_ep_read_senders) apply (rule reads_lrefl, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label EP) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label EP)
 2. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ep_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label EP)" apply (rule_tac ep="partition_label EP" and b="partition_label RM" in read_sync_ep_read_receivers) apply (rule reads_lrefl, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label EP) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label EP)
 2. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ep_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label EP)" apply (rule_tac t="partition_label SC" and p="partition_label NicC" in reads_read_thread_read_pages) apply (rule ep_reads_sc, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicC \<in> subjectReads SACAuthGraph (partition_label EP) proof (prove)
goal (2 subgoals):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label EP)
 2. (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ep_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label EP)" apply (rule_tac l="partition_label EP" and l'="partition_label SC" and auth="SyncSend" and ep="partition_label EP" in affects_reset) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label EP) proof (prove)
goal (4 subgoals):
 1. (partition_label EP, Reset, partition_label EP) \<in> SACAuthGraph
 2. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph
 3. SyncSend \<in> {SyncSend, Receive}
 4. (partition_label SC, Write, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ep_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label EP)" apply (rule_tac ep="partition_label NTFN2" in affects_ep_bound_trans) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label EP) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label NTFN2) \<in> SACAuthGraph \<and> (partition_label EP, Notify, ntfn) \<in> SACAuthGraph
theory PolicySystemSAC

lemma ep_affects_rm_controls : "x \<in> RMControls \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label EP)" apply (rule_tac l="partition_label EP" and ep="partition_label EP" and auth="SyncSend" and l'="partition_label RM" in affects_send) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> RMControls \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label EP) proof (prove)
goal (4 subgoals):
 1. x \<in> RMControls \<Longrightarrow> (partition_label EP, SyncSend, partition_label EP) \<in> SACAuthGraph
 2. x \<in> RMControls \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. x \<in> RMControls \<Longrightarrow> (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 4. x \<in> RMControls \<Longrightarrow> (partition_label RM, Write, x) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn1_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NTFN1)" apply (rule_tac ep="partition_label NTFN1" in read_sync_ep_read_receivers) apply (rule reads_lrefl, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label NTFN1) proof (prove)
goal (2 subgoals):
 1. partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label NTFN1)
 2. (partition_label SC, Receive, partition_label NTFN1) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn1_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN1)" apply (rule_tac b="partition_label RM" and ep="partition_label EP" in read_sync_ep_read_receivers) apply (rule ntfn1_reads_ep, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN1) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN1)
 2. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn2_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN2)" apply (rule_tac ep="partition_label NTFN2" in read_sync_ep_read_receivers) apply (rule reads_lrefl, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN2) proof (prove)
goal (2 subgoals):
 1. partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label NTFN2)
 2. (partition_label RM, Receive, partition_label NTFN2) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn2_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN2)" apply (rule_tac ep="partition_label EP" and auth="Receive" and t="partition_label RM" and auth'="Reset" and a="partition_label EP" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp, rule ntfn2_reads_rm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN2) proof (prove)
goal (5 subgoals):
 1. (partition_label EP, Reset, partition_label EP) \<in> SACAuthGraph
 2. Reset \<in> {Notify, SyncSend, Reset}
 3. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 4. Receive \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN2) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn3_reads_r : "partition_label R \<in> subjectReads SACAuthGraph (partition_label NTFN3)" apply (rule_tac ep="partition_label NTFN3" in read_sync_ep_read_receivers) apply (rule reads_lrefl, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label R \<in> subjectReads SACAuthGraph (partition_label NTFN3) proof (prove)
goal (2 subgoals):
 1. partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label NTFN3)
 2. (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn3_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN3)" apply (rule_tac b="partition_label R" in reads_read_page_read_thread) apply (rule ntfn3_reads_r, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN3) proof (prove)
goal (2 subgoals):
 1. partition_label R \<in> subjectReads SACAuthGraph (partition_label NTFN3)
 2. (partition_label RM, Write, partition_label R) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn3_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN3)" apply (rule_tac t="partition_label RM" and auth="Receive" and auth'="SyncSend" and a="partition_label SC" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp, rule ntfn3_reads_rm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN3) proof (prove)
goal (5 subgoals):
 1. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph
 2. SyncSend \<in> {Notify, SyncSend, Reset}
 3. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 4. Receive \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN3) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn123_reads_c : "x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) apply (erule insertE, simp only:, rule ntfn1_reads_sc, erule insertE, simp only:, rule ntfn2_reads_sc, erule insertE, simp only:, rule ntfn3_reads_sc, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label x)
 2. x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal (1 subgoal):
 1. x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!