theory Example_Valid_StateH

lemma kh0H_dom_distinct:
  "init_globals_frame \<notin> cnode_offs_range Silc_cnode_ptr"
  "idle_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr"
  "High_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr"
  "Low_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr"
  "irq_cnode_ptr \<notin> cnode_offs_range Silc_cnode_ptr"
  "ntfn_ptr \<notin> cnode_offs_range Silc_cnode_ptr"
  "init_globals_frame \<notin> cnode_offs_range Low_cnode_ptr"
  "idle_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr"
  "High_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr"
  "Low_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr"
  "irq_cnode_ptr \<notin> cnode_offs_range Low_cnode_ptr"
  "ntfn_ptr \<notin> cnode_offs_range Low_cnode_ptr"
  "init_globals_frame \<notin> cnode_offs_range High_cnode_ptr"
  "idle_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr"
  "High_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr"
  "Low_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr"
  "irq_cnode_ptr \<notin> cnode_offs_range High_cnode_ptr"
  "ntfn_ptr \<notin> cnode_offs_range High_cnode_ptr"
  "init_globals_frame \<notin> pd_offs_range Low_pd_ptr"
  "idle_tcb_ptr \<notin> pd_offs_range Low_pd_ptr"
  "High_tcb_ptr \<notin> pd_offs_range Low_pd_ptr"
  "Low_tcb_ptr \<notin> pd_offs_range Low_pd_ptr"
  "irq_cnode_ptr \<notin> pd_offs_range Low_pd_ptr"
  "ntfn_ptr \<notin> pd_offs_range Low_pd_ptr"
  "init_globals_frame \<notin> pd_offs_range High_pd_ptr"
  "idle_tcb_ptr \<notin> pd_offs_range High_pd_ptr"
  "High_tcb_ptr \<notin> pd_offs_range High_pd_ptr"
  "Low_tcb_ptr \<notin> pd_offs_range High_pd_ptr"
  "irq_cnode_ptr \<notin> pd_offs_range High_pd_ptr"
  "ntfn_ptr \<notin> pd_offs_range High_pd_ptr"
  "init_globals_frame \<notin> pd_offs_range init_global_pd"
  "idle_tcb_ptr \<notin> pd_offs_range init_global_pd"
  "High_tcb_ptr \<notin> pd_offs_range init_global_pd"
  "Low_tcb_ptr \<notin> pd_offs_range init_global_pd"
  "irq_cnode_ptr \<notin> pd_offs_range init_global_pd"
  "ntfn_ptr \<notin> pd_offs_range init_global_pd"
  "init_globals_frame \<notin> pt_offs_range Low_pt_ptr"
  "idle_tcb_ptr \<notin> pt_offs_range Low_pt_ptr"
  "High_tcb_ptr \<notin> pt_offs_range Low_pt_ptr"
  "Low_tcb_ptr \<notin> pt_offs_range Low_pt_ptr"
  "irq_cnode_ptr \<notin> pt_offs_range Low_pt_ptr"
  "ntfn_ptr \<notin> pt_offs_range Low_pt_ptr"
  "init_globals_frame \<notin> pt_offs_range High_pt_ptr"
  "idle_tcb_ptr \<notin> pt_offs_range High_pt_ptr"
  "High_tcb_ptr \<notin> pt_offs_range High_pt_ptr"
  "Low_tcb_ptr \<notin> pt_offs_range High_pt_ptr"
  "irq_cnode_ptr \<notin> pt_offs_range High_pt_ptr"
  "ntfn_ptr \<notin> pt_offs_range High_pt_ptr"
  "init_globals_frame \<notin> tcb_offs_range Low_tcb_ptr"
  "idle_tcb_ptr \<notin> tcb_offs_range Low_tcb_ptr"
  "High_tcb_ptr \<notin> tcb_offs_range Low_tcb_ptr"
  "irq_cnode_ptr \<notin> tcb_offs_range Low_tcb_ptr"
  "ntfn_ptr \<notin> tcb_offs_range Low_tcb_ptr"
  "init_globals_frame \<notin> tcb_offs_range High_tcb_ptr"
  "idle_tcb_ptr \<notin> tcb_offs_range High_tcb_ptr"
  "Low_tcb_ptr \<notin> tcb_offs_range High_tcb_ptr"
  "irq_cnode_ptr \<notin> tcb_offs_range High_tcb_ptr"
  "ntfn_ptr \<notin> tcb_offs_range High_tcb_ptr"
  "init_globals_frame \<notin> tcb_offs_range idle_tcb_ptr"
  "High_tcb_ptr \<notin> tcb_offs_range idle_tcb_ptr"
  "Low_tcb_ptr \<notin> tcb_offs_range idle_tcb_ptr"
  "irq_cnode_ptr \<notin> tcb_offs_range idle_tcb_ptr"
  "ntfn_ptr \<notin> tcb_offs_range idle_tcb_ptr" by (clarsimp simp: cnode_offs_range_def pd_offs_range_def pt_offs_range_def tcb_offs_range_def kh0H_obj_def s0_ptr_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((init_globals_frame \<notin> cnode_offs_range Silc_cnode_ptr &&& idle_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr &&& High_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr) &&& (Low_tcb_ptr \<notin> cnode_offs_range Silc_cnode_ptr &&& irq_cnode_ptr \<notin> cnode_offs_range Silc_cnode_ptr) &&& ntfn_ptr \<notin> cnode_offs_range Silc_cnode_ptr &&& init_globals_frame \<notin> cnode_offs_range Low_cnode_ptr) &&& ((idle_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr &&& High_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr) &&& Low_tcb_ptr \<notin> cnode_offs_range Low_cnode_ptr &&& irq_cnode_ptr \<notin> cnode_offs_range Low_cnode_ptr) &&& (ntfn_ptr \<notin> cnode_offs_range Low_cnode_ptr &&& init_globals_frame \<notin> cnode_offs_range High_cnode_ptr) &&& idle_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr &&& High_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr) &&& (((Low_tcb_ptr \<notin> cnode_offs_range High_cnode_ptr &&& irq_cnode_ptr \<notin> cnode_offs_range High_cnode_ptr) &&& ntfn_ptr \<notin> cnode_offs_range High_cnode_ptr &&& init_globals_frame \<notin> pd_offs_range Low_pd_ptr) &&& (idle_tcb_ptr \<notin> pd_offs_range Low_pd_ptr &&& High_tcb_ptr \<notin> pd_offs_range Low_pd_ptr) &&& Low_tcb_ptr \<notin> pd_offs_range Low_pd_ptr &&& irq_cnode_ptr \<notin> pd_offs_range Low_pd_ptr) &&& ((ntfn_ptr \<notin> pd_offs_range Low_pd_ptr &&& init_globals_frame \<notin> pd_offs_range High_pd_ptr) &&& idle_tcb_ptr \<notin> pd_offs_range High_pd_ptr &&& High_tcb_ptr \<notin> pd_offs_range High_pd_ptr) &&& (Low_tcb_ptr \<notin> pd_offs_range High_pd_ptr &&& irq_cnode_ptr \<notin> pd_offs_range High_pd_ptr) &&& ntfn_ptr \<notin> pd_offs_range High_pd_ptr &&& init_globals_frame \<notin> pd_offs_range init_global_pd) &&& ((((idle_tcb_ptr \<notin> pd_offs_range init_global_pd &&& High_tcb_ptr \<notin> pd_offs_range init_global_pd) &&& Low_tcb_ptr \<notin> pd_offs_range init_global_pd &&& irq_cnode_ptr \<notin> pd_offs_range init_global_pd) &&& (ntfn_ptr \<notin> pd_offs_range init_global_pd &&& init_globals_frame \<notin> pt_offs_range Low_pt_ptr) &&& idle_tcb_ptr \<notin> pt_offs_range Low_pt_ptr &&& High_tcb_ptr \<notin> pt_offs_range Low_pt_ptr) &&& ((Low_tcb_ptr \<notin> pt_offs_range Low_pt_ptr &&& irq_cnode_ptr \<notin> pt_offs_range Low_pt_ptr) &&& ntfn_ptr \<notin> pt_offs_range Low_pt_ptr &&& init_globals_frame \<notin> pt_offs_range High_pt_ptr) &&& (idle_tcb_ptr \<notin> pt_offs_range High_pt_ptr &&& High_tcb_ptr \<notin> pt_offs_range High_pt_ptr) &&& Low_tcb_ptr \<notin> pt_offs_range High_pt_ptr &&& irq_cnode_ptr \<notin> pt_offs_range High_pt_ptr) &&& (((ntfn_ptr \<notin> pt_offs_range High_pt_ptr &&& init_globals_frame \<notin> tcb_offs_range Low_tcb_ptr) &&& idle_tcb_ptr \<notin> tcb_offs_range Low_tcb_ptr &&& High_tcb_ptr \<notin> tcb_offs_range Low_tcb_ptr) &&& (irq_cnode_ptr \<notin> tcb_offs_range Low_tcb_ptr &&& ntfn_ptr \<notin> tcb_offs_range Low_tcb_ptr) &&& init_globals_frame \<notin> tcb_offs_range High_tcb_ptr &&& idle_tcb_ptr \<notin> tcb_offs_range High_tcb_ptr) &&& ((Low_tcb_ptr \<notin> tcb_offs_range High_tcb_ptr &&& irq_cnode_ptr \<notin> tcb_offs_range High_tcb_ptr) &&& ntfn_ptr \<notin> tcb_offs_range High_tcb_ptr &&& init_globals_frame \<notin> tcb_offs_range idle_tcb_ptr) &&& (High_tcb_ptr \<notin> tcb_offs_range idle_tcb_ptr &&& Low_tcb_ptr \<notin> tcb_offs_range idle_tcb_ptr) &&& irq_cnode_ptr \<notin> tcb_offs_range idle_tcb_ptr &&& ntfn_ptr \<notin> tcb_offs_range idle_tcb_ptr