theory FinalCaps

lemma set_cap_silc_inv:
  "\<lbrace>(\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
         \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                      pasObjectAbs aag (fst lslot) = SilcLabel)) and
    silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
   set_cap cap slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: valid_def silc_inv_def) apply (intro conjI impI allI) apply (erule use_valid) apply (rule hoare_vcg_ex_lift) apply (rule cap_table_at_lift_valid[OF set_cap_typ_at]) apply blast apply (case_tac "slot = (a,ba)") apply (subgoal_tac "cap = capa") apply (simp) apply (erule impE) apply (simp add: intra_label_cap_def) apply (elim conjE exE) apply (blast dest: cte_wp_at_eqD2) apply (elim exE conjE) apply (rule_tac x=aa in exI, simp) apply (rule_tac x=bb in exI) apply (erule use_valid[OF _ set_cap_slots_holding_overlapping_caps_other[where aag=aag]]) apply fastforce apply (rule cte_wp_at_eqD2) apply blast apply (drule_tac s=slot in sym, simp) apply (erule use_valid[OF _ set_cap_cte_wp_at_triv], rule TrueI) apply (drule_tac x=a in spec, drule_tac x=ba in spec, drule_tac x= capa in spec) apply (erule impE, rule conjI) apply (fastforce elim!: hoare_contrapositive[OF set_cap_neg_cte_wp_at_other, simplified]) apply (rule_tac P="\<lambda> s. intra_label_cap aag (a, ba) s" in hoare_contrapositive) apply (rule intra_label_cap_pres) apply (erule set_cap_neg_cte_wp_at_other) apply (erule conjE, assumption) apply assumption apply clarsimp apply (rule_tac x=aa in exI, simp) apply (rule_tac x=bb in exI) apply (erule use_valid[OF _ set_cap_slots_holding_overlapping_caps_other[where aag=aag]]) apply fastforce apply (erule use_valid[OF _ set_cap_rvk_cdt_ct_ms(4)],simp) apply (simp add: silc_dom_equiv_def) apply (rule equiv_forI) apply (erule use_valid) unfolding set_cap_def apply (wp set_object_wp get_object_wp hoare_weak_lift_imp | simp add: split_def | wpc)+ apply clarsimp apply (rule conjI) apply fastforce apply (fastforce elim: equiv_forE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (fst slot) \<noteq> SilcLabel \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel)) and silc_inv aag st\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 (4 subgoals):
 1. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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>?P29 s b x\<rbrace> set_cap cap slot \<lbrace>\<lambda>a b. \<exists>sz. cap_table_at sz x b\<rbrace>
 2. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> ?P29 s b x s
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b x sz. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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>?P32 s b x sz\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. cap_table_at sz x\<rbrace>
 2. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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. ?P32 s b x xa s
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) s); \<not> cap_points_to_label aag capa (pasObjectAbs aag a) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (6 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag a)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa; \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 4. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 6. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (6 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag a)) \<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); cte_wp_at ((=) capa) (a, ba) b \<and> (\<exists>cap. cte_wp_at ((=) cap) (a, ba) b \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag a)); slot = (a, ba); cap = capa\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag a)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa; \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 4. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 6. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (6 subgoals):
 1. \<And>s b a ba capa capaa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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> (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> cap_points_to_label aag cap (pasObjectAbs aag a)) \<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); slot = (a, ba); cap = capa; cte_wp_at ((=) capa) (a, ba) b; cte_wp_at ((=) capaa) (a, ba) b; \<not> cap_points_to_label aag capaa (pasObjectAbs aag a)\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag a)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa; \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 4. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 6. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba); cap = capa; \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); slot = (a, ba); cap = capa; cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); slot = (a, ba); cap = capa; cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>ba. (aa, ba) \<in> slots_holding_overlapping_caps capa b
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; ((), b) \<in> fst (set_cap capa (a, ba) 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); slot = (a, ba); cap = capa; cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps capa b
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag a \<noteq> SilcLabel; 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); slot = (a, ba); cap = capa; cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst (aa, bb)) \<noteq> pasObjectAbs aag (fst (a, ba))
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cap = capa
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) (?p187 s b a ba capa) (?s187 s b a ba capa)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (?p187 s b a ba capa) (?s187 s b a ba capa)
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot = (a, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (a, ba) b
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) slot b \<and> \<not> intra_label_cap aag slot b; (a, ba) = slot\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) slot b
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); cte_wp_at ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); cte_wp_at ((=) capa) (a, ba) s \<and> \<not> intra_label_cap aag (a, ba) s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) capa) (a, ba) s
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, ba) s
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, ba) s
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (6 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<lbrace>intra_label_cap aag (a, ba)\<rbrace> ?f238 s b a ba capa \<lbrace>?Q238 s b a ba capa\<rbrace>
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<not> ?Q238 s b a ba capa (?r238 s b a ba capa) (?s'238 s b a ba capa)
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> (?r238 s b a ba capa, ?s'238 s b a ba capa) \<in> fst (?f238 s b a ba capa s)
 4. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 6. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (6 subgoals):
 1. \<And>s b a ba capa P. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P (a, ba) s\<rbrace> ?f238 s b a ba capa \<lbrace>\<lambda>_ s. \<not> cte_wp_at P (a, ba) s\<rbrace>
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, ba) (?s'238 s b a ba capa)
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> (?r238 s b a ba capa, ?s'238 s b a ba capa) \<in> fst (?f238 s b a ba capa s)
 4. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 6. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (5 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (a, ba) (?s'238 s b a ba capa)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> (?r238 s b a ba capa, ?s'238 s b a ba capa) \<in> fst (set_cap (?cap243 s b a ba capa) slot s)
 3. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 5. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (4 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba)\<rbrakk> \<Longrightarrow> (?r238 s b a ba capa, b) \<in> fst (set_cap (?cap243 s b a ba capa) slot s)
 2. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 4. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 ((=) capa) (a, ba) b \<and> \<not> intra_label_cap aag (a, ba) b; slot \<noteq> (a, ba); \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); slot \<noteq> (a, ba); cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>ba. (a, ba) \<in> slots_holding_overlapping_caps capa b) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); slot \<noteq> (a, ba); cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>ba. (aa, ba) \<in> slots_holding_overlapping_caps capa b
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); slot \<noteq> (a, ba); cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps capa b
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (3 subgoals):
 1. \<And>s b a ba capa aa bb. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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); slot \<noteq> (a, ba); cte_wp_at ((=) capa) (a, ba) b; \<not> intra_label_cap aag (a, ba) b; pasObjectAbs aag aa = SilcLabel; (aa, bb) \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> (aa, bb) \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst (aa, bb)) \<noteq> pasObjectAbs aag (fst slot)
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 3. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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)
 2. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> silc_dom_equiv aag st b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; ((), b) \<in> fst (set_cap cap slot s); \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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 (2 subgoals):
 1. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> \<lbrace>?P279 s b x\<rbrace> set_cap cap slot \<lbrace>\<lambda>a b. kheap st x = kheap b x\<rbrace>
 2. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> ?P279 s b x s proof (prove)
goal (2 subgoals):
 1. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> \<lbrace>?P279 s b x\<rbrace> case slot of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>a b. kheap st x = kheap b x\<rbrace>
 2. \<And>s b x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> ?P279 s b x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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> \<forall>ko. ko_at ko (fst slot) s \<longrightarrow> (x = fst slot \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd slot \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> kheap st (fst slot) = Some (CNode x (\<lambda>a. if a = snd slot then Some cap else xa a))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_reply := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_caller := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)))))))) \<and> (x \<noteq> fst slot \<longrightarrow> (\<forall>xa xb. ko = CNode xa xb \<longrightarrow> snd slot \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> kheap st x = kheap s x) \<and> ((\<exists>x. ko = TCB x) \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st x = kheap s x)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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; ko_at ko (fst slot) s\<rbrakk> \<Longrightarrow> (x = fst slot \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd slot \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> kheap st (fst slot) = Some (CNode x (\<lambda>a. if a = snd slot then Some cap else xa a))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_reply := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_caller := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)))))))) \<and> (x \<noteq> fst slot \<longrightarrow> (\<forall>xa xb. ko = CNode xa xb \<longrightarrow> snd slot \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> kheap st x = kheap s x) \<and> ((\<exists>x. ko = TCB x) \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st x = kheap s x)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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; ko_at ko (fst slot) s\<rbrakk> \<Longrightarrow> x = fst slot \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd slot \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> kheap st (fst slot) = Some (CNode x (\<lambda>a. if a = snd slot then Some cap else xa a))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_reply := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_caller := cap\<rparr>))) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st (fst slot) = Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)))))))
 2. \<And>s x ko. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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; ko_at ko (fst slot) s\<rbrakk> \<Longrightarrow> x \<noteq> fst slot \<longrightarrow> (\<forall>xa xb. ko = CNode xa xb \<longrightarrow> snd slot \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> kheap st x = kheap s x) \<and> ((\<exists>x. ko = TCB x) \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st x = kheap s x))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>pasObjectAbs aag (fst slot) \<noteq> SilcLabel; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); 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; ko_at ko (fst slot) s\<rbrakk> \<Longrightarrow> x \<noteq> fst slot \<longrightarrow> (\<forall>xa xb. ko = CNode xa xb \<longrightarrow> snd slot \<in> dom xb \<and> well_formed_cnode_n xa xb \<longrightarrow> kheap st x = kheap s x) \<and> ((\<exists>x. ko = TCB x) \<longrightarrow> (snd slot = tcb_cnode_index 0 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd slot = tcb_cnode_index (Suc 0) \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd slot = tcb_cnode_index 2 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd slot = tcb_cnode_index 3 \<longrightarrow> kheap st x = kheap s x) \<and> (snd slot \<noteq> tcb_cnode_index 3 \<longrightarrow> snd slot = tcb_cnode_index 4 \<longrightarrow> kheap st x = kheap s x))))) proof (prove)
goal:
No subgoals!