kings-crown/FVELER_Isabelle huggingface dataset:
theory PolicyExample

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

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

lemma C_in_subjectAffects_CTR:
  "partition_label C \<in> subjectAffects example_auth_graph (partition_label CTR)" apply(rule affects_write[where auth="Write"], auto) done

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

lemma EP_in_subjectAffects_CTR:
  "partition_label EP \<in> subjectAffects example_auth_graph (partition_label CTR)" apply(rule affects_ep, auto) done

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

lemma NTFN1_in_subjectAffects_CTR:
  "partition_label NTFN1 \<in> subjectAffects example_auth_graph (partition_label CTR)" apply(rule affects_ep, auto) done

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

lemma RM_in_subjectAffects_CTR:
  "partition_label RM \<in> subjectAffects example_auth_graph (partition_label CTR)" apply(rule affects_send, auto) done

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

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

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

lemma CTR_in_subjectAffects_C:
  "partition_label CTR \<in> subjectAffects example_auth_graph (partition_label C)" apply(rule affects_write[where auth=Write], auto) done

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

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

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

lemma RM_in_subjectAffects_EP:
  "partition_label RM \<in> subjectAffects example_auth_graph (partition_label EP)" apply(rule affects_send, auto) done

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

lemma C_in_subjectAffects_EP:
  "partition_label C \<in> subjectAffects example_auth_graph (partition_label EP)" apply(rule affects_reset[where ep="partition_label EP" and l'="partition_label CTR"], auto) done

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

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

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

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

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

lemma EP_in_subjectAffects_RM:
  "partition_label EP \<in> subjectAffects example_auth_graph (partition_label RM)" apply(rule affects_ep, auto) done

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

lemma CTR_in_subjectAffects_RM:
  "partition_label CTR \<in> subjectAffects example_auth_graph (partition_label RM)" apply(rule affects_recv, auto) done

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

lemma NTFN2_in_subjectAffects_RM:
  "partition_label NTFN2 \<in> subjectAffects example_auth_graph (partition_label RM)" apply(rule affects_ep, auto) done

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

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

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

lemma partsSubjectAffects_T:
  "partsSubjectAffects example_auth_graph T = {Partition T,Partition NTFN1, Partition NTFN2, Partition CTR, Partition C, Partition EP, Partition RM}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_T | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph T = {Partition T, Partition NTFN1, Partition NTFN2, Partition CTR, Partition C, Partition EP, Partition RM} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_NTFN1:
  "partsSubjectAffects example_auth_graph NTFN1 = {Partition NTFN1, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_NTFN1 | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph NTFN1 = {Partition NTFN1, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_NTFN2:
  "partsSubjectAffects example_auth_graph NTFN2 = {Partition NTFN2, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN1}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_NTFN2 | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph NTFN2 = {Partition NTFN2, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN1} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_CTR:
  "partsSubjectAffects example_auth_graph CTR = {Partition NTFN1, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_CTR | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph CTR = {Partition NTFN1, Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_RM:
  "partsSubjectAffects example_auth_graph RM = {Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2, Partition NTFN1}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads subjectAffects_RM | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph RM = {Partition CTR, Partition C, Partition EP, Partition RM, Partition NTFN2, Partition NTFN1} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectReads_Low: "subjectReads example_auth_graph2 (partition_label Low) = {partition_label Low,partition_label SharedPage}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct, fastforce+) apply (auto intro: reads_read) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph2 (partition_label Low) = {partition_label Low, partition_label SharedPage} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph2 (partition_label Low) \<subseteq> {partition_label Low, partition_label SharedPage}
 2. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label Low) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph2 (partition_label Low) \<Longrightarrow> x \<in> {partition_label Low, partition_label SharedPage}
 2. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label Low) proof (prove)
goal (1 subgoal):
 1. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label Low) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectReads_SharedPage: "subjectReads example_auth_graph2 (partition_label SharedPage) = {partition_label Low,partition_label SharedPage}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct, fastforce+) apply (auto intro: reads_read_page_read_thread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph2 (partition_label SharedPage) = {partition_label Low, partition_label SharedPage} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph2 (partition_label SharedPage) \<subseteq> {partition_label Low, partition_label SharedPage}
 2. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label SharedPage) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph2 (partition_label SharedPage) \<Longrightarrow> x \<in> {partition_label Low, partition_label SharedPage}
 2. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label SharedPage) proof (prove)
goal (1 subgoal):
 1. {partition_label Low, partition_label SharedPage} \<subseteq> subjectReads example_auth_graph2 (partition_label SharedPage) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma High_in_subjectReads_NTFN:
  "partition_label High \<in> subjectReads example_auth_graph2 (partition_label NTFN)" apply(rule read_sync_ep_read_receivers) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label High \<in> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal (2 subgoals):
 1. ?ep \<in> subjectReads example_auth_graph2 (partition_label NTFN)
 2. (partition_label High, Receive, ?ep) \<in> example_auth_graph2 proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma SharedPage_in_subjectReads_NTFN:
  "partition_label SharedPage \<in> subjectReads example_auth_graph2 (partition_label NTFN)" apply(rule reads_read_thread_read_pages[OF High_in_subjectReads_NTFN]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SharedPage \<in> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal (1 subgoal):
 1. (partition_label High, Read, partition_label SharedPage) \<in> example_auth_graph2 proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma Low_in_subjectReads_NTFN:
  "partition_label Low \<in> subjectReads example_auth_graph2 (partition_label NTFN)" apply(rule reads_read_page_read_thread[OF SharedPage_in_subjectReads_NTFN]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label Low \<in> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal (1 subgoal):
 1. (partition_label Low, Write, partition_label SharedPage) \<in> example_auth_graph2 proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectReads_NTFN: "subjectReads example_auth_graph2 (partition_label NTFN) = {partition_label NTFN,partition_label High,partition_label SharedPage, partition_label Low}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct, fastforce+) apply (auto intro: High_in_subjectReads_NTFN Low_in_subjectReads_NTFN SharedPage_in_subjectReads_NTFN simp del: example_auth_graph2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph2 (partition_label NTFN) = {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph2 (partition_label NTFN) \<subseteq> {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low}
 2. {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph2 (partition_label NTFN) \<Longrightarrow> x \<in> {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low}
 2. {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal (1 subgoal):
 1. {partition_label NTFN, partition_label High, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label NTFN) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma SharedPage_in_subjectReads_High:
  "partition_label SharedPage \<in> subjectReads example_auth_graph2 (partition_label High)" apply(fastforce intro: reads_read_thread_read_pages) done

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

lemma Low_in_subjectReads_High:
  "partition_label Low \<in> subjectReads example_auth_graph2 (partition_label High)" apply(fastforce intro: reads_read_page_read_thread[OF SharedPage_in_subjectReads_High]) done

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

lemma subjectReads_High: "subjectReads example_auth_graph2 (partition_label High) = {partition_label High,partition_label NTFN, partition_label SharedPage,partition_label Low}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct, fastforce+) apply(auto intro: NTFN_in_subjectReads_High SharedPage_in_subjectReads_High Low_in_subjectReads_High simp del: example_auth_graph2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph2 (partition_label High) = {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low} proof (prove)
goal (2 subgoals):
 1. subjectReads example_auth_graph2 (partition_label High) \<subseteq> {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low}
 2. {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label High) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads example_auth_graph2 (partition_label High) \<Longrightarrow> x \<in> {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low}
 2. {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label High) proof (prove)
goal (1 subgoal):
 1. {partition_label High, partition_label NTFN, partition_label SharedPage, partition_label Low} \<subseteq> subjectReads example_auth_graph2 (partition_label High) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma SharedPage_in_subjectAffects_Low:
  "partition_label SharedPage \<in> subjectAffects example_auth_graph2 (partition_label Low)" apply(fastforce intro: affects_write) done

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

lemma NTFN_in_subjectAffects_Low:
  "partition_label NTFN \<in> subjectAffects example_auth_graph2 (partition_label Low)" apply(fastforce intro: affects_ep) done

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

lemma High_in_subjectAffects_Low:
  "partition_label High \<in> subjectAffects example_auth_graph2 (partition_label Low)" apply(rule affects_send[where ep="partition_label NTFN"]) apply(auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label High \<in> subjectAffects example_auth_graph2 (partition_label Low) proof (prove)
goal (4 subgoals):
 1. (partition_label Low, ?auth, partition_label NTFN) \<in> example_auth_graph2
 2. ?auth \<in> {SyncSend, Notify, Call}
 3. (?l', Receive, partition_label NTFN) \<in> example_auth_graph2
 4. (?l', Write, partition_label High) \<in> example_auth_graph2 proof (prove)
goal:
No subgoals!