[STATEMENT]
lemma DynPDG_ddep_edge_only_first_edge:
  "\<lbrakk>n -{V}a#as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a#as)) s\<rbrakk> \<Longrightarrow> 
    state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -{V}a # as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -{V}a # as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(erule DynPDG_edge.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na n'a asa. \<lbrakk>preds (kinds (a # as)) s; n = na; Some V = None; a # as = asa; n' = n'a; na controls n'a via asa\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
 2. \<And>na Va n'a asa. \<lbrakk>preds (kinds (a # as)) s; n = na; Some V = Some Va; a # as = asa; n' = n'a; na influences Va in n'a via asa\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(frule dyn_influence_Cons_source)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as; sourcenode a = n\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(frule dyn_influence_source_notin_tl_edges)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as; sourcenode a = n; n \<notin> set (sourcenodes as)\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
by(erule dyn_influence_only_first_edge)