theory Detype_R

lemma valid_obj':
  "\<lbrakk> valid_obj' obj s; ko_wp_at' ((=) obj) p s \<rbrakk> \<Longrightarrow> valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs]) apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs]) apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (rename_tac notification) apply (case_tac notification, simp_all add: valid_ntfn'_def valid_bound_tcb'_def)[1] apply (rename_tac ntfn bound) apply (case_tac ntfn, simp_all split:option.splits)[1] apply ((clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs] refs_notRange)+)[4] apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs] refs_notRange) apply (frule sym_refs_ko_wp_atD [OF _ sym_refs]) apply (clarsimp simp: valid_tcb'_def ko_wp_at'_def
                          objBits_simps) apply (rule conjI) apply (erule ballEI, clarsimp elim!: ranE) apply (rule_tac p="p + x" in valid_cap2) apply (erule(2) cte_wp_at_tcbI') apply fastforce apply simp apply (rename_tac tcb) apply (case_tac "tcbState tcb";
           clarsimp simp: valid_tcb_state'_def valid_bound_ntfn'_def
                   dest!: refs_notRange split: option.splits) apply (clarsimp simp: valid_cte'_def) apply (rule_tac p=p in valid_cap2) apply (clarsimp simp: ko_wp_at'_def objBits_simps' cte_level_bits_def[symmetric]) apply (erule(2) cte_wp_at_cteI') apply simp apply (rename_tac arch_kernel_object) apply (case_tac "arch_kernel_object", simp_all) apply (rename_tac asidpool) apply (case_tac asidpool, clarsimp simp: page_directory_at'_def) apply (rename_tac pte) apply (case_tac pte, simp_all add: valid_mapping'_def) apply(rename_tac pde) apply (case_tac pde, simp_all add: valid_mapping'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_obj' obj s; ko_wp_at' ((=) obj) p s\<rbrakk> \<Longrightarrow> valid_obj' obj state' proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>valid_ep' x1 s; ko_wp_at' ((=) (KOEndpoint x1)) p s; obj = KOEndpoint x1\<rbrakk> \<Longrightarrow> valid_ep' x1 state'
 2. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>endpoint. \<lbrakk>valid_ep' endpoint s; ko_wp_at' ((=) (KOEndpoint endpoint)) p s; obj = KOEndpoint endpoint\<rbrakk> \<Longrightarrow> valid_ep' endpoint state'
 2. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (6 subgoals):
 1. \<And>endpoint x1. \<lbrakk>x1 \<noteq> [] \<and> (\<forall>t\<in>set x1. tcb_at' t s) \<and> distinct x1; ko_wp_at' ((=) (KOEndpoint (Structures_H.endpoint.RecvEP x1))) p s; obj = KOEndpoint (Structures_H.endpoint.RecvEP x1); endpoint = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x1. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 2. \<And>endpoint x3. \<lbrakk>x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3; ko_wp_at' ((=) (KOEndpoint (Structures_H.endpoint.SendEP x3))) p s; obj = KOEndpoint (Structures_H.endpoint.SendEP x3); endpoint = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x3. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 3. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 4. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 5. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 6. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (6 subgoals):
 1. \<And>x1 t. \<lbrakk>obj = KOEndpoint (Structures_H.endpoint.RecvEP x1); t \<in> set x1; x1 \<noteq> []; \<forall>t\<in>set x1. tcb_at' t s; distinct x1; state_refs_of' s p = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. (p, TCBBlockedRecv) \<in> state_refs_of' s x; base \<le> t; t \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False
 2. \<And>endpoint x3. \<lbrakk>x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3; ko_wp_at' ((=) (KOEndpoint (Structures_H.endpoint.SendEP x3))) p s; obj = KOEndpoint (Structures_H.endpoint.SendEP x3); endpoint = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x3. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 3. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 4. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 5. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 6. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (6 subgoals):
 1. \<And>x1 t. \<lbrakk>obj = KOEndpoint (Structures_H.endpoint.RecvEP x1); t \<in> set x1; x1 \<noteq> []; distinct x1; state_refs_of' s p = set x1 \<times> {EPRecv}; base \<le> t; t \<le> base + (2 ^ bits - 1); tcb_at' t s; (p, TCBBlockedRecv) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> False
 2. \<And>endpoint x3. \<lbrakk>x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3; ko_wp_at' ((=) (KOEndpoint (Structures_H.endpoint.SendEP x3))) p s; obj = KOEndpoint (Structures_H.endpoint.SendEP x3); endpoint = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x3. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 3. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 4. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 5. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 6. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>endpoint x3. \<lbrakk>x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3; ko_wp_at' ((=) (KOEndpoint (Structures_H.endpoint.SendEP x3))) p s; obj = KOEndpoint (Structures_H.endpoint.SendEP x3); endpoint = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x3. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 2. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>x3 t. \<lbrakk>obj = KOEndpoint (Structures_H.endpoint.SendEP x3); t \<in> set x3; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; state_refs_of' s p = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. (p, TCBBlockedSend) \<in> state_refs_of' s x; base \<le> t; t \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>x3 t. \<lbrakk>obj = KOEndpoint (Structures_H.endpoint.SendEP x3); t \<in> set x3; x3 \<noteq> []; distinct x3; state_refs_of' s p = set x3 \<times> {EPSend}; base \<le> t; t \<le> base + (2 ^ bits - 1); tcb_at' t s; (p, TCBBlockedSend) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>valid_ntfn' x2 s; ko_wp_at' ((=) (KONotification x2)) p s; obj = KONotification x2\<rbrakk> \<Longrightarrow> valid_ntfn' x2 state'
 2. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>notification. \<lbrakk>valid_ntfn' notification s; ko_wp_at' ((=) (KONotification notification)) p s; obj = KONotification notification\<rbrakk> \<Longrightarrow> valid_ntfn' notification state'
 2. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>notification x1 x2. \<lbrakk>(case x1 of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN x1 x2) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case x2 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s); ko_wp_at' ((=) (KONotification (NTFN x1 x2))) p s; obj = KONotification (NTFN x1 x2); notification = NTFN x1 x2\<rbrakk> \<Longrightarrow> (case x1 of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t state') \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN x1 x2) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case x2 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s \<and> (base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)))
 2. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>notification ntfn bound. \<lbrakk>(case ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN ntfn bound) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case bound of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s); ko_wp_at' ((=) (KONotification (NTFN ntfn bound))) p s; obj = KONotification (NTFN ntfn bound); notification = NTFN ntfn bound\<rbrakk> \<Longrightarrow> (case ntfn of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t state') \<and> distinct ts \<and> (case ntfnBoundTCB (NTFN ntfn bound) of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case bound of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at' t s \<and> (base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)))
 2. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (7 subgoals):
 1. \<And>notification ntfn bound x2. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN Structures_H.ntfn.IdleNtfn (Some x2)))) p s; obj = KONotification (NTFN Structures_H.ntfn.IdleNtfn (Some x2)); notification = NTFN Structures_H.ntfn.IdleNtfn (Some x2); ntfn = Structures_H.ntfn.IdleNtfn; bound = Some x2; tcb_at' x2 s\<rbrakk> \<Longrightarrow> base \<le> x2 \<longrightarrow> \<not> x2 \<le> base + (2 ^ bits - 1)
 2. \<And>notification ntfn bound x2 x2a. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.ActiveNtfn x2) (Some x2a)))) p s; obj = KONotification (NTFN (Structures_H.ntfn.ActiveNtfn x2) (Some x2a)); notification = NTFN (Structures_H.ntfn.ActiveNtfn x2) (Some x2a); ntfn = Structures_H.ntfn.ActiveNtfn x2; bound = Some x2a; tcb_at' x2a s\<rbrakk> \<Longrightarrow> base \<le> x2a \<longrightarrow> \<not> x2a \<le> base + (2 ^ bits - 1)
 3. \<And>notification ntfn bound x3. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.WaitingNtfn x3) None))) p s; obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn x3) None); notification = NTFN (Structures_H.ntfn.WaitingNtfn x3) None; ntfn = Structures_H.ntfn.WaitingNtfn x3; bound = None; x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x3. base \<le> t \<longrightarrow> \<not> t \<le> base + (2 ^ bits - 1)
 4. \<And>notification ntfn bound x2. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)))) p s; obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)); notification = NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2); ntfn = Structures_H.ntfn.WaitingNtfn [x2]; bound = Some x2; tcb_at' x2 s\<rbrakk> \<Longrightarrow> base \<le> x2 \<longrightarrow> \<not> x2 \<le> base + (2 ^ bits - 1)
 5. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 6. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 7. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>x3 t. \<lbrakk>obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn x3) None); t \<in> set x3; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; state_refs_of' s p = set x3 \<times> {NTFNSignal}; \<forall>x\<in>set x3. (p, TCBSignal) \<in> state_refs_of' s x; base \<le> t; t \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False
 2. \<And>notification ntfn bound x2. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)))) p s; obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)); notification = NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2); ntfn = Structures_H.ntfn.WaitingNtfn [x2]; bound = Some x2; tcb_at' x2 s\<rbrakk> \<Longrightarrow> base \<le> x2 \<longrightarrow> \<not> x2 \<le> base + (2 ^ bits - 1)
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>x3 t. \<lbrakk>obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn x3) None); t \<in> set x3; x3 \<noteq> []; distinct x3; state_refs_of' s p = set x3 \<times> {NTFNSignal}; base \<le> t; t \<le> base + (2 ^ bits - 1); tcb_at' t s; (p, TCBSignal) \<in> state_refs_of' s t\<rbrakk> \<Longrightarrow> False
 2. \<And>notification ntfn bound x2. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)))) p s; obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)); notification = NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2); ntfn = Structures_H.ntfn.WaitingNtfn [x2]; bound = Some x2; tcb_at' x2 s\<rbrakk> \<Longrightarrow> base \<le> x2 \<longrightarrow> \<not> x2 \<le> base + (2 ^ bits - 1)
 3. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>notification ntfn bound x2. \<lbrakk>ko_wp_at' ((=) (KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)))) p s; obj = KONotification (NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2)); notification = NTFN (Structures_H.ntfn.WaitingNtfn [x2]) (Some x2); ntfn = Structures_H.ntfn.WaitingNtfn [x2]; bound = Some x2; tcb_at' x2 s\<rbrakk> \<Longrightarrow> base \<le> x2 \<longrightarrow> \<not> x2 \<le> base + (2 ^ bits - 1)
 2. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 2. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 3. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>valid_tcb' x6 s; ko_wp_at' ((=) (KOTCB x6)) p s; obj = KOTCB x6; \<exists>ko. KOTCB x6 = ko \<and> state_refs_of' s p = refs_of' ko \<and> (\<forall>(x, tp)\<in>refs_of' ko. (p, symreftype tp) \<in> state_refs_of' s x)\<rbrakk> \<Longrightarrow> valid_tcb' x6 state'
 2. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 3. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) state') \<and> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 2. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 3. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) state'
 2. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>x6 a b x. \<lbrakk>obj = KOTCB x6; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority; valid_cap' (cteCap (a x6)) s; tcb_cte_cases x = Some (a, b)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a x6)) state'
 2. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>x6 a b x. \<lbrakk>obj = KOTCB x6; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority; valid_cap' (cteCap (a x6)) s; tcb_cte_cases x = Some (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap (a x6)) (p + x) s
 2. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (5 subgoals):
 1. \<And>x6 a b x. \<lbrakk>obj = KOTCB x6; state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority; valid_cap' (cteCap (a x6)) s; tcb_cte_cases x = Some (a, b)\<rbrakk> \<Longrightarrow> tcb_cte_cases (p + x - p) = Some (?getF147 x6 a b x, ?setF147 x6 a b x)
 2. \<And>x6 a b x. \<lbrakk>obj = KOTCB x6; state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority; valid_cap' (cteCap (a x6)) s; tcb_cte_cases x = Some (a, b)\<rbrakk> \<Longrightarrow> cteCap (?getF147 x6 a b x x6) = cteCap (a x6)
 3. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 4. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 5. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (4 subgoals):
 1. \<And>x6 a b x. \<lbrakk>obj = KOTCB x6; state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority; valid_cap' (cteCap (a x6)) s; tcb_cte_cases x = Some (a, b)\<rbrakk> \<Longrightarrow> cteCap (a x6) = cteCap (a x6)
 2. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 3. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 4. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>obj = KOTCB x6; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF x6)) s; ksPSpace s p = Some (KOTCB x6); state_refs_of' s p = tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6); \<forall>x\<in>tcb_st_refs_of' (tcbState x6) \<union> tcb_bound_refs' (tcbBoundNotification x6). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState x6) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer x6) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification x6) s; tcbDomain x6 \<le> maxDomain; tcbPriority x6 \<le> maxPriority; tcbMCP x6 \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState x6) state' \<and> valid_bound_ntfn' (tcbBoundNotification x6) state'
 2. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 3. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>obj = KOTCB tcb; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s; ksPSpace s p = Some (KOTCB tcb); state_refs_of' s p = tcb_st_refs_of' (tcbState tcb) \<union> tcb_bound_refs' (tcbBoundNotification tcb); \<forall>x\<in>tcb_st_refs_of' (tcbState tcb) \<union> tcb_bound_refs' (tcbBoundNotification tcb). case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x; valid_tcb_state' (tcbState tcb) s; is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s; is_aligned (tcbIPCBuffer tcb) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification tcb) s; tcbDomain tcb \<le> maxDomain; tcbPriority tcb \<le> maxPriority; tcbMCP tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' (tcbState tcb) state' \<and> valid_bound_ntfn' (tcbBoundNotification tcb) state'
 2. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 3. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>valid_cte' x7 s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cte' x7 state'
 2. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>valid_cap' (cteCap x7) s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> valid_cap' (cteCap x7) state'
 2. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>valid_cap' (cteCap x7) s; ko_wp_at' ((=) (KOCTE x7)) p s; obj = KOCTE x7\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap x7) p s
 2. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>valid_cap' (cteCap x7) s; obj = KOCTE x7; ksPSpace s p = Some (KOCTE x7); is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = cteCap x7) p s
 2. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>valid_cap' (cteCap x7) s; obj = KOCTE x7; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> cteCap x7 = cteCap x7
 2. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>valid_arch_obj' x8 s; ko_wp_at' ((=) (KOArch x8)) p s; obj = KOArch x8\<rbrakk> \<Longrightarrow> valid_arch_obj' x8 state' proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. \<lbrakk>valid_arch_obj' arch_kernel_object s; ko_wp_at' ((=) (KOArch arch_kernel_object)) p s; obj = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> valid_arch_obj' arch_kernel_object state' proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_object x1. \<lbrakk>valid_asid_pool' x1 s; ko_wp_at' ((=) (KOArch (KOASIDPool x1))) p s; obj = KOArch (KOASIDPool x1); arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> valid_asid_pool' x1 state'
 2. \<And>arch_kernel_object x2. \<lbrakk>valid_pte' x2 s; ko_wp_at' ((=) (KOArch (KOPTE x2))) p s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 state'
 3. \<And>arch_kernel_object x3. \<lbrakk>valid_pde' x3 s; ko_wp_at' ((=) (KOArch (KOPDE x3))) p s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 state' proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_object asidpool. \<lbrakk>valid_asid_pool' asidpool s; ko_wp_at' ((=) (KOArch (KOASIDPool asidpool))) p s; obj = KOArch (KOASIDPool asidpool); arch_kernel_object = KOASIDPool asidpool\<rbrakk> \<Longrightarrow> valid_asid_pool' asidpool state'
 2. \<And>arch_kernel_object x2. \<lbrakk>valid_pte' x2 s; ko_wp_at' ((=) (KOArch (KOPTE x2))) p s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 state'
 3. \<And>arch_kernel_object x3. \<lbrakk>valid_pde' x3 s; ko_wp_at' ((=) (KOArch (KOPDE x3))) p s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 state' proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_object x2. \<lbrakk>valid_pte' x2 s; ko_wp_at' ((=) (KOArch (KOPTE x2))) p s; obj = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> valid_pte' x2 state'
 2. \<And>arch_kernel_object x3. \<lbrakk>valid_pde' x3 s; ko_wp_at' ((=) (KOArch (KOPDE x3))) p s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 state' proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_object pte. \<lbrakk>valid_pte' pte s; ko_wp_at' ((=) (KOArch (KOPTE pte))) p s; obj = KOArch (KOPTE pte); arch_kernel_object = KOPTE pte\<rbrakk> \<Longrightarrow> valid_pte' pte state'
 2. \<And>arch_kernel_object x3. \<lbrakk>valid_pde' x3 s; ko_wp_at' ((=) (KOArch (KOPDE x3))) p s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 state' proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object x3. \<lbrakk>valid_pde' x3 s; ko_wp_at' ((=) (KOArch (KOPDE x3))) p s; obj = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> valid_pde' x3 state' proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object pde. \<lbrakk>valid_pde' pde s; ko_wp_at' ((=) (KOArch (KOPDE pde))) p s; obj = KOArch (KOPDE pde); arch_kernel_object = KOPDE pde\<rbrakk> \<Longrightarrow> valid_pde' pde state' proof (prove)
goal:
No subgoals!