theory ADT_H

lemma absCDTList_correct:
notes split_paired_All[simp del] split_paired_Ex[simp del]
assumes valid_mdb:  "valid_mdb s"
assumes valid_mdb': "valid_mdb' s'"
assumes valid_list: "valid_list s"
assumes valid_objs: "valid_objs s"
assumes pspace_aligned: "pspace_aligned s"
assumes pspace_aligned': "pspace_aligned' s'"
assumes pspace_distinct: "pspace_distinct s"
assumes pspace_distinct': "pspace_distinct' s'"
assumes rel:  "(s,s') \<in> state_relation"
shows
  "absCDTList (cteMap (gsCNodes s')) (ctes_of s') = cdt_list s" apply (simp add: absCDTList_def) apply (subst absCDT_correct[where s=s]) apply (simp add: assms)+ apply (rule partial_sort_cdt.sort_cdt_list_correct[where s'=s']) apply (simp add: partial_sort_cdt_def) apply (rule context_conjI') apply unfold_locales apply (simp add: assms)+ apply (simp add: partial_sort_cdt_axioms_def) apply (elim conjE exE) apply (rule ancestor_comparable,assumption+) apply (elim conjE) apply (rule cte_map_inj_eq) apply (rule no_loops_sym_eq[where m="ctes_of s'"]) apply (rule valid_mdb'_no_loops[OF valid_mdb']) apply (simp add: assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absCDTList (cteMap (gsCNodes s')) (ctes_of s') = cdt_list s proof (prove)
goal (1 subgoal):
 1. sort_cdt_list (absCDT (cteMap (gsCNodes s')) (ctes_of s')) (ctes_of s') = cdt_list s proof (prove)
goal (8 subgoals):
 1. pspace_aligned s
 2. pspace_distinct s
 3. pspace_aligned' s'
 4. pspace_distinct' s'
 5. valid_objs s
 6. valid_mdb s
 7. (s, s') \<in> state_relation
 8. sort_cdt_list (cdt s) (ctes_of s') = cdt_list s proof (prove)
goal (1 subgoal):
 1. sort_cdt_list (cdt s) (ctes_of s') = cdt_list s proof (prove)
goal (1 subgoal):
 1. partial_sort_cdt (ctes_of s') s s' proof (prove)
goal (1 subgoal):
 1. partial_sort (\<lambda>x y. ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y) (\<lambda>x y. cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y)) \<and> partial_sort_cdt_axioms (ctes_of s') s s' proof (prove)
goal (2 subgoals):
 1. partial_sort_cdt_axioms (ctes_of s') s s'
 2. partial_sort_cdt_axioms (ctes_of s') s s' \<Longrightarrow> partial_sort (\<lambda>x y. ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y) (\<lambda>x y. cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y)) proof (prove)
goal (12 subgoals):
 1. ctes_of s' = ctes_of s'
 2. (s, s') \<in> state_relation
 3. valid_mdb s
 4. pspace_aligned s
 5. pspace_distinct s
 6. pspace_aligned' s'
 7. pspace_distinct' s'
 8. valid_objs s
 9. valid_list s
 10. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<or> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<or> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y); ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<and> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>(s, s') \<in> state_relation \<and> valid_mdb s \<and> pspace_aligned s \<and> pspace_distinct s \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> valid_objs s \<and> valid_mdb s \<and> valid_list s; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<or> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y); ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<and> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (3 subgoals):
 1. \<And>x y p. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at (\<lambda>_. True) x s; valid_mdb s; cte_wp_at (\<lambda>_. True) y s; pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s; ctes_of s' \<turnstile> p \<rightarrow> cte_map x; ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<or> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y); ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<and> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s \<and> cte_wp_at (\<lambda>_. True) y s \<and> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y); ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y \<and> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_map x = cte_map y
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x (?s26 x y)
 3. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y (?s26 x y)
 4. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> valid_objs (?s26 x y)
 5. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_aligned (?s26 x y)
 6. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_distinct (?s26 x y)
 7. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (9 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> no_loops (ctes_of s')
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y
 3. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
 4. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x (?s26 x y)
 5. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y (?s26 x y)
 6. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> valid_objs (?s26 x y)
 7. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_aligned (?s26 x y)
 8. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_distinct (?s26 x y)
 9. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y
 2. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x
 3. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x (?s26 x y)
 4. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y (?s26 x y)
 5. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> valid_objs (?s26 x y)
 6. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_aligned (?s26 x y)
 7. \<And>x y. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; cte_wp_at (\<lambda>_. True) x s; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map x; cte_wp_at (\<lambda>_. True) y s; \<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map x \<and> ctes_of s' \<turnstile> p \<rightarrow> cte_map y\<rbrakk> \<Longrightarrow> pspace_distinct (?s26 x y)
 8. \<And>x y z. \<lbrakk>partial_sort_cdt_axioms (ctes_of s') s s'; ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map y; ctes_of s' \<turnstile> cte_map y \<leadsto>\<^sup>* cte_map z\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map x \<leadsto>\<^sup>* cte_map z proof (prove)
goal:
No subgoals!