theory CSpace_R

lemma dlist' [simp]:
  "valid_dlist n'" using src dest apply (unfold valid_dlist_def3 n_direct_eq' n'_prev_eq) apply (split if_split) apply (split if_split) apply (split if_split) apply (split if_split) apply (split if_split) apply (split if_split) apply (split if_split) apply simp apply (intro conjI impI allI notI) apply (fastforce simp: src_next_eq') apply (clarsimp simp: src_next_eq split: if_split_asm) apply (simp add: mdb_ptr_src.p_next) apply (erule (1) dlist_nextD0) apply clarsimp apply clarsimp apply clarsimp apply (erule (1) dlist_prevD0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist n' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. valid_dlist n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c') \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (\<forall>c c'. (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c') \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c') \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (\<forall>c c'. (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c') \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c') \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (\<forall>c c'. (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c') \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c') \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (\<forall>c c'. (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')))) \<and> (\<forall>c c'. (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = src then c' = dest else if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = mdbNext src_node \<and> c' \<noteq> 0 then c = dest else if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')))) \<and> (\<forall>c c'. (c = src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest)) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest))) \<and> (c \<noteq> src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest)) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest))) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))))) \<and> (\<forall>c c'. (c = src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest)) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest))) \<and> (c \<noteq> src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c')) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> (if c = dest then m \<turnstile> src \<leadsto> c' else m \<turnstile> c \<leadsto> c'))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest)) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> c = dest))) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> (c = dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> c' = dest \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c')) \<and> (c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> (if c' = dest then c = src else m \<turnstile> c \<leftarrow> c'))))) \<and> (\<forall>c c'. (c = dest \<longrightarrow> (c = src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest)) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest))) \<and> (c \<noteq> src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> c') \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> c')) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> c') \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> c')))) \<and> (c \<noteq> dest \<longrightarrow> (c = src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest)) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest) \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> c' = dest))) \<and> (c \<noteq> src \<longrightarrow> (c' = dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c') \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> c = src \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c')) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c = dest \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c') \<and> (\<not> (c' = mdbNext src_node \<and> c' \<noteq> 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c'))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> (\<forall>c c'. (c' = dest \<longrightarrow> dest = mdbNext src_node \<longrightarrow> c \<noteq> mdbNext src_node \<longrightarrow> c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> mdbNext src_node \<longrightarrow> mdbNext src_node = 0) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> c \<noteq> dest \<longrightarrow> c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> mdbNext src_node \<longrightarrow> mdbNext src_node = 0) \<and> ((c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0) \<longrightarrow> (c = dest \<longrightarrow> m \<turnstile> src \<leadsto> c' \<longrightarrow> c' = 0) \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src \<longrightarrow> m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leftarrow> c')))) \<and> (\<forall>c c'. (c = dest \<longrightarrow> (c' = dest \<longrightarrow> dest = mdbNext src_node \<longrightarrow> mdbNext src_node \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node) \<and> (c' \<noteq> dest \<longrightarrow> c' = mdbNext src_node \<and> c' \<noteq> 0 \<longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node)) \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src \<longrightarrow> (c' = dest \<longrightarrow> dest = mdbNext src_node \<longrightarrow> c = mdbNext src_node \<longrightarrow> mdbNext src_node = 0) \<and> (c' \<noteq> dest \<longrightarrow> (c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0) \<longrightarrow> m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c'))) proof (prove)
goal (8 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' = dest; dest = mdbNext src_node; c \<noteq> mdbNext src_node; c \<noteq> src; m \<turnstile> c \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c = dest; m \<turnstile> src \<leadsto> c'\<rbrakk> \<Longrightarrow> c' = 0
 4. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
 5. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' = dest; dest = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 6. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 7. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 8. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (7 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c = dest; m \<turnstile> src \<leadsto> c'\<rbrakk> \<Longrightarrow> c' = 0
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
 4. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' = dest; dest = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 5. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 6. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 7. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (6 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c = dest; m \<turnstile> src \<leadsto> c'\<rbrakk> \<Longrightarrow> c' = 0
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' = dest; dest = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 4. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 5. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 6. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (5 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; c \<noteq> dest; c \<noteq> src; m \<turnstile> c \<leadsto> c'; c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' = dest; dest = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 4. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 5. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (4 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' = dest; dest = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 4. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (3 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c = dest; c' \<noteq> dest; c' = mdbNext src_node \<and> c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> mdbNext src_node
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 3. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' = dest; dest = mdbNext src_node; c = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0
 2. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); c \<noteq> dest; c \<noteq> src; c' \<noteq> dest; c' = mdbNext src_node \<longrightarrow> mdbNext src_node = 0; m \<turnstile> c \<leftarrow> c'; c \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' proof (prove)
goal:
No subgoals!