[STATEMENT]
lemma slice_intra_edges_no_nodes_in_slice:
  "\<lbrakk>slice_edges S cs as = []; \<forall>a \<in> set as. intra_kind (kind a);
    \<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk>
  \<Longrightarrow> \<forall>nx \<in> set(sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
proof(induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>slice_edges S cs [] = []; \<forall>a\<in>set []. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes []). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
slice_edges S cs [] = []
\<forall>a\<in>set []. intra_kind (kind a)
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<lbrakk>slice_edges S cs [] = []; \<forall>a\<in>set []. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes []). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs [] = []
\<forall>a\<in>set []. intra_kind (kind a)
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes []). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(fastforce simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes []). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case (Cons a' as')
[PROOF STATE]
proof (state)
this:
\<lbrakk>slice_edges S cs as' = []; \<forall>a\<in>set as'. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
slice_edges S cs (a' # as') = []
\<forall>a\<in>set (a' # as'). intra_kind (kind a)
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
note IH = \<open> \<lbrakk>slice_edges S cs as' = []; \<forall>a\<in>set as'. intra_kind (kind a);
    \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk>
    \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>slice_edges S cs as' = []; \<forall>a\<in>set as'. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>\<forall>a\<in>set (a' # as'). intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a' # as'). intra_kind (kind a)
[PROOF STEP]
have "intra_kind (kind a')" and "\<forall>a\<in>set as'. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a' # as'). intra_kind (kind a)

goal (1 subgoal):
 1. intra_kind (kind a') &&& \<forall>a\<in>set as'. intra_kind (kind a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
intra_kind (kind a')
\<forall>a\<in>set as'. intra_kind (kind a)

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>slice_edges S cs (a' # as') = []\<close> \<open>intra_kind (kind a')\<close>
    \<open>\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs (a' # as') = []
intra_kind (kind a')
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have "sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>" and "slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs (a' # as') = []
intra_kind (kind a')
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> &&& slice_edges S cs as' = []
[PROOF STEP]
by(cases "slice_edge S cs a'",auto simp:intra_kind_def slice_edge_def)+
[PROOF STATE]
proof (state)
this:
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
slice_edges S cs as' = []

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from IH[OF \<open>slice_edges S cs as' = []\<close> \<open>\<forall>a\<in>set as'. intra_kind (kind a)\<close>
    \<open>\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have "\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>\<lbrakk>slice_edges S cs as = []; \<forall>a\<in>set as. intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; slice_edges S cs (a # as) = []; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>nx\<in>set (sourcenodes (a # as)). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
with \<open>sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>nx\<in>set (sourcenodes as'). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes (a' # as')). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes (a' # as')). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed