theory Example_Valid_StateH

lemma kh0H_dom_sets_distinct:
  "irq_node_offs_range \<inter> cnode_offs_range Silc_cnode_ptr = {}"
  "irq_node_offs_range \<inter> cnode_offs_range High_cnode_ptr = {}"
  "irq_node_offs_range \<inter> cnode_offs_range Low_cnode_ptr = {}"
  "irq_node_offs_range \<inter> pd_offs_range init_global_pd = {}"
  "irq_node_offs_range \<inter> pd_offs_range High_pd_ptr = {}"
  "irq_node_offs_range \<inter> pd_offs_range Low_pd_ptr = {}"
  "irq_node_offs_range \<inter> pt_offs_range High_pt_ptr = {}"
  "irq_node_offs_range \<inter> pt_offs_range Low_pt_ptr = {}"
  "irq_node_offs_range \<inter> tcb_offs_range High_tcb_ptr = {}"
  "irq_node_offs_range \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "irq_node_offs_range \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> cnode_offs_range High_cnode_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> cnode_offs_range Low_cnode_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range init_global_pd = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> cnode_offs_range Low_cnode_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> pd_offs_range init_global_pd = {}"
  "cnode_offs_range High_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range init_global_pd = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "pd_offs_range init_global_pd \<inter> pd_offs_range High_pd_ptr = {}"
  "pd_offs_range init_global_pd \<inter> pd_offs_range Low_pd_ptr = {}"
  "pd_offs_range init_global_pd \<inter> pt_offs_range High_pt_ptr = {}"
  "pd_offs_range init_global_pd \<inter> pt_offs_range Low_pt_ptr = {}"
  "pd_offs_range init_global_pd \<inter> tcb_offs_range High_tcb_ptr = {}"
  "pd_offs_range init_global_pd \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "pd_offs_range init_global_pd \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> pd_offs_range Low_pd_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> pt_offs_range High_pt_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "pd_offs_range High_pd_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "pd_offs_range Low_pd_ptr \<inter> pt_offs_range High_pt_ptr = {}"
  "pd_offs_range Low_pd_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "pd_offs_range Low_pd_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "pd_offs_range Low_pd_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "pd_offs_range Low_pd_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "pt_offs_range High_pt_ptr \<inter> pt_offs_range Low_pt_ptr = {}"
  "pt_offs_range High_pt_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "pt_offs_range High_pt_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "pt_offs_range High_pt_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "pt_offs_range Low_pt_ptr \<inter> tcb_offs_range High_tcb_ptr = {}"
  "pt_offs_range Low_pt_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "pt_offs_range Low_pt_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "tcb_offs_range High_tcb_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}"
  "tcb_offs_range High_tcb_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}"
  "tcb_offs_range Low_tcb_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}" by (rule disjointI,
      clarsimp simp: irq_node_offs_range_def cnode_offs_range_def pd_offs_range_def pt_offs_range_def tcb_offs_range_def s0_ptr_defs,
      drule(1) order_trans le_less_trans,
      fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((((irq_node_offs_range \<inter> cnode_offs_range Silc_cnode_ptr = {} &&& irq_node_offs_range \<inter> cnode_offs_range High_cnode_ptr = {}) &&& irq_node_offs_range \<inter> cnode_offs_range Low_cnode_ptr = {} &&& irq_node_offs_range \<inter> pd_offs_range init_global_pd = {}) &&& (irq_node_offs_range \<inter> pd_offs_range High_pd_ptr = {} &&& irq_node_offs_range \<inter> pd_offs_range Low_pd_ptr = {}) &&& irq_node_offs_range \<inter> pt_offs_range High_pt_ptr = {} &&& irq_node_offs_range \<inter> pt_offs_range Low_pt_ptr = {}) &&& ((irq_node_offs_range \<inter> tcb_offs_range High_tcb_ptr = {} &&& irq_node_offs_range \<inter> tcb_offs_range Low_tcb_ptr = {}) &&& irq_node_offs_range \<inter> tcb_offs_range idle_tcb_ptr = {} &&& cnode_offs_range Silc_cnode_ptr \<inter> cnode_offs_range High_cnode_ptr = {}) &&& (cnode_offs_range Silc_cnode_ptr \<inter> cnode_offs_range Low_cnode_ptr = {} &&& cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range init_global_pd = {}) &&& cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {} &&& cnode_offs_range Silc_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {}) &&& (((cnode_offs_range Silc_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {} &&& cnode_offs_range Silc_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {}) &&& cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {} &&& cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}) &&& (cnode_offs_range Silc_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {} &&& cnode_offs_range High_cnode_ptr \<inter> cnode_offs_range Low_cnode_ptr = {}) &&& cnode_offs_range High_cnode_ptr \<inter> pd_offs_range init_global_pd = {} &&& cnode_offs_range High_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {}) &&& ((cnode_offs_range High_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {} &&& cnode_offs_range High_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {}) &&& cnode_offs_range High_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {} &&& cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {}) &&& (cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {} &&& cnode_offs_range High_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}) &&& cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range init_global_pd = {} &&& cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range High_pd_ptr = {} &&& cnode_offs_range Low_cnode_ptr \<inter> pd_offs_range Low_pd_ptr = {}) &&& ((((cnode_offs_range Low_cnode_ptr \<inter> pt_offs_range High_pt_ptr = {} &&& cnode_offs_range Low_cnode_ptr \<inter> pt_offs_range Low_pt_ptr = {}) &&& cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range High_tcb_ptr = {} &&& cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}) &&& (cnode_offs_range Low_cnode_ptr \<inter> tcb_offs_range idle_tcb_ptr = {} &&& pd_offs_range init_global_pd \<inter> pd_offs_range High_pd_ptr = {}) &&& pd_offs_range init_global_pd \<inter> pd_offs_range Low_pd_ptr = {} &&& pd_offs_range init_global_pd \<inter> pt_offs_range High_pt_ptr = {}) &&& ((pd_offs_range init_global_pd \<inter> pt_offs_range Low_pt_ptr = {} &&& pd_offs_range init_global_pd \<inter> tcb_offs_range High_tcb_ptr = {}) &&& pd_offs_range init_global_pd \<inter> tcb_offs_range Low_tcb_ptr = {} &&& pd_offs_range init_global_pd \<inter> tcb_offs_range idle_tcb_ptr = {}) &&& (pd_offs_range High_pd_ptr \<inter> pd_offs_range Low_pd_ptr = {} &&& pd_offs_range High_pd_ptr \<inter> pt_offs_range High_pt_ptr = {}) &&& pd_offs_range High_pd_ptr \<inter> pt_offs_range Low_pt_ptr = {} &&& pd_offs_range High_pd_ptr \<inter> tcb_offs_range High_tcb_ptr = {}) &&& (((pd_offs_range High_pd_ptr \<inter> tcb_offs_range Low_tcb_ptr = {} &&& pd_offs_range High_pd_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}) &&& pd_offs_range Low_pd_ptr \<inter> pt_offs_range High_pt_ptr = {} &&& pd_offs_range Low_pd_ptr \<inter> pt_offs_range Low_pt_ptr = {}) &&& (pd_offs_range Low_pd_ptr \<inter> tcb_offs_range High_tcb_ptr = {} &&& pd_offs_range Low_pd_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}) &&& pd_offs_range Low_pd_ptr \<inter> tcb_offs_range idle_tcb_ptr = {} &&& pt_offs_range High_pt_ptr \<inter> pt_offs_range Low_pt_ptr = {}) &&& ((pt_offs_range High_pt_ptr \<inter> tcb_offs_range High_tcb_ptr = {} &&& pt_offs_range High_pt_ptr \<inter> tcb_offs_range Low_tcb_ptr = {}) &&& pt_offs_range High_pt_ptr \<inter> tcb_offs_range idle_tcb_ptr = {} &&& pt_offs_range Low_pt_ptr \<inter> tcb_offs_range High_tcb_ptr = {}) &&& (pt_offs_range Low_pt_ptr \<inter> tcb_offs_range Low_tcb_ptr = {} &&& pt_offs_range Low_pt_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}) &&& tcb_offs_range High_tcb_ptr \<inter> tcb_offs_range Low_tcb_ptr = {} &&& tcb_offs_range High_tcb_ptr \<inter> tcb_offs_range idle_tcb_ptr = {} &&& tcb_offs_range Low_tcb_ptr \<inter> tcb_offs_range idle_tcb_ptr = {}