theory CSpace1_R

lemma subtree_prev_0:
  assumes s: "m \<turnstile> a \<rightarrow> b"
  assumes n: "m b = Some cte" "mdbPrev (cteMDBNode cte) = 0"
  assumes d: "valid_dlist m"
  assumes 0: "no_0 m"
  shows "False" using s n proof induct case (direct_parent c) have "m \<turnstile> a \<leadsto> c" by fact+ then obtain cte' where a: "m a = Some cte'" and "mdbNext (cteMDBNode cte') = c" by (auto simp add: mdb_next_unfold) moreover have "m c = Some cte" by fact+ moreover have "c \<noteq> 0" by fact+ ultimately have "mdbPrev (cteMDBNode cte) = a" using d by (fastforce simp add: valid_dlist_def Let_def) moreover have "mdbPrev (cteMDBNode cte) = 0" by fact+ moreover from a have "a \<noteq> 0" using assms by auto ultimately show False by simp next case (trans_parent c' c) have "m \<turnstile> c' \<leadsto> c" by fact+ then obtain cte' where c': "m c' = Some cte'" and "mdbNext (cteMDBNode cte') = c" by (auto simp add: mdb_next_unfold) moreover have "m c = Some cte" by fact+ moreover have "c \<noteq> 0" by fact+ ultimately have "mdbPrev (cteMDBNode cte) = c'" using d by (fastforce simp add: valid_dlist_def Let_def) moreover have "mdbPrev (cteMDBNode cte) = 0" by fact+ moreover from c' have "c' \<noteq> 0" using assms by auto ultimately show False by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> a \<rightarrow> b
m b = Some cte
mdbPrev (cteMDBNode cte) = 0

goal (1 subgoal):
 1. False proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m \<turnstile> a \<leadsto> c
c \<noteq> 0
m \<turnstile> a parentOf c
m c = Some cte
mdbPrev (cteMDBNode cte) = 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> a \<leadsto> c proof (state)
this:
m \<turnstile> a \<leadsto> c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m \<turnstile> a \<leadsto> c proof (prove)
using this:
m \<turnstile> a \<leadsto> c

goal (1 subgoal):
 1. (\<And>cte'. \<lbrakk>m a = Some cte'; mdbNext (cteMDBNode cte') = c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m a = Some cte'
mdbNext (cteMDBNode cte') = c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m a = Some cte'
mdbNext (cteMDBNode cte') = c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m c = Some cte proof (state)
this:
m c = Some cte

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m c = Some cte

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 proof (state)
this:
c \<noteq> 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m a = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0 proof (prove)
using this:
m a = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = a proof (prove)
using this:
m a = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0
valid_dlist m

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = a proof (state)
this:
mdbPrev (cteMDBNode cte) = a

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
mdbPrev (cteMDBNode cte) = a

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = 0 proof (state)
this:
mdbPrev (cteMDBNode cte) = 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
mdbPrev (cteMDBNode cte) = 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m a = Some cte' proof (prove)
using this:
m a = Some cte'

goal (1 subgoal):
 1. a \<noteq> 0 proof (prove)
using this:
m a = Some cte'
m \<turnstile> a \<rightarrow> b
m b = Some cte
mdbPrev (cteMDBNode cte) = 0
valid_dlist m
no_0 m

goal (1 subgoal):
 1. a \<noteq> 0 proof (state)
this:
a \<noteq> 0

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> a \<leadsto> c'; c' \<noteq> 0; m \<turnstile> a parentOf c'; m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
mdbPrev (cteMDBNode cte) = a
mdbPrev (cteMDBNode cte) = 0
a \<noteq> 0 proof (prove)
using this:
mdbPrev (cteMDBNode cte) = a
mdbPrev (cteMDBNode cte) = 0
a \<noteq> 0

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m \<turnstile> a \<rightarrow> c'
\<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
m \<turnstile> c' \<leadsto> c
c \<noteq> 0
m \<turnstile> a parentOf c
m c = Some cte
mdbPrev (cteMDBNode cte) = 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> c' \<leadsto> c proof (state)
this:
m \<turnstile> c' \<leadsto> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m \<turnstile> c' \<leadsto> c proof (prove)
using this:
m \<turnstile> c' \<leadsto> c

goal (1 subgoal):
 1. (\<And>cte'. \<lbrakk>m c' = Some cte'; mdbNext (cteMDBNode cte') = c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m c' = Some cte'
mdbNext (cteMDBNode cte') = c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m c' = Some cte'
mdbNext (cteMDBNode cte') = c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m c = Some cte proof (state)
this:
m c = Some cte

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
m c = Some cte

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m c' = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0 proof (prove)
using this:
m c' = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = c' proof (prove)
using this:
m c' = Some cte'
mdbNext (cteMDBNode cte') = c
m c = Some cte
c \<noteq> 0
valid_dlist m

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = c' proof (state)
this:
mdbPrev (cteMDBNode cte) = c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
mdbPrev (cteMDBNode cte) = c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = 0 proof (state)
this:
mdbPrev (cteMDBNode cte) = 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (state)
this:
mdbPrev (cteMDBNode cte) = 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
m c' = Some cte' proof (prove)
using this:
m c' = Some cte'

goal (1 subgoal):
 1. c' \<noteq> 0 proof (prove)
using this:
m c' = Some cte'
m \<turnstile> a \<rightarrow> b
m b = Some cte
mdbPrev (cteMDBNode cte) = 0
valid_dlist m
no_0 m

goal (1 subgoal):
 1. c' \<noteq> 0 proof (state)
this:
c' \<noteq> 0

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> a \<rightarrow> c'; \<lbrakk>m c' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> a parentOf c''; m c'' = Some cte; mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
mdbPrev (cteMDBNode cte) = c'
mdbPrev (cteMDBNode cte) = 0
c' \<noteq> 0 proof (prove)
using this:
mdbPrev (cteMDBNode cte) = c'
mdbPrev (cteMDBNode cte) = 0
c' \<noteq> 0

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!