[STATEMENT]
lemma cc_SDG_path_Append:
  "\<lbrakk>n'' cc-ns'\<rightarrow>\<^sub>d* n'; n cc-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n cc-ns@ns'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' cc-ns'\<rightarrow>\<^sub>d* n'; n cc-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n cc-ns @ ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:call_cdep_SDG_path.induct,
   auto intro:call_cdep_SDG_path.intros simp:append_assoc[THEN sym]
                                        simp del:append_assoc)


[STATEMENT]
lemma cdep_SDG_path_cc_SDG_path:
  "n cd-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n cc-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n cd-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n cc-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:cdep_SDG_path.induct,auto intro:call_cdep_SDG_path.intros)