theory PolicyExample

lemma RM_in_subjectReads_CTR:
  "partition_label RM \<in> subjectReads example_auth_graph (partition_label CTR)" apply(clarsimp) apply(rule_tac ep="partition_label EP" in read_sync_ep_read_receivers) apply(rule EP_in_subjectReads_CTR[simplified]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads example_auth_graph (partition_label CTR) 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 CTR) 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 CTR)
 2. (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 (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!