theory ExampleSystemPolicyFlows

lemma Sys3_policyFlows_correct_fw : "(a,b) \<in> policyFlows Sys3AuthGraph \<Longrightarrow> (a,b) \<in> Sys3PolicyFlows" apply (induct a b rule:policyFlows.induct) apply (simp add:partsSubjectAffects_def label_can_affect_partition_def) 
   (* Partition l *)
    apply (erule imageE) apply simp apply (case_tac "x \<in> {T3, UT3, EP3}") 
    (* x in {T3, UT3, EP3} *)
     apply (simp add:Sys3Reads_correct Sys3Reads_def) apply (case_tac "l \<in> {T3, UT3}") 
     (* l in {T3, UT3} *)
      apply (simp add:Sys3Affects_correct Sys3Affects_def Sys3PolicyFlows_def) apply (erule exE) apply ((erule disjE)+, simp, simp, simp)+ 
    (* l not in {T3, UT3} *)
     apply (simp) apply (case_tac l) apply (simp, simp, simp) apply (auto simp:Sys3PolicyFlows_def)[1] apply (simp add:Sys3PolicyFlows_def) apply (erule exE) apply (erule conjE, drule IRQ3Affects) apply (blast) 
    (* x not in {T3, UT3, EP3} *)
     apply (case_tac x) apply (simp, simp, simp, simp) apply (erule exE) apply (erule conjE) apply (frule IRQ3ReadsAndAffects, assumption) apply (simp add: Sys3PolicyFlows_def) 
   (* PSched *)
    apply (case_tac d, simp add: Sys3PolicyFlows_def) apply (rename_tac a) apply (case_tac a) apply (auto simp: Sys3PolicyFlows_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> policyFlows Sys3AuthGraph \<Longrightarrow> (a, b) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l. d \<in> partsSubjectAffects Sys3AuthGraph l \<Longrightarrow> (Partition l, d) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l. d \<in> Partition ` {x. \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x)} \<Longrightarrow> (Partition l, d) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l. d \<in> Partition ` {x. \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x)} \<Longrightarrow> (Partition l, d) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; x \<in> {x. \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x)}\<rbrakk> \<Longrightarrow> (Partition l, d) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x)\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (4 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (4 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (4 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3; x = T3 \<or> x = UT3 \<or> x = EP3; l = T3 \<or> l = UT3\<rbrakk> \<Longrightarrow> l = UT3 \<and> x = UT3 \<or> l = UT3 \<and> x = EP3 \<or> l = UT3 \<and> x = T3 \<or> l = T3 \<and> x = T3 \<or> l = T3 \<and> x = UT3 \<or> l = T3 \<and> x = EP3 \<or> l = EP3 \<and> x = UT3 \<or> l = EP3 \<and> x = EP3 \<or> l = EP3 \<and> x = T3 \<or> l = IRQ3 \<and> x = IRQ3
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (4 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition x; x = T3 \<or> x = UT3 \<or> x = EP3; l = T3 \<or> l = UT3; da = OrdinaryLabel UT3 \<or> da = OrdinaryLabel EP3 \<or> da = OrdinaryLabel T3\<rbrakk> \<Longrightarrow> l = UT3 \<and> x = UT3 \<or> l = UT3 \<and> x = EP3 \<or> l = UT3 \<and> x = T3 \<or> l = T3 \<and> x = T3 \<or> l = T3 \<and> x = UT3 \<or> l = T3 \<and> x = EP3 \<or> l = EP3 \<and> x = UT3 \<or> l = EP3 \<and> x = EP3 \<or> l = EP3 \<and> x = T3 \<or> l = IRQ3 \<and> x = IRQ3
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<notin> {T3, UT3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (6 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = UT3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = T3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = EP3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 5. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 6. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (4 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel EP3) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l = EP3\<rbrakk> \<Longrightarrow> (Partition EP3, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l \<noteq> T3 \<and> l \<noteq> UT3; l = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<and> (d = OrdinaryLabel UT3 \<or> d = OrdinaryLabel EP3 \<or> d = OrdinaryLabel T3); x = T3 \<or> x = UT3 \<or> x = EP3; l = IRQ3\<rbrakk> \<Longrightarrow> x = IRQ3
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition x; x = T3 \<or> x = UT3 \<or> x = EP3; l = IRQ3; da \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<and> (da = OrdinaryLabel UT3 \<or> da = OrdinaryLabel EP3 \<or> da = OrdinaryLabel T3)\<rbrakk> \<Longrightarrow> x = IRQ3
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (3 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition x; x = T3 \<or> x = UT3 \<or> x = EP3; l = IRQ3; da = OrdinaryLabel UT3 \<or> da = OrdinaryLabel EP3 \<or> da = OrdinaryLabel T3; da = OrdinaryLabel IRQ3\<rbrakk> \<Longrightarrow> x = IRQ3
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (5 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}; x = UT3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 2. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}; x = T3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 3. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}; x = EP3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 4. \<And>d l x. \<lbrakk>d = Partition x; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel x); x \<notin> {T3, UT3, EP3}; x = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition x) \<in> Sys3PolicyFlows
 5. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x. \<lbrakk>d = Partition IRQ3; \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3); x = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition IRQ3) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition IRQ3; x = IRQ3; da \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l) \<and> da \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)\<rbrakk> \<Longrightarrow> (Partition l, Partition IRQ3) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition IRQ3; x = IRQ3; da \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l); da \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)\<rbrakk> \<Longrightarrow> (Partition l, Partition IRQ3) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d l x da. \<lbrakk>d = Partition IRQ3; x = IRQ3; da \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel l); da \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3); l = IRQ3\<rbrakk> \<Longrightarrow> (Partition l, Partition IRQ3) \<in> Sys3PolicyFlows
 2. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (1 subgoal):
 1. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (1 subgoal):
 1. \<And>d. (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d x1. d = Partition x1 \<Longrightarrow> x1 = EP3 \<or> x1 = UT3 \<or> x1 = T3 \<or> x1 = IRQ3
 2. \<And>d. d = PSched \<Longrightarrow> (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (2 subgoals):
 1. \<And>d a. d = Partition a \<Longrightarrow> a = EP3 \<or> a = UT3 \<or> a = T3 \<or> a = IRQ3
 2. \<And>d. d = PSched \<Longrightarrow> (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal (5 subgoals):
 1. \<And>d a. \<lbrakk>d = Partition a; a = UT3\<rbrakk> \<Longrightarrow> a = EP3 \<or> a = UT3 \<or> a = T3 \<or> a = IRQ3
 2. \<And>d a. \<lbrakk>d = Partition a; a = T3\<rbrakk> \<Longrightarrow> a = EP3 \<or> a = UT3 \<or> a = T3 \<or> a = IRQ3
 3. \<And>d a. \<lbrakk>d = Partition a; a = EP3\<rbrakk> \<Longrightarrow> a = EP3 \<or> a = UT3 \<or> a = T3 \<or> a = IRQ3
 4. \<And>d a. \<lbrakk>d = Partition a; a = IRQ3\<rbrakk> \<Longrightarrow> a = EP3 \<or> a = UT3 \<or> a = T3 \<or> a = IRQ3
 5. \<And>d. d = PSched \<Longrightarrow> (PSched, d) \<in> Sys3PolicyFlows proof (prove)
goal:
No subgoals!