[STATEMENT]
lemma Step_determ:
 "\<lbrakk>(M,l,s,n,l1,t) \<in> Step; (M,l,s,m,l2,r):Step\<rbrakk> \<Longrightarrow> n=m \<and> t=r \<and> l1=l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, t) \<in> Step; (M, l, s, m, l2, r) \<in> Step\<rbrakk> \<Longrightarrow> n = m \<and> t = r \<and> l1 = l2
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, t) \<in> Step; (M, l, s, m, l2, r) \<in> Step\<rbrakk> \<Longrightarrow> n = m \<and> t = r \<and> l1 = l2
[PROOF STEP]
apply (insert StepExec_determ_Aux[of n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, t) \<in> Step; (M, l, s, m, l2, r) \<in> Step; (\<forall>n1 l M s l1 t. n1 \<le> n \<longrightarrow> (M, l, s, n1, l1, t) \<in> Step \<longrightarrow> (\<forall>n2 l2 r. (M, l, s, n2, l2, r) \<in> Step \<longrightarrow> n1 = n2 \<and> t = r \<and> l1 = l2)) \<and> (\<forall>n1 l M s h v. n1 \<le> n \<longrightarrow> (M, l, s, n1, h, v) \<in> Exec \<longrightarrow> (\<forall>n2 k w. (M, l, s, n2, k, w) \<in> Exec \<longrightarrow> n1 = n2 \<and> h = k \<and> v = w))\<rbrakk> \<Longrightarrow> n = m \<and> t = r \<and> l1 = l2
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, t) \<in> Step; (M, l, s, m, l2, r) \<in> Step; \<forall>n1 l M s l1 t. n1 \<le> n \<longrightarrow> (M, l, s, n1, l1, t) \<in> Step \<longrightarrow> (\<forall>n2 l2 r. (M, l, s, n2, l2, r) \<in> Step \<longrightarrow> n1 = n2 \<and> t = r \<and> l1 = l2); \<forall>n1 l M s h v. n1 \<le> n \<longrightarrow> (M, l, s, n1, h, v) \<in> Exec \<longrightarrow> (\<forall>n2 k w. (M, l, s, n2, k, w) \<in> Exec \<longrightarrow> n1 = n2 \<and> h = k \<and> v = w)\<rbrakk> \<Longrightarrow> n = m \<and> t = r \<and> l1 = l2
[PROOF STEP]
apply (rotate_tac -1, erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, l1, t) \<in> Step; (M, l, s, m, l2, r) \<in> Step; \<forall>n1 l M s l1 t. n1 \<le> n \<longrightarrow> (M, l, s, n1, l1, t) \<in> Step \<longrightarrow> (\<forall>n2 l2 r. (M, l, s, n2, l2, r) \<in> Step \<longrightarrow> n1 = n2 \<and> t = r \<and> l1 = l2)\<rbrakk> \<Longrightarrow> n = m \<and> t = r \<and> l1 = l2
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Exec_determ:
 "\<lbrakk>(M,l,s,n,h,v) \<in> Exec; (M,l,s,m,k,w):Exec\<rbrakk> \<Longrightarrow> n=m \<and> h=k \<and> v=w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, h, v) \<in> Exec; (M, l, s, m, k, w) \<in> Exec\<rbrakk> \<Longrightarrow> n = m \<and> h = k \<and> v = w
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, h, v) \<in> Exec; (M, l, s, m, k, w) \<in> Exec\<rbrakk> \<Longrightarrow> n = m \<and> h = k \<and> v = w
[PROOF STEP]
apply (insert StepExec_determ_Aux[of n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, h, v) \<in> Exec; (M, l, s, m, k, w) \<in> Exec; (\<forall>n1 l M s l1 t. n1 \<le> n \<longrightarrow> (M, l, s, n1, l1, t) \<in> Step \<longrightarrow> (\<forall>n2 l2 r. (M, l, s, n2, l2, r) \<in> Step \<longrightarrow> n1 = n2 \<and> t = r \<and> l1 = l2)) \<and> (\<forall>n1 l M s h v. n1 \<le> n \<longrightarrow> (M, l, s, n1, h, v) \<in> Exec \<longrightarrow> (\<forall>n2 k w. (M, l, s, n2, k, w) \<in> Exec \<longrightarrow> n1 = n2 \<and> h = k \<and> v = w))\<rbrakk> \<Longrightarrow> n = m \<and> h = k \<and> v = w
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(M, l, s, n, h, v) \<in> Exec; (M, l, s, m, k, w) \<in> Exec; \<forall>n1 l M s l1 t. n1 \<le> n \<longrightarrow> (M, l, s, n1, l1, t) \<in> Step \<longrightarrow> (\<forall>n2 l2 r. (M, l, s, n2, l2, r) \<in> Step \<longrightarrow> n1 = n2 \<and> t = r \<and> l1 = l2); \<forall>n1 l M s h v. n1 \<le> n \<longrightarrow> (M, l, s, n1, h, v) \<in> Exec \<longrightarrow> (\<forall>n2 k w. (M, l, s, n2, k, w) \<in> Exec \<longrightarrow> n1 = n2 \<and> h = k \<and> v = w)\<rbrakk> \<Longrightarrow> n = m \<and> h = k \<and> v = w
[PROOF STEP]
apply (rotate_tac -2, erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n1 l M s h v. n1 \<le> n \<longrightarrow> (M, l, s, n1, h, v) \<in> Exec \<longrightarrow> (\<forall>n2 k w. (M, l, s, n2, k, w) \<in> Exec \<longrightarrow> n1 = n2 \<and> h = k \<and> v = w); (M, l, s, n, h, v) \<in> Exec; (M, l, s, m, k, w) \<in> Exec\<rbrakk> \<Longrightarrow> n = m \<and> h = k \<and> v = w
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_bhc_ga[autoref_ga_rules]:
  "\<lbrakk> GEN_ALGO_tag (is_bounded_hashcode R eq1 bhc1);
     GEN_ALGO_tag (is_bounded_hashcode S eq2 bhc2)\<rbrakk>
  \<Longrightarrow> is_bounded_hashcode (R\<times>\<^sub>rS) (prod_eq eq1 eq2) (prod_bhc bhc1 bhc2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GEN_ALGO_tag (is_bounded_hashcode R eq1 bhc1); GEN_ALGO_tag (is_bounded_hashcode S eq2 bhc2)\<rbrakk> \<Longrightarrow> is_bounded_hashcode (R \<times>\<^sub>r S) (prod_eq eq1 eq2) (prod_bhc bhc1 bhc2)
[PROOF STEP]
unfolding is_bounded_hashcode_def prod_bhc_def prod_eq_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n))\<rbrakk> \<Longrightarrow> (\<lambda>x1 x2. case x1 of (a1, b1) \<Rightarrow> case x2 of (a2, b2) \<Rightarrow> eq1 a1 a2 \<and> eq2 b1 b2, (=)) \<in> R \<times>\<^sub>r S \<rightarrow> R \<times>\<^sub>r S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain (R \<times>\<^sub>r S). \<forall>y\<in>Domain (R \<times>\<^sub>r S). (case x of (a1, b1) \<Rightarrow> case y of (a2, b2) \<Rightarrow> eq1 a1 a2 \<and> eq2 b1 b2) \<longrightarrow> (case x of (a, b) \<Rightarrow> (bhc1 n a * 33 + bhc2 n b) mod n) = (case y of (a, b) \<Rightarrow> (bhc1 n a * 33 + bhc2 n b) mod n)) \<and> (\<forall>n x. 1 < n \<longrightarrow> (case x of (a, b) \<Rightarrow> (bhc1 n a * 33 + bhc2 n b) mod n) < n)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); ((a, b), aa, ba) \<in> R \<times>\<^sub>r S; ((ab, bb), ac, bc) \<in> R \<times>\<^sub>r S; eq1 a ab; eq2 b bb\<rbrakk> \<Longrightarrow> aa = ac
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); ((a, b), aa, ba) \<in> R \<times>\<^sub>r S; ((ab, bb), ac, bc) \<in> R \<times>\<^sub>r S; eq1 a ab; eq2 b bb\<rbrakk> \<Longrightarrow> ba = bc
 3. \<And>a b aa ba ab bb ac bc. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); ((a, b), ac, bc) \<in> R \<times>\<^sub>r S; ((ab, bb), ac, bc) \<in> R \<times>\<^sub>r S\<rbrakk> \<Longrightarrow> eq1 a ab
 4. \<And>a b aa ba ab bb ac bc. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); ((a, b), ac, bc) \<in> R \<times>\<^sub>r S; ((ab, bb), ac, bc) \<in> R \<times>\<^sub>r S\<rbrakk> \<Longrightarrow> eq2 b bb
 5. \<And>n a b aa ba bb bc bd be. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); (a, bb) \<in> R; (b, bc) \<in> S; (aa, bd) \<in> R; (ba, be) \<in> S; eq1 a aa; eq2 b ba\<rbrakk> \<Longrightarrow> (bhc1 n a * 33 + bhc2 n b) mod n = (bhc1 n aa * 33 + bhc2 n ba) mod n
 6. \<And>n a b. \<lbrakk>GEN_ALGO_tag ((eq1, (=)) \<in> R \<rightarrow> R \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain R. \<forall>y\<in>Domain R. eq1 x y \<longrightarrow> bhc1 n x = bhc1 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc1 n x < n)); GEN_ALGO_tag ((eq2, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel \<and> (\<forall>n. \<forall>x\<in>Domain S. \<forall>y\<in>Domain S. eq2 x y \<longrightarrow> bhc2 n x = bhc2 n y) \<and> (\<forall>n x. 1 < n \<longrightarrow> bhc2 n x < n)); 1 < n\<rbrakk> \<Longrightarrow> (bhc1 n a * 33 + bhc2 n b) mod n < n
[PROOF STEP]
apply (auto dest: fun_relD simp: Domain_unfold; metis)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_dhs_ga[autoref_ga_rules]:
  "\<lbrakk> GEN_ALGO_tag (is_valid_def_hm_size TYPE('a) n1);
     GEN_ALGO_tag (is_valid_def_hm_size TYPE('b) n2) \<rbrakk>
   \<Longrightarrow> is_valid_def_hm_size TYPE('a*'b) (n1+n2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GEN_ALGO_tag (is_valid_def_hm_size TYPE('a) n1); GEN_ALGO_tag (is_valid_def_hm_size TYPE('b) n2)\<rbrakk> \<Longrightarrow> is_valid_def_hm_size TYPE('a \<times> 'b) (n1 + n2)
[PROOF STEP]
unfolding is_valid_def_hm_size_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GEN_ALGO_tag (1 < n1); GEN_ALGO_tag (1 < n2)\<rbrakk> \<Longrightarrow> 1 < n1 + n2
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]: "valid_edge a \<Longrightarrow> valid_node (sourcenode a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge a \<Longrightarrow> valid_node (sourcenode a)
[PROOF STEP]
by(fastforce simp:valid_node_def)


[STATEMENT]
lemma [simp]: "valid_edge a \<Longrightarrow> valid_node (targetnode a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge a \<Longrightarrow> valid_node (targetnode a)
[PROOF STEP]
by(fastforce simp:valid_node_def)


[STATEMENT]
lemma path_valid_node:
  assumes "n -as\<rightarrow>* n'" shows "valid_node n" and "valid_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_node n &&& valid_node n'
[PROOF STEP]
using \<open>n -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'

goal (1 subgoal):
 1. valid_node n &&& valid_node n'
[PROOF STEP]
by(induct rule:path.induct,auto)


[STATEMENT]
lemma empty_path_nodes [dest]:"n -[]\<rightarrow>* n' \<Longrightarrow> n = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -[]\<rightarrow>* n' \<Longrightarrow> n = n'
[PROOF STEP]
by(fastforce elim:path.cases)


[STATEMENT]
lemma path_valid_edges:"n -as\<rightarrow>* n' \<Longrightarrow> \<forall>a \<in> set as. valid_edge a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>* n' \<Longrightarrow> \<forall>a\<in>set as. valid_edge a
[PROOF STEP]
by(induct rule:path.induct) auto


[STATEMENT]
lemma path_edge:"valid_edge a \<Longrightarrow> sourcenode a -[a]\<rightarrow>* targetnode a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge a \<Longrightarrow> sourcenode a -[a]\<rightarrow>* targetnode a
[PROOF STEP]
by(fastforce intro:Cons_path empty_path)


[STATEMENT]
lemma path_Entry_target [dest]:
  assumes "n -as\<rightarrow>* (_Entry_)"
  shows "n = (_Entry_)" and "as = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = (_Entry_) &&& as = []
[PROOF STEP]
using \<open>n -as\<rightarrow>* (_Entry_)\<close>
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* (_Entry_)

goal (1 subgoal):
 1. n = (_Entry_) &&& as = []
[PROOF STEP]
proof(induct n as n'\<equiv>"(_Entry_)" rule:path.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
case (Cons_path n'' as a n)
[PROOF STATE]
proof (state)
this:
n'' -as\<rightarrow>* (_Entry_)
n'' = (_Entry_)
as = []
valid_edge a
sourcenode a = n
targetnode a = n''

goal (4 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
from \<open>targetnode a = n''\<close> \<open>valid_edge a\<close> \<open>n'' = (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = n''
valid_edge a
n'' = (_Entry_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
targetnode a = n''
valid_edge a
n'' = (_Entry_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(rule Entry_target,simp_all)
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
with \<open>False\<close>
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. n = (_Entry_)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (3 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
 3. \<And>n'' as a n. \<lbrakk>n'' -as\<rightarrow>* (_Entry_); n'' = (_Entry_); as = []; valid_edge a; sourcenode a = n; targetnode a = n''\<rbrakk> \<Longrightarrow> a # as = []
[PROOF STEP]
with \<open>False\<close>
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. a # as = []
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
a # as = []

goal (2 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
a # as = []

goal (2 subgoals):
 1. valid_node (_Entry_) \<Longrightarrow> (_Entry_) = (_Entry_)
 2. valid_node (_Entry_) \<Longrightarrow> [] = []
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma path_Append:"\<lbrakk>n -as\<rightarrow>* n''; n'' -as'\<rightarrow>* n'\<rbrakk>
  \<Longrightarrow> n -as@as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n''; n'' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
by(induct rule:path.induct,auto intro:Cons_path)


[STATEMENT]
lemma path_split:
  assumes "n -as@a#as'\<rightarrow>* n'"
  shows "n -as\<rightarrow>* sourcenode a" and "valid_edge a" and "targetnode a -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>* sourcenode a &&& valid_edge a &&& targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
using \<open>n -as@a#as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (prove)
using this:
n -as @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* sourcenode a &&& valid_edge a &&& targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
proof(induct as arbitrary:n)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> n -[]\<rightarrow>* sourcenode a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 3. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 6. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> n -[]\<rightarrow>* sourcenode a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 3. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 6. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
n -[] @ a # as'\<rightarrow>* n'

goal (6 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> n -[]\<rightarrow>* sourcenode a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 3. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 6. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[] @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. n -[]\<rightarrow>* sourcenode a
[PROOF STEP]
by(fastforce elim:path.cases intro:empty_path)
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* sourcenode a

goal (5 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
n -[] @ a # as'\<rightarrow>* n'

goal (5 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
 2. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 5. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[] @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. valid_edge a
[PROOF STEP]
by(fastforce elim:path.cases intro:path_edge)
[PROOF STATE]
proof (state)
this:
valid_edge a

goal (4 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
n -[] @ a # as'\<rightarrow>* n'

goal (4 subgoals):
 1. \<And>n. n -[] @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 4. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[] @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
by(fastforce elim:path.cases)
[PROOF STATE]
proof (state)
this:
targetnode a -as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case (Cons ax asx)
[PROOF STATE]
proof (state)
this:
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> ?n -asx\<rightarrow>* sourcenode a
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
note IH1 = \<open>\<And>n. n -asx@a#as'\<rightarrow>* n' \<Longrightarrow> n -asx\<rightarrow>* sourcenode a\<close>
[PROOF STATE]
proof (state)
this:
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> ?n -asx\<rightarrow>* sourcenode a

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
note IH2 = \<open>\<And>n. n -asx@a#as'\<rightarrow>* n' \<Longrightarrow> valid_edge a\<close>
[PROOF STATE]
proof (state)
this:
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
note IH3 = \<open>\<And>n. n -asx@a#as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (state)
this:
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?n -asx @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
hence "sourcenode ax = n" and "targetnode ax -asx@a#as'\<rightarrow>* n'" and "valid_edge ax"
[PROOF STATE]
proof (prove)
using this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. sourcenode ax = n &&& targetnode ax -asx @ a # as'\<rightarrow>* n' &&& valid_edge ax
[PROOF STEP]
by(auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
sourcenode ax = n
targetnode ax -asx @ a # as'\<rightarrow>* n'
valid_edge ax

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
from IH1[OF \<open> targetnode ax -asx@a#as'\<rightarrow>* n'\<close>]
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx\<rightarrow>* sourcenode a
[PROOF STEP]
have "targetnode ax -asx\<rightarrow>* sourcenode a"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx\<rightarrow>* sourcenode a

goal (1 subgoal):
 1. targetnode ax -asx\<rightarrow>* sourcenode a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
targetnode ax -asx\<rightarrow>* sourcenode a

goal (3 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> n -aa # as\<rightarrow>* sourcenode a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 3. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
with \<open>sourcenode ax = n\<close> \<open>valid_edge ax\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax = n
valid_edge ax
targetnode ax -asx\<rightarrow>* sourcenode a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode ax = n
valid_edge ax
targetnode ax -asx\<rightarrow>* sourcenode a

goal (1 subgoal):
 1. n -ax # asx\<rightarrow>* sourcenode a
[PROOF STEP]
by(fastforce intro:Cons_path)
[PROOF STATE]
proof (state)
this:
n -ax # asx\<rightarrow>* sourcenode a

goal (2 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (2 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
hence "targetnode ax -asx@a#as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. targetnode ax -asx @ a # as'\<rightarrow>* n'
[PROOF STEP]
by(auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
targetnode ax -asx @ a # as'\<rightarrow>* n'

goal (2 subgoals):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> valid_edge a
 2. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
from IH2[OF this]
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_edge a

goal (1 subgoal):
 1. valid_edge a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
valid_edge a

goal (1 subgoal):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
hence "targetnode ax -asx@a#as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -(ax # asx) @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. targetnode ax -asx @ a # as'\<rightarrow>* n'
[PROOF STEP]
by(auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
targetnode ax -asx @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>aa as n. \<lbrakk>\<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> n -as\<rightarrow>* sourcenode a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> valid_edge a; \<And>n. n -as @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'; n -(aa # as) @ a # as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
from IH3[OF this]
[PROOF STATE]
proof (chain)
picking this:
targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
targetnode a -as'\<rightarrow>* n'

goal (1 subgoal):
 1. targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
targetnode a -as'\<rightarrow>* n'

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?na2 -(ax # asx) @ a # as'\<rightarrow>* n' \<Longrightarrow> targetnode a -as'\<rightarrow>* n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_split_Cons:
  assumes "n -as\<rightarrow>* n'" and "as \<noteq> []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
obtain a' as' where "as = a'#as'"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

goal (1 subgoal):
 1. (\<And>a' as'. as = a' # as' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases as) auto
[PROOF STATE]
proof (state)
this:
as = a' # as'

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = a' # as'
[PROOF STEP]
have "n -[]@a'#as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = a' # as'

goal (1 subgoal):
 1. n -[] @ a' # as'\<rightarrow>* n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n -[] @ a' # as'\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "n -[]\<rightarrow>* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -[] @ a' # as'\<rightarrow>* n'

goal (1 subgoal):
 1. n -[]\<rightarrow>* sourcenode a' &&& valid_edge a' &&& targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
by(rule path_split)+
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* sourcenode a'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>n -[]\<rightarrow>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -[]\<rightarrow>* sourcenode a'
[PROOF STEP]
have "n = sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
n -[]\<rightarrow>* sourcenode a'

goal (1 subgoal):
 1. n = sourcenode a'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
n = sourcenode a'

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; n = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>as = a'#as'\<close> \<open>valid_edge a'\<close> \<open>targetnode a' -as'\<rightarrow>* n'\<close> that
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'
\<lbrakk>as = ?a' # ?as'; n = sourcenode ?a'; valid_edge ?a'; targetnode ?a' -?as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis
n = sourcenode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'
\<lbrakk>as = ?a' # ?as'; n = sourcenode ?a'; valid_edge ?a'; targetnode ?a' -?as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis
n = sourcenode a'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_split_snoc:
  assumes "n -as\<rightarrow>* n'" and "as \<noteq> []"
  obtains a' as' where "as = as'@[a']" and "n -as'\<rightarrow>* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
obtain a' as' where "as = as'@[a']"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

goal (1 subgoal):
 1. (\<And>as' a'. as = as' @ [a'] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases as rule:rev_cases) auto
[PROOF STATE]
proof (state)
this:
as = as' @ [a']

goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = as' @ [a']
[PROOF STEP]
have "n -as'@a'#[]\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = as' @ [a']

goal (1 subgoal):
 1. n -as' @ [a']\<rightarrow>* n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n -as' @ [a']\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "n -as'\<rightarrow>* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as' @ [a']\<rightarrow>* n'

goal (1 subgoal):
 1. n -as'\<rightarrow>* sourcenode a' &&& valid_edge a' &&& targetnode a' -[]\<rightarrow>* n'
[PROOF STEP]
by(rule path_split)+
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>* sourcenode a'
valid_edge a'
targetnode a' -[]\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>targetnode a' -[]\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' -[]\<rightarrow>* n'
[PROOF STEP]
have "n' = targetnode a'"
[PROOF STATE]
proof (prove)
using this:
targetnode a' -[]\<rightarrow>* n'

goal (1 subgoal):
 1. n' = targetnode a'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
n' = targetnode a'

goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* sourcenode a'; valid_edge a'; n' = targetnode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>as = as'@[a']\<close> \<open>valid_edge a'\<close> \<open>n -as'\<rightarrow>* sourcenode a'\<close> that
[PROOF STATE]
proof (chain)
picking this:
as = as' @ [a']
valid_edge a'
n -as'\<rightarrow>* sourcenode a'
\<lbrakk>as = ?as' @ [?a']; n -?as'\<rightarrow>* sourcenode ?a'; valid_edge ?a'; n' = targetnode ?a'\<rbrakk> \<Longrightarrow> thesis
n' = targetnode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ [a']
valid_edge a'
n -as'\<rightarrow>* sourcenode a'
\<lbrakk>as = ?as' @ [?a']; n -?as'\<rightarrow>* sourcenode ?a'; valid_edge ?a'; n' = targetnode ?a'\<rbrakk> \<Longrightarrow> thesis
n' = targetnode a'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_split_second:
  assumes "n -as@a#as'\<rightarrow>* n'" shows "sourcenode a -a#as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sourcenode a -a # as'\<rightarrow>* n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sourcenode a -a # as'\<rightarrow>* n'
[PROOF STEP]
from \<open>n -as@a#as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as @ a # as'\<rightarrow>* n'
[PROOF STEP]
have "valid_edge a" and "targetnode a -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as @ a # as'\<rightarrow>* n'

goal (1 subgoal):
 1. valid_edge a &&& targetnode a -as'\<rightarrow>* n'
[PROOF STEP]
by(auto intro:path_split)
[PROOF STATE]
proof (state)
this:
valid_edge a
targetnode a -as'\<rightarrow>* n'

goal (1 subgoal):
 1. sourcenode a -a # as'\<rightarrow>* n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge a
targetnode a -as'\<rightarrow>* n'

goal (1 subgoal):
 1. sourcenode a -a # as'\<rightarrow>* n'
[PROOF STEP]
by(fastforce intro:Cons_path)
[PROOF STATE]
proof (state)
this:
sourcenode a -a # as'\<rightarrow>* n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_Entry_Cons:
  assumes "(_Entry_) -as\<rightarrow>* n'" and "n' \<noteq> (_Entry_)"
  obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
  and "n -tl as\<rightarrow>* n'" and "valid_edge a" and "a = hd as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a n. \<lbrakk>sourcenode a = (_Entry_); targetnode a = n; n -tl as\<rightarrow>* n'; valid_edge a; a = hd as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a n. \<lbrakk>sourcenode a = (_Entry_); targetnode a = n; n -tl as\<rightarrow>* n'; valid_edge a; a = hd as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>(_Entry_) -as\<rightarrow>* n'\<close> \<open>n' \<noteq> (_Entry_)\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>* n'
n' \<noteq> (_Entry_)
[PROOF STEP]
have "as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>* n'
n' \<noteq> (_Entry_)

goal (1 subgoal):
 1. as \<noteq> []
[PROOF STEP]
by(cases as,auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
as \<noteq> []

goal (1 subgoal):
 1. (\<And>a n. \<lbrakk>sourcenode a = (_Entry_); targetnode a = n; n -tl as\<rightarrow>* n'; valid_edge a; a = hd as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>(_Entry_) -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) -as\<rightarrow>* n'
as \<noteq> []
[PROOF STEP]
obtain a' as' where "as = a'#as'"
    and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) -as\<rightarrow>* n'
as \<noteq> []

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; (_Entry_) = sourcenode a'; valid_edge a'; targetnode a' -as'\<rightarrow>* n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule path_split_Cons)
[PROOF STATE]
proof (state)
this:
as = a' # as'
(_Entry_) = sourcenode a'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>a n. \<lbrakk>sourcenode a = (_Entry_); targetnode a = n; n -tl as\<rightarrow>* n'; valid_edge a; a = hd as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>sourcenode ?a = (_Entry_); targetnode ?a = ?n; ?n -tl as\<rightarrow>* n'; valid_edge ?a; ?a = hd as\<rbrakk> \<Longrightarrow> thesis
as = a' # as'
(_Entry_) = sourcenode a'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sourcenode ?a = (_Entry_); targetnode ?a = ?n; ?n -tl as\<rightarrow>* n'; valid_edge ?a; ?a = hd as\<rbrakk> \<Longrightarrow> thesis
as = a' # as'
(_Entry_) = sourcenode a'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_det:
  "\<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
proof(induct as arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n -[]\<rightarrow>* n'; n -[]\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
 2. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* n'
n -[]\<rightarrow>* n''

goal (2 subgoals):
 1. \<And>n. \<lbrakk>n -[]\<rightarrow>* n'; n -[]\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
 2. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[]\<rightarrow>* n'
n -[]\<rightarrow>* n''

goal (1 subgoal):
 1. n' = n''
[PROOF STEP]
by(auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
n' = n''

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
case (Cons a' as')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -as'\<rightarrow>* n'; ?n -as'\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
n -a' # as'\<rightarrow>* n'
n -a' # as'\<rightarrow>* n''

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
note IH = \<open>\<And>n. \<lbrakk>n -as'\<rightarrow>* n'; n -as'\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -as'\<rightarrow>* n'; ?n -as'\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
from \<open>n -a'#as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a' # as'\<rightarrow>* n'
[PROOF STEP]
have "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -a' # as'\<rightarrow>* n'

goal (1 subgoal):
 1. targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
by(fastforce elim:path_split_Cons)
[PROOF STATE]
proof (state)
this:
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
from \<open>n -a'#as'\<rightarrow>* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a' # as'\<rightarrow>* n''
[PROOF STEP]
have "targetnode a' -as'\<rightarrow>* n''"
[PROOF STATE]
proof (prove)
using this:
n -a' # as'\<rightarrow>* n''

goal (1 subgoal):
 1. targetnode a' -as'\<rightarrow>* n''
[PROOF STEP]
by(fastforce elim:path_split_Cons)
[PROOF STATE]
proof (state)
this:
targetnode a' -as'\<rightarrow>* n''

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; n -as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''; n -a # as\<rightarrow>* n'; n -a # as\<rightarrow>* n''\<rbrakk> \<Longrightarrow> n' = n''
[PROOF STEP]
from IH[OF \<open>targetnode a' -as'\<rightarrow>* n'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
n' = n''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' = n''

goal (1 subgoal):
 1. n' = n''
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
n' = n''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_sourcenode:
  "\<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> hd (sourcenodes as) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> hd (sourcenodes as) = n
[PROOF STEP]
by(fastforce elim:path_split_Cons simp:sourcenodes_def)


[STATEMENT]
lemma path_targetnode:
  "\<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> last (targetnodes as) = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> last (targetnodes as) = n'
[PROOF STEP]
by(fastforce elim:path_split_snoc simp:targetnodes_def)


[STATEMENT]
lemma sourcenodes_is_n_Cons_butlast_targetnodes:
  "\<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow>
  sourcenodes as = n#(butlast (targetnodes as))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as)
[PROOF STEP]
proof(induct as arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n -[]\<rightarrow>* n'; [] \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes [] = n # butlast (targetnodes [])
 2. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* n'
[] \<noteq> []

goal (2 subgoals):
 1. \<And>n. \<lbrakk>n -[]\<rightarrow>* n'; [] \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes [] = n # butlast (targetnodes [])
 2. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[]\<rightarrow>* n'
[] \<noteq> []

goal (1 subgoal):
 1. sourcenodes [] = n # butlast (targetnodes [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sourcenodes [] = n # butlast (targetnodes [])

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
case (Cons a' as')
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -as'\<rightarrow>* n'; as' \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as' = ?n # butlast (targetnodes as')
n -a' # as'\<rightarrow>* n'
a' # as' \<noteq> []

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
note IH = \<open>\<And>n. \<lbrakk>n -as'\<rightarrow>* n'; as' \<noteq> []\<rbrakk>
            \<Longrightarrow> sourcenodes as' = n#(butlast (targetnodes as'))\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -as'\<rightarrow>* n'; as' \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as' = ?n # butlast (targetnodes as')

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
from \<open>n -a'#as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a' # as'\<rightarrow>* n'
[PROOF STEP]
have "n = sourcenode a'" and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -a' # as'\<rightarrow>* n'

goal (1 subgoal):
 1. n = sourcenode a' &&& targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
by(auto elim:path_split_Cons)
[PROOF STATE]
proof (state)
this:
n = sourcenode a'
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>a as n. \<lbrakk>\<And>n. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes as = n # butlast (targetnodes as); n -a # as\<rightarrow>* n'; a # as \<noteq> []\<rbrakk> \<Longrightarrow> sourcenodes (a # as) = n # butlast (targetnodes (a # as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
 2. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
 2. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
with \<open>targetnode a' -as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' -as'\<rightarrow>* n'
as' = []
[PROOF STEP]
have "targetnode a' = n'"
[PROOF STATE]
proof (prove)
using this:
targetnode a' -as'\<rightarrow>* n'
as' = []

goal (1 subgoal):
 1. targetnode a' = n'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
targetnode a' = n'

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
 2. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
with True \<open>n = sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = []
n = sourcenode a'
targetnode a' = n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as' = []
n = sourcenode a'
targetnode a' = n'

goal (1 subgoal):
 1. sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
by(simp add:sourcenodes_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
from IH[OF \<open>targetnode a' -as'\<rightarrow>* n'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as' = targetnode a' # butlast (targetnodes as')
[PROOF STEP]
have "sourcenodes as' = targetnode a' # butlast (targetnodes as')"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as' = targetnode a' # butlast (targetnodes as')

goal (1 subgoal):
 1. sourcenodes as' = targetnode a' # butlast (targetnodes as')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sourcenodes as' = targetnode a' # butlast (targetnodes as')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
with \<open>n = sourcenode a'\<close> False
[PROOF STATE]
proof (chain)
picking this:
n = sourcenode a'
as' \<noteq> []
sourcenodes as' = targetnode a' # butlast (targetnodes as')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = sourcenode a'
as' \<noteq> []
sourcenodes as' = targetnode a' # butlast (targetnodes as')

goal (1 subgoal):
 1. sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))
[PROOF STEP]
by(simp add:sourcenodes_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sourcenodes (a' # as') = n # butlast (targetnodes (a' # as'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma targetnodes_is_tl_sourcenodes_App_n':
  "\<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow>
    targetnodes as = (tl (sourcenodes as))@[n']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes as = tl (sourcenodes as) @ [n']
[PROOF STEP]
proof(induct as arbitrary:n' rule:rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>n -[]\<rightarrow>* n'; [] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes [] = tl (sourcenodes []) @ [n']
 2. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* n'
[] \<noteq> []

goal (2 subgoals):
 1. \<And>n'. \<lbrakk>n -[]\<rightarrow>* n'; [] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes [] = tl (sourcenodes []) @ [n']
 2. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n -[]\<rightarrow>* n'
[] \<noteq> []

goal (1 subgoal):
 1. targetnodes [] = tl (sourcenodes []) @ [n']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
targetnodes [] = tl (sourcenodes []) @ [n']

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
case (snoc a' as')
[PROOF STATE]
proof (state)
this:
\<lbrakk>n -as'\<rightarrow>* ?n'; as' \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes as' = tl (sourcenodes as') @ [?n']
n -as' @ [a']\<rightarrow>* n'
as' @ [a'] \<noteq> []

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
note IH = \<open>\<And>n'. \<lbrakk>n -as'\<rightarrow>* n'; as' \<noteq> []\<rbrakk>
    \<Longrightarrow> targetnodes as' = tl (sourcenodes as') @ [n']\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>n -as'\<rightarrow>* ?n'; as' \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes as' = tl (sourcenodes as') @ [?n']

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
from \<open>n -as'@[a']\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as' @ [a']\<rightarrow>* n'
[PROOF STEP]
have "n -as'\<rightarrow>* sourcenode a'" and "n' = targetnode a'"
[PROOF STATE]
proof (prove)
using this:
n -as' @ [a']\<rightarrow>* n'

goal (1 subgoal):
 1. n -as'\<rightarrow>* sourcenode a' &&& n' = targetnode a'
[PROOF STEP]
by(auto elim:path_split_snoc)
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>* sourcenode a'
n' = targetnode a'

goal (1 subgoal):
 1. \<And>x xs n'. \<lbrakk>\<And>n'. \<lbrakk>n -xs\<rightarrow>* n'; xs \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes xs = tl (sourcenodes xs) @ [n']; n -xs @ [x]\<rightarrow>* n'; xs @ [x] \<noteq> []\<rbrakk> \<Longrightarrow> targetnodes (xs @ [x]) = tl (sourcenodes (xs @ [x])) @ [n']
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
 2. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
 2. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
with \<open>n -as'\<rightarrow>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as'\<rightarrow>* sourcenode a'
as' = []
[PROOF STEP]
have "n = sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
n -as'\<rightarrow>* sourcenode a'
as' = []

goal (1 subgoal):
 1. n = sourcenode a'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
n = sourcenode a'

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
 2. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
with True \<open>n' = targetnode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = []
n' = targetnode a'
n = sourcenode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as' = []
n' = targetnode a'
n = sourcenode a'

goal (1 subgoal):
 1. targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
by(simp add:sourcenodes_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
from IH[OF \<open>n -as'\<rightarrow>* sourcenode a'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
targetnodes as' = tl (sourcenodes as') @ [sourcenode a']
[PROOF STEP]
have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']"
[PROOF STATE]
proof (prove)
using this:
targetnodes as' = tl (sourcenodes as') @ [sourcenode a']

goal (1 subgoal):
 1. targetnodes as' = tl (sourcenodes as') @ [sourcenode a']
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
targetnodes as' = tl (sourcenodes as') @ [sourcenode a']

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
with \<open>n' = targetnode a'\<close> False
[PROOF STATE]
proof (chain)
picking this:
n' = targetnode a'
as' \<noteq> []
targetnodes as' = tl (sourcenodes as') @ [sourcenode a']
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' = targetnode a'
as' \<noteq> []
targetnodes as' = tl (sourcenodes as') @ [sourcenode a']

goal (1 subgoal):
 1. targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']
[PROOF STEP]
by(simp add:sourcenodes_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
targetnodes (as' @ [a']) = tl (sourcenodes (as' @ [a'])) @ [n']

goal:
No subgoals!
[PROOF STEP]
qed