theory CSpace_C

lemma capSwapForDelete_ccorres:
  "ccorres dc xfdc
          (valid_mdb' and pspace_aligned')
          (UNIV \<inter> {s. slot1_' s = Ptr slot1} \<inter> {s. slot2_' s = Ptr slot2})
          []
          (capSwapForDelete slot1 slot2)
          (Call capSwapForDelete_'proc)" apply (cinit lift: slot1_' slot2_' simp del: return_bind)
  \<comment> \<open>***Main goal***\<close>
  \<comment> \<open>--- instruction: when (slot1 \<noteq> slot2) \<dots> / IF Ptr slot1 = Ptr slot2 THEN \<dots>\<close> apply (simp add:when_def) apply (rule ccorres_if_cond_throws2 [where Q = \<top> and Q' = \<top>]) apply (case_tac "slot1=slot2"; simp) apply (rule ccorres_return_void_C)

  \<comment> \<open>***Main goal***\<close>
  \<comment> \<open>--- ccorres goal with 2 affectations (cap1 and cap2) on both on Haskell and C\<close>
  \<comment> \<open>---   \<Longrightarrow> execute each part independently\<close> apply (simp add: liftM_def cong: call_ignore_cong) apply (rule ccorres_pre_getCTE)+ apply (rule ccorres_move_c_guard_cte, rule ccorres_symb_exec_r)+
  \<comment> \<open>***Main goal***\<close> apply (ctac (no_vcg) add: cteSwap_ccorres)
       \<comment> \<open>C Hoare triple for \<acute>cap2 :== \<dots>\<close> apply vcg
       \<comment> \<open>C existential Hoare triple for \<acute>cap2 :== \<dots>\<close> apply simp apply (rule conseqPre) apply vcg apply simp
     \<comment> \<open>C Hoare triple for \<acute>cap1 :== \<dots>\<close> apply vcg
     \<comment> \<open>C existential Hoare triple for \<acute>cap1 :== \<dots>\<close> apply simp apply (rule conseqPre) apply vcg apply simp

  \<comment> \<open>Hoare triple for return_void\<close> apply vcg

  \<comment> \<open>***Generalized preconditions***\<close> apply simp apply (clarsimp simp: cte_wp_at_ctes_of map_comp_Some_iff
    typ_heap_simps ccap_relation_def) apply (simp add: cl_valid_cte_def c_valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_mdb' and pspace_aligned') (UNIV \<inter> \<lbrace>\<acute>slot1 = cte_Ptr slot1\<rbrace> \<inter> \<lbrace>\<acute>slot2 = cte_Ptr slot2\<rbrace>) [] (capSwapForDelete slot1 slot2) (Call capSwapForDelete_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q290 slot2a slot1a) (?Q'290 slot2a slot1a) [SKIP] (when (slot1 \<noteq> slot2) (do cap1 <- liftM cteCap (getCTE slot1);
cap2 <- liftM cteCap (getCTE slot2);
cteSwap cap1 slot1 cap2 slot2
od)) (IF slot1a = slot2a THEN
  return_void_C
FI;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slot1a} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slot2a} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(\<acute>cap1,slot1a,\<acute>cap2,slot2a))))
 2. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q290 slot2a slot1a s \<and> s' \<in> ?Q'290 slot2a slot1a proof (prove)
goal (2 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q290 (cte_Ptr slot2) (cte_Ptr slot1)) (?Q'290 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (if slot1 \<noteq> slot2 then do cap1 <- liftM cteCap (getCTE slot1);
cap2 <- liftM cteCap (getCTE slot2);
cteSwap cap1 slot1 cap2 slot2
od else return ()) (IF slot1 = slot2 THEN
  return_void_C
FI;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2))))
 2. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q290 slot2a slot1a s \<and> s' \<in> ?Q'290 slot2a slot1a proof (prove)
goal (5 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> (\<not> slot1 \<noteq> slot2) = (s' \<in> \<lbrace>slot1 = slot2\<rbrace>)
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; \<not> slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R311 (cte_Ptr slot2) (cte_Ptr slot1)) (?R'307 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (return ()) return_void_C
 3. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U309 (cte_Ptr slot2) (cte_Ptr slot1)) (?U'303 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (do cap1 <- liftM cteCap (getCTE slot1);
cap2 <- liftM cteCap (getCTE slot2);
cteSwap cap1 slot1 cap2 slot2
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2)))
 4. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 5. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> ?R311 slot2a slot1a s) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> ?U309 slot2a slot1a s)) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?R'307 slot2a slot1a \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?U'303 slot2a slot1a)} proof (prove)
goal (4 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; \<not> slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R311 (cte_Ptr slot2) (cte_Ptr slot1)) (?R'307 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (return ()) return_void_C
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U309 (cte_Ptr slot2) (cte_Ptr slot1)) (?U'303 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (do cap1 <- liftM cteCap (getCTE slot1);
cap2 <- liftM cteCap (getCTE slot2);
cteSwap cap1 slot1 cap2 slot2
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2)))
 3. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 4. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> ?R311 slot2a slot1a s) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> ?U309 slot2a slot1a s)) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?R'307 slot2a slot1a \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?U'303 slot2a slot1a)} proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U309 (cte_Ptr slot2) (cte_Ptr slot1)) (?U'303 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (do cap1 <- liftM cteCap (getCTE slot1);
cap2 <- liftM cteCap (getCTE slot2);
cteSwap cap1 slot1 cap2 slot2
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2)))
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> ?U309 slot2a slot1a s)) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?U'303 slot2a slot1a)} proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?U309 (cte_Ptr slot2) (cte_Ptr slot1)) (?U'303 (cte_Ptr slot2) (cte_Ptr slot1)) [SKIP] (do x <- getCTE slot1;
xa <- getCTE slot2;
cteSwap (cteCap x) slot1 (cteCap xa) slot2
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2)))
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> ?U309 slot2a slot1a s)) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> ?U'303 slot2a slot1a)} proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?P339 (cte_Ptr slot2) (cte_Ptr slot1) rv a rva) (?P'337 rv rva) [SKIP] (cteSwap (cteCap rv) slot1 (cteCap rva) slot2) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot1} (\<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot2} (\<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])));;
CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2)))
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s slot2 = Some ctea \<longrightarrow> ?P339 slot2a slot1a cte s ctea)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?P'338 slot2a slot1a cte' cte'a}})}
flex-flex pairs:
?P'338 (cte_Ptr slot2) (cte_Ptr slot1) \<equiv>\<^sup>? \<lambda>cte' cte'a. ?P'337 (cte_to_H cte') (cte_to_H cte'a) proof (prove)
goal (7 subgoals):
 1. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A358 (cte_Ptr slot2) (cte_Ptr slot1) rv rva) (?Q'361 slot2a slot1a rv rva) [SKIP] (cteSwap (cteCap rv) slot1 (cteCap rva) slot2) (CALL cteSwap_'proc(cte_Ptr slot1,cte_Ptr slot2))
 2. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'356 slot2a slot1a rv rva) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) (?Q'361 slot2a slot1a rv rva)
 3. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; ?A358 (cte_Ptr slot2) (cte_Ptr slot1) rv rva s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'356 slot2a slot1a rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 4. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (?C'356 slot2a slot1a rv rva \<inter> \<lbrace>True\<rbrace>)
 5. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (?A358 (cte_Ptr slot2) (cte_Ptr slot1) rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 6. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 7. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s slot2 = Some ctea \<longrightarrow> (?A358 slot2a slot1a cte ctea and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (6 subgoals):
 1. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'356 slot2a slot1a rv rva) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s. slot2_'_update (\<lambda>_. cte_Ptr slot2) (slot1_'_update (\<lambda>_. cte_Ptr slot1) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot1 = cte_Ptr slot1\<rbrace> \<inter> \<lbrace>\<acute>slot2 = cte_Ptr slot2\<rbrace> \<inter> \<lbrace>ccap_relation (cteCap rv) \<acute>cap1\<rbrace> \<inter> \<lbrace>ccap_relation (cteCap rva) \<acute>cap2\<rbrace>}
 2. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'356 slot2a slot1a rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 3. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (?C'356 slot2a slot1a rv rva \<inter> \<lbrace>True\<rbrace>)
 4. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 5. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 6. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (5 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 3. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 4. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 5. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (5 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 3. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 4. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 5. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (6 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'379 slot2a slot1a rv rva s) \<acute>cap2 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'379 slot2a slot1a rv rva s
 3. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 4. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 5. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 6. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (5 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s\<rbrakk> \<Longrightarrow> \<lbrace>ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, cap2_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals sa))) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C'']))) sa) \<in> rf_sr}
 2. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 3. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 4. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 5. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (4 subgoals):
 1. \<And>slot2a slot1a rv rva. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) \<acute>cap1 \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> \<lbrace>True\<rbrace>)
 2. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'346 rv rva \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 3. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 4. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> ?C'345 slot2a slot1a cte' cte'a \<inter> \<lbrace>True\<rbrace>}})}
flex-flex pairs:
\<lambda>cte' cte'a. ?C'346 (cte_to_H cte') (cte_to_H cte'a) \<equiv>\<^sup>? ?C'345 (cte_Ptr slot2) (cte_Ptr slot1) proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot2))) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>True \<and> cte_Ptr slot1 = cte_Ptr slot1 \<and> cte_Ptr slot2 = cte_Ptr slot2 \<and> ccap_relation (cteCap rv) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>_. True) slot2 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ccap_relation (cteCap rv) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (4 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>_. True) slot2 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'391 slot2a slot1a rv rva s) \<acute>cap1 :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C''])) {s'. (s, s') \<in> rf_sr}
 2. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>_. True) slot2 s\<rbrakk> \<Longrightarrow> \<lbrace>ccap_relation (cteCap rv) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'391 slot2a slot1a rv rva s
 3. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 4. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (3 subgoals):
 1. \<And>slot2a slot1a rv rva s. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; slot1 \<noteq> slot2; cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> valid_mdb' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>_. True) slot2 s\<rbrakk> \<Longrightarrow> \<lbrace>ccap_relation (cteCap rv) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap rva) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, cap1_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals sa))) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) sa) \<in> rf_sr}
 2. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 3. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (2 subgoals):
 1. \<And>slot2a slot1a. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?PT'305 (cte_Ptr slot2) (cte_Ptr slot1)) return_void_C {},UNIV
 2. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> ?PT'305 slot2a slot1a) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (1 subgoal):
 1. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> slot1 \<noteq> slot2 \<longrightarrow> True) and (\<lambda>s. slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte. ctes_of s slot1 = Some cte \<longrightarrow> (\<forall>cte. ctes_of s slot2 = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot1 and cte_wp_at' (\<lambda>_. True) slot2 and valid_mdb' and pspace_aligned' and (\<lambda>_. slot1 \<noteq> slot2) and cte_wp_at' (\<lambda>_. True) (ptr_val slot2a) and cte_wp_at' (\<lambda>_. True) (ptr_val slot1a)) s)))) s \<and> s' \<in> \<lbrace>True\<rbrace> \<inter> {s. (s \<in> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>) \<and> (s \<notin> \<lbrace>slot1 = slot2\<rbrace> \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) slot1a = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) slot2a = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>True \<and> slot1a = slot1a \<and> slot2a = slot2a \<and> ccap_relation (cteCap (cte_to_H cte')) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot1a\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cteCap (cte_to_H cte'a)) (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slot2a\<rightarrow>[''cap_C'']))) \<and> True\<rbrace> \<inter> \<lbrace>True\<rbrace>}})} proof (prove)
goal (1 subgoal):
 1. \<And>slot2a slot1a s s'. \<lbrakk>slot2a = cte_Ptr slot2; slot1a = cte_Ptr slot1; (s, s') \<in> rf_sr; valid_mdb' s \<and> pspace_aligned' s\<rbrakk> \<Longrightarrow> (slot1 \<noteq> slot2 \<longrightarrow> (\<exists>cte. ctes_of s slot1 = Some cte) \<longrightarrow> (\<exists>cte. ctes_of s slot2 = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot1 s \<and> cte_wp_at' (\<lambda>_. True) slot2 s \<and> cte_wp_at' (\<lambda>_. True) slot1 s) \<and> (slot1 \<noteq> slot2 \<longrightarrow> (\<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot1) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> (\<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot2) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> ccap_relation (cap_to_H (cap_CL cte')) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot1\<rightarrow>[''cap_C'']))) \<and> ccap_relation (cap_to_H (cap_CL cte'a)) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot2\<rightarrow>[''cap_C''])))))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte' cte'a k' k'a. \<lbrakk>(s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; slot1 \<noteq> slot2; cl_valid_cte cte'; cslift s' (cte_Ptr slot1) = Some k'; cte_lift k' = Some cte'; cl_valid_cte cte'a; cslift s' (cte_Ptr slot2) = Some k'a; cte_lift k'a = Some cte'a\<rbrakk> \<Longrightarrow> c_valid_cap (cte_C.cap_C k') \<and> c_valid_cap (cte_C.cap_C k'a) proof (prove)
goal:
No subgoals!