theory CSpace1_R

lemma prev_update_subtree [simp]:
  "modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b = m' \<turnstile> a \<rightarrow> b"
  (is "?m' = ?m") proof assume "?m" thus ?m' proof induct case (direct_parent c) thus ?case apply - apply (rule subtree.direct_parent) apply (clarsimp simp add: mdb_next_unfold modify_map_def) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def) apply fastforce done next case (trans_parent c c') thus ?case apply - apply (rule subtree.trans_parent) apply (rule trans_parent.hyps) apply (clarsimp simp add: mdb_next_unfold modify_map_def) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def) apply fastforce done qed next assume "?m'" thus ?m proof induct case (direct_parent c) thus ?case apply - apply (rule subtree.direct_parent) apply (clarsimp simp add: mdb_next_unfold modify_map_def split: if_split_asm) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def split: if_split_asm) done next case (trans_parent c c') thus ?case apply - apply (rule subtree.trans_parent) apply (rule trans_parent.hyps) apply (clarsimp simp add: mdb_next_unfold modify_map_def split: if_split_asm) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def split: if_split_asm) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b = m' \<turnstile> a \<rightarrow> b proof (state)
goal (2 subgoals):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b \<Longrightarrow> m' \<turnstile> a \<rightarrow> b
 2. m' \<turnstile> a \<rightarrow> b \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b proof (state)
this:
m' \<turnstile> a \<rightarrow> b

goal (2 subgoals):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b \<Longrightarrow> m' \<turnstile> a \<rightarrow> b
 2. m' \<turnstile> a \<rightarrow> b \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b proof (prove)
using this:
m' \<turnstile> a \<rightarrow> b

goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'' proof (state)
this:
m' \<turnstile> a \<leadsto> c
c \<noteq> 0
m' \<turnstile> a parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> a \<leadsto> c
c \<noteq> 0
m' \<turnstile> a parentOf c

goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c
 2. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m' \<turnstile> a \<leadsto> c; c \<noteq> 0; m' c = Some cte; m' a = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (a = x \<longrightarrow> (c = x \<longrightarrow> (\<exists>cte' cte. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte) \<and> (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte') \<and> isMDBParentOf cte' cte)) \<and> (c \<noteq> x \<longrightarrow> (\<exists>cte'. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte') \<and> isMDBParentOf cte' cte))) \<and> (a \<noteq> x \<longrightarrow> c = x \<longrightarrow> (\<exists>cte. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte) \<and> isMDBParentOf cte' cte)) proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'' proof (state)
this:
m' \<turnstile> a \<rightarrow> c
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c
m' \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> a parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> a \<rightarrow> c
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c
m' \<turnstile> c \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> a parentOf c'

goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> ?c'5
 2. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> ?c'5 \<leadsto> c'
 3. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'
 2. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c' proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>m' \<turnstile> a \<rightarrow> c; (\<lambda>a. if a = x then map_option (cteMDBNode_update (mdbPrev_update f)) (m' x) else m' a) \<turnstile> a \<rightarrow> c; m' \<turnstile> c \<leadsto> c'; c' \<noteq> 0; m' c' = Some cte; m' a = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> (a = x \<longrightarrow> (c' = x \<longrightarrow> (\<exists>cte' cte. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte) \<and> (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte') \<and> isMDBParentOf cte' cte)) \<and> (c' \<noteq> x \<longrightarrow> (\<exists>cte'. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte') \<and> isMDBParentOf cte' cte))) \<and> (a \<noteq> x \<longrightarrow> c' = x \<longrightarrow> (\<exists>cte. (\<exists>z. m' x = Some z \<and> cteMDBNode_update (mdbPrev_update f) z = cte) \<and> isMDBParentOf cte' cte)) proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'

goal:
No subgoals! proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b

goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b \<Longrightarrow> m' \<turnstile> a \<rightarrow> b proof (state)
goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b \<Longrightarrow> m' \<turnstile> a \<rightarrow> b proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b

goal (1 subgoal):
 1. modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b \<Longrightarrow> m' \<turnstile> a \<rightarrow> b proof (prove)
using this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b

goal (1 subgoal):
 1. m' \<turnstile> a \<rightarrow> b proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'' proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c
c \<noteq> 0
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'' proof (prove)
using this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c
c \<noteq> 0
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c

goal (1 subgoal):
 1. m' \<turnstile> a \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<leadsto> c
 2. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> c; c \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> a \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'' proof (state)
this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c
m' \<turnstile> a \<rightarrow> c
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'
c' \<noteq> 0
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c'; m' \<turnstile> a \<rightarrow> c'; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c'' proof (prove)
using this:
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c
m' \<turnstile> a \<rightarrow> c
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'
c' \<noteq> 0
modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'

goal (1 subgoal):
 1. m' \<turnstile> a \<rightarrow> c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> c' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a \<rightarrow> ?c'5
 2. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> ?c'5 \<leadsto> c'
 3. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 4. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> c \<leadsto> c'
 2. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> c; m' \<turnstile> a \<rightarrow> c; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> c \<leadsto> c'; c' \<noteq> 0; modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> a parentOf c' proof (prove)
goal:
No subgoals! proof (state)
this:
m' \<turnstile> a \<rightarrow> c'

goal:
No subgoals! proof (state)
this:
m' \<turnstile> a \<rightarrow> b

goal:
No subgoals!