theory DomainSepInv

lemma set_simple_ko_neg_cte_wp_at[wp]:
  "set_simple_ko f a b \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace>" apply (simp add: set_simple_ko_def) apply (wp set_object_wp_strong get_object_wp
         | simp add: partial_inv_def a_type_def split: kernel_object.splits)+ apply (case_tac "a = fst slot") apply (clarsimp split: kernel_object.splits) apply (fastforce elim: cte_wp_atE simp: obj_at_def) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_simple_ko f a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do obj <- get_object a;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. partial_inv f obj = Some y);
set_object a (f b)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at P slot s \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a = fst slot\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>)))))
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a = fst slot\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) (fst slot) s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) (fst slot) s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) (fst slot) s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) (fst slot) s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) (fst slot) s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) (fst slot) s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) (fst slot) s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) (fst slot) s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) (fst slot) s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) (fst slot) s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) (fst slot) s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) (fst slot) s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) (fst slot) s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) (fst slot) s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) (fst slot) s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) (fst slot) s \<longrightarrow> (\<forall>x5a. ako_at x5a (fst slot) s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) (fst slot) s \<longrightarrow> (\<forall>x5a. ako_at x5a (fst slot) s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> ArchObj x5)\<rparr>)))))
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))))) \<and> (\<not> well_formed_cnode_n x11 x12 \<longrightarrow> f b = CNode x11 x12 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x12a. \<not> well_formed_cnode_n x11 x12a \<longrightarrow> ko_at (CNode x11 x12a) a s \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode x11 x12)\<rparr>)))))) \<and> (\<forall>x2. f b = TCB x2 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x2. ko_at (TCB x2) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB x2)\<rparr>)))) \<and> (\<forall>x3. f b = Endpoint x3 \<longrightarrow> (\<forall>ko. (\<forall>x3a. ko = Endpoint x3a \<longrightarrow> (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> ko_at (Endpoint x3a) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<exists>x3. ko_at (Endpoint x3) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f b = Notification x4 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)) \<and> (\<forall>x4a. ko = Notification x4a \<longrightarrow> (\<exists>!y. f y = Notification x4a) \<longrightarrow> ko_at (Notification x4a) a s \<longrightarrow> (\<exists>x4. ko_at (Notification x4) a s) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> Notification x4)\<rparr>)))) \<and> (\<forall>x5. f b = ArchObj x5 \<longrightarrow> (\<forall>ko. (\<forall>x3. ko = Endpoint x3 \<longrightarrow> (\<exists>!y. f y = Endpoint x3) \<longrightarrow> ko_at (Endpoint x3) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))) \<and> (\<forall>x4. ko = Notification x4 \<longrightarrow> (\<exists>!y. f y = Notification x4) \<longrightarrow> ko_at (Notification x4) a s \<longrightarrow> (\<forall>x5a. ako_at x5a a s \<longrightarrow> aa_type x5 = aa_type x5a \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> ArchObj x5)\<rparr>))))) proof (prove)
goal:
No subgoals!