kings-crown/FVELER_Isabelle huggingface dataset:
theory PolicyExample

lemma C_in_subjectReads_NTFN2:
  "partition_label C \<in> subjectReads example_auth_graph (partition_label NTFN2)" apply(rule reads_read_thread_read_pages) apply (rule CTR_in_subjectReads_NTFN2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectReads example_auth_graph (partition_label NTFN2) proof (prove)
goal (2 subgoals):
 1. ?t \<in> subjectReads example_auth_graph (partition_label NTFN2)
 2. (?t, Read, partition_label C) \<in> example_auth_graph proof (prove)
goal (1 subgoal):
 1. (partition_label CTR, Read, partition_label C) \<in> example_auth_graph proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectReads_NTFN2:
  "partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label NTFN2)" apply(rule reads_read_queued_thread_read_ep[where t="partition_label CTR" and a="partition_label NTFN1"], auto intro: CTR_in_subjectReads_NTFN2[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectReads_CTR:
  "partition_label EP \<in> subjectReads example_auth_graph (partition_label CTR)" apply(rule_tac a="partition_label CTR" and t="partition_label CTR" in reads_read_queued_thread_read_ep) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads example_auth_graph (partition_label CTR) proof (prove)
goal (5 subgoals):
 1. (partition_label CTR, ?auth', partition_label EP) \<in> example_auth_graph
 2. ?auth' \<in> {Notify, SyncSend, Reset}
 3. (partition_label CTR, ?auth, partition_label EP) \<in> example_auth_graph
 4. ?auth \<in> {SyncSend, Receive}
 5. partition_label CTR \<in> subjectReads example_auth_graph (partition_label CTR) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectReads_CTR:
  "partition_label C \<in> subjectReads example_auth_graph (partition_label CTR)" apply(rule reads_read, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectReads example_auth_graph (partition_label CTR) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectReads_CTR:
  "partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label CTR)" apply(rule_tac t="partition_label CTR" and auth="Receive" and a="partition_label T" and auth'="Notify" in reads_read_queued_thread_read_ep) apply (auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label CTR) proof (prove)
goal (5 subgoals):
 1. (partition_label T, Notify, partition_label NTFN1) \<in> example_auth_graph
 2. Notify \<in> {Notify, SyncSend, Reset}
 3. (partition_label CTR, Receive, partition_label NTFN1) \<in> example_auth_graph
 4. Receive \<in> {SyncSend, Receive}
 5. partition_label CTR \<in> subjectReads example_auth_graph (partition_label CTR) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectReads_C:
  "partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label C)" apply(rule_tac a="partition_label T" and ep="partition_label NTFN1" and t="partition_label CTR" in reads_read_queued_thread_read_ep) apply (auto intro: reads_read) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal (5 subgoals):
 1. (partition_label T, ?auth', partition_label NTFN1) \<in> example_auth_graph
 2. ?auth' \<in> {Notify, SyncSend, Reset}
 3. (partition_label CTR, ?auth, partition_label NTFN1) \<in> example_auth_graph
 4. ?auth \<in> {SyncSend, Receive}
 5. partition_label CTR \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectReads_C:
  "partition_label EP \<in> subjectReads example_auth_graph (partition_label C)" apply(rule_tac a="partition_label CTR" and t="partition_label CTR" in reads_read_queued_thread_read_ep) apply (auto intro: reads_read) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal (5 subgoals):
 1. (partition_label CTR, ?auth', partition_label EP) \<in> example_auth_graph
 2. ?auth' \<in> {Notify, SyncSend, Reset}
 3. (partition_label CTR, ?auth, partition_label EP) \<in> example_auth_graph
 4. ?auth \<in> {SyncSend, Receive}
 5. partition_label CTR \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma RM_in_subjectReads_C:
  "partition_label RM \<in> subjectReads example_auth_graph (partition_label C)" apply(clarsimp) apply(rule read_sync_ep_read_receivers[OF EP_in_subjectReads_C[simplified]]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label C) proof (prove)
goal (1 subgoal):
 1. (partition_label RM, Receive, partition_label EP) \<in> insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y}))))))))) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectReads_C:
  "partition_label CTR \<in> subjectReads example_auth_graph (partition_label C)" apply(rule reads_read, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads example_auth_graph (partition_label C) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectReads_EP:
  "partition_label CTR \<in> subjectReads example_auth_graph (partition_label EP)" apply(clarsimp) apply(rule_tac ep="partition_label EP" in read_sync_ep_read_senders) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label EP) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label EP)
 2. (partition_label CTR, SyncSend, partition_label EP) \<in> insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y}))))))))) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectReads_EP:
  "partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label EP)" apply(rule reads_read_queued_thread_read_ep[where a="partition_label NTFN1", OF _ _ _ _ CTR_in_subjectReads_EP]) apply(auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal (4 subgoals):
 1. (partition_label NTFN1, ?auth', partition_label NTFN1) \<in> example_auth_graph
 2. ?auth' \<in> {Notify, SyncSend, Reset}
 3. (partition_label CTR, ?auth, partition_label NTFN1) \<in> example_auth_graph
 4. ?auth \<in> {SyncSend, Receive} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectReads_EP:
  "partition_label C \<in> subjectReads example_auth_graph (partition_label EP)" apply(rule reads_read_thread_read_pages[OF CTR_in_subjectReads_EP]) apply(auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal (1 subgoal):
 1. (partition_label CTR, Read, partition_label C) \<in> example_auth_graph proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN2_in_subjectReads_EP:
  "partition_label NTFN2 \<in> subjectReads example_auth_graph (partition_label EP)" apply(rule reads_read_queued_thread_read_ep[where a="partition_label NTFN2", OF _ _ _ _ RM_in_subjectReads_EP]) apply(auto) done

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

lemma subjectReads_EP:
  "subjectReads example_auth_graph (partition_label EP) = {partition_label EP,partition_label CTR,partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct; auto) apply(auto simp: subjectReads_EP'[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph (partition_label EP) = {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph (partition_label EP) \<subseteq> {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2}
 2. {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2} \<subseteq> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph (partition_label EP) \<Longrightarrow> x \<in> {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2}
 2. {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2} \<subseteq> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal (1 subgoal):
 1. {partition_label EP, partition_label CTR, partition_label NTFN1, partition_label C, partition_label RM, partition_label NTFN2} \<subseteq> subjectReads example_auth_graph (partition_label EP) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN2_in_subjectReads_RM:
   "partition_label NTFN2 \<in> subjectReads example_auth_graph (partition_label RM)" apply(rule reads_ep, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectReads_RM:
   "partition_label EP \<in> subjectReads example_auth_graph (partition_label RM)" apply(rule reads_ep, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectReads_RM:
   "partition_label CTR \<in> subjectReads example_auth_graph (partition_label RM)" apply(rule read_sync_ep_read_senders[where ep="partition_label EP", OF EP_in_subjectReads_RM], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectReads_RM:
   "partition_label C \<in> subjectReads example_auth_graph (partition_label RM)" apply(rule reads_read_thread_read_pages[where t="partition_label CTR", OF CTR_in_subjectReads_RM], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectReads_RM:
   "partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label RM)" apply(rule reads_read_queued_thread_read_ep[where a="partition_label T" and t="partition_label CTR", OF _ _ _ _ CTR_in_subjectReads_RM], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectReads_RM:
  "subjectReads example_auth_graph (partition_label RM) = {partition_label RM, partition_label NTFN2,partition_label EP,partition_label CTR, partition_label C, partition_label NTFN1}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct; auto) apply(auto simp: subjectReads_RM'[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph (partition_label RM) = {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph (partition_label RM) \<subseteq> {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1}
 2. {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1} \<subseteq> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph (partition_label RM) \<Longrightarrow> x \<in> {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1}
 2. {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1} \<subseteq> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal (1 subgoal):
 1. {partition_label RM, partition_label NTFN2, partition_label EP, partition_label CTR, partition_label C, partition_label NTFN1} \<subseteq> subjectReads example_auth_graph (partition_label RM) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN1_in_subjectAffects_T:
  "partition_label NTFN1 \<in> subjectAffects example_auth_graph (partition_label T)
" apply(auto intro: affects_ep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN1 \<in> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN2_in_subjectAffects_T:
  "partition_label NTFN2 \<in> subjectAffects example_auth_graph (partition_label T)
" apply(auto intro: affects_ep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN2 \<in> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectAffects_T:
  "partition_label C \<in> subjectAffects example_auth_graph (partition_label T)
" apply(rule affects_send[where auth="Notify" and ep="partition_label NTFN1"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectAffects_T:
  "partition_label CTR \<in> subjectAffects example_auth_graph (partition_label T)
" apply(rule affects_send[where auth="Notify" and ep="partition_label NTFN1"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma RM_in_subjectAffects_T:
  "partition_label RM \<in> subjectAffects example_auth_graph (partition_label T)
" apply(rule affects_send[where auth="Notify" and ep="partition_label NTFN2"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectAffects_T:
  "partition_label EP \<in> subjectAffects example_auth_graph (partition_label T)" by (rule affects_ep_bound_trans, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects example_auth_graph (partition_label T)
theory PolicyExample

lemma subjectAffects_T:
  "subjectAffects example_auth_graph (partition_label T) = {partition_label NTFN1,partition_label NTFN2,partition_label T,partition_label C, partition_label CTR, partition_label RM, partition_label EP}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.cases; fastforce) apply(auto simp: subjectAffects_T'[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph (partition_label T) = {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP}
 2. {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP} \<subseteq> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph (partition_label T) \<Longrightarrow> x \<in> {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP}
 2. {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP} \<subseteq> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal (1 subgoal):
 1. {partition_label NTFN1, partition_label NTFN2, partition_label T, partition_label C, partition_label CTR, partition_label RM, partition_label EP} \<subseteq> subjectAffects example_auth_graph (partition_label T) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma CTR_in_subjectAffects_NTFN1:
  "partition_label CTR \<in> subjectAffects example_auth_graph (partition_label NTFN1)" apply(rule affects_send[where ep="partition_label NTFN1"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label CTR \<in> subjectAffects example_auth_graph (partition_label NTFN1) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma C_in_subjectAffects_NTFN1:
  "partition_label C \<in> subjectAffects example_auth_graph (partition_label NTFN1)" apply(rule affects_send[where ep="partition_label NTFN1"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label C \<in> subjectAffects example_auth_graph (partition_label NTFN1) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectAffects_NTFN1:
  "subjectAffects example_auth_graph (partition_label NTFN1) = {partition_label NTFN1,partition_label CTR,partition_label C}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.cases; fastforce) apply(auto simp: subjectAffects_NTFN1'[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph (partition_label NTFN1) = {partition_label NTFN1, partition_label CTR, partition_label C} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph (partition_label NTFN1) \<subseteq> {partition_label NTFN1, partition_label CTR, partition_label C}
 2. {partition_label NTFN1, partition_label CTR, partition_label C} \<subseteq> subjectAffects example_auth_graph (partition_label NTFN1) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph (partition_label NTFN1) \<Longrightarrow> x \<in> {partition_label NTFN1, partition_label CTR, partition_label C}
 2. {partition_label NTFN1, partition_label CTR, partition_label C} \<subseteq> subjectAffects example_auth_graph (partition_label NTFN1) proof (prove)
goal (1 subgoal):
 1. {partition_label NTFN1, partition_label CTR, partition_label C} \<subseteq> subjectAffects example_auth_graph (partition_label NTFN1) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma RM_in_subjectAffects_NTFN2:
  "partition_label RM \<in> subjectAffects example_auth_graph (partition_label NTFN2)" apply(rule affects_send[where ep="partition_label NTFN2"], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectAffects example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma EP_in_subjectAffects_NTFN2:
  "partition_label EP \<in> subjectAffects example_auth_graph (partition_label NTFN2)" apply(rule affects_ep_bound_trans, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects example_auth_graph (partition_label NTFN2) proof (prove)
goal:
No subgoals!