theory FinalCaps

lemma silc_inv_pres:
  assumes l: "\<And>ptr P.
              \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and K (pasObjectAbs aag ptr = SilcLabel)\<rbrace>
              f
              \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>"
  assumes ncte: "\<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>"
  shows "\<lbrace>silc_inv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (clarsimp simp: valid_def silc_inv_def) apply (clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (rule conjI) apply (intro allI impI) apply (frule_tac x=x in spec, erule (1) impE) apply (erule exE, rename_tac sz, rule_tac x=sz in exI) apply (simp add: obj_at_def) apply (elim exE conjE, rename_tac ko) apply (rule_tac x=ko in exI, simp) apply (erule use_valid[OF _ l]) apply simp apply (clarsimp simp: silc_inv_def obj_at_def slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (rule conjI) apply clarsimp apply (frule_tac x=aa in spec, drule_tac x=ba in spec, drule_tac x=cap in spec) apply (subgoal_tac "cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa,ba) s") apply (erule (1) impE) apply (elim exE conjE)+ apply (rule_tac x=ab in exI, rule conjI, rule_tac x=bb in exI) apply (erule use_valid[OF _ cte_wp_at_pres_from_kheap'[where R="silc_inv aag st"]]) apply (rule l) apply simp apply (clarsimp simp: silc_inv_def tcb_at_typ obj_at_def
                           slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply assumption apply (rule conjI) apply (erule (1) hoare_contrapositive[OF ncte, simplified]) apply (rule hoare_contrapositive[OF intra_label_cap_pres, simplified, OF ncte], assumption+) apply (rule conjI) apply (erule use_valid[OF _ c]) apply simp apply (simp add: silc_dom_equiv_def) apply (rule equiv_forI) apply (erule use_valid[OF _ l]) apply (fastforce simp: silc_inv_def obj_at_def slots_holding_overlapping_caps_def2
                         ctes_wp_at_def silc_dom_equiv_def
                   elim: equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x b)) \<and> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps cap b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x b)) \<and> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>sz. cap_table_at sz x b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; \<exists>sz. cap_table_at sz x s\<rbrakk> \<Longrightarrow> \<exists>sz. cap_table_at sz x b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x sz. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; cap_table_at sz x s\<rbrakk> \<Longrightarrow> cap_table_at sz x b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x sz. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz ko. kheap s x = Some ko \<and> is_cap_table sz ko); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; \<exists>ko. kheap s x = Some ko \<and> is_cap_table sz ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap b x = Some ko \<and> is_cap_table sz ko
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x sz ko. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz ko. kheap s x = Some ko \<and> is_cap_table sz ko); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; kheap s x = Some ko; is_cap_table sz ko\<rbrakk> \<Longrightarrow> \<exists>ko. kheap b x = Some ko \<and> is_cap_table sz ko
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x sz ko. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz ko. kheap s x = Some ko \<and> is_cap_table sz ko); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; kheap s x = Some ko; is_cap_table sz ko\<rbrakk> \<Longrightarrow> kheap b x = Some ko
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x sz ko. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz ko. kheap s x = Some ko \<and> is_cap_table sz ko); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; kheap s x = Some ko; is_cap_table sz ko\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>s. kheap s x = Some ko) and K (pasObjectAbs aag x = SilcLabel)) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s x sz ko. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz ko. kheap s x = Some ko \<and> is_cap_table sz ko); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel; kheap s x = Some ko; is_cap_table sz ko\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> (\<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> \<forall>a ba cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b \<longrightarrow> (\<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s; \<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, ba) b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) b
 2. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag ab = SilcLabel
 3. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s a b aa ba cap ab bb ptr P. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and K (pasObjectAbs (?aag70 s a b aa ba cap ab bb) ptr = ?l70 s a b aa ba cap ab bb)\<rbrace> f \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>s a b aa ba cap ab bb. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) and silc_inv aag st and K (pasObjectAbs (?aag70 s a b aa ba cap ab bb) (fst (ab, bb)) = ?l70 s a b aa ba cap ab bb)) s
 3. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag ab = SilcLabel
 4. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 5. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s a b aa ba cap ab bb. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) and silc_inv aag st and K (pasObjectAbs aag (fst (ab, bb)) = SilcLabel)) s
 2. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag ab = SilcLabel
 3. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b aa ba cap ab bb. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag ab = SilcLabel
 3. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba cap ab bb. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s; \<not> intra_label_cap aag (aa, ba) s; pasObjectAbs aag ab = SilcLabel; cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (ab, bb) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag ab = SilcLabel
 2. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s
 2. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (aa, ba) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba cap. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); cte_wp_at ((=) cap) (aa, ba) b; \<not> intra_label_cap aag (aa, ba) b; cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (aa, ba) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st)\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> kheap st x = kheap b x proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) (a, b) s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>s. kheap st x = kheap s x) and K (pasObjectAbs aag x = SilcLabel)) s proof (prove)
goal:
No subgoals!