theory Example_Valid_StateH

lemma kh0H_SomeD:
  "kh0H x = Some y \<Longrightarrow>
        x = init_globals_frame \<and> y = KOUserData \<or>
        x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or>
        x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or>
        x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or>
        x = ntfn_ptr \<and> y = KONotification ntfnH \<or>
        x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or>
        x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap Null_mdb) \<or>
        x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or>
        x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or>
        x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or>
        x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or>
        x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or>
        x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or>
        x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or>
        x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)" apply (frule kh0H_SomeD') apply (elim disjE) apply (clarsimp | frule offs_range_correct)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kh0H x = Some y \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh0H x = Some y; x = init_globals_frame \<or> x = idle_tcb_ptr \<or> x = High_tcb_ptr \<or> x = Low_tcb_ptr \<or> x = irq_cnode_ptr \<or> x = ntfn_ptr \<or> x \<in> irq_node_offs_range \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<or> x \<in> cnode_offs_range High_cnode_ptr \<or> x \<in> cnode_offs_range Low_cnode_ptr \<or> x \<in> pd_offs_range init_global_pd \<or> x \<in> pd_offs_range High_pd_ptr \<or> x \<in> pd_offs_range Low_pd_ptr \<or> x \<in> pt_offs_range High_pt_ptr \<or> x \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x) proof (prove)
goal (15 subgoals):
 1. \<lbrakk>kh0H x = Some y; x = init_globals_frame\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 2. \<lbrakk>kh0H x = Some y; x = idle_tcb_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 3. \<lbrakk>kh0H x = Some y; x = High_tcb_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 4. \<lbrakk>kh0H x = Some y; x = Low_tcb_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 5. \<lbrakk>kh0H x = Some y; x = irq_cnode_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 6. \<lbrakk>kh0H x = Some y; x = ntfn_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 7. \<lbrakk>kh0H x = Some y; x \<in> irq_node_offs_range\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 8. \<lbrakk>kh0H x = Some y; x \<in> cnode_offs_range Silc_cnode_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 9. \<lbrakk>kh0H x = Some y; x \<in> cnode_offs_range High_cnode_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
 10. \<lbrakk>kh0H x = Some y; x \<in> cnode_offs_range Low_cnode_ptr\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = KOUserData \<or> x = idle_tcb_ptr \<and> y = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> y = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> y = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> y = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> y = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> y = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> y = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> y = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> y = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> y = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> y = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> y = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> y = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> y = the (Low_ptH Low_pt_ptr x)
A total of 15 subgoals... proof (prove)
goal:
No subgoals!