theory Syscall_IF

lemma cap_revoke_spec_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del] drop_spec_ev[wp_split del]
        rec_del.simps[simp del] split_paired_All[simp del] split_paired_Ex[simp del]
  shows "spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs
                                                        and simple_sched_action and pas_refined aag
                                                        and K (is_subject aag (fst slot)))
                               (cap_revoke slot)" proof (induct rule: cap_revoke.induct[where ?a1.0=s]) case (1 slot s) show ?case apply (rule spec_gen_asm) apply (rule spec_equiv_valid_guard_imp) apply (subst cap_revoke.simps) apply (subst spec_equiv_valid_def2) apply (subst rel_sum_comb_equals[symmetric]) apply (rule_tac R'="(=)" in spec_equiv_valid_2_inv_bindE) apply (rule_tac R'="equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id"
                     in spec_equiv_valid_2_inv_bindE) apply (rule_tac R'="(=)" in spec_equiv_valid_2_inv_bindE) apply (simp add: rel_sum_comb_equals
                          del: Inr_in_liftE_simp without_preemption_def fun_app_def) apply (rule spec_equiv_valid_2_inv_by_spec_equiv_valid[OF _ refl refl refl]) apply (wp whenE_spec_ev) apply (rule "1.hyps") apply (assumption | erule | simp)+ apply (wp drop_spec_ev[OF preemption_point_reads_respects_f]
                                 drop_spec_ev[OF cap_delete_reads_respects_f[where st=st]]
                                 select_ext_ev preemption_point_inv'
                                 cap_delete_pas_refined cap_delete_silc_inv[where st=st]
                                 cap_delete_only_timer_irq_inv[where st=st' and irq=irq]
                                 drop_spec_ev[OF assertE_ev] drop_spec_ev[OF liftE_ev]
                                 get_cap_wp select_ev drop_spec_ev2_inv[OF liftE_ev2]
                                 reads_respects_f[OF get_cap_rev, where st=st and aag=aag]
                              | simp (no_asm) add: returnOk_def | rule next_revoke_eq'
                              | (simp add: pred_conj_def, erule conjE, assumption)
                              | (rule irq_state_independent_A_conjI, simp)+)+ apply (rule_tac P="K(all_children (\<lambda>x. aag_can_read aag (fst x)) rva)"
                       and P'="K(all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a)"
                        in drop_spec_ev2_inv[OF return_ev2]) apply simp apply (rule_tac P="\<lambda>x. aag_can_read aag (fst x)" in all_children_descendants_equal) apply (frule aag_can_read_self) apply (simp add: equiv_for_def split del: if_split)+ apply (wp drop_spec_ev2_inv[OF liftE_ev2] gets_evrv | simp)+ apply (wp drop_spec_ev2_inv[OF liftE_ev2] gets_evrv
               reads_respects_f[OF get_cap_rev, where st=st and Q=\<top>,simplified equiv_valid_def2]) apply clarsimp+ apply (frule all_children_subjectReads[simplified comp_def]) apply clarsimp apply (rule conjI) apply (force simp: reads_equiv_f_def intro: equiv_forI
                  elim: reads_equivE affects_equivE equiv_forD) apply clarsimp apply (rule conjI, erule(1) all_children_descendants_of, force) apply (clarsimp simp: conj_comms) apply (intro conjI) by (case_tac "next_revoke_cap slot s", force simp: emptyable_def dest: reply_slot_not_descendant
        | force elim: all_children_descendants_of[OF cdt_change_allowed_all_children])+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot) 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> spec_reads_respects_f stg aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot)) \<Longrightarrow> spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot) 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> spec_reads_respects_f ?stg aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot)

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> spec_reads_respects_f stg aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot)) \<Longrightarrow> spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot) proof (prove)
goal (1 subgoal):
 1. spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot) proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<Longrightarrow> spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) (cap_revoke slot) proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> spec_reads_respects_f s aag l ?P'2 (cap_revoke slot)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> spec_reads_respects_f s aag l ?P'2 (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)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) (=) ?P'2 ?P'2 (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) (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)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P'2 ?P'2 (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) (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)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (5 subgoals):
 1. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?Q14 rv) (?Q'14 rv') (doE cdt <- without_preemption $ gets cdt;
descendants <- returnOk $ descendants_of slot cdt;
whenE (rv \<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) (doE cdt <- without_preemption $ gets cdt;
descendants <- returnOk $ descendants_of slot cdt;
whenE (rv' \<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)
 2. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>?Q14\<rbrace>, -
 3. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>?Q'14\<rbrace>, -
 4. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 5. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s proof (prove)
goal (8 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'a (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?Q16 rv s' rv' rva) (?Q'16 rv s' rv' rv'a) (doE descendants <- returnOk $ descendants_of slot rva;
whenE (rv \<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) (doE descendants <- returnOk $ descendants_of slot rv'a;
whenE (rv' \<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)
 2. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>?Q16 rv s' rv'\<rbrace>, -
 3. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>?Q'16 rv s' rv'\<rbrace>, -
 4. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 6. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 7. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 8. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s proof (prove)
goal (11 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rvb, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'b (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?Q22 rv s' rv' rva s'a rv'a rvb) (?Q'22 rv s' rv' rva s'a rv'a rv'b) (whenE (rv \<noteq> NullCap \<and> rvb \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) rvb;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE)) (whenE (rv' \<noteq> NullCap \<and> rv'b \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) rv'b;
cap <- without_preemption $ get_cap child;
assertE (cap \<noteq> NullCap);
cap_delete child;
preemption_point;
cap_revoke slot
odE))
 2. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv s' rv' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>?Q22 rv s' rv' rva s'a rv'a\<rbrace>, -
 3. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'27 rv s' rv' rv'a\<rbrace> returnOk $ descendants_of slot rv'a \<lbrace>?Q'22 rv s' rv' rva s'a rv'a\<rbrace>, -
 4. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'a (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?P24 rv s' rv' rva) (?P'26 rv s' rv' rv'a) (returnOk $ descendants_of slot rva) (returnOk $ descendants_of slot rv'a)
 5. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. ?P24 rv s' rv' rva and ?S25 rv s' rv' rva\<rbrace>, -
 6. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. ?P'26 rv s' rv' rv'a and ?S'27 rv s' rv' rv'a\<rbrace>, -
 7. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 8. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 9. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 10. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'b (reads_equiv_f aag) (affects_equiv aag l) (=) (?Q22 rv' s' rv' rva s'a rv'a rv'b) (?Q'22 rv' s' rv' rva s'a rv'a rv'b) (whenE (rv' \<noteq> NullCap \<and> rv'b \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) rv'b;
cap <- without_preemption $ get_cap child;
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE)) (whenE (rv' \<noteq> NullCap \<and> rv'b \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) rv'b;
cap <- without_preemption $ get_cap child;
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE))
 2. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv s' rv' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>?Q22 rv s' rv' rva s'a rv'a\<rbrace>, -
 3. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'27 rv s' rv' rv'a\<rbrace> returnOk $ descendants_of slot rv'a \<lbrace>?Q'22 rv s' rv' rva s'a rv'a\<rbrace>, -
 4. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'a (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?P24 rv s' rv' rva) (?P'26 rv s' rv' rv'a) (returnOk $ descendants_of slot rva) (returnOk $ descendants_of slot rv'a)
 5. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. ?P24 rv s' rv' rva and ?S25 rv s' rv' rva\<rbrace>, -
 6. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. ?P'26 rv s' rv' rv'a and ?S'27 rv s' rv' rv'a\<rbrace>, -
 7. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 8. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 9. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 10. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b\<rbrakk> \<Longrightarrow> spec_reads_respects_f s'b aag l (?Q36 s' rv' rv' rva s'a rv'a rv'b) (whenE (rv' \<noteq> NullCap \<and> rv'b \<noteq> {}) (doE child <- without_preemption $ select_ext (next_revoke_cap slot) rv'b;
cap <- without_preemption $ get_cap child;
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE))
 2. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S25 rv s' rv' rva\<rbrace> returnOk $ descendants_of slot rva \<lbrace>?Q36 s' rv rv' rva s'a rv'a\<rbrace>, -
 3. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?S'27 rv s' rv' rv'a\<rbrace> returnOk $ descendants_of slot rv'a \<lbrace>?Q'37 s' rv rv' rva s'a rv'a\<rbrace>, -
 4. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'a (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?P24 rv s' rv' rva) (?P'26 rv s' rv' rv'a) (returnOk $ descendants_of slot rva) (returnOk $ descendants_of slot rv'a)
 5. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. ?P24 rv s' rv' rva and ?S25 rv s' rv' rva\<rbrace>, -
 6. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. ?P'26 rv s' rv' rv'a and ?S'27 rv s' rv' rv'a\<rbrace>, -
 7. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 8. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 9. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 10. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
A total of 11 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?Q'37 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?Q36 s' rv' rv' proof (prove)
goal (21 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''d aag l (?Q69 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg) (cap_revoke slot)
 2. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''c aag l (?P'73 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf) preemption_point
 3. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b)\<rbrakk> \<Longrightarrow> \<lbrace>?P''72 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf\<rbrace> preemption_point \<lbrace>?Q69 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c\<rbrace>, -
 4. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''b aag l (?P'68 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve) (cap_delete rvc)
 5. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a)\<rbrakk> \<Longrightarrow> \<lbrace>?P''67 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve\<rbrace> cap_delete rvc \<lbrace>\<lambda>a b. ?P'73 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b a b \<and> ?P''72 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b a b\<rbrace>, -
 6. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s'')\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''a aag l (?P'63 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd) (assertE (rvd \<noteq> NullCap))
 7. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P''62 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. ?P'68 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a a b \<and> ?P''67 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a a b\<rbrace>, -
 8. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s''. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s'' aag l (?P'58 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc) (without_preemption $ get_cap rvc)
 9. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s''. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b)\<rbrakk> \<Longrightarrow> \<lbrace>?P''57 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>\<lambda>a b. ?P'63 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' a b \<and> ?P''62 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' a b\<rbrace>, -
 10. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}\<rbrakk> \<Longrightarrow> spec_reads_respects_f s'b aag l (?P'48 s' rv' rv' rva s'a rv'a rv'b) (without_preemption $ select_ext (next_revoke_cap slot) rv'b)
A total of 21 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?P'50 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P'48 s' rv' rv'
\<lambda>s' rv'. ?P''49 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P''47 s' rv' rv' proof (prove)
goal (29 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rv75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?st75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst ((without_preemption $ get_cap slot) s)
 2. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rva75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?sta75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst ((without_preemption $ gets cdt) (?st75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 3. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rvb75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?stb75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst ((returnOk $ descendants_of slot (?rva75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d)) (?sta75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 4. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> ?rv75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d \<noteq> NullCap \<and> ?rvb75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d \<noteq> {}
 5. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rvc75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?stc75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) (?rvb75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d)) (?stb75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 6. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rvd75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?std75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst ((without_preemption $ get_cap (?rvc75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d)) (?stc75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 7. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rve75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?ste75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst (assertE (?rvd75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d \<noteq> NullCap) (?std75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 8. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rvf75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), ?stf75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) \<in> fst (cap_delete (?rvc75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d) (?ste75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 9. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b); (Inr rvg, s''d) \<in> fst (preemption_point s''c)\<rbrakk> \<Longrightarrow> (Inr (?rvg75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d), s''d) \<in> fst (preemption_point (?stf75 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c rvg s''d))
 10. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''c aag l (?P'73 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf) preemption_point
A total of 29 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?P'50 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P'48 s' rv' rv'
\<lambda>s' rv'. ?P''49 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P''47 s' rv' rv' proof (prove)
goal (20 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a s''b s''c. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst (returnOk (descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (rvc, s'') \<in> fst (select_ext (next_revoke_cap slot) rv'b s'b); (rvd, s''a) \<in> fst (get_cap rvc s''); (Inr (), s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr (), s''c) \<in> fst (cap_delete rvc s''b)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''c aag l (?P'73 rv' s' rv' rva s'a rv'a rv'b s'b rv'b rvc s'' rvd s''a () s''b ()) preemption_point
 2. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf s''c. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a); (Inr rvf, s''c) \<in> fst (cap_delete rvc s''b)\<rbrakk> \<Longrightarrow> \<lbrace>?P''72 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b rvf\<rbrace> preemption_point \<lbrace>\<lambda>a. silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))\<rbrace>, -
 3. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''b aag l (?P'68 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve) (cap_delete rvc)
 4. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s''); (Inr rve, s''b) \<in> fst (assertE (rvd \<noteq> NullCap) s''a)\<rbrakk> \<Longrightarrow> \<lbrace>?P''67 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve\<rbrace> cap_delete rvc \<lbrace>\<lambda>a b. ?P'73 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b a b \<and> ?P''72 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a rve s''b a b\<rbrace>, -
 5. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s'')\<rbrakk> \<Longrightarrow> spec_reads_respects_f s''a aag l (?P'63 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd) (assertE (rvd \<noteq> NullCap))
 6. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b); (Inr rvd, s''a) \<in> fst ((without_preemption $ get_cap rvc) s'')\<rbrakk> \<Longrightarrow> \<lbrace>?P''62 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd\<rbrace> assertE (rvd \<noteq> NullCap) \<lbrace>\<lambda>a b. ?P'68 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a a b \<and> ?P''67 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' rvd s''a a b\<rbrace>, -
 7. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s''. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b)\<rbrakk> \<Longrightarrow> spec_reads_respects_f s'' aag l (?P'58 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc) (without_preemption $ get_cap rvc)
 8. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s''. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}; (Inr rvc, s'') \<in> fst ((without_preemption $ select_ext (next_revoke_cap slot) rv'b) s'b)\<rbrakk> \<Longrightarrow> \<lbrace>?P''57 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc\<rbrace> without_preemption $ get_cap rvc \<lbrace>\<lambda>a b. ?P'63 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' a b \<and> ?P''62 rv s' rv' rva s'a rv'a rvb s'b rv'b rvc s'' a b\<rbrace>, -
 9. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}\<rbrakk> \<Longrightarrow> spec_reads_respects_f s'b aag l (?P'48 s' rv' rv' rva s'a rv'a rv'b) (without_preemption $ select_ext (next_revoke_cap slot) rv'b)
 10. \<And>rv s' rv' rva s'a rv'a rvb s'b rv'b. \<lbrakk>is_subject aag (fst slot); (Inr rv', s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; (Inr rv'b, s'b) \<in> fst ((returnOk $ descendants_of slot rva) s'a); rvb = rv'b; rv' \<noteq> NullCap \<and> rv'b \<noteq> {}\<rbrakk> \<Longrightarrow> \<lbrace>?P''47 s' rv' rv' rva s'a rv'a rv'b\<rbrace> without_preemption $ select_ext (next_revoke_cap slot) rv'b \<lbrace>\<lambda>a b. ?P'58 rv s' rv' rva s'a rv'a rvb s'b rv'b a b \<and> ?P''57 rv s' rv' rva s'a rv'a rvb s'b rv'b a b\<rbrace>, -
A total of 20 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?P'50 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P'48 s' rv' rv'
\<lambda>s' rv'. ?P''49 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?P''47 s' rv' rv' proof (prove)
goal (8 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s'a (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) (?P24 rv s' rv' rva) (?P'26 rv s' rv' rv'a) (return (Inr (descendants_of slot rva))) (return (Inr (descendants_of slot rv'a)))
 2. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. ?P24 rv s' rv' rva and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv rv' (descendants_of slot rva) a cap) (?st'396 s' rv rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 3. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. ?P'26 rv s' rv' rv'a and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 4. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 6. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 7. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 8. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s
flex-flex pairs:
\<lambda>s' rv'. ?irq397 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq398 s' rv' rv'
\<lambda>s' rv'. ?st'395 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'396 s' rv' rv'
\<lambda>s' rv' rva rv'b s cap. ?irq377 s' rv' rva rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv' rva. ?irq398 s' rv' rv'
\<lambda>s' rv' rva rv'b s cap. ?st'375 s' rv' rva rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv' rva. ?st'396 s' rv' rv' proof (prove)
goal (8 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'; (Inr rva, s'a) \<in> fst ((without_preemption $ gets cdt) s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; K (all_children (\<lambda>x. aag_can_read aag (fst x)) rva) s; K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) t; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> ((=) \<oplus> (=)) (Inr (descendants_of slot rva)) (Inr (descendants_of slot rv'a))
 2. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rva) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv rv' (descendants_of slot rva) a cap) (?st'396 s' rv rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 3. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 4. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 6. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 7. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 8. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s
flex-flex pairs:
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq397 s' rv' rv'
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'395 s' rv' rv'
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv' rv'b s cap. ?irq407 s' rv' rv'b (next_revoke_cap slot s) cap ()
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv' rv'b s cap. ?st'406 s' rv' rv'b (next_revoke_cap slot s) cap () proof (prove)
goal (8 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> descendants_of slot rva = descendants_of slot rv'a
 2. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rva) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv rv' (descendants_of slot rva) a cap) (?st'396 s' rv rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 3. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 4. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 6. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 7. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 8. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s
flex-flex pairs:
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq397 s' rv' rv'
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'395 s' rv' rv'
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv' rv'b s cap. ?irq407 s' rv' rv'b (next_revoke_cap slot s) cap ()
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv' rv'b s cap. ?st'406 s' rv' rv'b (next_revoke_cap slot s) cap () proof (prove)
goal (11 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. aag_can_read aag (fst x)) id rva rv'a
 2. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. aag_can_read aag (fst x)) rva
 3. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a
 4. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> aag_can_read aag (fst slot)
 5. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rva) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv rv' (descendants_of slot rva) a cap) (?st'396 s' rv rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 6. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 7. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 8. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 9. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 10. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
A total of 11 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq397 s' rv' rv'
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'395 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?irq407 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?irq398 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?st'406 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?st'396 s' rv' rv' proof (prove)
goal (11 subgoals):
 1. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t; aag_can_read aag (fst slot)\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. aag_can_read aag (fst x)) id rva rv'a
 2. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. aag_can_read aag (fst x)) rva
 3. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a
 4. \<And>rv s' rv' rva s'a rv'a s t. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'; (rva, s'a) \<in> fst (gets cdt s'); equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rva rv'a; all_children (\<lambda>x. aag_can_read aag (fst x)) rva; all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a; reads_equiv_f aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> aag_can_read aag (fst slot)
 5. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rva. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rva) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv rv' (descendants_of slot rva) a cap) (?st'396 s' rv rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 6. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 7. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 8. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 9. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 10. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
A total of 11 subgoals...
flex-flex pairs:
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq397 s' rv' rv'
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'395 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?irq407 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?irq398 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?st'406 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?st'396 s' rv' rv' proof (prove)
goal (7 subgoals):
 1. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (rv', s') \<in> fst (get_cap slot s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S19 rv'\<rbrace> liftE (gets cdt) \<lbrace>\<lambda>rva. (\<lambda>a. all_children (\<lambda>x. aag_can_read aag (fst x)) rva) and (\<lambda>a. next_revoke_cap slot a \<in> descendants_of slot rva \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq398 s' rv' rv' (descendants_of slot rva) a cap) (?st'396 s' rv' rv' (descendants_of slot rva) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a))\<rbrace>, -
 2. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'21 rv'\<rbrace> without_preemption $ gets cdt \<lbrace>\<lambda>rv'a. K (all_children (\<lambda>x. aag_can_read aag (fst x)) rv'a) and (\<lambda>a. True \<and> (next_revoke_cap slot a \<in> descendants_of slot rv'a \<longrightarrow> silc_inv aag st a \<and> aag_can_read aag (fst (next_revoke_cap slot a)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a) \<longrightarrow> silc_inv aag st a) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot a) a \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st a \<and> only_timer_irq_inv (?irq397 s' rv rv' (descendants_of slot rv'a) a cap) (?st'395 s' rv rv' (descendants_of slot rv'a) a cap) a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> silc_inv aag st a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> only_timer_irq_inv irq st' a \<and> invs a \<and> emptyable (next_revoke_cap slot a) a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> cdt_change_allowed' aag (next_revoke_cap slot a) a \<and> pas_refined aag a \<and> invs a \<and> valid_list a \<and> valid_sched a \<and> simple_sched_action a \<and> emptyable (next_revoke_cap slot a) a \<and> is_subject aag (fst slot))))\<rbrace>, -
 3. \<And>rv s' rv'. \<lbrakk>is_subject aag (fst slot); (Inr rv, s') \<in> fst ((without_preemption $ get_cap slot) s); rv = rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id) (?P18 rv) (?P'20 rv') (without_preemption $ gets cdt) (without_preemption $ gets cdt)
 4. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv. ?P18 rv and ?S19 rv\<rbrace>, -
 5. is_subject aag (fst slot) \<Longrightarrow> \<lbrace>?S14\<rbrace> without_preemption $ get_cap slot \<lbrace>\<lambda>rv'. ?P'20 rv' and ?S'21 rv'\<rbrace>, -
 6. is_subject aag (fst slot) \<Longrightarrow> spec_equiv_valid_2_inv s (reads_equiv_f aag) (affects_equiv aag l) ((=) \<oplus> (=)) ?P14 ?P14 (without_preemption $ get_cap slot) (without_preemption $ get_cap slot)
 7. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and ?S14) s
flex-flex pairs:
\<lambda>s' rv'. ?irq398 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?irq397 s' rv' rv'
\<lambda>s' rv'. ?st'396 s' rv' rv' \<equiv>\<^sup>? \<lambda>s' rv'. ?st'395 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?irq407 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?irq398 s' rv' rv'
\<lambda>s' rv' rv'b s cap. ?st'406 s' rv' rv'b (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s' rv'. ?st'396 s' rv' rv' proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<Longrightarrow> equiv_valid_rv_inv (reads_equiv_f aag) (affects_equiv aag l) (=) ?P14 (get_cap slot)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (?P14 and (\<lambda>s. K (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (cdt s) (cdt t)) s \<and> all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s) \<and> (next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s) \<longrightarrow> silc_inv aag st s) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> invs s \<and> emptyable (next_revoke_cap slot s) s \<and> only_timer_irq_inv irq st' s \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> emptyable (next_revoke_cap slot s) s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s)))) s
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and (\<lambda>_. True)) s\<rbrakk> \<Longrightarrow> silc_inv aag st s
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and K (aag_can_read aag (fst slot)) and (\<lambda>_. True) and (\<lambda>s. K (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (cdt s) (cdt t)) s \<and> all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s) \<and> (next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> ((\<exists>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s) \<longrightarrow> silc_inv aag st s) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> invs s \<and> emptyable (next_revoke_cap slot s) s \<and> only_timer_irq_inv irq st' s \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> emptyable (next_revoke_cap slot s) s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (next_revoke_cap slot s) s)))) s
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (\<lambda>a. aag_can_read_or_affect aag l (fst a)) (\<lambda>a. a) (cdt s) (cdt t)) \<and> all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s) \<and> (next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s))
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (\<lambda>a. aag_can_read_or_affect aag l (fst a)) (\<lambda>a. a) (cdt s) (cdt t)) \<and> all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s) \<and> (next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s))
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (\<lambda>a. aag_can_read_or_affect aag l (fst a)) (\<lambda>a. a) (cdt s) (cdt t)) \<and> (next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s))
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s)\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> equiv_for (\<lambda>a. aag_can_read_or_affect aag l (fst a)) (\<lambda>a. a) (cdt s) (cdt t)
 2. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s)\<rbrakk> \<Longrightarrow> next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s)
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s)\<rbrakk> \<Longrightarrow> next_revoke_cap slot s \<in> descendants_of slot (cdt s) \<longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s)
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> aag_can_read aag (fst (next_revoke_cap slot s)) \<and> (\<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s)
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (next_revoke_cap slot s) s \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s \<and> 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 \<and> emptyable (next_revoke_cap slot s) s
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) cap) (next_revoke_cap slot s) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> emptyable (next_revoke_cap slot s) s \<and> cdt_change_allowed' aag (next_revoke_cap slot s) s \<and> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) cap) (next_revoke_cap slot s) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> emptyable (next_revoke_cap slot s) s
 2. \<And>s cap. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) cap) (next_revoke_cap slot s) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (next_revoke_cap slot s) s
 3. \<And>s cap. \<lbrakk>is_subject aag (fst slot); silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; all_children (\<lambda>x. aag_can_read aag (fst x)) (cdt s); next_revoke_cap slot s \<in> descendants_of slot (cdt s); cte_wp_at ((=) cap) (next_revoke_cap slot s) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> only_timer_irq_inv (?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) (?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()) s
flex-flex pairs:
\<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?st'496 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap ()
\<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () \<equiv>\<^sup>? \<lambda>s cap. ?irq497 (descendants_of slot (cdt s)) (next_revoke_cap slot s) cap () proof (state)
this:
spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and K (is_subject aag (fst slot))) (cap_revoke slot)

goal:
No subgoals!