theory Example_Valid_StateH

lemma mdb_next_trancl_s0H:
  "p' \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' =
     (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or>
     p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or>
     p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or>
     p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or>
     p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or>
     p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or>
     p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30)" apply (rule iffI) apply (erule converse_trancl_induct) apply (clarsimp simp: mdb_next_s0H) apply (elim disjE, simp_all add: mdb_next_s0H s0_ptr_defs)[1] apply (elim disjE) apply (rule r_into_trancl, simp add: mdb_next_s0H) apply (rule r_into_trancl, simp add: mdb_next_s0H) apply (rule r_r_into_trancl[where b="Silc_cnode_ptr + 0x13E0"]) apply (simp add: mdb_next_s0H s0_ptr_defs) apply (simp add: mdb_next_s0H) apply (rule r_into_trancl, simp add: mdb_next_s0H)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<noteq> 0 \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' = (p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> y \<leadsto> p'\<rbrakk> \<Longrightarrow> y = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> y = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> y = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> y = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> y = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<And>y z. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> y \<leadsto> z; map_to_ctes kh0H \<turnstile> z \<leadsto>\<^sup>+ p'; z = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> z = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> z = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> z = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> z = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> z = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> z = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> y = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> y = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> y = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> y = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> y = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 3. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> y \<leadsto> z; map_to_ctes kh0H \<turnstile> z \<leadsto>\<^sup>+ p'; z = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> z = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> z = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> z = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> z = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> z = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> z = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> y = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> y = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> y = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> y = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> y = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> y = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0 \<or> p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0 \<or> p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20 \<or> p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30 \<or> p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20 \<or> p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = Silc_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> 0; p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 7. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Silc_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto> Silc_cnode_ptr + 0x13E0
 2. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> Silc_cnode_ptr + 0x13E0 \<leadsto> p'
 3. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 6. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Low_cnode_ptr + 0x13E0 \<and> p' = High_cnode_ptr + 0x13E0\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> Silc_cnode_ptr + 0x13E0 \<leadsto> p'
 2. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 5. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr \<and> p' = Low_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>p' \<noteq> 0; p = Low_tcb_ptr + 0x10 \<and> p' = Low_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 3. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr \<and> p' = High_cnode_ptr + 0x20\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'
 4. \<lbrakk>p' \<noteq> 0; p = High_tcb_ptr + 0x10 \<and> p' = High_cnode_ptr + 0x30\<rbrakk> \<Longrightarrow> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal:
No subgoals!