theory BCorres2_AI

lemma cap_revoke_s_bcorres:
  shows
  "s_bcorres (cap_revoke slot) (cap_revoke slot) s" proof (induct rule: cap_revoke.induct[where ?a1.0=s]) case (1 slot s) show ?case apply (simp add: cap_revoke.simps) apply wp apply (wp gets_s_bcorres_underlyingE' | simp)+ apply (subgoal_tac "(Inr (exst s'a),s'a) \<in> fst (liftE (gets exst) s'a)") prefer 2 apply (simp add: in_monad) apply (rule "1"[simplified],(simp add: in_monad | force)+) apply (simp add:  | force | wp drop_sbcorres_underlying)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres (cap_revoke slot) (cap_revoke slot) s proof (state)
goal (1 subgoal):
 1. \<And>slot s. (\<And>rv st rva sta rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<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> s_bcorres (cap_revoke slot) (cap_revoke slot) stg) \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s 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> s_bcorres (cap_revoke slot) (cap_revoke slot) ?stg

goal (1 subgoal):
 1. \<And>slot s. (\<And>rv st rva sta rvb stb rvc stc rvd std rve ste rvf stf rvg stg. \<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> s_bcorres (cap_revoke slot) (cap_revoke slot) stg) \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (cap_revoke slot) (cap_revoke slot) s proof (prove)
goal (1 subgoal):
 1. s_bcorres (doE cap <- liftE (get_cap slot);
cdt <- liftE (gets cdt);
whenE (cap \<noteq> NullCap \<and> descendants_of slot cdt \<noteq> {}) (doE child <- liftE (select_ext (next_revoke_cap slot) (descendants_of slot cdt));
cap <- liftE (get_cap child);
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE)
odE) (doE cap <- liftE (get_cap slot);
cdt <- liftE (gets cdt);
whenE (cap \<noteq> NullCap \<and> descendants_of slot cdt \<noteq> {}) (doE child <- liftE (select_ext (next_revoke_cap slot) (descendants_of slot cdt));
cap <- liftE (get_cap child);
y <- assertE (cap \<noteq> NullCap);
y <- cap_delete child;
y <- preemption_point;
cap_revoke slot
odE)
odE) s proof (prove)
goal (9 subgoals):
 1. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e rf s'f. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd); (Inr rf, s'f) \<in> fst (preemption_point s'e)\<rbrakk> \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s'f
 2. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 3. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 4. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 5. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 6. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 7. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 8. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 9. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal (9 subgoals):
 1. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e)\<rbrakk> \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s'f
 2. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 3. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 4. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 5. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 6. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 7. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 8. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 9. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal (10 subgoals):
 1. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e); (Inr (exst s'a), s'a) \<in> fst (liftE (gets exst) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s'f
 2. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e)\<rbrakk> \<Longrightarrow> (Inr (exst s'a), s'a) \<in> fst (liftE (gets exst) s'a)
 3. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 4. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 5. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 6. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 7. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 8. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 9. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 10. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal (10 subgoals):
 1. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e)\<rbrakk> \<Longrightarrow> (Inr (exst s'a), s'a) \<in> fst (liftE (gets exst) s'a)
 2. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e); (Inr (exst s'a), s'a) \<in> fst (liftE (gets exst) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s'f
 3. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 4. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 5. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 6. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 7. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 8. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 9. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 10. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal (9 subgoals):
 1. \<And>r s' ra s'a rb s'b rc s'c s'd s'e s'f. \<lbrakk>(r, s') \<in> fst (get_cap slot s); (ra, s'a) \<in> fst (gets cdt s'); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot ra) s'a); (rc, s'c) \<in> fst (get_cap rb s'b); (Inr (), s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr (), s'e) \<in> fst (cap_delete rb s'd); (Inr (), s'f) \<in> fst (preemption_point s'e); (Inr (exst s'a), s'a) \<in> fst (liftE (gets exst) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (cap_revoke slot) (cap_revoke slot) s'f
 2. \<And>r s' ra s'a rb s'b rc s'c rd s'd re s'e. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c); (Inr re, s'e) \<in> fst (cap_delete rb s'd)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 3. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 4. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 5. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 6. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 7. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 8. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 9. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal (8 subgoals):
 1. \<And>r s' ra rb s'b rc s'c s'e. \<lbrakk>(r, s') \<in> fst (get_cap slot s); ra = cdt s'; r \<noteq> NullCap \<and> descendants_of slot (cdt s') \<noteq> {}; (rb, s'b) \<in> fst (select_ext (next_revoke_cap slot) (descendants_of slot (cdt s')) s'); (rc, s'c) \<in> fst (get_cap rb s'b); rc \<noteq> NullCap; (Inr (), s'e) \<in> fst (cap_delete rb s'c)\<rbrakk> \<Longrightarrow> s_bcorres preemption_point preemption_point s'e
 2. \<And>r s' ra s'a rb s'b rc s'c rd s'd. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b); (Inr rd, s'd) \<in> fst (assertE (rc \<noteq> NullCap) s'c)\<rbrakk> \<Longrightarrow> s_bcorres (cap_delete rb) (cap_delete rb) s'd
 3. \<And>r s' ra s'a rb s'b rc s'c. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a); (Inr rc, s'c) \<in> fst (liftE (get_cap rb) s'b)\<rbrakk> \<Longrightarrow> s_bcorres (assertE (rc \<noteq> NullCap)) (assertE (rc \<noteq> NullCap)) s'c
 4. \<And>r s' ra s'a rb s'b. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}; (Inr rb, s'b) \<in> fst (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra)) s'a)\<rbrakk> \<Longrightarrow> s_bcorres (liftE (get_cap rb)) (liftE (get_cap rb)) s'b
 5. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s'); (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}); r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}\<rbrakk> \<Longrightarrow> s_bcorres (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) (liftE (select_ext (next_revoke_cap slot) (descendants_of slot ra))) s'a
 6. \<And>r s' ra s'a. \<lbrakk>(Inr r, s') \<in> fst (liftE (get_cap slot) s); (Inr ra, s'a) \<in> fst (liftE (gets cdt) s')\<rbrakk> \<Longrightarrow> (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {}) = (r \<noteq> NullCap \<and> descendants_of slot ra \<noteq> {})
 7. \<And>r s'. (Inr r, s') \<in> fst (liftE (get_cap slot) s) \<Longrightarrow> s_bcorres (liftE (gets cdt)) (liftE (gets cdt)) s'
 8. s_bcorres (liftE (get_cap slot)) (liftE (get_cap slot)) s proof (prove)
goal:
No subgoals! proof (state)
this:
s_bcorres (cap_revoke slot) (cap_revoke slot) s

goal:
No subgoals!