theory Example_Valid_StateH

lemma range_tcb_not_kh0H_dom:
  "{(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> (x && ~~ mask 9) \<noteq> High_tcb_ptr"
  "{(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> (x && ~~ mask 9) \<noteq> Low_tcb_ptr"
  "{(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> (x && ~~ mask 9) \<noteq> idle_tcb_ptr" apply clarsimp apply (drule int_not_emptyD) apply (clarsimp simp: kh0H_dom) apply (subgoal_tac "xa \<in> tcb_offs_range High_tcb_ptr") prefer 2 apply (clarsimp simp: tcb_offs_range_def objBitsKO_def) apply (rule_tac y="High_tcb_ptr + 1" in order_trans) apply (simp add: s0_ptr_defs) apply simp apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply ((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2]
          | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1])+)[1] apply (clarsimp simp: s0_ptr_defs tcb_offs_range_def) apply clarsimp apply (drule int_not_emptyD) apply (clarsimp simp: kh0H_dom) apply (subgoal_tac "xa \<in> tcb_offs_range Low_tcb_ptr") prefer 2 apply (clarsimp simp: tcb_offs_range_def objBitsKO_def) apply (rule_tac y="Low_tcb_ptr + 1" in order_trans) apply (simp add: s0_ptr_defs) apply simp apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply ((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2]
         | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1])+)[1] apply (clarsimp simp: s0_ptr_defs tcb_offs_range_def) apply clarsimp apply (drule int_not_emptyD) apply (clarsimp simp: kh0H_dom) apply (subgoal_tac "xa \<in> tcb_offs_range idle_tcb_ptr") prefer 2 apply (clarsimp simp: tcb_offs_range_def objBitsKO_def) apply (rule_tac y="idle_tcb_ptr + 1" in order_trans) apply (simp add: s0_ptr_defs) apply simp apply (clarsimp simp: kh0H_dom_distinct[THEN set_mem_neq]) apply ((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2]
        | clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1])+)[1] apply (clarsimp simp: s0_ptr_defs tcb_offs_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> High_tcb_ptr) &&& ({(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr) &&& ({(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>{High_tcb_ptr + 1..0x1FF + High_tcb_ptr} \<inter> dom kh0H \<noteq> {}; x && ~~ mask 9 = High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; \<exists>x. x \<in> {High_tcb_ptr + 1..0x1FF + High_tcb_ptr} \<and> x \<in> dom kh0H\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range High_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range High_tcb_ptr
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> High_tcb_ptr \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> High_tcb_ptr \<le> High_tcb_ptr + 1
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> High_tcb_ptr + 1 \<le> xa
 3. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 5. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> High_tcb_ptr + 1 \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + High_tcb_ptr; xa = High_tcb_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x && ~~ mask 9 = High_tcb_ptr; High_tcb_ptr = - 1; High_tcb_ptr \<le> 0x1FF + High_tcb_ptr; High_tcb_ptr \<in> tcb_offs_range High_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> Low_tcb_ptr
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{Low_tcb_ptr + 1..0x1FF + Low_tcb_ptr} \<inter> dom kh0H \<noteq> {}; x && ~~ mask 9 = Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; \<exists>x. x \<in> {Low_tcb_ptr + 1..0x1FF + Low_tcb_ptr} \<and> x \<in> dom kh0H\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range Low_tcb_ptr
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range Low_tcb_ptr
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> Low_tcb_ptr \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> Low_tcb_ptr \<le> Low_tcb_ptr + 1
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> Low_tcb_ptr + 1 \<le> xa
 3. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 4. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> Low_tcb_ptr + 1 \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 3. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + Low_tcb_ptr; xa = Low_tcb_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && ~~ mask 9 = Low_tcb_ptr; Low_tcb_ptr = - 1; Low_tcb_ptr \<le> 0x1FF + Low_tcb_ptr; Low_tcb_ptr \<in> tcb_offs_range Low_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (1 subgoal):
 1. {(x && ~~ mask 9) + 1..(x && ~~ mask 9) + 2 ^ 9 - 1} \<inter> dom kh0H \<noteq> {} \<Longrightarrow> x && ~~ mask 9 \<noteq> idle_tcb_ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{idle_tcb_ptr + 1..0x1FF + idle_tcb_ptr} \<inter> dom kh0H \<noteq> {}; x && ~~ mask 9 = idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; \<exists>x. x \<in> {idle_tcb_ptr + 1..0x1FF + idle_tcb_ptr} \<and> x \<in> dom kh0H\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range idle_tcb_ptr proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> xa \<in> tcb_offs_range idle_tcb_ptr
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> idle_tcb_ptr \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> idle_tcb_ptr \<le> idle_tcb_ptr + 1
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> idle_tcb_ptr + 1 \<le> xa
 3. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr\<rbrakk> \<Longrightarrow> idle_tcb_ptr + 1 \<le> xa
 2. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = init_globals_frame \<or> xa = idle_tcb_ptr \<or> xa = High_tcb_ptr \<or> xa = Low_tcb_ptr \<or> xa = irq_cnode_ptr \<or> xa = ntfn_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr + 1 \<le> xa; xa \<le> 0x1FF + idle_tcb_ptr; xa = idle_tcb_ptr \<or> xa \<in> irq_node_offs_range \<or> xa \<in> cnode_offs_range Silc_cnode_ptr \<or> xa \<in> cnode_offs_range High_cnode_ptr \<or> xa \<in> cnode_offs_range Low_cnode_ptr \<or> xa \<in> pd_offs_range init_global_pd \<or> xa \<in> pd_offs_range High_pd_ptr \<or> xa \<in> pd_offs_range Low_pd_ptr \<or> xa \<in> pt_offs_range High_pt_ptr \<or> xa \<in> pt_offs_range Low_pt_ptr; xa \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask 9 = idle_tcb_ptr; idle_tcb_ptr = - 1; idle_tcb_ptr \<le> 0x1FF + idle_tcb_ptr; idle_tcb_ptr \<in> tcb_offs_range idle_tcb_ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!