theory FinalCaps

lemma silc_inv_triv:
  assumes kheap: "\<And>P x. \<lbrace>\<lambda>s. P (kheap s x)\<rbrace> f \<lbrace>\<lambda>_ s. P (kheap s x)\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda> _ s. P (cdt s)\<rbrace>"
  assumes cte: "\<And>Q P slot. \<lbrace>\<lambda>s. Q (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (cte_wp_at P slot s)\<rbrace>"
  assumes typ_at: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at T p 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 (rule conjI) apply (intro allI impI) apply (erule use_valid) apply (rule hoare_vcg_ex_lift) apply (rule cap_table_at_lift_valid[OF typ_at]) apply blast apply (rule conjI) apply (clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (drule_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 (elim exE conjE | simp)+ apply (rule_tac x=ab in exI, rule conjI, rule_tac x=bb in exI) apply (erule (1) use_valid[OF _ cte]) apply (assumption) apply (rule conjI) apply (case_tac "cte_wp_at ((=) cap) (aa, ba) s") apply assumption apply (drule use_valid[OF _ cte[where Q="\<lambda> x. \<not> x"]]) apply assumption apply blast apply (case_tac "intra_label_cap aag (aa, ba) s") apply (drule_tac use_valid[OF _ intra_label_cap_pres[OF cte]]) apply assumption apply blast apply assumption apply (simp add: silc_dom_equiv_def) apply (rule conjI) apply (erule use_valid[OF _ c]) apply simp apply (rule equiv_forI) apply (erule use_valid[OF _ kheap]) apply (fastforce 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 (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. (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)
 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. (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>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 (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. (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); 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. (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>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 (3 subgoals):
 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. (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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<lbrace>?P24 s a b x\<rbrace> f \<lbrace>\<lambda>a b. \<exists>sz. cap_table_at sz x b\<rbrace>
 2. \<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. (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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> ?P24 s a b x 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. (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>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 (3 subgoals):
 1. \<And>s a b x sz. \<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. (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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<lbrace>?P27 s a b x sz\<rbrace> f \<lbrace>\<lambda>rv. cap_table_at sz x\<rbrace>
 2. \<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. (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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>xa. ?P27 s a b x xa 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. (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>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 (2 subgoals):
 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. (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); pasObjectAbs aag x = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>xa. cap_table_at xa x 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. (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>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. (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>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 (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. (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>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)
 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. (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> 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. (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> 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; 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. (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> 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; 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; 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. (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> 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; 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; 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. (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> 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; 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; 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; 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. (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> 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; 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; 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. (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> 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; 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. (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> 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; 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; 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. (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> 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. \<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; 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\<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; 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); \<not> cte_wp_at ((=) cap) (aa, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s
 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; 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
 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. (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> 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; 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); \<not> cte_wp_at ((=) cap) (aa, ba) s\<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; 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. (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> 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. \<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; 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); \<not> cte_wp_at ((=) cap) (aa, ba) s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at (?P78 s a b aa ba cap) (?slot78 s a b aa ba cap) s
 2. \<And>s a b aa ba cap. \<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; 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); \<not> cte_wp_at ((=) cap) (aa, ba) s; \<not> cte_wp_at (?P78 s a b aa ba cap) (?slot78 s a b aa ba cap) b\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (aa, ba) s
 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; 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
 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. (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> 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>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; 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); \<not> cte_wp_at ((=) cap) (aa, ba) s; \<not> cte_wp_at ((=) cap) (aa, ba) b\<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; 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. (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> 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; 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. (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> 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; 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); intra_label_cap aag (aa, ba) s\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (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; 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); \<not> intra_label_cap aag (aa, ba) s\<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. (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> 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. \<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; 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); intra_label_cap aag (aa, ba) s\<rbrakk> \<Longrightarrow> intra_label_cap (?aag85 s a b aa ba cap) (?slot85 s a b aa ba cap) s
 2. \<And>s a b aa ba cap. \<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; 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); intra_label_cap aag (aa, ba) s; intra_label_cap (?aag85 s a b aa ba cap) (?slot85 s a b aa ba cap) b\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (aa, ba) s
 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; 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); \<not> intra_label_cap aag (aa, ba) s\<rbrakk> \<Longrightarrow> \<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. (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> 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>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; 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); intra_label_cap aag (aa, ba) s; intra_label_cap aag (aa, ba) b\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (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; 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); \<not> intra_label_cap aag (aa, ba) s\<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. (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> 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; 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); \<not> intra_label_cap aag (aa, ba) s\<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. (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> 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. (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> 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. (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); 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> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt b) \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap 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. (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); 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> 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. (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); 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 (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. (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); 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> 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. (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); 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. \<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); 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. (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); 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. (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); 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 s x proof (prove)
goal:
No subgoals!