[STATEMENT]
lemma slp_to_intra_path_with_slice_edges:
  assumes "n -as\<rightarrow>\<^bsub>sl\<^esub>* n'" and "slice_edges S cs as = []"
  obtains as' where "n -as'\<rightarrow>\<^sub>\<iota>* n'" and "slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as'. \<lbrakk>n -as'\<rightarrow>\<^sub>\<iota>* n'; 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'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^bsub>sl\<^esub>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'
[PROOF STEP]
have "n -as\<rightarrow>* n'" and "same_level_path as"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& same_level_path as
[PROOF STEP]
by(simp_all add:slp_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
same_level_path as

goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>same_level_path as\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path as
[PROOF STEP]
have "same_level_path_aux [] as" and "upd_cs [] as = []"
[PROOF STATE]
proof (prove)
using this:
same_level_path as

goal (1 subgoal):
 1. same_level_path_aux [] as &&& upd_cs [] as = []
[PROOF STEP]
by(simp_all add:same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] as
upd_cs [] as = []

goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>n -as\<rightarrow>* n'\<close> \<open>same_level_path_aux [] as\<close> \<open>upd_cs [] as = []\<close>
    \<open>slice_edges S cs as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
same_level_path_aux [] as
upd_cs [] as = []
slice_edges S cs as = []
[PROOF STEP]
show "\<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
same_level_path_aux [] as
upd_cs [] as = []
slice_edges S cs as = []

goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
proof(induct as arbitrary:n cs rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n cs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. x -ys\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] ys \<longrightarrow> upd_cs [] ys = [] \<longrightarrow> (\<forall>xa. slice_edges S xa ys = [] \<longrightarrow> (\<exists>as'. x -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S xa as' = []))); n -xs\<rightarrow>* n'; same_level_path_aux [] xs; upd_cs [] xs = []; slice_edges S cs xs = []\<rbrakk> \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
fix as n cs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n cs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. x -ys\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] ys \<longrightarrow> upd_cs [] ys = [] \<longrightarrow> (\<forall>xa. slice_edges S xa ys = [] \<longrightarrow> (\<exists>as'. x -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S xa as' = []))); n -xs\<rightarrow>* n'; same_level_path_aux [] xs; upd_cs [] xs = []; slice_edges S cs xs = []\<rbrakk> \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
assume IH:"\<forall>as''. length as'' < length as \<longrightarrow>
      (\<forall>n''. n'' -as''\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] as'' \<longrightarrow>
           upd_cs [] as'' = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' as'' = [] \<longrightarrow>
           (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))"
      and "n -as\<rightarrow>* n'" and "same_level_path_aux [] as" and "upd_cs [] as = []"
      and "slice_edges S cs as = []"
[PROOF STATE]
proof (state)
this:
\<forall>as''. length as'' < length as \<longrightarrow> (\<forall>n''. n'' -as''\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] as'' \<longrightarrow> upd_cs [] as'' = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' as'' = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))
n -as\<rightarrow>* n'
same_level_path_aux [] as
upd_cs [] as = []
slice_edges S cs as = []

goal (1 subgoal):
 1. \<And>xs n cs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. x -ys\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] ys \<longrightarrow> upd_cs [] ys = [] \<longrightarrow> (\<forall>xa. slice_edges S xa ys = [] \<longrightarrow> (\<exists>as'. x -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S xa as' = []))); n -xs\<rightarrow>* n'; same_level_path_aux [] xs; upd_cs [] xs = []; slice_edges S cs xs = []\<rbrakk> \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
show "\<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
proof(cases as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = [] \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
as = []

goal (2 subgoals):
 1. as = [] \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = []

goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
by(fastforce simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []

goal (1 subgoal):
 1. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
case (Cons a' as')
[PROOF STATE]
proof (state)
this:
as = a' # as'

goal (1 subgoal):
 1. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>n -as\<rightarrow>* n'\<close> Cons
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = a' # as'
as = a' # as'
[PROOF STEP]
have "n = sourcenode a'" and "valid_edge a'"
        and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = a' # as'
as = a' # as'

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

goal (1 subgoal):
 1. \<And>a list. as = a # list \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
proof(cases "kind a'" rule:edge_kind_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
case Intra
[PROOF STATE]
proof (state)
this:
intra_kind (kind a')

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with Cons \<open>same_level_path_aux [] as\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
same_level_path_aux [] as
intra_kind (kind a')
[PROOF STEP]
have "same_level_path_aux [] as'"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
same_level_path_aux [] as
intra_kind (kind a')

goal (1 subgoal):
 1. same_level_path_aux [] as'
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] as'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] as'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from Intra Cons \<open>upd_cs [] as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a')
as = a' # as'
upd_cs [] as = []
[PROOF STEP]
have "upd_cs [] as' = []"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a')
as = a' # as'
upd_cs [] as = []

goal (1 subgoal):
 1. upd_cs [] as' = []
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
upd_cs [] as' = []

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
upd_cs [] as' = []

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>slice_edges S cs as = []\<close> Cons Intra
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = []
as = a' # as'
intra_kind (kind a')
[PROOF STEP]
have "slice_edges S cs as' = []" and "\<not> slice_edge S cs a'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = []
as = a' # as'
intra_kind (kind a')

goal (1 subgoal):
 1. slice_edges S cs as' = [] &&& \<not> slice_edge S cs a'
[PROOF STEP]
by(cases "slice_edge S cs a'",auto simp:intra_kind_def)+
[PROOF STATE]
proof (state)
this:
slice_edges S cs as' = []
\<not> slice_edge S cs a'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux [] as'
upd_cs [] as' = []
slice_edges S cs as' = []
\<not> slice_edge S cs a'
[PROOF STEP]
obtain as'' where "targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'"
          and "slice_edges S cs as'' = []"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [] as'
upd_cs [] as' = []
slice_edges S cs as' = []
\<not> slice_edge S cs a'

goal (1 subgoal):
 1. (\<And>as''. \<lbrakk>targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using IH Cons \<open>targetnode a' -as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [] as'
upd_cs [] as' = []
slice_edges S cs as' = []
\<not> slice_edge S cs a'
\<forall>as''. length as'' < length as \<longrightarrow> (\<forall>n''. n'' -as''\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] as'' \<longrightarrow> upd_cs [] as'' = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' as'' = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))
as = a' # as'
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>as''. \<lbrakk>targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule_tac x="as'" in allE) auto
[PROOF STATE]
proof (state)
this:
targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs as'' = []

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>n = sourcenode a'\<close> \<open>valid_edge a'\<close> Intra \<open>targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n = sourcenode a'
valid_edge a'
intra_kind (kind a')
targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -a'#as''\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
n = sourcenode a'
valid_edge a'
intra_kind (kind a')
targetnode a' -as''\<rightarrow>\<^sub>\<iota>* n'

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

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n -a' # as''\<rightarrow>\<^sub>\<iota>* n'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>slice_edges S cs as'' = []\<close> \<open>\<not> slice_edge S cs a'\<close> Intra
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as'' = []
\<not> slice_edge S cs a'
intra_kind (kind a')
[PROOF STEP]
have "slice_edges S cs (a'#as'') = []"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as'' = []
\<not> slice_edge S cs a'
intra_kind (kind a')

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

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n -a' # as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs (a' # as'') = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -a' # as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs (a' # as'') = []

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
case (Call Q r p f)
[PROOF STATE]
proof (state)
this:
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with Cons \<open>same_level_path_aux [] as\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
same_level_path_aux [] as
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have "same_level_path_aux [a'] as'"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
same_level_path_aux [] as
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. same_level_path_aux [a'] as'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
same_level_path_aux [a'] as'

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from Call Cons \<open>upd_cs [] as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
as = a' # as'
upd_cs [] as = []
[PROOF STEP]
have "upd_cs [a'] as' = []"
[PROOF STATE]
proof (prove)
using this:
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
as = a' # as'
upd_cs [] as = []

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
hence "as' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
upd_cs [a'] as' = []

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>upd_cs [a'] as' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs [a'] as' = []
as' \<noteq> []
[PROOF STEP]
obtain xs ys where "as' = xs@ys" and "xs \<noteq> []"
        and "upd_cs [a'] xs = []" and "upd_cs [] ys = []"
        and "\<forall>xs' ys'. xs = xs'@ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
upd_cs [a'] as' = []
as' \<noteq> []

goal (1 subgoal):
 1. (\<And>xs ys. \<lbrakk>as' = xs @ ys; xs \<noteq> []; upd_cs [a'] xs = []; upd_cs [] ys = []; \<forall>xs' ys'. xs = xs' @ ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule upd_cs_empty_split,auto)
[PROOF STATE]
proof (state)
this:
as' = xs @ ys
xs \<noteq> []
upd_cs [a'] xs = []
upd_cs [] ys = []
\<forall>xs' ys'. xs = xs' @ ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>same_level_path_aux [a'] as'\<close> \<open>as' = xs@ys\<close> \<open>upd_cs [a'] xs = []\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux [a'] as'
as' = xs @ ys
upd_cs [a'] xs = []
[PROOF STEP]
have "same_level_path_aux [a'] xs"  and "same_level_path_aux [] ys"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [a'] as'
as' = xs @ ys
upd_cs [a'] xs = []

goal (1 subgoal):
 1. same_level_path_aux [a'] xs &&& same_level_path_aux [] ys
[PROOF STEP]
by(rule slpa_split)+
[PROOF STATE]
proof (state)
this:
same_level_path_aux [a'] xs
same_level_path_aux [] ys

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>upd_cs [a'] xs = []\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs [a'] xs = []
same_level_path_aux [a'] xs
same_level_path_aux [] ys
[PROOF STEP]
have "upd_cs ([a']@cs) xs = []@cs"
[PROOF STATE]
proof (prove)
using this:
upd_cs [a'] xs = []
same_level_path_aux [a'] xs
same_level_path_aux [] ys

goal (1 subgoal):
 1. upd_cs ([a'] @ cs) xs = [] @ cs
[PROOF STEP]
by(fastforce intro:same_level_path_upd_cs_callstack_Append)
[PROOF STATE]
proof (state)
this:
upd_cs ([a'] @ cs) xs = [] @ cs

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>slice_edges S cs as = []\<close> Cons Call
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = []
as = a' # as'
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have "slice_edges S (a'#cs) as' = []" and "\<not> slice_edge S cs a'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = []
as = a' # as'
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. slice_edges S (a' # cs) as' = [] &&& \<not> slice_edge S cs a'
[PROOF STEP]
by(cases "slice_edge S cs a'",auto)+
[PROOF STATE]
proof (state)
this:
slice_edges S (a' # cs) as' = []
\<not> slice_edge S cs a'

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>slice_edges S (a'#cs) as' = []\<close> \<open>as' = xs@ys\<close>
          \<open>upd_cs ([a']@cs) xs = []@cs\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S (a' # cs) as' = []
as' = xs @ ys
upd_cs ([a'] @ cs) xs = [] @ cs
[PROOF STEP]
have "slice_edges S cs ys = []"
[PROOF STATE]
proof (prove)
using this:
slice_edges S (a' # cs) as' = []
as' = xs @ ys
upd_cs ([a'] @ cs) xs = [] @ cs

goal (1 subgoal):
 1. slice_edges S cs ys = []
[PROOF STEP]
by(fastforce dest:slice_edges_Nil_split)
[PROOF STATE]
proof (state)
this:
slice_edges S cs ys = []

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>same_level_path_aux [a'] xs\<close> \<open>upd_cs [a'] xs = []\<close>
          \<open>\<forall>xs' ys'. xs = xs'@ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux [a'] xs
upd_cs [a'] xs = []
\<forall>xs' ys'. xs = xs' @ ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []
[PROOF STEP]
have "last xs \<in> get_return_edges (last [a'])"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [a'] xs
upd_cs [a'] xs = []
\<forall>xs' ys'. xs = xs' @ ys' \<and> ys' \<noteq> [] \<longrightarrow> upd_cs [a'] xs' \<noteq> []

goal (1 subgoal):
 1. last xs \<in> get_return_edges (last [a'])
[PROOF STEP]
by(fastforce intro!:slpa_get_return_edges)
[PROOF STATE]
proof (state)
this:
last xs \<in> get_return_edges (last [a'])

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with \<open>valid_edge a'\<close> Call
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
last xs \<in> get_return_edges (last [a'])
[PROOF STEP]
obtain a where "valid_edge a" and "sourcenode a = sourcenode a'"
          and "targetnode a = targetnode (last xs)" and "kind a = (\<lambda>cf. False)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
last xs \<in> get_return_edges (last [a'])

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>valid_edge a; sourcenode a = sourcenode a'; targetnode a = targetnode (last xs); kind a = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(drule call_return_node_edge,auto)
[PROOF STATE]
proof (state)
this:
valid_edge a
sourcenode a = sourcenode a'
targetnode a = targetnode (last xs)
kind a = (\<lambda>cf. False)\<^sub>\<surd>

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>targetnode a = targetnode (last xs)\<close> \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = targetnode (last xs)
xs \<noteq> []
[PROOF STEP]
have "targetnode a = targetnode (last (a'#xs))"
[PROOF STATE]
proof (prove)
using this:
targetnode a = targetnode (last xs)
xs \<noteq> []

goal (1 subgoal):
 1. targetnode a = targetnode (last (a' # xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
targetnode a = targetnode (last (a' # xs))

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>as' = xs@ys\<close> \<open>xs \<noteq> []\<close> Cons
[PROOF STATE]
proof (chain)
picking this:
as' = xs @ ys
xs \<noteq> []
as = a' # as'
[PROOF STEP]
have "length ys < length as"
[PROOF STATE]
proof (prove)
using this:
as' = xs @ ys
xs \<noteq> []
as = a' # as'

goal (1 subgoal):
 1. length ys < length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length ys < length as

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>targetnode a' -as'\<rightarrow>* n'\<close> \<open>as' = xs@ys\<close> \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' -as'\<rightarrow>* n'
as' = xs @ ys
xs \<noteq> []
[PROOF STEP]
have "targetnode (last (a'#xs)) -ys\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
targetnode a' -as'\<rightarrow>* n'
as' = xs @ ys
xs \<noteq> []

goal (1 subgoal):
 1. targetnode (last (a' # xs)) -ys\<rightarrow>* n'
[PROOF STEP]
by(cases xs rule:rev_cases,auto dest:path_split)
[PROOF STATE]
proof (state)
this:
targetnode (last (a' # xs)) -ys\<rightarrow>* n'

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with IH \<open>length ys < length as\<close> \<open>same_level_path_aux [] ys\<close>
          \<open>upd_cs [] ys = []\<close> \<open>slice_edges S cs ys = []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>as''. length as'' < length as \<longrightarrow> (\<forall>n''. n'' -as''\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] as'' \<longrightarrow> upd_cs [] as'' = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' as'' = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))
length ys < length as
same_level_path_aux [] ys
upd_cs [] ys = []
slice_edges S cs ys = []
targetnode (last (a' # xs)) -ys\<rightarrow>* n'
[PROOF STEP]
obtain as'' where "targetnode (last (a'#xs)) -as''\<rightarrow>\<^sub>\<iota>* n'"
          and "slice_edges S cs as'' = []"
[PROOF STATE]
proof (prove)
using this:
\<forall>as''. length as'' < length as \<longrightarrow> (\<forall>n''. n'' -as''\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] as'' \<longrightarrow> upd_cs [] as'' = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' as'' = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))
length ys < length as
same_level_path_aux [] ys
upd_cs [] ys = []
slice_edges S cs ys = []
targetnode (last (a' # xs)) -ys\<rightarrow>* n'

goal (1 subgoal):
 1. (\<And>as''. \<lbrakk>targetnode (last (a' # xs)) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="ys" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as''. \<lbrakk>targetnode (last (a' # xs)) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis; length ys < length as; same_level_path_aux [] ys; upd_cs [] ys = []; slice_edges S cs ys = []; targetnode (last (a' # xs)) -ys\<rightarrow>* n'; length ys < length as \<longrightarrow> (\<forall>n''. n'' -ys\<rightarrow>* n' \<longrightarrow> same_level_path_aux [] ys \<longrightarrow> upd_cs [] ys = [] \<longrightarrow> (\<forall>cs'. slice_edges S cs' ys = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as''. \<lbrakk>targetnode (if xs = [] then a' else last xs) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis; length ys < length as; same_level_path_aux [] ys; upd_cs [] ys = []; slice_edges S cs ys = []; targetnode (if xs = [] then a' else last xs) -ys\<rightarrow>* n'; \<forall>n''. n'' -ys\<rightarrow>* n' \<longrightarrow> (\<forall>cs'. slice_edges S cs' ys = [] \<longrightarrow> (\<exists>as'. n'' -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = []))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="targetnode (last (a'#xs))" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as''. \<lbrakk>targetnode (if xs = [] then a' else last xs) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis; length ys < length as; same_level_path_aux [] ys; upd_cs [] ys = []; slice_edges S cs ys = []; targetnode (if xs = [] then a' else last xs) -ys\<rightarrow>* n'; targetnode (last (a' # xs)) -ys\<rightarrow>* n' \<longrightarrow> (\<forall>cs'. slice_edges S cs' ys = [] \<longrightarrow> (\<exists>as'. targetnode (last (a' # xs)) -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = []))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as''. \<lbrakk>targetnode (if xs = [] then a' else last xs) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis; length ys < length as; same_level_path_aux [] ys; upd_cs [] ys = []; slice_edges S cs ys = []; targetnode (if xs = [] then a' else last xs) -ys\<rightarrow>* n'; \<forall>cs'. slice_edges S cs' ys = [] \<longrightarrow> (\<exists>as'. targetnode (if xs = [] then a' else last xs) -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs' as' = [])\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule_tac x="cs" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as''. \<lbrakk>targetnode (if xs = [] then a' else last xs) -as''\<rightarrow>\<^sub>\<iota>* n'; slice_edges S cs as'' = []\<rbrakk> \<Longrightarrow> thesis; length ys < length as; same_level_path_aux [] ys; upd_cs [] ys = []; slice_edges S cs ys = []; targetnode (if xs = [] then a' else last xs) -ys\<rightarrow>* n'; slice_edges S cs ys = [] \<longrightarrow> (\<exists>as'. targetnode (if xs = [] then a' else last xs) -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = [])\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
targetnode (last (a' # xs)) -as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs as'' = []

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>sourcenode a = sourcenode a'\<close> \<open>n = sourcenode a'\<close>
          \<open>targetnode a = targetnode (last (a'#xs))\<close> \<open>valid_edge a\<close>
          \<open>kind a = (\<lambda>cf. False)\<^sub>\<surd>\<close> \<open>targetnode (last (a'#xs)) -as''\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = sourcenode a'
n = sourcenode a'
targetnode a = targetnode (last (a' # xs))
valid_edge a
kind a = (\<lambda>cf. False)\<^sub>\<surd>
targetnode (last (a' # xs)) -as''\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -a#as''\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode a = sourcenode a'
n = sourcenode a'
targetnode a = targetnode (last (a' # xs))
valid_edge a
kind a = (\<lambda>cf. False)\<^sub>\<surd>
targetnode (last (a' # xs)) -as''\<rightarrow>\<^sub>\<iota>* n'

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n -a # as''\<rightarrow>\<^sub>\<iota>* n'

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
from \<open>kind a = (\<lambda>cf. False)\<^sub>\<surd>\<close> \<open>slice_edges S cs as'' = []\<close>
          \<open>\<not> slice_edge S cs a'\<close> \<open>sourcenode a = sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = (\<lambda>cf. False)\<^sub>\<surd>
slice_edges S cs as'' = []
\<not> slice_edge S cs a'
sourcenode a = sourcenode a'
[PROOF STEP]
have "slice_edges S cs (a#as'') = []"
[PROOF STATE]
proof (prove)
using this:
kind a = (\<lambda>cf. False)\<^sub>\<surd>
slice_edges S cs as'' = []
\<not> slice_edge S cs a'
sourcenode a = sourcenode a'

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n -a # as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs (a # as'') = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -a # as''\<rightarrow>\<^sub>\<iota>* n'
slice_edges S cs (a # as'') = []

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

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
case (Return Q p f)
[PROOF STATE]
proof (state)
this:
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
with Cons \<open>same_level_path_aux [] as\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
same_level_path_aux [] as
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
same_level_path_aux [] as
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f

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

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>as'. n -as'\<rightarrow>\<^sub>\<iota>* n' \<and> slice_edges S cs as' = []

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tom_split_snoc:
  assumes "S,f \<turnstile> (ms,s) =as\<Rightarrow>* (ms',s')" and "as \<noteq> []"
  obtains asx asx' ms'' s'' where "as = asx@[last asx']"
  and "S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'')" and "S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>asx asx' ms'' s''. \<lbrakk>as = asx @ [last asx']; S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s''); S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>asx asx' ms'' s''. as = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow>* (ms',s')
as \<noteq> []
[PROOF STEP]
show "\<exists>asx asx' ms'' s''. as = asx @ [last asx'] \<and>
    S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow>* (ms',s')
as \<noteq> []

goal (1 subgoal):
 1. \<exists>asx asx' ms'' s''. as = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')
[PROOF STEP]
proof(induct rule:trans_observable_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ms s S f. \<lbrakk>length ms = length s; [] \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms'' s''. [] = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms,s)
 2. \<And>S f ms s as ms' s' as' ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s''); last as # as' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
case (tom_Cons S f ms s as ms' s' as' ms'' s'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
last as # as' \<noteq> []

goal (2 subgoals):
 1. \<And>ms s S f. \<lbrakk>length ms = length s; [] \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms'' s''. [] = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms,s)
 2. \<And>S f ms s as ms' s' as' ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s''); last as # as' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
note IH = \<open>as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' msx sx. as' = asx @ [last asx'] \<and>
      S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (msx,sx) \<and> S,f \<turnstile> (msx,sx) =asx'\<Rightarrow> (ms'',s'')\<close>
[PROOF STATE]
proof (state)
this:
as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' msx sx. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (msx,sx) \<and> S,f \<turnstile> (msx,sx) =asx'\<Rightarrow> (ms'',s'')

goal (2 subgoals):
 1. \<And>ms s S f. \<lbrakk>length ms = length s; [] \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms'' s''. [] = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms,s)
 2. \<And>S f ms s as ms' s' as' ms'' s''. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s''); last as # as' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
 2. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
 2. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
with \<open>S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
as' = []
[PROOF STEP]
have [simp]:"ms'' = ms'" "s'' = s'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
as' = []

goal (1 subgoal):
 1. ms'' = ms' &&& s'' = s'
[PROOF STEP]
by(auto elim:trans_observable_moves.cases)
[PROOF STATE]
proof (state)
this:
ms'' = ms'
s'' = s'

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
 2. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
[PROOF STEP]
have "length ms = length s"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')

goal (1 subgoal):
 1. length ms = length s
[PROOF STEP]
by(rule observable_moves_equal_length)
[PROOF STATE]
proof (state)
this:
length ms = length s

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
 2. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
hence "S,f \<turnstile> (ms,s) =[]\<Rightarrow>* (ms,s)"
[PROOF STATE]
proof (prove)
using this:
length ms = length s

goal (1 subgoal):
 1. S,f \<turnstile> (ms,s) =[]\<Rightarrow>* (ms,s)
[PROOF STEP]
by(rule tom_Nil)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) =[]\<Rightarrow>* (ms,s)

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
 2. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
with \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')\<close> True
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
as' = []
S,f \<turnstile> (ms,s) =[]\<Rightarrow>* (ms,s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
as' = []
S,f \<turnstile> (ms,s) =[]\<Rightarrow>* (ms,s)

goal (1 subgoal):
 1. \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>asx asx' msx sx. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (msx,sx) \<and> S,f \<turnstile> (msx,sx) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
obtain xs xs' msx sx where "as' = xs @ [last xs']"
        and "S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx)"
        and "S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')"
[PROOF STATE]
proof (prove)
using this:
\<exists>asx asx' msx sx. as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms',s') =asx\<Rightarrow>* (msx,sx) \<and> S,f \<turnstile> (msx,sx) =asx'\<Rightarrow> (ms'',s'')

goal (1 subgoal):
 1. (\<And>xs xs' msx sx. \<lbrakk>as' = xs @ [last xs']; S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx); S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as' = xs @ [last xs']
S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx)
S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')\<close> \<open>S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx)
[PROOF STEP]
have "S,f \<turnstile> (ms,s) =(last as)#xs\<Rightarrow>* (msx,sx)"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
S,f \<turnstile> (ms',s') =xs\<Rightarrow>* (msx,sx)

goal (1 subgoal):
 1. S,f \<turnstile> (ms,s) =last as # xs\<Rightarrow>* (msx,sx)
[PROOF STEP]
by(rule trans_observable_moves.tom_Cons)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) =last as # xs\<Rightarrow>* (msx,sx)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
with \<open>S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')\<close> \<open>as' = xs @ [last xs']\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')
as' = xs @ [last xs']
S,f \<turnstile> (ms,s) =last as # xs\<Rightarrow>* (msx,sx)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (msx,sx) =xs'\<Rightarrow> (ms'',s'')
as' = xs @ [last xs']
S,f \<turnstile> (ms,s) =last as # xs\<Rightarrow>* (msx,sx)

goal (1 subgoal):
 1. \<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>asx asx' ms''a s''a. last as # as' = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms''a,s''a) \<and> S,f \<turnstile> (ms''a,s''a) =asx'\<Rightarrow> (ms'',s'')

goal (1 subgoal):
 1. \<And>ms s S f. \<lbrakk>length ms = length s; [] \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asx asx' ms'' s''. [] = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms,s)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<exists>asx asx' ms'' s''. as = asx @ [last asx'] \<and> S,f \<turnstile> (ms,s) =asx\<Rightarrow>* (ms'',s'') \<and> S,f \<turnstile> (ms'',s'') =asx'\<Rightarrow> (ms',s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tom_preserves_stacks:
  assumes "S,f \<turnstile> (m#ms,s) =as\<Rightarrow>* (m'#ms',s')" and "valid_node m"
  and "valid_call_list cs m" and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)"
  and "valid_return_list rs m" and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "\<forall>i < length rs'. rs'!i \<in> get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'"
  and "ms' = targetnodes rs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow>* (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
show "\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
    (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and>
    length rs' = length cs' \<and> ms' = targetnodes rs'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow>* (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m ms cs rs
      rule:trans_observable_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s S f cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
 2. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
case (tom_Nil sx n\<^sub>c f)
[PROOF STATE]
proof (state)
this:
length (m' # ms') = length sx
valid_node m'
valid_call_list cs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m'
length rs = length cs
ms' = targetnodes rs

goal (2 subgoals):
 1. \<And>s S f cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
 2. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (m' # ms') = length sx
valid_node m'
valid_call_list cs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m'
length rs = length cs
ms' = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
apply(rule_tac x="cs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (m' # ms') = length sx; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs \<and> ms' = targetnodes rs'
[PROOF STEP]
apply(rule_tac x="rs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (m' # ms') = length sx; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs m' \<and> length rs = length cs \<and> ms' = targetnodes rs
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'

goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
case (tom_Cons S f sx as msx' sx' as' sx'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')
S,f \<turnstile> (msx',sx') =as'\<Rightarrow>* (m' # ms',sx'')
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
note IH = \<open>\<And>m ms cs rs. \<lbrakk>msx' = m # ms; valid_node m; valid_call_list cs m;
      \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m;
      length rs = length cs; ms = targetnodes rs\<rbrakk>
      \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
      (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
      valid_return_list rs' m' \<and> length rs' = length cs' \<and>
      ms' = targetnodes rs'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'

goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')
[PROOF STEP]
obtain m'' ms'' where "msx' = m''#ms''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')

goal (1 subgoal):
 1. (\<And>m'' ms''. msx' = m'' # ms'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(cases msx')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>m'' ms''. msx' = m'' # ms'' \<Longrightarrow> thesis; S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx'); msx' = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a list. \<lbrakk>\<And>m'' ms''. msx' = m'' # ms'' \<Longrightarrow> thesis; S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx'); msx' = a # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto elim!:observable_moves.cases observable_move.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as aa sa Q p f' msaa. \<lbrakk>msx' = []; as = as @ [aa]; S,f \<turnstile> (m # ms,sx) =as\<Rightarrow>\<^sub>\<tau> (msaa,sa); pred (f aa) sa; valid_edge aa; kind aa = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; length msaa = Suc (length (transfer (f aa) sa)); length sa = Suc (length (transfer (f aa) sa)); transfer (f aa) sa \<noteq> []; hd msaa = sourcenode aa; hd [] = targetnode aa; [] = tl msaa; sx' = transfer (f aa) sa\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac "msaa") auto
[PROOF STATE]
proof (state)
this:
msx' = m'' # ms''

goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
with \<open>S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')\<close> \<open>valid_node m\<close>
      \<open>valid_call_list cs m\<close> \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
      \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close> \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
msx' = m'' # ms''
[PROOF STEP]
obtain cs'' rs'' where "valid_node m''" and "valid_call_list cs'' m''"
      and "\<forall>i < length rs''. rs''!i \<in> get_return_edges (cs''!i)"
      and "valid_return_list rs'' m''" and "length rs'' = length cs''"
      and "ms'' = targetnodes rs''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,sx) =as\<Rightarrow> (msx',sx')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
msx' = m'' # ms''

goal (1 subgoal):
 1. (\<And>cs'' rs''. \<lbrakk>valid_node m''; valid_call_list cs'' m''; \<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i); valid_return_list rs'' m''; length rs'' = length cs''; ms'' = targetnodes rs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:observable_moves_preserves_stack)
[PROOF STATE]
proof (state)
this:
valid_node m''
valid_call_list cs'' m''
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' m''
length rs'' = length cs''
ms'' = targetnodes rs''

goal (1 subgoal):
 1. \<And>S f s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
from IH[OF \<open>msx' = m''#ms''\<close> this(1-6)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs'

goal:
No subgoals!
[PROOF STEP]
qed