[STATEMENT]
lemma DynPDG_path_split:
  "n -as\<rightarrow>\<^sub>d* n' \<Longrightarrow>
  (as = [] \<and> n = n') \<or>
  (\<exists>n'' asx asx'. (n -asx\<rightarrow>\<^sub>c\<^sub>d n'') \<and> (n'' -asx'\<rightarrow>\<^sub>d* n') \<and>
        (as = asx@asx')) \<or>
  (\<exists>n'' V asx asx'. (n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'') \<and> (n'' -asx'\<rightarrow>\<^sub>d* n') \<and>
        (as = asx@asx'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>\<^sub>d* n' \<Longrightarrow> as = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as = asx @ asx')
[PROOF STEP]
proof(induct rule:DynPDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. valid_node n \<Longrightarrow> [] = [] \<and> n = n \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx')
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
case (DynPDG_path_Nil n)
[PROOF STATE]
proof (state)
this:
valid_node n

goal (3 subgoals):
 1. \<And>n. valid_node n \<Longrightarrow> [] = [] \<and> n = n \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx')
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node n

goal (1 subgoal):
 1. [] = [] \<and> n = n \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] = [] \<and> n = n \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n \<and> [] = asx @ asx')

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
case (DynPDG_path_Append_cdep n as n'' as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
note IH = \<open>as = [] \<and> n = n'' \<or>
    (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx') \<or>
    (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx')\<close>
[PROOF STATE]
proof (state)
this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "as = [] \<and> n = n''"
[PROOF STATE]
proof (state)
this:
as = [] \<and> n = n''

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
as = [] \<and> n = n''
[PROOF STEP]
have "valid_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
as = [] \<and> n = n''

goal (1 subgoal):
 1. valid_node n'
[PROOF STEP]
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
                        DynPDG_path_cdep)
[PROOF STATE]
proof (state)
this:
valid_node n'

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>as = [] \<and> n = n''\<close> \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = [] \<and> n = n''
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
valid_node n'
[PROOF STEP]
have "\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
as = [] \<and> n = n''
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
valid_node n'

goal (1 subgoal):
 1. \<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by(auto intro:DynPDG_path_Nil)
[PROOF STATE]
proof (state)
this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx') \<or>
      (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx')"
[PROOF STATE]
proof (state)
this:
(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx'"
[PROOF STATE]
proof (state)
this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'
[PROOF STEP]
obtain nx asx asx' where "n -asx\<rightarrow>\<^sub>c\<^sub>d nx" and "nx -asx'\<rightarrow>\<^sub>d* n''"
        and "as = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. (\<And>asx nx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d nx; nx -asx'\<rightarrow>\<^sub>d* n''; as = asx @ asx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
nx -asx'\<rightarrow>\<^sub>d* n''
as = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule DynPDG_path_cdep)
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>nx -asx'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "nx -asx'@as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:DynPDG_path_Append)
[PROOF STATE]
proof (state)
this:
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n -asx\<rightarrow>\<^sub>c\<^sub>d nx\<close> \<open>as = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx'"
[PROOF STATE]
proof (state)
this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'
[PROOF STEP]
obtain nx V asx asx' where "n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx" and "nx -asx'\<rightarrow>\<^sub>d* n''"
        and "as = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. (\<And>V asx nx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx; nx -asx'\<rightarrow>\<^sub>d* n''; as = asx @ asx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx
nx -asx'\<rightarrow>\<^sub>d* n''
as = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule DynPDG_path_cdep)
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>nx -asx'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "nx -asx'@as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:DynPDG_path_Append)
[PROOF STATE]
proof (state)
this:
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx\<close> \<open>as = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
case (DynPDG_path_Append_ddep n as n'' V as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
note IH = \<open>as = [] \<and> n = n'' \<or>
    (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx') \<or>
    (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx')\<close>
[PROOF STATE]
proof (state)
this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; as = [] \<and> n = n'' \<or> (\<exists>n''a asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>n''a V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''a \<and> n''a -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
as = [] \<and> n = n'' \<or> (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "as = [] \<and> n = n''"
[PROOF STATE]
proof (state)
this:
as = [] \<and> n = n''

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
as = [] \<and> n = n''
[PROOF STEP]
have "valid_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
as = [] \<and> n = n''

goal (1 subgoal):
 1. valid_node n'
[PROOF STEP]
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
                        DynPDG_path_ddep)
[PROOF STATE]
proof (state)
this:
valid_node n'

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>as = [] \<and> n = n''\<close> \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = [] \<and> n = n''
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
valid_node n'
[PROOF STEP]
have "\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
as = [] \<and> n = n''
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
valid_node n'

goal (1 subgoal):
 1. \<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by(fastforce intro:DynPDG_path_Nil)
[PROOF STATE]
proof (state)
this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (2 subgoals):
 1. as = [] \<and> n = n'' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx') \<or>
      (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx')"
[PROOF STATE]
proof (state)
this:
(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. (\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx') \<or> (\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx')

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx'"
[PROOF STATE]
proof (state)
this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'
[PROOF STEP]
obtain nx asx asx' where "n -asx\<rightarrow>\<^sub>c\<^sub>d nx" and "nx -asx'\<rightarrow>\<^sub>d* n''"
        and "as = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. (\<And>asx nx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d nx; nx -asx'\<rightarrow>\<^sub>d* n''; as = asx @ asx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
nx -asx'\<rightarrow>\<^sub>d* n''
as = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule DynPDG_path_ddep)
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>nx -asx'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "nx -asx'@as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:DynPDG_path_Append)
[PROOF STATE]
proof (state)
this:
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n -asx\<rightarrow>\<^sub>c\<^sub>d nx\<close> \<open>as = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
n -asx\<rightarrow>\<^sub>c\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (2 subgoals):
 1. \<exists>nx asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
 2. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
assume "\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx@asx'"
[PROOF STATE]
proof (state)
this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'
[PROOF STEP]
obtain nx V' asx asx' where "n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx" and "nx -asx'\<rightarrow>\<^sub>d* n''"
        and "as = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx'

goal (1 subgoal):
 1. (\<And>V' asx nx asx'. \<lbrakk>n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx; nx -asx'\<rightarrow>\<^sub>d* n''; as = asx @ asx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx
nx -asx'\<rightarrow>\<^sub>d* n''
as = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
from \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(rule DynPDG_path_ddep)
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>nx -asx'\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "nx -asx'@as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
nx -asx'\<rightarrow>\<^sub>d* n''
n'' -as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(fastforce intro:DynPDG_path_Append)
[PROOF STATE]
proof (state)
this:
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
with \<open>n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx\<close> \<open>as = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as@as' = asx@asx'"
[PROOF STATE]
proof (prove)
using this:
n -{V'}asx\<rightarrow>\<^sub>d\<^sub>d nx
as = asx @ asx'
nx -asx' @ as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. \<exists>nx V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d nx \<and> nx -asx'\<rightarrow>\<^sub>d* n'' \<and> as = asx @ asx' \<Longrightarrow> as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx'

goal (1 subgoal):
 1. as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
as @ as' = [] \<and> n = n' \<or> (\<exists>n'' asx asx'. n -asx\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx') \<or> (\<exists>n'' V asx asx'. n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n'' \<and> n'' -asx'\<rightarrow>\<^sub>d* n' \<and> as @ as' = asx @ asx')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynPDG_path_rev_cases [consumes 1,
  case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
  "\<lbrakk>n -as\<rightarrow>\<^sub>d* n'; \<lbrakk>as = []; n = n'\<rbrakk> \<Longrightarrow> Q;
    \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n';
                       as = asx@asx'\<rbrakk> \<Longrightarrow> Q;
    \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n';
                       as = asx@asx'\<rbrakk> \<Longrightarrow> Q\<rbrakk>
  \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>\<^sub>d* n'; \<lbrakk>as = []; n = n'\<rbrakk> \<Longrightarrow> Q; \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; as = asx @ asx'\<rbrakk> \<Longrightarrow> Q; \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; as = asx @ asx'\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by(blast dest:DynPDG_path_split)


[STATEMENT]
lemma DynPDG_ddep_edge_no_shorter_ddep_edge:
  assumes ddep:"n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'"
  shows "\<forall>as' a as''. tl as = as'@a#as'' \<longrightarrow> \<not> sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
from ddep
[PROOF STATE]
proof (chain)
picking this:
n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have influence:"n influences V in n' via as"
[PROOF STATE]
proof (prove)
using this:
n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n influences V in n' via as
[PROOF STEP]
by(auto elim!:DynPDG_edge.cases)
[PROOF STATE]
proof (state)
this:
n influences V in n' via as

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n influences V in n' via as
[PROOF STEP]
obtain  a asx where as:"as = a#asx"
    and notin:"n \<notin> set (sourcenodes asx)"
[PROOF STATE]
proof (prove)
using this:
n influences V in n' via as

goal (1 subgoal):
 1. (\<And>a asx. \<lbrakk>as = a # asx; n \<notin> set (sourcenodes asx)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest:dyn_influence_source_notin_tl_edges simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
as = a # asx
n \<notin> set (sourcenodes asx)

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
from influence as
[PROOF STATE]
proof (chain)
picking this:
n influences V in n' via as
as = a # asx
[PROOF STEP]
have imp:"\<forall>nx \<in> set (sourcenodes asx). V \<notin> Def nx"
[PROOF STATE]
proof (prove)
using this:
n influences V in n' via as
as = a # asx

goal (1 subgoal):
 1. \<forall>nx\<in>set (sourcenodes asx). V \<notin> Def nx
[PROOF STEP]
by(auto simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes asx). V \<notin> Def nx

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>nx\<in>set (sourcenodes asx). V \<notin> Def nx

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
fix as' a' as''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
assume eq:"tl as = as'@a'#as''"
      and ddep':"sourcenode a' -{V}a'#as''\<rightarrow>\<^sub>d\<^sub>d n'"
[PROOF STATE]
proof (state)
this:
tl as = as' @ a' # as''
sourcenode a' -{V}a' # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
from eq as notin
[PROOF STATE]
proof (chain)
picking this:
tl as = as' @ a' # as''
as = a # asx
n \<notin> set (sourcenodes asx)
[PROOF STEP]
have noteq:"sourcenode a' \<noteq> n"
[PROOF STATE]
proof (prove)
using this:
tl as = as' @ a' # as''
as = a # asx
n \<notin> set (sourcenodes asx)

goal (1 subgoal):
 1. sourcenode a' \<noteq> n
[PROOF STEP]
by(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenode a' \<noteq> n

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
from ddep'
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' -{V}a' # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "V \<in> Def (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' -{V}a' # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. V \<in> Def (sourcenode a')
[PROOF STEP]
by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
V \<in> Def (sourcenode a')

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
with eq as noteq imp
[PROOF STATE]
proof (chain)
picking this:
tl as = as' @ a' # as''
as = a # asx
sourcenode a' \<noteq> n
\<forall>nx\<in>set (sourcenodes asx). V \<notin> Def nx
V \<in> Def (sourcenode a')
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
tl as = as' @ a' # as''
as = a # asx
sourcenode a' \<noteq> n
\<forall>nx\<in>set (sourcenodes asx). V \<notin> Def nx
V \<in> Def (sourcenode a')

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

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>tl as = ?as'2 @ ?a'2 # ?as''2; sourcenode ?a'2 -{V}?a'2 # ?as''2\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tl as = ?as'2 @ ?a'2 # ?as''2; sourcenode ?a'2 -{V}?a'2 # ?as''2\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>as' a as''. tl as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_ddep_same_state:
  assumes path:"n -as\<rightarrow>* n'" and Uses:"V \<in> Use n'" and preds:"preds (kinds as) s"
  and no_dep:"\<forall>as' a as''. as = as'@a#as'' \<longrightarrow> \<not> sourcenode a -{V}a#as''\<rightarrow>\<^sub>d\<^sub>d n'"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
fix n''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
assume inset:"n'' \<in> set (sourcenodes as)" and Defs:"V \<in> Def n''"
[PROOF STATE]
proof (state)
this:
n'' \<in> set (sourcenodes as)
V \<in> Def n''

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
hence "\<exists>nx \<in> set (sourcenodes as). V \<in> Def nx"
[PROOF STATE]
proof (prove)
using this:
n'' \<in> set (sourcenodes as)
V \<in> Def n''

goal (1 subgoal):
 1. \<exists>nx\<in>set (sourcenodes as). V \<in> Def nx
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>nx\<in>set (sourcenodes as). V \<in> Def nx

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>nx\<in>set (sourcenodes as). V \<in> Def nx
[PROOF STEP]
obtain nx ns' ns'' where nodes:"sourcenodes as = ns'@nx#ns''"
        and Defs':"V \<in> Def nx" and notDef:"\<forall>nx' \<in> set ns''. V \<notin> Def nx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>nx\<in>set (sourcenodes as). V \<in> Def nx

goal (1 subgoal):
 1. (\<And>ns' nx ns''. \<lbrakk>sourcenodes as = ns' @ nx # ns''; V \<in> Def nx; \<forall>nx'\<in>set ns''. V \<notin> Def nx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:rightmost_element_property)
[PROOF STATE]
proof (state)
this:
sourcenodes as = ns' @ nx # ns''
V \<in> Def nx
\<forall>nx'\<in>set ns''. V \<notin> Def nx'

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
from nodes
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ns' @ nx # ns''
[PROOF STEP]
obtain as' a as''
      where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
      and source:"sourcenode a = nx"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ns' @ nx # ns''

goal (1 subgoal):
 1. (\<And>as'' as' a. \<lbrakk>sourcenodes as'' = ns''; as = as' @ a # as''; sourcenode a = nx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes as'' = ns''
as = as' @ a # as''
sourcenode a = nx

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
from as path
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
n -as\<rightarrow>* n'
[PROOF STEP]
have path':"sourcenode a -a#as''\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
n -as\<rightarrow>* n'

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

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
from notDef as'' source
[PROOF STATE]
proof (chain)
picking this:
\<forall>nx'\<in>set ns''. V \<notin> Def nx'
sourcenodes as'' = ns''
sourcenode a = nx
[PROOF STEP]
have "\<forall>n'' \<in> set (sourcenodes as''). V \<notin> Def n''"
[PROOF STATE]
proof (prove)
using this:
\<forall>nx'\<in>set ns''. V \<notin> Def nx'
sourcenodes as'' = ns''
sourcenode a = nx

goal (1 subgoal):
 1. \<forall>n''\<in>set (sourcenodes as''). V \<notin> Def n''
[PROOF STEP]
by(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>n''\<in>set (sourcenodes as''). V \<notin> Def n''

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
with path' Defs' Uses source
[PROOF STATE]
proof (chain)
picking this:
sourcenode a -a # as''\<rightarrow>* n'
V \<in> Def nx
V \<in> Use n'
sourcenode a = nx
\<forall>n''\<in>set (sourcenodes as''). V \<notin> Def n''
[PROOF STEP]
have influence:"nx influences V in n' via (a#as'')"
[PROOF STATE]
proof (prove)
using this:
sourcenode a -a # as''\<rightarrow>* n'
V \<in> Def nx
V \<in> Use n'
sourcenode a = nx
\<forall>n''\<in>set (sourcenodes as''). V \<notin> Def n''

goal (1 subgoal):
 1. nx influences V in n' via a # as''
[PROOF STEP]
by(simp add:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
nx influences V in n' via a # as''

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
hence "nx \<notin> set (sourcenodes as'')"
[PROOF STATE]
proof (prove)
using this:
nx influences V in n' via a # as''

goal (1 subgoal):
 1. nx \<notin> set (sourcenodes as'')
[PROOF STEP]
by(rule dyn_influence_source_notin_tl_edges)
[PROOF STATE]
proof (state)
this:
nx \<notin> set (sourcenodes as'')

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
with influence source
[PROOF STATE]
proof (chain)
picking this:
nx influences V in n' via a # as''
sourcenode a = nx
nx \<notin> set (sourcenodes as'')
[PROOF STEP]
have "\<exists>asx a'. sourcenode a' -{V}a'#asx\<rightarrow>\<^sub>d\<^sub>d n' \<and> sourcenode a' = nx \<and>
          (\<exists>asx'. a#as'' = asx'@a'#asx)"
[PROOF STATE]
proof (prove)
using this:
nx influences V in n' via a # as''
sourcenode a = nx
nx \<notin> set (sourcenodes as'')

goal (1 subgoal):
 1. \<exists>asx a'. sourcenode a' -{V}a' # asx\<rightarrow>\<^sub>d\<^sub>d n' \<and> sourcenode a' = nx \<and> (\<exists>asx'. a # as'' = asx' @ a' # asx)
[PROOF STEP]
by(fastforce intro:DynPDG_ddep_edge)
[PROOF STATE]
proof (state)
this:
\<exists>asx a'. sourcenode a' -{V}a' # asx\<rightarrow>\<^sub>d\<^sub>d n' \<and> sourcenode a' = nx \<and> (\<exists>asx'. a # as'' = asx' @ a' # asx)

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
with nodes no_dep as
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ns' @ nx # ns''
\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
as = as' @ a # as''
\<exists>asx a'. sourcenode a' -{V}a' # asx\<rightarrow>\<^sub>d\<^sub>d n' \<and> sourcenode a' = nx \<and> (\<exists>asx'. a # as'' = asx' @ a' # asx)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ns' @ nx # ns''
\<forall>as' a as''. as = as' @ a # as'' \<longrightarrow> \<not> sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d n'
as = as' @ a # as''
\<exists>asx a'. sourcenode a' -{V}a' # asx\<rightarrow>\<^sub>d\<^sub>d n' \<and> sourcenode a' = nx \<and> (\<exists>asx'. a # as'' = asx' @ a' # asx)

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

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n''2 \<in> set (sourcenodes as); V \<in> Def ?n''2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
hence "\<forall>n \<in> set (sourcenodes as). V \<notin> Def n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n''2 \<in> set (sourcenodes as); V \<in> Def ?n''2\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>n\<in>set (sourcenodes as). V \<notin> Def n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
with wf path preds
[PROOF STATE]
proof (chain)
picking this:
wf {(x, y). x < y}
n -as\<rightarrow>* n'
preds (kinds as) s
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf {(x, y). x < y}
n -as\<rightarrow>* n'
preds (kinds as) s
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
by(fastforce intro:CFG_path_no_Def_equal)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s) V = state_val s V

goal:
No subgoals!
[PROOF STEP]
qed