theory FinalCaps

lemma cap_insert_silc_inv:
  "\<lbrace>silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) and
    K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and>
       pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace>
   cap_insert cap slot slot'
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cap_insert_def 
  (* The order here matters. The first two need to be first. *)
   apply (wp assert_wp hoare_weak_lift_imp_conj set_cap_silc_inv hoare_vcg_ex_lift
            set_untyped_cap_as_full_slots_holding_overlapping_caps_other[where aag=aag]
            get_cap_wp update_cdt_silc_inv | simp | wp (once) hoare_drop_imps)+ apply clarsimp apply (rule disj_dup) apply (rule conjI) apply (rule impI) apply (drule is_derived_overlaps) apply (erule nonempty_refs) apply (drule overlapping_slots_have_labelled_overlapping_caps) apply assumption apply simp apply fastforce apply (rule conjI) apply (rule impI) apply (drule cte_wp_at_norm) apply (elim conjE exE) apply (drule (1) cte_wp_at_eqD2) apply simp apply (drule_tac cap'=capa in is_derived_overlaps2) apply assumption apply (erule nonempty_refs) apply (drule overlapping_slots_have_labelled_overlapping_caps) apply assumption apply simp apply fastforce apply (drule silc_inv_all_children) apply (rule conjI) apply (fastforce simp: all_children_def simp del: split_paired_All)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) and K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace> cap_insert cap slot slot' \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) and K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace> do src_cap <- get_cap slot;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap slot';
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap slot;
set_cap cap slot';
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original slot) cap dest_original;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s slot');
update_cdt (\<lambda>cdt. cdt(slot' := if src_parent then Some slot else cdt slot));
do_extended_op (cap_insert_ext src_parent slot slot' src_p dest_p);
set_original slot' dest_original
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) and K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace> do src_cap <- get_cap slot;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap slot';
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap slot;
set_cap cap slot';
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original slot) cap dest_original;
src_p <- gets (\<lambda>s. cdt s slot);
dest_p <- gets (\<lambda>s. cdt s slot');
update_cdt (\<lambda>cdt. cdt(slot' := if src_parent then Some slot else cdt slot));
do_extended_op (cap_insert_ext src_parent slot slot' src_p dest_p);
set_original slot' dest_original
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> cte_wp_at (is_derived (cdt s) slot cap) slot s \<and> pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag (fst slot') \<noteq> SilcLabel \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) slot s \<longrightarrow> cte_wp_at ((=) NullCap) slot' s \<longrightarrow> (\<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> (\<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> (\<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> \<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 \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> silc_inv aag (?st139 s capa) s
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot')); \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a \<noteq> pasObjectAbs aag (fst slot') \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> (\<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot'))\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); \<exists>c. cte_wp_at ((=) c) slot s \<and> is_derived (cdt s) slot cap c\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); cte_wp_at ((=) c) slot s; is_derived (cdt s) slot cap c\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); cte_wp_at ((=) c) slot s; is_derived (cdt s) slot cap c; c = capa\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); cte_wp_at ((=) capa) slot s; is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> is_derived (cdt s) slot (?cap164 s capa c) capa
 2. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> obj_refs capa \<noteq> {} \<or> cap_irqs capa \<noteq> {}
 3. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; slot \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> obj_refs capa \<noteq> {} \<or> cap_irqs capa \<noteq> {}
 2. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; slot \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; slot \<in> slots_holding_overlapping_caps capa s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (4 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> silc_inv aag (?st167 s capa c) s
 2. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot))
 3. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 4. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (3 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot))
 2. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 3. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa c. \<lbrakk>silc_inv aag st s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) NullCap) slot' s; \<not> cap_points_to_label aag capa (pasObjectAbs aag (fst slot')); is_derived (cdt s) slot cap capa; c = capa; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps capa s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps capa s) \<and> pasObjectAbs aag a = SilcLabel
 2. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>silc_inv aag st s; cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a) \<and> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then Some slot else cdt s a)
 2. \<And>s capa. \<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s; pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot'); pasObjectAbs aag (fst slot') \<noteq> SilcLabel; cte_wp_at ((=) capa) slot s; cte_wp_at ((=) NullCap) slot' s; all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (\<lambda>a. if a = slot' then cdt s slot else cdt s a) proof (prove)
goal:
No subgoals!