theory CSpace1_R

lemma parent_m:
  "m \<turnstile> p \<rightarrow> p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' \<and> (p' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest)" apply (cases "p=src", simp add: src_no_parent) apply (erule subtree.induct) apply (rule conjI) apply (rule direct_parent) apply (clarsimp simp: n_direct_eq) apply assumption apply (fastforce simp add: parentOf_def n src new_src_def) apply clarsimp apply (rule trans_parent [where c'=src]) apply (rule direct_parent) apply (simp add: n_direct_eq) apply (rule notI, simp) apply simp apply (simp add: parentOf_def n src new_src_def) apply (clarsimp simp: dest dest_cap) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def dest src n) apply (rule conjI, clarsimp simp: dest dest_cap) apply (clarsimp intro!: parent_preserved) apply clarsimp apply (case_tac "c'=src") apply simp apply (erule trans_parent [where c'=dest]) apply (clarsimp simp: n_direct_eq) apply clarsimp apply (fastforce simp: parentOf_def dest src n) apply clarsimp apply (rule conjI) apply (erule trans_parent) apply (simp add: n_direct_eq) apply clarsimp apply assumption apply (fastforce simp: parentOf_def dest src n new_src_def) apply clarsimp apply (rule trans_parent [where c'=src]) apply (erule trans_parent) apply (simp add: n_direct_eq) apply clarsimp apply simp apply (fastforce simp: parentOf_def dest src n new_src_def) apply (simp add: n_direct_eq) apply simp apply (fastforce simp: parentOf_def dest src n new_src_def
                  intro!: parent_preserved) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> p' \<Longrightarrow> n \<turnstile> p \<rightarrow> p' \<and> (p' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<rightarrow> p'; p \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> p' \<and> (p' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest)
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (5 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> c'
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 5. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' \<noteq> 0
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 4. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c'
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> src
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 5. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<leadsto> src
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 5. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 6. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 7. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> p \<noteq> dest
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 5. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 6. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 7. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 5. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 6. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 5. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; \<exists>cte'. m p = Some cte' \<and> isMDBParentOf cte' (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> p = dest \<longrightarrow> isMDBParentOf new_dest (CTE src_cap src_node)
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 4. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 5. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 3. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 4. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m \<turnstile> p parentOf src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m p = Some cte'; isMDBParentOf cte' (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> isMDBParentOf new_dest new_dest) \<and> (p \<noteq> dest \<longrightarrow> isMDBParentOf cte' new_dest)
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<leadsto> src; m p = Some cte'; isMDBParentOf cte' (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> isMDBParentOf cte' new_dest
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; n \<turnstile> p \<rightarrow> c' \<and> (c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest); m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest)
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; n \<turnstile> p \<rightarrow> dest; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> dest \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 4. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> src; m \<turnstile> src \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> src; c' = src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c'' \<and> (c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest) proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> c' \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 4. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (4 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' = dest \<longrightarrow> m \<turnstile> src \<leadsto> c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 4. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (3 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' \<noteq> 0
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 3. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf c''
 2. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> c'' = src \<longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> dest proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p \<rightarrow> src
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (6 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> c' \<leadsto> src
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 5. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 6. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (6 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> c' \<noteq> dest
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 5. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 6. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (5 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 5. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (4 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf src
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 4. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> src \<leadsto> dest
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 3. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>p \<noteq> src; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> src; m \<turnstile> p parentOf src; n \<turnstile> p \<rightarrow> c'; c' \<noteq> src\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf dest proof (prove)
goal:
No subgoals!