theory ADT_H

lemma absCDT_correct':
assumes pspace_aligned: "pspace_aligned s"
assumes pspace_distinct: "pspace_distinct s"
assumes pspace_aligned': "pspace_aligned' s'"
assumes pspace_distinct': "pspace_distinct' s'"
assumes valid_objs: "valid_objs s"
assumes valid_mdb:  "valid_mdb s"
assumes rel:  "(s,s') \<in> state_relation"
shows
  "absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s" (is ?P)
  "(case (cdt s x) of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not>(ctes_of s' \<turnstile> q \<rightarrow> cte_map x)) |
             Some p \<Rightarrow>
             ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and>
                   (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and>
                        ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow>
                        cte_map p = q))" (is ?Q) proof - have cnp:
  "\<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow>
         (cteMap (gsCNodes s')) (cte_map (a, b)) = (a, b)" using cteMap_correct[OF rel valid_objs pspace_aligned pspace_distinct
                            pspace_aligned' pspace_distinct'] by (clarsimp simp: dom_def) from rel have descs_eq:
    "\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow>
           {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} =
               descendants_of' (cte_map (a, b)) (ctes_of s')" apply (clarsimp simp add: state_relation_def) apply (clarsimp simp add: swp_def cdt_relation_def image_def) done from rel have pspace_relation: "pspace_relation (kheap s) (ksPSpace s')" by (clarsimp simp add: state_relation_def) note cdt_has_caps = mdb_cte_atD[OF _ valid_mdb_mdb_cte_at[OF valid_mdb]] note descendants_of_simps =
    descendants_of_def cdt_parent_rel_def is_cdt_parent_def have descendants_implies:
    "\<And>p p'. p' \<in> descendants_of p (cdt s) \<Longrightarrow>
            \<exists>cap cap'. caps_of_state s p = Some cap \<and>
                       caps_of_state s p' = Some cap'" apply (clarsimp simp: descendants_of_simps) apply (frule tranclD2, drule tranclD) apply (auto dest: cdt_has_caps) done let ?cnp = "cteMap (gsCNodes s')" have subtree_implies:
  "\<And>p p'. subtree (ctes_of s') p p' \<Longrightarrow>
           \<exists>cap cap'. ?cnp p' \<in> descendants_of (?cnp p) (cdt s) \<and>
                      caps_of_state s (?cnp p) = Some cap \<and>
                      caps_of_state s (?cnp p') = Some cap' \<and>
           (\<exists>cte cte'. ctes_of s' p = Some cte \<and> ctes_of s' p' = Some cte')" apply (subgoal_tac "(ctes_of s') \<turnstile> p parentOf p'") prefer 2 apply (erule subtree.cases, simp+) apply (clarsimp simp add: parentOf_def) apply (frule_tac x=p in
      pspace_relation_cte_wp_atI[OF pspace_relation _ valid_objs]) apply clarsimp apply (frule descs_eq[rule_format, OF cte_wp_at_weakenE], simp) apply (simp add: descendants_of'_def Collect_eq) apply (drule spec, drule(1) iffD2) apply (clarsimp simp: cnp cte_wp_at_caps_of_state) apply (frule descendants_implies) apply (clarsimp simp: cnp) done have is_parent:
  "\<And>a b p cap cap' a' b' c.
       \<lbrakk>cdt s (a, b) = Some (a', b')\<rbrakk>
       \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and>
          (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and>
               ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow>
               cte_map (a', b') = q)" apply (frule cdt_has_caps) using descs_eq pspace_relation apply (frule_tac x=a' in spec, erule_tac x=b' in allE) apply (simp add: cte_wp_at_caps_of_state Collect_eq descendants_of_simps
                      descendants_of'_def) apply (rule conjI) apply fastforce apply clarsimp apply (drule subtree_implies)+ apply (clarsimp simp: cnp) using valid_mdb apply (clarsimp simp: cnp descendants_of_simps valid_mdb_def no_mloop_def) apply (drule_tac x="?cnp q" and y="(a, b)" in tranclD2) apply clarsimp apply (fastforce intro: trancl_rtrancl_trancl) done show ?P apply (rule ext) using descs_eq pspace_relation apply (simp add: absCDT_def) apply (rule conjI[rotated]) apply clarsimp apply (rule sym, rule ccontr, clarsimp) apply (frule cdt_has_caps) using cnp apply fastforce apply clarsimp apply (clarsimp simp: parent_of'_def) apply (rule conjI) apply clarsimp apply (rule sym, rule ccontr, clarsimp) apply (simp add: descendants_of_simps descendants_of'_def) apply (rename_tac a' b') apply (erule_tac x=a' in allE, erule_tac x=b' in allE) apply (erule_tac x="cte_map (a', b')" in allE, erule notE) apply (frule cdt_has_caps) apply (clarsimp simp: cte_wp_at_caps_of_state Collect_eq) apply fastforce apply clarsimp apply (drule subtree_implies) apply clarsimp apply (case_tac "cdt s (a, b)") apply (simp add: descendants_of_simps descendants_of'_def) apply (drule tranclD2) apply clarsimp apply clarsimp apply (rename_tac a' b') apply (frule cdt_has_caps) apply clarsimp apply (rule trans[rotated]) apply (rule cnp[rule_format], simp) apply (rule arg_cong[where f="?cnp"]) apply (rule the_equality) apply (rule is_parent,assumption) apply clarsimp apply (rule ccontr) apply (drule_tac x="cte_map (a', b')" in spec, drule mp) apply simp_all apply (drule subtree_implies) apply clarsimp apply (drule_tac p=pa in ctes_of_cte_wp_atD) apply (drule pspace_relation_cte_wp_atI'[OF pspace_relation _ valid_objs]) apply (clarsimp simp add: cte_wp_at_caps_of_state cnp) apply (thin_tac "(a, b) \<in> descendants_of (?cnp p) (cdt s)",
           thin_tac "caps_of_state s (?cnp p) = Some cap") apply (unfold descendants_of'_def) apply (erule_tac x=a' in allE) apply (erule_tac x=b' in allE) apply (simp add: Collect_eq) apply (erule_tac x="cte_map (a, b)" in allE) apply (drule iffD1) apply (rule_tac x="(a, b)" in bexI, simp) apply (clarsimp simp: cnp descendants_of_simps) apply (rule trancl.intros(1)) apply simp_all apply (rule descs_eq[simplified descendants_of'_def Collect_eq,
                         rule_format, THEN iffD1]) apply (clarsimp simp add: cte_wp_at_caps_of_state) apply (rule_tac x="(a', b')" in bexI, simp) apply (clarsimp simp: descendants_of_simps) apply (drule_tac x="(aa,ba)" and y="(a, b)" in tranclD2) apply clarsimp apply (drule rtranclD, erule disjE, simp_all)[1] done thus ?Q apply (case_tac x) apply (case_tac "cdt s (a, b)") apply (drule sym) apply (simp add: mdb_cte_at_def) apply (simp add: absCDT_def split_def) apply (simp add: parent_of'_def split: if_split_asm) apply (intro impI) apply (frule_tac a=a and b=b in cnp[simplified,rule_format]) apply simp apply simp apply (clarsimp simp: is_parent) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s &&& case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (state)
goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) proof (prove)
using this:
?p \<in> dom (caps_of_state s) \<longrightarrow> cteMap (gsCNodes s') (cte_map ?p) = ?p

goal (1 subgoal):
 1. \<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) proof (state)
this:
\<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (chain)
picking this:
(s, s') \<in> state_relation proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. \<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s') proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s')

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (chain)
picking this:
(s, s') \<in> state_relation proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. pspace_relation (kheap s) (ksPSpace s') proof (state)
this:
pspace_relation (kheap s) (ksPSpace s')

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (state)
this:
cdt s ?c = Some ?p \<Longrightarrow> (\<exists>c. caps_of_state s ?p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s ?c = Some c \<and> cap.NullCap \<noteq> c)

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (state)
this:
descendants_of ?p ?t \<equiv> {q. ?t \<Turnstile> ?p \<rightarrow> q}
cdt_parent_rel ?t \<equiv> {(p, c). is_cdt_parent ?t p c}
is_cdt_parent ?t ?p ?c \<equiv> ?t ?c = Some ?p

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. p' \<in> descendants_of p (cdt s) \<Longrightarrow> \<exists>cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<Longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (\<exists>cap'. caps_of_state s (aa, ba) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<exists>z. ((a, b), z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, aa, ba) \<in> {(p, c). cdt s c = Some p}; \<exists>z. ((a, b), z) \<in> {(p, c). cdt s c = Some p} \<and> (z, aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (\<exists>cap'. caps_of_state s (aa, ba) = Some cap') proof (prove)
goal:
No subgoals! proof (state)
this:
?p' \<in> descendants_of ?p (cdt s) \<Longrightarrow> \<exists>cap cap'. caps_of_state s ?p = Some cap \<and> caps_of_state s ?p' = Some cap'

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (state)
goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>p p'. ctes_of s' \<turnstile> p \<rightarrow> p' \<Longrightarrow> \<exists>cap cap'. cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') p) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') p') = Some cap' \<and> (\<exists>cte cte'. ctes_of s' p = Some cte \<and> ctes_of s' p' = Some cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p'. \<lbrakk>ctes_of s' \<turnstile> p \<rightarrow> p'; ctes_of s' \<turnstile> p parentOf p'\<rbrakk> \<Longrightarrow> \<exists>cap cap'. cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') p) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') p') = Some cap' \<and> (\<exists>cte cte'. ctes_of s' p = Some cte \<and> ctes_of s' p' = Some cte')
 2. \<And>p p'. ctes_of s' \<turnstile> p \<rightarrow> p' \<Longrightarrow> ctes_of s' \<turnstile> p parentOf p' proof (prove)
goal (2 subgoals):
 1. \<And>p p'. ctes_of s' \<turnstile> p \<rightarrow> p' \<Longrightarrow> ctes_of s' \<turnstile> p parentOf p'
 2. \<And>p p'. \<lbrakk>ctes_of s' \<turnstile> p \<rightarrow> p'; ctes_of s' \<turnstile> p parentOf p'\<rbrakk> \<Longrightarrow> \<exists>cap cap'. cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') p) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') p') = Some cap' \<and> (\<exists>cte cte'. ctes_of s' p = Some cte \<and> ctes_of s' p' = Some cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p'. \<lbrakk>ctes_of s' \<turnstile> p \<rightarrow> p'; ctes_of s' \<turnstile> p parentOf p'\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') p) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') \<and> (\<exists>cte. ctes_of s' p = Some cte) \<and> (\<exists>cte'. ctes_of s' p' = Some cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte' cte. \<lbrakk>ctes_of s' \<turnstile> p \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') p) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte' cte. \<lbrakk>ctes_of s' \<turnstile> p \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' p = Some cte'; isMDBParentOf cte' cte; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte') \<and> p = cte_map slot\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') p) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>p' cte' cte c a b. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') (cte_map (a, b))) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>p' cte' cte c a b. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte'); {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') (cte_map (a, b))) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>p' cte' cte c a b. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte'); \<forall>y. (\<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') (cte_map (a, b))) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>p' cte' cte c a b. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> p'; ctes_of s' p' = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte'); \<exists>x\<in>descendants_of (a, b) (cdt s). p' = cte_map x\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') p' \<in> descendants_of (cteMap (gsCNodes s') (cte_map (a, b))) (cdt s) \<and> (\<exists>cap. caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') p') = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte c a b aa ba. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map (aa, ba); ctes_of s' (cte_map (aa, ba)) = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; caps_of_state s (a, b) = Some c; cap_relation c (cteCap cte'); (aa, ba) \<in> descendants_of (a, b) (cdt s)\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map (aa, ba)) \<in> descendants_of (a, b) (cdt s) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') (cte_map (aa, ba))) = Some cap') proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte c a b aa ba. \<lbrakk>ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map (aa, ba); ctes_of s' (cte_map (aa, ba)) = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; isMDBParentOf cte' cte; caps_of_state s (a, b) = Some c; cap_relation c (cteCap cte'); (aa, ba) \<in> descendants_of (a, b) (cdt s); \<exists>cap cap'. caps_of_state s (a, b) = Some cap \<and> caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map (aa, ba)) \<in> descendants_of (a, b) (cdt s) \<and> (\<exists>cap'. caps_of_state s (cteMap (gsCNodes s') (cte_map (aa, ba))) = Some cap') proof (prove)
goal:
No subgoals! proof (state)
this:
ctes_of s' \<turnstile> ?p \<rightarrow> ?p' \<Longrightarrow> \<exists>cap cap'. cteMap (gsCNodes s') ?p' \<in> descendants_of (cteMap (gsCNodes s') ?p) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') ?p) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') ?p') = Some cap' \<and> (\<exists>cte cte'. ctes_of s' ?p = Some cte \<and> ctes_of s' ?p' = Some cte')

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' a' b' c. cdt s (a, b) = Some (a', b') \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' a' b' c. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q) proof (prove)
using this:
\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s')
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. \<And>a b p cap cap' a' b' c. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' a' b' c. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c); \<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); \<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cte_wp_at (\<lambda>_. True) (a', b') s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a', b') (cdt s). y = cte_map x} = descendants_of' (cte_map (a', b')) (ctes_of s')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b'. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b'. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)
 2. \<And>a b a' b'. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> \<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b'. \<lbrakk>cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> \<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q; ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; \<exists>cap cap'. cteMap (gsCNodes s') q \<in> descendants_of (cteMap (gsCNodes s') (cte_map (a', b'))) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') (cte_map (a', b'))) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') q) = Some cap' \<and> (\<exists>cte cte'. ctes_of s' (cte_map (a', b')) = Some cte \<and> ctes_of s' q = Some cte'); \<exists>cap cap'. cteMap (gsCNodes s') (cte_map (a, b)) \<in> descendants_of (cteMap (gsCNodes s') q) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') q) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap' \<and> (\<exists>cte cte'. ctes_of s' q = Some cte \<and> ctes_of s' (cte_map (a, b)) = Some cte')\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca cte' cap' cte cte'a. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; cteMap (gsCNodes s') q \<in> descendants_of (a', b') (cdt s); (a, b) \<in> descendants_of (cteMap (gsCNodes s') q) (cdt s); ctes_of s' (cte_map (a, b)) = Some cte'; caps_of_state s (cteMap (gsCNodes s') q) = Some cap'; ctes_of s' (cte_map (a', b')) = Some cte; ctes_of s' q = Some cte'a\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. \<And>a b a' b' q c ca cte' cap' cte cte'a. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; cteMap (gsCNodes s') q \<in> descendants_of (a', b') (cdt s); (a, b) \<in> descendants_of (cteMap (gsCNodes s') q) (cdt s); ctes_of s' (cte_map (a, b)) = Some cte'; caps_of_state s (cteMap (gsCNodes s') q) = Some cap'; ctes_of s' (cte_map (a', b')) = Some cte; ctes_of s' q = Some cte'a\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca cte' cap' cte cte'a. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; ((a', b'), cteMap (gsCNodes s') q) \<in> {(p, c). cdt s c = Some p}\<^sup>+; (cteMap (gsCNodes s') q, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+; ctes_of s' (cte_map (a, b)) = Some cte'; caps_of_state s (cteMap (gsCNodes s') q) = Some cap'; ctes_of s' (cte_map (a', b')) = Some cte; ctes_of s' q = Some cte'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> {(p, c). cdt s c = Some p}\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca cte' cap' cte cte'a. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; ((a', b'), cteMap (gsCNodes s') q) \<in> {(p, c). cdt s c = Some p}\<^sup>+; ctes_of s' (cte_map (a, b)) = Some cte'; caps_of_state s (cteMap (gsCNodes s') q) = Some cap'; ctes_of s' (cte_map (a', b')) = Some cte; ctes_of s' q = Some cte'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> {(p, c). cdt s c = Some p}\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<exists>z. (cteMap (gsCNodes s') q, z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, a, b) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal (1 subgoal):
 1. \<And>a b a' b' q c ca cte' cap' cte cte'a. \<lbrakk>cdt s (a, b) = Some (a', b'); \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>y. (\<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)) = ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> y); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca; ((a', b'), cteMap (gsCNodes s') q) \<in> {(p, c). cdt s c = Some p}\<^sup>+; ctes_of s' (cte_map (a, b)) = Some cte'; caps_of_state s (cteMap (gsCNodes s') q) = Some cap'; ctes_of s' (cte_map (a', b')) = Some cte; ctes_of s' q = Some cte'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); \<forall>a b. ((a, b), a, b) \<notin> {(p, c). cdt s c = Some p}\<^sup>+; untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); (cteMap (gsCNodes s') q, a', b') \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> cte_map (a', b') = q proof (prove)
goal:
No subgoals! proof (state)
this:
cdt s (?a, ?b) = Some (?a', ?b') \<Longrightarrow> ctes_of s' \<turnstile> cte_map (?a', ?b') \<rightarrow> cte_map (?a, ?b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (?a', ?b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (?a, ?b) \<longrightarrow> cte_map (?a', ?b') = q)

goal (2 subgoals):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s proof (prove)
goal (1 subgoal):
 1. \<And>x. absCDT (cteMap (gsCNodes s')) (ctes_of s') x = cdt s x proof (prove)
using this:
\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s')
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. \<And>x. absCDT (cteMap (gsCNodes s')) (ctes_of s') x = cdt s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> (cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x) \<and> (cteMap (gsCNodes s') (cte_map x) \<noteq> x \<longrightarrow> None = cdt s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) \<noteq> x \<longrightarrow> None = cdt s x
 2. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b)\<rbrakk> \<Longrightarrow> None = cdt s (a, b)
 2. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b); cdt s (a, b) = Some (aa, ba); (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
using this:
\<forall>a b. caps_of_state s (a, b) \<noteq> None \<longrightarrow> cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)

goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b); cdt s (a, b) = Some (aa, ba); (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (cte_map x) = x \<longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map x)) = cdt s x proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map (a, b))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> ((\<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> None = cdt s (a, b)) \<and> ((\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> None = cdt s (a, b)
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> None = cdt s (a, b)
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b); cdt s (a, b) = Some (a', b')\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<forall>p. \<not> ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b); cdt s (a, b) = Some (a', b'); cte_wp_at (\<lambda>_. True) (a', b') s \<longrightarrow> {y. \<exists>a b. ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (a, b)} = {c'. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> c'}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); cdt s (a, b) = Some (a', b'); cte_wp_at (\<lambda>_. True) (a', b') s \<longrightarrow> {y. \<exists>a b. ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (a, b)} = {c'. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> c'}\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); cdt s (a, b) = Some (a', b'); cte_wp_at (\<lambda>_. True) (a', b') s \<longrightarrow> {y. \<exists>a b. ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (a, b)} = {c'. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> c'}; (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b a' b' c ca. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); cdt s (a, b) = Some (a', b'); \<forall>y. (\<exists>a b. ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (a, b)) = ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> y; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; caps_of_state s (a, b) = Some ca; cap.NullCap \<noteq> ca\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)
 2. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> (\<exists>p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)) \<longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); \<exists>cap cap'. cteMap (gsCNodes s') (cte_map (a, b)) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') p) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap' \<and> (\<exists>cte cte'. ctes_of s' p = Some cte \<and> ctes_of s' (cte_map (a, b)) = Some cte')\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = None\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b)
 2. \<And>a b p cap cap' cte cte' aa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (cteMap (gsCNodes s') p, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+; caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>a b p cap cap' cte cte' aa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>aa ba. ((a, b), aa, ba) \<in> {(p, c). cdt s c = Some p}\<^sup>+ \<and> y = cte_map (aa, ba)} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = None; \<exists>z. (cteMap (gsCNodes s') p, z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, a, b) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b p cap cap' cte cte' aa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' aa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> Some (cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q))) = cdt s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' aa ba. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b')\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = (a', b') proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b'. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); (\<exists>c. caps_of_state s (a', b') = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = (a', b') proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = (a', b') proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> ?s100 a b p cap cap' cte cte' a' b' c = (a', b')
 2. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = ?s100 a b p cap cap' cte cte' a' b' c proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cteMap (gsCNodes s') (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = cteMap (gsCNodes s') (cte_map (a', b')) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> (THE p. ctes_of s' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> p = q)) = cte_map (a', b') proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte' a' b' c. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map (a', b') = q)
 2. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> pa = q)\<rbrakk> \<Longrightarrow> pa = cte_map (a', b') proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> pa = q)\<rbrakk> \<Longrightarrow> pa = cte_map (a', b') proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b); \<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> pa = q\<rbrakk> \<Longrightarrow> pa = cte_map (a', b') proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b); \<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> pa = q; pa \<noteq> cte_map (a', b')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b); pa \<noteq> cte_map (a', b')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)
 2. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b); pa \<noteq> cte_map (a', b'); pa = cte_map (a', b')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a, b); pa \<noteq> cte_map (a', b')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; pa \<noteq> cte_map (a', b'); \<exists>cap cap'. cteMap (gsCNodes s') (cte_map (a, b)) \<in> descendants_of (cteMap (gsCNodes s') pa) (cdt s) \<and> caps_of_state s (cteMap (gsCNodes s') pa) = Some cap \<and> caps_of_state s (cteMap (gsCNodes s') (cte_map (a, b))) = Some cap' \<and> (\<exists>cte cte'. ctes_of s' pa = Some cte \<and> ctes_of s' (cte_map (a, b)) = Some cte')\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa capa ctea. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; pa \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (cteMap (gsCNodes s') pa) (cdt s); caps_of_state s (cteMap (gsCNodes s') pa) = Some capa; ctes_of s' pa = Some ctea\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa capa ctea. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; pa \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (cteMap (gsCNodes s') pa) (cdt s); caps_of_state s (cteMap (gsCNodes s') pa) = Some capa; cte_wp_at' ((=) ctea) pa s'\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c pa capa ctea. \<lbrakk>\<forall>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); cteMap (gsCNodes s') (cte_map (a, b)) = (a, b); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; pa \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (cteMap (gsCNodes s') pa) (cdt s); caps_of_state s (cteMap (gsCNodes s') pa) = Some capa; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap ctea) \<and> pa = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> pa \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); (a, b) \<in> descendants_of (cteMap (gsCNodes s') p) (cdt s); caps_of_state s (cteMap (gsCNodes s') p) = Some cap; caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = descendants_of' (cte_map (a, b)) (ctes_of s'); pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<longrightarrow> {y. \<exists>x\<in>descendants_of (a, b) (cdt s). y = cte_map x} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); \<forall>b. (\<exists>cap. caps_of_state s (a', b) = Some cap) \<longrightarrow> {y. \<exists>x\<in>descendants_of (a', b) (cdt s). y = cte_map x} = {c'. ctes_of s' \<turnstile> cte_map (a', b) \<rightarrow> c'}\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); (\<exists>cap. caps_of_state s (a', b') = Some cap) \<longrightarrow> {y. \<exists>x\<in>descendants_of (a', b') (cdt s). y = cte_map x} = {c'. ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> c'}\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); \<forall>y. (\<exists>x\<in>descendants_of (a', b') (cdt s). y = cte_map x) = ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> y\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); (\<exists>x\<in>descendants_of (a', b') (cdt s). cte_map (a, b) = cte_map x) = ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> \<exists>x\<in>descendants_of (a', b') (cdt s). cte_map (a, b) = cte_map x
 2. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> (a, b) \<in> descendants_of (a', b') (cdt s)
 2. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); ((aa, ba), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+; caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+
 2. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); ((aa, ba), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+; caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea)\<rbrakk> \<Longrightarrow> ((a', b'), a, b) \<in> {(p, c). cdt s c = Some p}
 2. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') \<and> ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (aa, ba) \<rightarrow> cte_map (a', b') proof (prove)
goal (2 subgoals):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s
 2. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>descendants_of (aa, ba) (cdt s). cte_map (a', b') = cte_map x proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>descendants_of (aa, ba) (cdt s). cte_map (a', b') = cte_map x proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); (a, b) \<in> descendants_of (aa, ba) (cdt s); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> (a', b') \<in> descendants_of (aa, ba) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); ((aa, ba), a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+; caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b)\<rbrakk> \<Longrightarrow> ((aa, ba), a', b') \<in> {(p, c). cdt s c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b); \<exists>z. ((aa, ba), z) \<in> {(p, c). cdt s c = Some p}\<^sup>* \<and> (z, a, b) \<in> {(p, c). cdt s c = Some p}\<rbrakk> \<Longrightarrow> ((aa, ba), a', b') \<in> {(p, c). cdt s c = Some p}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b p cap' cte cte' a' b' c capa ctea aa ba. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); caps_of_state s (a, b) = Some cap'; ctes_of s' p = Some cte; ctes_of s' (cte_map (a, b)) = Some cte'; cdt s (a, b) = Some (a', b'); cap.NullCap \<noteq> cap'; caps_of_state s (a', b') = Some c; cap.NullCap \<noteq> c; cte_map (aa, ba) \<noteq> cte_map (a', b'); caps_of_state s (aa, ba) = Some capa; cap_relation capa (cteCap ctea); ctes_of s' \<turnstile> cte_map (a', b') \<rightarrow> cte_map (a, b); ((aa, ba), a', b') \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> ((aa, ba), a', b') \<in> {(p, c). cdt s c = Some p}\<^sup>+ proof (prove)
goal:
No subgoals! proof (state)
this:
absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s

goal (1 subgoal):
 1. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
using this:
absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s

goal (1 subgoal):
 1. case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b)\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = None\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q)
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>x = (a, b); cdt s (a, b) = None; cdt s = absCDT (cteMap (gsCNodes s')) (ctes_of s')\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q)
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>x = (a, b); absCDT (cteMap (gsCNodes s')) (ctes_of s') (a, b) = None; cdt s = absCDT (cteMap (gsCNodes s')) (ctes_of s')\<rbrakk> \<Longrightarrow> (\<exists>y. caps_of_state s (a, b) = Some y) \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b))
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>x = (a, b); (if cteMap (gsCNodes s') (cte_map (a, b)) = (a, b) then map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map (a, b))) else None) = None; cdt s = (\<lambda>p. if cteMap (gsCNodes s') (cte_map p) = p then map_option (cteMap (gsCNodes s')) (parent_of' (subtree (ctes_of s')) (cte_map p)) else None)\<rbrakk> \<Longrightarrow> (\<exists>y. caps_of_state s (a, b) = Some y) \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b))
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cdt s = (\<lambda>p. if cteMap (gsCNodes s') (cte_map p) = p then map_option (cteMap (gsCNodes s')) (if \<forall>pa. \<not> ctes_of s' \<turnstile> pa \<rightarrow> cte_map p then None else Some (THE pa. ctes_of s' \<turnstile> pa \<rightarrow> cte_map p \<and> (\<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map p \<longrightarrow> pa = q))) else None); x = (a, b); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b)\<rbrakk> \<Longrightarrow> (\<exists>y. caps_of_state s (a, b) = Some y) \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b))
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cdt s = (\<lambda>p. if cteMap (gsCNodes s') (cte_map p) = p then map_option (cteMap (gsCNodes s')) (if \<forall>pa. \<not> ctes_of s' \<turnstile> pa \<rightarrow> cte_map p then None else Some (THE pa. ctes_of s' \<turnstile> pa \<rightarrow> cte_map p \<and> (\<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map p \<longrightarrow> pa = q))) else None); x = (a, b); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b); \<exists>y. caps_of_state s (a, b) = Some y\<rbrakk> \<Longrightarrow> \<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b)
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cdt s = (\<lambda>p. if cteMap (gsCNodes s') (cte_map p) = p then map_option (cteMap (gsCNodes s')) (if \<forall>pa. \<not> ctes_of s' \<turnstile> pa \<rightarrow> cte_map p then None else Some (THE pa. ctes_of s' \<turnstile> pa \<rightarrow> cte_map p \<and> (\<forall>q. ctes_of s' \<turnstile> pa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map p \<longrightarrow> pa = q))) else None); x = (a, b); cteMap (gsCNodes s') (cte_map (a, b)) \<noteq> (a, b); \<exists>y. caps_of_state s (a, b) = Some y; cteMap (gsCNodes s') (cte_map (a, b)) = (a, b)\<rbrakk> \<Longrightarrow> \<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b)
 2. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s; x = (a, b); cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map aa \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map aa \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map aa = q) proof (prove)
goal:
No subgoals! proof (state)
this:
case cdt s x of None \<Rightarrow> caps_of_state s x \<noteq> None \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map x) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map x \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map x \<longrightarrow> cte_map p = q)

goal:
No subgoals!