theory FinalCaps

lemma cap_revoke_silc_inv':
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
        drop_spec_ev[wp_split del] rec_del.simps[simp del]
  shows
  "s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs
                        and simple_sched_action and K (is_subject aag (fst slot))\<rbrace>
       cap_revoke slot
       \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" proof(induct rule: cap_revoke.induct[where ?a1.0=s]) case (1 slot s) show ?case apply (subst cap_revoke.simps) apply (rule hoare_pre_spec_validE) apply (wp "1.hyps") apply (wp spec_valid_conj_liftE2 | simp)+ apply (wp drop_spec_validE[OF valid_validE[OF preemption_point_silc_inv]]
                      cap_delete_silc_inv preemption_point_inv' | simp)+ apply (rule spec_valid_conj_liftE1) apply (rule validE_validE_R'[OF valid_validE[OF cap_delete_pas_refined]]) apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule drop_spec_validE[OF valid_validE[OF cap_delete_silc_inv]]) apply (wp drop_spec_validE[OF assertE_wp] drop_spec_validE[OF without_preemption_wp]
                    get_cap_wp drop_spec_validE[OF returnOk_wp])+ apply clarsimp apply (clarsimp cong: conj_cong simp: conj_comms) apply (rule conjI) apply (cases "next_revoke_cap slot s") apply (force simp: emptyable_def dest!: reply_slot_not_descendant split: if_splits) apply (rule all_children_descendants_of[OF cdt_change_allowed_all_children];
           force) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>slot s. (\<And>rv sta rva staa rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) sta); (Inr rvb, stb) \<in> fst ((returnOk $ descendants_of slot rva) staa); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stb); (Inr rvd, std) \<in> fst ((without_preemption $ get_cap rvc) stc); (Inr rve, ste) \<in> fst (assertE (rvd \<noteq> NullCap) std); (Inr rvf, stf) \<in> fst (cap_delete rvc ste); (Inr rvg, stg) \<in> fst (preemption_point stf)\<rbrakk> \<Longrightarrow> stg \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (state)
this:
\<lbrakk>(Inr ?rv, ?st) \<in> fst ((without_preemption $ get_cap slot) s); (Inr ?rva, ?sta) \<in> fst ((without_preemption $ gets cdt) ?st); (Inr ?rvb, ?stb) \<in> fst ((returnOk $ descendants_of slot ?rva) ?sta); ?rv \<noteq> NullCap \<and> ?rvb \<noteq> {}; (Inr ?rvc, ?stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) ?rvb) ?stb); (Inr ?rvd, ?std) \<in> fst ((without_preemption $ get_cap ?rvc) ?stc); (Inr ?rve, ?ste) \<in> fst (assertE (?rvd \<noteq> NullCap) ?std); (Inr ?rvf, ?stf) \<in> fst (cap_delete ?rvc ?ste); (Inr ?rvg, ?stg) \<in> fst (preemption_point ?stf)\<rbrakk> \<Longrightarrow> ?stg \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal (1 subgoal):
 1. \<And>slot s. (\<And>rv sta rva staa rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<lbrakk>(Inr rv, sta) \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, staa) \<in> fst ((without_preemption $ gets cdt) sta); (Inr rvb, stb) \<in> fst ((returnOk $ descendants_of slot rva) staa); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, stc) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) stb); (Inr rvd, std) \<in> fst ((without_preemption $ get_cap rvc) stc); (Inr rve, ste) \<in> fst (assertE (rvd \<noteq> NullCap) std); (Inr rvf, stf) \<in> fst (cap_delete rvc ste); (Inr rvg, stg) \<in> fst (preemption_point stf)\<rbrakk> \<Longrightarrow> stg \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>) \<Longrightarrow> s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> doE cap <- without_preemption $ get_cap slot;
cdt <- without_preemption $ gets cdt;
descendants <- returnOk $ descendants_of slot cdt;
whenE (cap \<noteq> NullCap \<and> descendants \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) descendants;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE)
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. s \<turnstile> \<lbrace>?P'\<rbrace> doE cap <- without_preemption $ get_cap slot;
cdt <- without_preemption $ gets cdt;
descendants <- returnOk $ descendants_of slot cdt;
whenE (cap \<noteq> NullCap \<and> descendants \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) descendants;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE)
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf s''f. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c); (Inr rve, s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d); (Inr rvf, s''f) \<in> fst (cap_delete rvc s''e)\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e rvf\<rbrace> preemption_point \<lbrace>\<lambda>rvg. silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c); (Inr rve, s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>?B16 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (10 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e s''f. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d); (Inr (), s''f) \<in> fst (cap_delete rvc s''e)\<rbrakk> \<Longrightarrow> \<lbrace>?P'29 rv s'' rva s''a rvb s''b rvc s''c rvd s''d () s''e ()\<rbrace> preemption_point \<lbrace>\<lambda>rv s. invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> is_subject aag (fst slot)\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e s''f. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d); (Inr (), s''f) \<in> fst (cap_delete rvc s''e)\<rbrakk> \<Longrightarrow> s''f \<turnstile> \<lbrace>?P'24 rv s'' rva s''a rvb s''b rvc s''c rvd s''d () s''e ()\<rbrace> preemption_point \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c); (Inr rve, s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve\<rbrace> cap_delete rvc \<lbrace>\<lambda>a b. (pas_refined aag b \<and> ?P'29 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e a b) \<and> ?P'24 rv s'' rva s''a rvb s''b rvc s''c rvd s''d rve s''e a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 10. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>a b. pas_refined aag b \<and> invs b \<and> valid_list b \<and> valid_sched b \<and> simple_sched_action b \<and> is_subject aag (fst slot) \<and> silc_inv aag st b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>?B14 rv s'' rva s''a rvb s''b rvc s''c rvd s''d\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (9 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> \<lbrace>?P81 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>, -
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'80 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. ?P81 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b \<and> ?P'80 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'80 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> ?P'80 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'91 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> ?P'91 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'103 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. valid_sched s \<and> simple_sched_action s \<and> is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> valid_list b \<and> ?P'103 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'115 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. simple_sched_action s \<and> is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> valid_list b \<and> (valid_sched and simple_sched_action) b \<and> ?P'115 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'127 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv s. is_subject aag (fst slot) \<and> silc_inv aag st s\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> valid_list b \<and> (valid_sched and simple_sched_action) b \<and> simple_sched_action b \<and> ?P'127 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (8 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d s''e. \<lbrakk>(rv, s'') \<in> fst (get_cap slot s); (rva, s''a) \<in> fst (gets cdt s''); (Inr rvb, s''b) \<in> fst (returnOk (descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (rvc, s''c) \<in> fst (select_ext (next_revoke_cap slot) rvb s''b); (rvd, s''d) \<in> fst (get_cap rvc s''c); (Inr (), s''e) \<in> fst (assertE (rvd \<noteq> NullCap) s''d)\<rbrakk> \<Longrightarrow> s''e \<turnstile> \<lbrace>?P'139 rv s'' rva s''a rvb s''b rvc s''c rvd s''d ()\<rbrace> cap_delete rvc \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> valid_list b \<and> (valid_sched and simple_sched_action) b \<and> simple_sched_action b \<and> is_subject aag (fst slot) \<and> ?P'139 rv s'' rva s''a rvb s''b rvc s''c rvd s''d a b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (7 subgoals):
 1. \<And>rv s'' rva s''a rvb s''b rvc s''c rvd s''d. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b); (Inr rvd, s''d) \<in> fst ((without_preemption $ get_cap rvc) s''c)\<rbrakk> \<Longrightarrow> s''d \<turnstile> \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. (cdt_change_allowed' aag rvc and pas_refined aag and einvs and simple_sched_action and emptyable rvc) b \<and> (invs and emptyable rvc) b \<and> valid_list b \<and> (valid_sched and simple_sched_action) b \<and> simple_sched_action b \<and> is_subject aag (fst slot) \<and> (silc_inv aag st and einvs and simple_sched_action and emptyable rvc and pas_refined aag and cdt_change_allowed' aag rvc) b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>rv s'' rva s''a rvb s''b rvc s''c. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}; (Inr rvc, s''c) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rvb) s''b)\<rbrakk> \<Longrightarrow> s''c \<turnstile> \<lbrace>?B12 rv s'' rva s''a rvb s''b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>?B13 rv s'' rva s''a rvb s''b rvc s''c\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>rv s'' rva s''a rvb s''b. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s''); (Inr rvb, s''b) \<in> fst ((returnOk $ descendants_of slot rva) s''a); rv \<noteq> NullCap \<and> rvb \<noteq> {}\<rbrakk> \<Longrightarrow> s''b \<turnstile> \<lbrace>?P11 rv s'' rva s''a rvb\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rvb \<lbrace>?B12 rv s'' rva s''a rvb s''b\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>rv s'' rva s''a. \<lbrakk>(Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s); (Inr rva, s''a) \<in> fst ((without_preemption $ gets cdt) s'')\<rbrakk> \<Longrightarrow> s''a \<turnstile> \<lbrace>?B5 rv s'' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>\<lambda>a b. (rv \<noteq> NullCap \<and> a \<noteq> {} \<longrightarrow> ?P11 rv s'' rva s''a a b) \<and> (\<not> (rv \<noteq> NullCap \<and> a \<noteq> {}) \<longrightarrow> silc_inv aag st b)\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>rv s''. (Inr rv, s'') \<in> fst ((without_preemption $ get_cap slot) s) \<Longrightarrow> s'' \<turnstile> \<lbrace>?B4 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?B5 rv s''\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. s \<turnstile> \<lbrace>?P'\<rbrace> without_preemption $ get_cap slot \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. (silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap \<noteq> NullCap \<and> descendants_of slot (cdt s) \<noteq> {} \<longrightarrow> next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (cdt_change_allowed' aag (next_revoke_cap slot s) and pas_refined aag and einvs and simple_sched_action and emptyable (next_revoke_cap slot s)) s \<and> (invs and emptyable (next_revoke_cap slot s)) s \<and> valid_list s \<and> (valid_sched and simple_sched_action) s \<and> simple_sched_action s \<and> is_subject aag (fst slot) \<and> (silc_inv aag st and einvs and simple_sched_action and emptyable (next_revoke_cap slot s) and pas_refined aag and cdt_change_allowed' aag (next_revoke_cap slot s)) s)) \<and> (\<not> (cap \<noteq> NullCap \<and> descendants_of slot (cdt s) \<noteq> {}) \<longrightarrow> silc_inv aag st s) proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> emptyable (next_revoke_cap slot s) s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> emptyable (next_revoke_cap slot s) s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s proof (prove)
goal (2 subgoals):
 1. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> emptyable (next_revoke_cap slot s) s
 2. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (next_revoke_cap slot s) s proof (prove)
goal (2 subgoals):
 1. \<And>cap capa a b. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap; next_revoke_cap slot s = (a, b)\<rbrakk> \<Longrightarrow> emptyable (next_revoke_cap slot s) s
 2. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (next_revoke_cap slot s) s proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>silc_inv aag st s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; cap \<noteq> NullCap; descendants_of slot (cdt s) \<noteq> {}; next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) capa) (next_revoke_cap slot s) s; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (next_revoke_cap slot s) s proof (prove)
goal:
No subgoals! proof (state)
this:
s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>

goal:
No subgoals!