[STATEMENT]
lemma observable_moves_singular_slice_edge:
  "\<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    \<forall>i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))\<rbrakk>
  \<Longrightarrow> slice_edges S cs as = [last as]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [last as]
[PROOF STEP]
proof(induct rule:observable_moves.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S f ms s as ms' s' a ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s''); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
case (observable_moves_snoc S f ms s as ms' s' a ms'' s'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s')
S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s'')
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' a ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s''); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s')\<close> \<open>tl ms = targetnodes rs\<close> \<open>length rs = length cs\<close>
    \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s')
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
obtain rs' where "slice_edges S cs as = []"
    and "tl ms' = targetnodes rs'" and "length rs' = length (upd_cs cs as)"
    and "\<forall>i<length (upd_cs cs as).
    call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s')
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))

goal (1 subgoal):
 1. (\<And>rs'. \<lbrakk>slice_edges S cs as = []; tl ms' = targetnodes rs'; length rs' = length (upd_cs cs as); \<forall>i<length (upd_cs cs as). call_of_return_node (tl ms' ! i) (sourcenode (upd_cs cs as ! i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:silent_moves_no_slice_edges)
[PROOF STATE]
proof (state)
this:
slice_edges S cs as = []
tl ms' = targetnodes rs'
length rs' = length (upd_cs cs as)
\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms' ! i) (sourcenode (upd_cs cs as ! i))

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' a ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s''); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
from \<open>S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s'')\<close> this
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s'')
slice_edges S cs as = []
tl ms' = targetnodes rs'
length rs' = length (upd_cs cs as)
\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms' ! i) (sourcenode (upd_cs cs as ! i))
[PROOF STEP]
have "slice_edge S (upd_cs cs as) a"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s'')
slice_edges S cs as = []
tl ms' = targetnodes rs'
length rs' = length (upd_cs cs as)
\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms' ! i) (sourcenode (upd_cs cs as ! i))

goal (1 subgoal):
 1. slice_edge S (upd_cs cs as) a
[PROOF STEP]
by -(rule observable_move_slice_edge)
[PROOF STATE]
proof (state)
this:
slice_edge S (upd_cs cs as) a

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' a ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s''); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
with \<open>slice_edges S cs as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = []
slice_edge S (upd_cs cs as) a
[PROOF STEP]
have "slice_edges S cs (as @ [a]) = []@[a]"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = []
slice_edge S (upd_cs cs as) a

goal (1 subgoal):
 1. slice_edges S cs (as @ [a]) = [] @ [a]
[PROOF STEP]
by(fastforce intro:slice_edges_Append)
[PROOF STATE]
proof (state)
this:
slice_edges S cs (as @ [a]) = [] @ [a]

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' a ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') -a\<rightarrow> (ms'',s''); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs (as @ [a]) = [] @ [a]

goal (1 subgoal):
 1. slice_edges S cs (as @ [a]) = [last (as @ [a])]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs (as @ [a]) = [last (as @ [a])]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma silent_moves_nonempty_nodestack_False:
  assumes "S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')" and "valid_node m"
  and "ms' \<noteq> []" and "CFG_node m' \<in> sum_SDG_slice1 nx" and "nx \<in> S"
  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from assms(1-4)
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
ms' \<noteq> []
CFG_node m' \<in> sum_SDG_slice1 nx
[PROOF STEP]
have "slice_edges S [] as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
ms' \<noteq> []
CFG_node m' \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> []
[PROOF STEP]
proof(induct ms' arbitrary:as m' s')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
case (Cons mx msx)
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,kind \<turnstile> ([m],[cf]) =?as\<Rightarrow>\<^sub>\<tau> (?m' # msx,?s'); valid_node m; msx \<noteq> []; CFG_node ?m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] ?as \<noteq> []
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
mx # msx \<noteq> []
CFG_node m' \<in> sum_SDG_slice1 nx

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
note IH = \<open>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # msx,s'); valid_node m;
      msx \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk>
      \<Longrightarrow> slice_edges S [] as \<noteq> []\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,kind \<turnstile> ([m],[cf]) =?as\<Rightarrow>\<^sub>\<tau> (?m' # msx,?s'); valid_node m; msx \<noteq> []; CFG_node ?m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] ?as \<noteq> []

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close> \<open>valid_node m\<close>
      \<open>CFG_node m' \<in> sum_SDG_slice1 nx\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
CFG_node m' \<in> sum_SDG_slice1 nx
[PROOF STEP]
obtain as' a as'' where "as = as'@a#as''" and "\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
      and "call_of_return_node mx (sourcenode a)"
      and "CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx"
      and "targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
CFG_node m' \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. (\<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node mx (sourcenode a); CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx; targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:silent_moves_called_node_in_slice1_hd_nodestack_in_slice1
      [of _ _ _ _ _ _ _ _ _ "[]" "[]"] simp:targetnodes_def valid_return_list_def)
[PROOF STATE]
proof (state)
this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node mx (sourcenode a)
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close> \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
as = as' @ a # as''
[PROOF STEP]
obtain xs x where "S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)"
      and "S,kind \<turnstile> (xs,x) =a#as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
as = as' @ a # as''

goal (1 subgoal):
 1. (\<And>xs x. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves_split)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> (xs,x) =a#as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
[PROOF STEP]
obtain ys y where "S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)"
      and "S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (1 subgoal):
 1. (\<And>ys y. \<lbrakk>S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)\<close> \<open>\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain xs' a' where "xs = sourcenode a#xs'"
      and "ys = targetnode a#targetnode a'#xs'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y); \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_move.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f aa s s' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; intra_kind (kind aa); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode aa; ms' = targetnode aa # tl ms\<rbrakk> \<Longrightarrow> thesis
 2. \<And>f aa s s' Q r p fs a' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; kind aa = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges aa; (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode aa; ms' = targetnode aa # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> thesis
 3. \<And>f aa s s' Q p f' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; kind aa = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode aa; hd (tl ms) = targetnode aa; ms' = tl ms\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:intra_kind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q r p fs a' m m'. \<lbrakk>\<And>xs' a'a. \<lbrakk>xs = sourcenode a # xs'; targetnode a' = targetnode a'a\<rbrakk> \<Longrightarrow> thesis; ys = targetnode a # targetnode a' # tl xs; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; Ball (set (tl xs)) return_node; length xs = length x; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x) = Suc (length x); hd xs = sourcenode a; y = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; m \<in> set (tl xs); call_of_return_node m m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>Q r p fs a'. \<lbrakk>\<And>xs' a'a. \<lbrakk>xs = sourcenode a # xs'; targetnode a' = targetnode a'a\<rbrakk> \<Longrightarrow> thesis; ys = targetnode a # targetnode a' # tl xs; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; Ball (set (tl xs)) return_node; length xs = length x; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x) = Suc (length x); hd xs = sourcenode a; y = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases xs,auto)+
[PROOF STATE]
proof (state)
this:
xs = sourcenode a # xs'
ys = targetnode a # targetnode a' # xs'

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close>
      \<open>ys = targetnode a#targetnode a'#xs'\<close> \<open>targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
ys = targetnode a # targetnode a' # xs'
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
have "mx = targetnode a'" and "xs' = msx"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
ys = targetnode a # targetnode a' # xs'
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (1 subgoal):
 1. mx = targetnode a' &&& xs' = msx
[PROOF STEP]
by(auto dest:silent_moves_same_level_path)
[PROOF STATE]
proof (state)
this:
mx = targetnode a'
xs' = msx

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
with \<open>xs = sourcenode a#xs'\<close> \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
xs = sourcenode a # xs'
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
mx = targetnode a'
xs' = msx
[PROOF STEP]
have "S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a#msx,x)"
[PROOF STATE]
proof (prove)
using this:
xs = sourcenode a # xs'
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
mx = targetnode a'
xs' = msx

goal (1 subgoal):
 1. S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []; S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; a # ms' \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice_edges S [] as \<noteq> []
[PROOF STEP]
proof(cases "msx = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
msx = []

goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a#msx,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)
[PROOF STEP]
obtain rs' where "msx = targetnodes rs' \<and> length rs' = length (upd_cs [] as')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)

goal (1 subgoal):
 1. (\<And>rs'. msx = targetnodes rs' \<and> length rs' = length (upd_cs [] as') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
                    simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
msx = targetnodes rs' \<and> length rs' = length (upd_cs [] as')

goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
msx = []
msx = targetnodes rs' \<and> length rs' = length (upd_cs [] as')
[PROOF STEP]
have "upd_cs [] as' = []"
[PROOF STATE]
proof (prove)
using this:
msx = []
msx = targetnodes rs' \<and> length rs' = length (upd_cs [] as')

goal (1 subgoal):
 1. upd_cs [] as' = []
[PROOF STEP]
by(cases rs')(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
upd_cs [] as' = []

goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
with \<open>CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<close> \<open>nx \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
nx \<in> S
upd_cs [] as' = []
[PROOF STEP]
have "slice_edge S (upd_cs [] as') a"
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
nx \<in> S
upd_cs [] as' = []

goal (1 subgoal):
 1. slice_edge S (upd_cs [] as') a
[PROOF STEP]
by(cases "kind a",auto intro:combSlice_refl
          simp:slice_edge_def SDG_to_CFG_set_def HRB_slice_def)
[PROOF STATE]
proof (state)
this:
slice_edge S (upd_cs [] as') a

goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
hence "slice_edges S (upd_cs [] as') (a#as'') \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
slice_edge S (upd_cs [] as') a

goal (1 subgoal):
 1. slice_edges S (upd_cs [] as') (a # as'') \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S (upd_cs [] as') (a # as'') \<noteq> []

goal (2 subgoals):
 1. msx = [] \<Longrightarrow> slice_edges S [] as \<noteq> []
 2. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
with \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
slice_edges S (upd_cs [] as') (a # as'') \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
slice_edges S (upd_cs [] as') (a # as'') \<noteq> []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> []
[PROOF STEP]
by(fastforce dest:slice_edges_Nil_split)
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
msx \<noteq> []

goal (1 subgoal):
 1. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
from IH[OF \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a#msx,x)\<close>
        \<open>valid_node m\<close> this \<open>CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<close>]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S [] as' \<noteq> []
[PROOF STEP]
have "slice_edges S [] as' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
slice_edges S [] as' \<noteq> []

goal (1 subgoal):
 1. slice_edges S [] as' \<noteq> []
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
slice_edges S [] as' \<noteq> []

goal (1 subgoal):
 1. msx \<noteq> [] \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
with \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
slice_edges S [] as' \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
slice_edges S [] as' \<noteq> []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> []
[PROOF STEP]
by(fastforce dest:slice_edges_Nil_split)
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; [] \<noteq> []; CFG_node m' \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> slice_edges S [] as \<noteq> []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. False
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
have "slice_edges S [] as = []"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. slice_edges S [] as = []
[PROOF STEP]
by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
                simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
slice_edges S [] as = []

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
slice_edges S [] as \<noteq> []
slice_edges S [] as = []
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
slice_edges S [] as \<noteq> []
slice_edges S [] as = []

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfers_intra_slice_kinds_slice_edges:
  "\<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s =
  transfers (slice_kinds S as) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s
[PROOF STEP]
proof(induct as arbitrary:s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs [])) s = transfers (slice_kinds S []) s
 2. \<And>a as s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<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. \<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs [])) s = transfers (slice_kinds S []) s
 2. \<And>a as s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<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. transfers (slice_kinds S (slice_edges S cs [])) s = transfers (slice_kinds S []) s
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs [])) s = transfers (slice_kinds S []) s

goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
case (Cons a' as')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as')) ?s = transfers (slice_kinds S as') ?s
\<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 s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
note IH = \<open>\<And>s. \<lbrakk>\<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>
    transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as')) ?s = transfers (slice_kinds S as') ?s

goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[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 s. \<lbrakk>\<And>s. \<lbrakk>\<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> transfers (slice_kinds S (slice_edges S cs as)) s = transfers (slice_kinds S as) s; \<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> transfers (slice_kinds S (slice_edges S cs (a # as))) s = transfers (slice_kinds S (a # as)) s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
proof(cases "slice_edge S cs a'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
 2. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
slice_edge S cs a'

goal (2 subgoals):
 1. slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
 2. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
with \<open>intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a')
slice_edge S cs a'
[PROOF STEP]
have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S cs as'))
                (transfer (slice_kind S a') s)"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a')
slice_edge S cs a'

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s)
[PROOF STEP]
by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s)

goal (2 subgoals):
 1. slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
 2. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
have "transfers (slice_kinds S (a'#as')) s
        = transfers (slice_kinds S as') (transfer (slice_kind S a') s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') (transfer (slice_kind S a') s)
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') (transfer (slice_kind S a') s)

goal (2 subgoals):
 1. slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
 2. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
with eq IH[OF \<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>,
      of "transfer (slice_kind S a') s"]
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s)
transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s) = transfers (slice_kinds S as') (transfer (slice_kind S a') s)
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') (transfer (slice_kind S a') s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s)
transfers (slice_kinds S (slice_edges S cs as')) (transfer (slice_kind S a') s) = transfers (slice_kinds S as') (transfer (slice_kind S a') s)
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') (transfer (slice_kind S a') s)

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> slice_edge S cs a'

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
with \<open>intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a')
\<not> slice_edge S cs a'
[PROOF STEP]
have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S cs as')) s"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a')
\<not> slice_edge S cs a'

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) s
[PROOF STEP]
by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) s

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
from False \<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:
\<not> slice_edge S cs a'
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>"
[PROOF STATE]
proof (prove)
using this:
\<not> slice_edge S cs a'
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>
[PROOF STEP]
by(fastforce simp:slice_edge_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
with \<open>intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a')
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have "transfer (slice_kind S a') s = s"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a')
sourcenode a' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. transfer (slice_kind S a') s = s
[PROOF STEP]
by(cases s)(auto,cases "kind a'",
        auto simp:slice_kind_def Let_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
transfer (slice_kind S a') s = s

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
hence "transfers (slice_kinds S (a'#as')) s
         = transfers (slice_kinds S as') s"
[PROOF STATE]
proof (prove)
using this:
transfer (slice_kind S a') s = s

goal (1 subgoal):
 1. transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') s
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') s

goal (1 subgoal):
 1. \<not> slice_edge S cs a' \<Longrightarrow> transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
with eq IH[OF \<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>,of s]
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) s
transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (slice_edges S cs as')) s
transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
transfers (slice_kinds S (a' # as')) s = transfers (slice_kinds S as') s

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S cs (a' # as'))) s = transfers (slice_kinds S (a' # as')) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_sliced_intra_path_preds:
  assumes "m -as\<rightarrow>\<^sub>\<iota>* m'" and "slice_edges S cs as = []"
  and "m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>" and "\<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  obtains as' where "m -as'\<rightarrow>\<^sub>\<iota>* m'" and "preds (slice_kinds S as') (cf#cfs)"
  and "slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as'. \<lbrakk>m -as'\<rightarrow>\<^sub>\<iota>* m'; preds (slice_kinds S as') (cf # cfs); slice_edges S cs as' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<iota>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
have "m -as\<rightarrow>* m'" and "\<forall>a \<in> set as. intra_kind(kind a)"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<iota>* m'

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

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<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:
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>
[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:
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>

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes as). nx \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(rule slice_intra_edges_no_nodes_in_slice)
[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. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>m -as\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<iota>* m'
m' \<in> \<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]
have "m' \<in> obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<iota>* m'
m' \<in> \<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. m' \<in> obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(fastforce intro:obs_intra_elem)
[PROOF STATE]
proof (state)
this:
m' \<in> obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
hence "obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}"
[PROOF STATE]
proof (prove)
using this:
m' \<in> obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
[PROOF STEP]
by(rule obs_intra_singleton_element)
[PROOF STATE]
proof (state)
this:
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>m -as\<rightarrow>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>* m'
[PROOF STEP]
have "valid_node m" and "valid_node m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>* m'

goal (1 subgoal):
 1. valid_node m &&& valid_node m'
[PROOF STEP]
by(fastforce dest:path_valid_node)+
[PROOF STATE]
proof (state)
this:
valid_node m
valid_node m'

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<iota>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
obtain x where "distance m m' x" and "x \<le> length as"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>distance m m' x; x \<le> length as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule every_path_distance)
[PROOF STATE]
proof (state)
this:
distance m m' x
x \<le> length as

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>distance m m' x\<close> \<open>obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<close>
[PROOF STATE]
proof (chain)
picking this:
distance m m' x
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
[PROOF STEP]
show "\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf#cfs) \<and>
              slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
using this:
distance m m' x
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
proof(induct x arbitrary:m rule:nat.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>distance m m' 0; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
distance m m' 0
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}

goal (2 subgoals):
 1. \<And>m. \<lbrakk>distance m m' 0; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>distance m m' 0\<close>
[PROOF STATE]
proof (chain)
picking this:
distance m m' 0
[PROOF STEP]
have "m = m'"
[PROOF STATE]
proof (prove)
using this:
distance m m' 0

goal (1 subgoal):
 1. m = m'
[PROOF STEP]
by(fastforce elim:distance.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
m = m'

goal (2 subgoals):
 1. \<And>m. \<lbrakk>distance m m' 0; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>valid_node m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
m = m'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m'
m = m'

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
by(rule_tac x="[]" in exI,
        auto intro:empty_path simp:slice_kinds_def intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distance ?m m' x; obs_intra ?m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. ?m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
distance m m' (Suc x)
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
note IH = \<open>\<And>m. \<lbrakk>distance m m' x; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk>
      \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and>
               slice_edges S cs as' = []\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>distance ?m m' x; obs_intra ?m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. ?m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>distance m m' (Suc x)\<close>
[PROOF STATE]
proof (chain)
picking this:
distance m m' (Suc x)
[PROOF STEP]
obtain a
      where "valid_edge a" and "m = sourcenode a" and "intra_kind(kind a)"
      and "distance (targetnode a) m' x"
      and target:"targetnode a = (SOME nx. \<exists>a'. sourcenode a = sourcenode a' \<and>
      distance (targetnode a') m' x \<and>
      valid_edge a' \<and> intra_kind(kind a') \<and> targetnode a' = nx)"
[PROOF STATE]
proof (prove)
using this:
distance m m' (Suc x)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; m = sourcenode a; intra_kind (kind a); distance (targetnode a) m' x; targetnode a = (SOME nx. \<exists>a'. sourcenode a = sourcenode a' \<and> distance (targetnode a') m' x \<and> valid_edge a' \<and> intra_kind (kind a') \<and> targetnode a' = nx)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:distance_successor_distance)
[PROOF STATE]
proof (state)
this:
valid_edge a
m = sourcenode a
intra_kind (kind a)
distance (targetnode a) m' x
targetnode a = (SOME nx. \<exists>a'. sourcenode a = sourcenode a' \<and> distance (targetnode a') m' x \<and> valid_edge a' \<and> intra_kind (kind a') \<and> targetnode a' = nx)

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
have "m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
assume "m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (state)
this:
m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
m = sourcenode a
[PROOF STEP]
have "valid_node m"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
m = sourcenode a

goal (1 subgoal):
 1. valid_node m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_node m

goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
with \<open>m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
valid_node m
[PROOF STEP]
have "obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m}"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
valid_node m

goal (1 subgoal):
 1. obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m}
[PROOF STEP]
by -(rule n_in_obs_intra)
[PROOF STATE]
proof (state)
this:
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m}

goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
with \<open>obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<close>
[PROOF STATE]
proof (chain)
picking this:
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m}
[PROOF STEP]
have "m = m'"
[PROOF STATE]
proof (prove)
using this:
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m}

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

goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m
m = m'
[PROOF STEP]
have "m -[]\<rightarrow>\<^sub>\<iota>* m'"
[PROOF STATE]
proof (prove)
using this:
valid_node m
m = m'

goal (1 subgoal):
 1. m -[]\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
by(fastforce intro:empty_path simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
m -[]\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. m \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> False
[PROOF STEP]
with \<open>distance m m' (Suc x)\<close>
[PROOF STATE]
proof (chain)
picking this:
distance m m' (Suc x)
m -[]\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
distance m m' (Suc x)
m -[]\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim:distance.cases)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>distance (targetnode a) m' x\<close> \<open>m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
distance (targetnode a) m' x
m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
obtain mx where "mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
distance (targetnode a) m' x
m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. (\<And>mx. mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:distance.cases path_ex_obs_intra)
[PROOF STATE]
proof (state)
this:
mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>intra_kind(kind a)\<close> \<open>m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
intra_kind (kind a)
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
[PROOF STEP]
have "obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<subseteq>
      obs_intra (sourcenode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
intra_kind (kind a)
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a

goal (1 subgoal):
 1. obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<subseteq> obs_intra (sourcenode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by -(rule edge_obs_intra_subset,auto)
[PROOF STATE]
proof (state)
this:
obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<subseteq> obs_intra (sourcenode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>m = sourcenode a\<close>
      \<open>obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<close>
[PROOF STATE]
proof (chain)
picking this:
mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<subseteq> obs_intra (sourcenode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have "m' \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
mx \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<subseteq> obs_intra (sourcenode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. m' \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m' \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
hence "obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}"
[PROOF STATE]
proof (prove)
using this:
m' \<in> obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
[PROOF STEP]
by(rule obs_intra_singleton_element)
[PROOF STATE]
proof (state)
this:
obs_intra (targetnode a) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from IH[OF \<open>distance (targetnode a) m' x\<close> this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as'. targetnode a -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
obtain as where "targetnode a -as\<rightarrow>\<^sub>\<iota>* m'" and "preds (slice_kinds S as) (cf#cfs)"
      and "slice_edges S cs as = []"
[PROOF STATE]
proof (prove)
using this:
\<exists>as'. targetnode a -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>targetnode a -as\<rightarrow>\<^sub>\<iota>* m'; preds (slice_kinds S as) (cf # cfs); slice_edges S cs as = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
targetnode a -as\<rightarrow>\<^sub>\<iota>* m'
preds (slice_kinds S as) (cf # cfs)
slice_edges S cs as = []

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>targetnode a -as\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>valid_edge a\<close> \<open>intra_kind(kind a)\<close>
      \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -as\<rightarrow>\<^sub>\<iota>* m'
valid_edge a
intra_kind (kind a)
m = sourcenode a
[PROOF STEP]
have "m -a#as\<rightarrow>\<^sub>\<iota>* m'"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as\<rightarrow>\<^sub>\<iota>* m'
valid_edge a
intra_kind (kind a)
m = sourcenode a

goal (1 subgoal):
 1. m -a # as\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
by(fastforce intro:Cons_path simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
m -a # as\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>\<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
      \<open>m = sourcenode a\<close> \<open>intra_kind(kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
intra_kind (kind a)
[PROOF STEP]
have "\<not> slice_edge S cs a"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
intra_kind (kind a)

goal (1 subgoal):
 1. \<not> slice_edge S cs a
[PROOF STEP]
by(fastforce simp:slice_edge_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<not> slice_edge S cs a

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>slice_edges S cs as = []\<close> \<open>intra_kind(kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = []
intra_kind (kind a)
\<not> slice_edge S cs a
[PROOF STEP]
have "slice_edges S cs (a#as) = []"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = []
intra_kind (kind a)
\<not> slice_edge S cs a

goal (1 subgoal):
 1. slice_edges S cs (a # as) = []
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
slice_edges S cs (a # as) = []

goal (1 subgoal):
 1. \<And>nat m. \<lbrakk>\<And>m. \<lbrakk>distance m m' nat; obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []; distance m m' (Suc nat); obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>intra_kind(kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a)

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
proof(cases "kind a")
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
case (UpdateEdge f)
[PROOF STATE]
proof (state)
this:
kind a = \<Up>f

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
kind a = \<Up>f
[PROOF STEP]
have "slice_kind S a = \<Up>id"
[PROOF STATE]
proof (prove)
using this:
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
kind a = \<Up>f

goal (1 subgoal):
 1. slice_kind S a = \<Up>id
[PROOF STEP]
by(fastforce intro:slice_kind_Upd)
[PROOF STATE]
proof (state)
this:
slice_kind S a = \<Up>id

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)"
        and "pred (slice_kind S a) (cf#cfs)"
[PROOF STATE]
proof (prove)
using this:
slice_kind S a = \<Up>id

goal (1 subgoal):
 1. transfer (slice_kind S a) (cf # cfs) = cf # cfs &&& pred (slice_kind S a) (cf # cfs)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>preds (slice_kinds S as) (cf#cfs)\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S as) (cf # cfs)
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)
[PROOF STEP]
have "preds (slice_kinds S (a#as)) (cf#cfs)"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S as) (cf # cfs)
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)

goal (1 subgoal):
 1. preds (slice_kinds S (a # as)) (cf # cfs)
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S (a # as)) (cf # cfs)

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>m -a#as\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>slice_edges S cs (a#as) = []\<close>
[PROOF STATE]
proof (chain)
picking this:
m -a # as\<rightarrow>\<^sub>\<iota>* m'
slice_edges S cs (a # as) = []
preds (slice_kinds S (a # as)) (cf # cfs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m -a # as\<rightarrow>\<^sub>\<iota>* m'
slice_edges S cs (a # as) = []
preds (slice_kinds S (a # as)) (cf # cfs)

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
case (PredicateEdge Q)
[PROOF STATE]
proof (state)
this:
kind a = (Q)\<^sub>\<surd>

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>m = sourcenode a\<close> \<open>distance m m' (Suc x)\<close>
        \<open>obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}\<close> \<open>distance (targetnode a) m' x\<close>
        target
[PROOF STATE]
proof (chain)
picking this:
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
distance m m' (Suc x)
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
distance (targetnode a) m' x
targetnode a = (SOME nx. \<exists>a'. sourcenode a = sourcenode a' \<and> distance (targetnode a') m' x \<and> valid_edge a' \<and> intra_kind (kind a') \<and> targetnode a' = nx)
kind a = (Q)\<^sub>\<surd>
[PROOF STEP]
have "slice_kind S a = (\<lambda>s. True)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
m \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
m = sourcenode a
distance m m' (Suc x)
obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = {m'}
distance (targetnode a) m' x
targetnode a = (SOME nx. \<exists>a'. sourcenode a = sourcenode a' \<and> distance (targetnode a') m' x \<and> valid_edge a' \<and> intra_kind (kind a') \<and> targetnode a' = nx)
kind a = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. slice_kind S a = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
[PROOF STATE]
proof (state)
this:
slice_kind S a = (\<lambda>s. True)\<^sub>\<surd>

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)"
        and "pred (slice_kind S a) (cf#cfs)"
[PROOF STATE]
proof (prove)
using this:
slice_kind S a = (\<lambda>s. True)\<^sub>\<surd>

goal (1 subgoal):
 1. transfer (slice_kind S a) (cf # cfs) = cf # cfs &&& pred (slice_kind S a) (cf # cfs)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>preds (slice_kinds S as) (cf#cfs)\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S as) (cf # cfs)
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)
[PROOF STEP]
have "preds (slice_kinds S (a#as)) (cf#cfs)"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S as) (cf # cfs)
transfer (slice_kind S a) (cf # cfs) = cf # cfs
pred (slice_kind S a) (cf # cfs)

goal (1 subgoal):
 1. preds (slice_kinds S (a # as)) (cf # cfs)
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S (a # as)) (cf # cfs)

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>m -a#as\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>slice_edges S cs (a#as) = []\<close>
[PROOF STATE]
proof (chain)
picking this:
m -a # as\<rightarrow>\<^sub>\<iota>* m'
slice_edges S cs (a # as) = []
preds (slice_kinds S (a # as)) (cf # cfs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m -a # as\<rightarrow>\<^sub>\<iota>* m'
slice_edges S cs (a # as) = []
preds (slice_kinds S (a # as)) (cf # cfs)

goal (1 subgoal):
 1. \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal (2 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
 2. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> \<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []
[PROOF STEP]
qed (auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as'. m -as'\<rightarrow>\<^sub>\<iota>* m' \<and> preds (slice_kinds S as') (cf # cfs) \<and> slice_edges S cs as' = []

goal:
No subgoals!
[PROOF STEP]
qed