[STATEMENT]
lemma limit_Append_path_nonelem_split: "p \<in> limit (Append T k) (\<P> k u) \<Longrightarrow> p \<notin> \<P> k u \<Longrightarrow>
  \<exists> q ts. p = q@ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q@ts) \<and> (\<forall> t \<in> set ts. t \<in> T) \<and>
    (\<forall> t \<in> set (butlast ts). chars_of_token t = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> limit (Append T k) (\<P> k u); p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
proof (induct rule: limit_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>p \<in> \<P> k u; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. \<And>p Y. \<lbrakk>\<And>q. \<lbrakk>q \<in> Y; q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []); p \<in> Append T k Y; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case (Init p)
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u
p \<notin> \<P> k u

goal (2 subgoals):
 1. \<And>p. \<lbrakk>p \<in> \<P> k u; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. \<And>p Y. \<lbrakk>\<And>q. \<lbrakk>q \<in> Y; q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []); p \<in> Append T k Y; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
p \<notin> \<P> k u

goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. \<lbrakk>q \<in> Y; q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []); p \<in> Append T k Y; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. \<lbrakk>q \<in> Y; q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []); p \<in> Append T k Y; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case (Iterate p Y)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q \<in> Y; ?q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. ?q = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
p \<in> Append T k Y
p \<notin> \<P> k u

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. \<lbrakk>q \<in> Y; q \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []); p \<in> Append T k Y; p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
proof (cases "p \<in> Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p \<in> Y

goal (2 subgoals):
 1. p \<in> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
from Iterate(1)[OF True Iterate(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<notin> Y

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
with Append_def Iterate(2)
[PROOF STATE]
proof (chain)
picking this:
Append ?Z ?k ?P = ?P \<union> {p @ [t] |p t. p \<in> by_length ?k ?P \<and> t \<in> ?Z \<and> admissible (p @ [t])}
p \<in> Append T k Y
p \<notin> Y
[PROOF STEP]
have "\<exists> q t. p = q@[t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])"
[PROOF STATE]
proof (prove)
using this:
Append ?Z ?k ?P = ?P \<union> {p @ [t] |p t. p \<in> by_length ?k ?P \<and> t \<in> ?Z \<and> admissible (p @ [t])}
p \<in> Append T k Y
p \<notin> Y

goal (1 subgoal):
 1. \<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])
[PROOF STEP]
obtain q t where qt: "p = q@[t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])"
[PROOF STATE]
proof (prove)
using this:
\<exists>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])

goal (1 subgoal):
 1. (\<And>q t. p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
from qt
[PROOF STATE]
proof (chain)
picking this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])
[PROOF STEP]
have qlen: "charslength q = k"
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])

goal (1 subgoal):
 1. charslength q = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength q = k

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
have "q \<in> \<P> k u \<or> q \<notin> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> \<P> k u \<or> q \<notin> \<P> k u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k u \<or> q \<notin> \<P> k u

goal (1 subgoal):
 1. p \<notin> Y \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> \<P> k u \<or> q \<notin> \<P> k u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> \<P> k u \<or> q \<notin> \<P> k u

goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
proof(induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k u

goal (2 subgoals):
 1. q \<in> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
 2. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
apply (rule_tac x=q in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
apply (rule_tac x="[t]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q @ [t] \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ [t]) \<and> (\<forall>t\<in>set [t]. t \<in> T) \<and> (\<forall>t\<in>set (butlast [t]). chars_of_token t = [])
[PROOF STEP]
using qlen
[PROOF STATE]
proof (prove)
using this:
charslength q = k

goal (1 subgoal):
 1. p = q @ [t] \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ [t]) \<and> (\<forall>t\<in>set [t]. t \<in> T) \<and> (\<forall>t\<in>set (butlast [t]). chars_of_token t = [])
[PROOF STEP]
by (simp add: qt 1)
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
q \<notin> \<P> k u

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
have q_in_Y: "q \<in> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> Y
[PROOF STEP]
using qt
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])

goal (1 subgoal):
 1. q \<in> Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> Y

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
from Iterate(1)[OF q_in_Y 2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
obtain q' ts where
        q'ts: "q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and>
               (\<forall>t\<in>set(butlast ts). chars_of_token t = [])"
[PROOF STATE]
proof (prove)
using this:
\<exists>qa ts. q = qa @ ts \<and> qa \<in> \<P> k u \<and> charslength qa = k \<and> admissible (qa @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. (\<And>q' ts. q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = []) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
with qlen
[PROOF STATE]
proof (chain)
picking this:
charslength q = k
q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
have "charslength ts = 0"
[PROOF STATE]
proof (prove)
using this:
charslength q = k
q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal (1 subgoal):
 1. charslength ts = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength ts = 0

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
hence empty: "\<forall> t \<in> set(ts). chars_of_token t = []"
[PROOF STATE]
proof (prove)
using this:
charslength ts = 0

goal (1 subgoal):
 1. \<forall>t\<in>set ts. chars_of_token t = []
[PROOF STEP]
apply (induct ts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. charslength [] = 0 \<Longrightarrow> \<forall>t\<in>set []. chars_of_token t = []
 2. \<And>a ts. \<lbrakk>charslength ts = 0 \<Longrightarrow> \<forall>t\<in>set ts. chars_of_token t = []; charslength (a # ts) = 0\<rbrakk> \<Longrightarrow> \<forall>t\<in>set (a # ts). chars_of_token t = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. chars_of_token t = []

goal (1 subgoal):
 1. q \<notin> \<P> k u \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
apply (rule_tac x=q' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ts. p = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> admissible (q' @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
apply (rule_tac x="ts@[t]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q' @ ts @ [t] \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> admissible (q' @ ts @ [t]) \<and> (\<forall>t\<in>set (ts @ [t]). t \<in> T) \<and> (\<forall>t\<in>set (butlast (ts @ [t])). chars_of_token t = [])
[PROOF STEP]
using qt q'ts empty
[PROOF STATE]
proof (prove)
using this:
p = q @ [t] \<and> q \<in> by_length k Y \<and> t \<in> T \<and> admissible (q @ [t])
q = q' @ ts \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
\<forall>t\<in>set ts. chars_of_token t = []

goal (1 subgoal):
 1. p = q' @ ts @ [t] \<and> q' \<in> \<P> k u \<and> charslength q' = k \<and> admissible (q' @ ts @ [t]) \<and> (\<forall>t\<in>set (ts @ [t]). t \<in> T) \<and> (\<forall>t\<in>set (butlast (ts @ [t])). chars_of_token t = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> T) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma limit_Append_path_nonelem_split':
  "p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u) \<Longrightarrow> p \<notin> \<P> k u \<Longrightarrow>
   \<exists> q ts. p = q@ts \<and> is_continuation k u q ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u); p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> is_continuation k u q ts
[PROOF STEP]
apply (simp only: is_continuation_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u); p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> \<exists>q ts. p = q @ ts \<and> q \<in> \<P> k u \<and> charslength q = k \<and> admissible (q @ ts) \<and> (\<forall>t\<in>set ts. t \<in> \<Z> k (Suc u)) \<and> (\<forall>t\<in>set (butlast ts). chars_of_token t = [])
[PROOF STEP]
apply (rule_tac limit_Append_path_nonelem_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u); p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
 2. \<lbrakk>p \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u); p \<notin> \<P> k u\<rbrakk> \<Longrightarrow> p \<notin> \<P> k u
[PROOF STEP]
by auto


[STATEMENT]
lemma final_step_of_path: "p \<in> \<P> k u \<Longrightarrow> p \<noteq> [] \<Longrightarrow> (\<exists> q ts k' u'. p = q@ts \<and> indexlt k' u' k u
  \<and> is_continuation k' u' q ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k u; p \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
proof (induct rule: \<P>_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>p' k' u'. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k'a u'a. p' = q @ ts \<and> indexlt k'a u'a k' u' \<and> is_continuation k'a u'a q ts; p \<in> \<P> k u; p \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
case (Induct p k u)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p' \<in> \<P> ?k' ?u'; indexlt ?k' ?u' k u; ?p' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k' u'. ?p' = q @ ts \<and> indexlt k' u' ?k' ?u' \<and> is_continuation k' u' q ts
p \<in> \<P> k u
p \<noteq> []

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>p' k' u'. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k'a u'a. p' = q @ ts \<and> indexlt k'a u'a k' u' \<and> is_continuation k'a u'a q ts; p \<in> \<P> k u; p \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
from Induct(2) Induct(3)
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k u
p \<noteq> []
[PROOF STEP]
have ku_0: "k > 0 \<or> u > 0"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
p \<noteq> []

goal (1 subgoal):
 1. 0 < k \<or> 0 < u
[PROOF STEP]
using nonempty_path_indices
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
p \<noteq> []
\<lbrakk>?p \<in> \<P> ?k ?u; ?p \<noteq> []\<rbrakk> \<Longrightarrow> 0 < ?k \<or> 0 < ?u

goal (1 subgoal):
 1. 0 < k \<or> 0 < u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < k \<or> 0 < u

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>p' k' u'. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k'a u'a. p' = q @ ts \<and> indexlt k'a u'a k' u' \<and> is_continuation k'a u'a q ts; p \<in> \<P> k u; p \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
proof (cases "u = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = 0

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
with ku_0
[PROOF STATE]
proof (chain)
picking this:
0 < k \<or> 0 < u
u = 0
[PROOF STEP]
have k_0: "k > 0"
[PROOF STATE]
proof (prove)
using this:
0 < k \<or> 0 < u
u = 0

goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 < k

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
with True Induct(2) base_paths
[PROOF STATE]
proof (chain)
picking this:
u = 0
p \<in> \<P> k u
\<lbrakk>?p \<in> \<P> ?k 0; 0 < ?k\<rbrakk> \<Longrightarrow> \<exists>u. ?p \<in> \<P> (?k - 1) u
0 < k
[PROOF STEP]
have "\<exists> u'. p \<in> \<P> (k - 1) u'"
[PROOF STATE]
proof (prove)
using this:
u = 0
p \<in> \<P> k u
\<lbrakk>?p \<in> \<P> ?k 0; 0 < ?k\<rbrakk> \<Longrightarrow> \<exists>u. ?p \<in> \<P> (?k - 1) u
0 < k

goal (1 subgoal):
 1. \<exists>u'. p \<in> \<P> (k - 1) u'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u'. p \<in> \<P> (k - 1) u'

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u'. p \<in> \<P> (k - 1) u'
[PROOF STEP]
obtain u' where u': "p \<in> \<P> (k - 1) u'"
[PROOF STATE]
proof (prove)
using this:
\<exists>u'. p \<in> \<P> (k - 1) u'

goal (1 subgoal):
 1. (\<And>u'. p \<in> \<P> (k - 1) u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \<P> (k - 1) u'

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
have indexlt: "indexlt (k - 1) u' k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indexlt (k - 1) u' k u
[PROOF STEP]
by (simp add: indexlt_simp k_0)
[PROOF STATE]
proof (state)
this:
indexlt (k - 1) u' k u

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
from Induct(1)[OF u' indexlt Induct(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a (k - 1) u' \<and> is_continuation k' u'a q ts
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a (k - 1) u' \<and> is_continuation k' u'a q ts

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
using indexlt indexlt_trans
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a (k - 1) u' \<and> is_continuation k' u'a q ts
indexlt (k - 1) u' k u
\<lbrakk>indexlt ?k'' ?u'' ?k' ?u'; indexlt ?k' ?u' ?k ?u\<rbrakk> \<Longrightarrow> indexlt ?k'' ?u'' ?k ?u

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> 0

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
[PROOF STEP]
have "\<exists> u'. u = Suc u'"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0

goal (1 subgoal):
 1. \<exists>u'. u = Suc u'
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<exists>u'. u = Suc u'

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u'. u = Suc u'
[PROOF STEP]
obtain u' where u': "u = Suc u'"
[PROOF STATE]
proof (prove)
using this:
\<exists>u'. u = Suc u'

goal (1 subgoal):
 1. (\<And>u'. u = Suc u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u = Suc u'

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
with Induct(2)
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k u
u = Suc u'
[PROOF STEP]
have p_limit: "p \<in> limit (Append (\<Z> k (Suc u')) k) (\<P> k u')"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
u = Suc u'

goal (1 subgoal):
 1. p \<in> limit (Append (\<Z> k (Suc u')) k) (\<P> k u')
[PROOF STEP]
using \<P>.simps(2)
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u
u = Suc u'
\<P> ?k (Suc ?u) = limit (Append (\<Z> ?k (Suc ?u)) ?k) (\<P> ?k ?u)

goal (1 subgoal):
 1. p \<in> limit (Append (\<Z> k (Suc u')) k) (\<P> k u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> limit (Append (\<Z> k (Suc u')) k) (\<P> k u')

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
from u'
[PROOF STATE]
proof (chain)
picking this:
u = Suc u'
[PROOF STEP]
have indexlt: "indexlt k u' k u"
[PROOF STATE]
proof (prove)
using this:
u = Suc u'

goal (1 subgoal):
 1. indexlt k u' k u
[PROOF STEP]
by (simp add: indexlt_simp)
[PROOF STATE]
proof (state)
this:
indexlt k u' k u

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
have "p \<in> \<P> k u' \<or> p \<notin> \<P> k u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k u' \<or> p \<notin> \<P> k u'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u' \<or> p \<notin> \<P> k u'

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k u' \<or> p \<notin> \<P> k u'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k u' \<or> p \<notin> \<P> k u'

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. p \<notin> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u'

goal (2 subgoals):
 1. p \<in> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
 2. p \<notin> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
from Induct(1)[OF 1 indexlt Induct(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a k u' \<and> is_continuation k' u'a q ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a k u' \<and> is_continuation k' u'a q ts

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
using indexlt indexlt_trans
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'a. p = q @ ts \<and> indexlt k' u'a k u' \<and> is_continuation k' u'a q ts
indexlt k u' k u
\<lbrakk>indexlt ?k'' ?u'' ?k' ?u'; indexlt ?k' ?u' ?k ?u\<rbrakk> \<Longrightarrow> indexlt ?k'' ?u'' ?k ?u

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. p \<notin> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<notin> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p \<notin> \<P> k u'

goal (1 subgoal):
 1. p \<notin> \<P> k u' \<Longrightarrow> \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
from limit_Append_path_nonelem_split'[OF p_limit 2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts. p = q @ ts \<and> is_continuation k u' q ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts. p = q @ ts \<and> is_continuation k u' q ts

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
using indexlt u'
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts. p = q @ ts \<and> is_continuation k u' q ts
indexlt k u' k u
u = Suc u'

goal (1 subgoal):
 1. \<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_in_\<L>\<^sub>P[simp]: "[] \<in> \<L>\<^sub>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> \<L>\<^sub>P
[PROOF STEP]
apply (simp add: \<L>\<^sub>P_def is_derivation_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ex (derives [\<SS>])
[PROOF STEP]
apply (rule_tac x="[\<SS>]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives [\<SS>] [\<SS>]
[PROOF STEP]
by simp


[STATEMENT]
lemma \<PP>_are_admissible: "p \<in> \<PP> \<Longrightarrow> admissible p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<PP> \<Longrightarrow> admissible p
[PROOF STEP]
proof (induct rule: \<PP>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. admissible []
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> admissible q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. admissible []
 2. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> admissible q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
admissible []

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> admissible q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> admissible q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
case (Induct p k u)
[PROOF STATE]
proof (state)
this:
?q \<in> \<P> k u \<Longrightarrow> admissible ?q
p \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<And>p k u. \<lbrakk>\<And>q. q \<in> \<P> k u \<Longrightarrow> admissible q; p \<in> \<P> k (Suc u)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
from Induct(2)[simplified]
[PROOF STATE]
proof (chain)
picking this:
p \<in> limit (Append (\<Y> (\<Z> k u) (\<P> k u) k) k) (\<P> k u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> limit (Append (\<Y> (\<Z> k u) (\<P> k u) k) k) (\<P> k u)

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
proof (induct rule: limit_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> admissible p
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
case (Init p)
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k u

goal (2 subgoals):
 1. \<And>p. p \<in> \<P> k u \<Longrightarrow> admissible p
 2. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
from Induct(1)[OF Init]
[PROOF STATE]
proof (chain)
picking this:
admissible p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
admissible p

goal (1 subgoal):
 1. admissible p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
admissible p

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
case (Iterate p Y)
[PROOF STATE]
proof (state)
this:
?q \<in> Y \<Longrightarrow> admissible ?q
p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
have "\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k
[PROOF STEP]
by (metis \<Z>.simps(2) \<Z>_subset_\<X>)
[PROOF STATE]
proof (state)
this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k
[PROOF STEP]
have 1: "Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y"
[PROOF STATE]
proof (prove)
using this:
\<Y> (\<Z> k u) (\<P> k u) k \<subseteq> \<X> k

goal (1 subgoal):
 1. Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y
[PROOF STEP]
by (rule Append_mono, simp)
[PROOF STATE]
proof (state)
this:
Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
have 2: "p \<in> Append (\<X> k) k Y \<Longrightarrow> admissible p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Append (\<X> k) k Y \<Longrightarrow> admissible p
[PROOF STEP]
apply (auto simp add: Append_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Y \<Longrightarrow> admissible p
[PROOF STEP]
by (simp add: Iterate)
[PROOF STATE]
proof (state)
this:
p \<in> Append (\<X> k) k Y \<Longrightarrow> admissible p

goal (1 subgoal):
 1. \<And>p Y. \<lbrakk>\<And>q. q \<in> Y \<Longrightarrow> admissible q; p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible p
[PROOF STEP]
apply (rule 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Append (\<X> k) k Y
[PROOF STEP]
using "1" Iterate(2)
[PROOF STATE]
proof (prove)
using this:
Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y \<subseteq> Append (\<X> k) k Y
p \<in> Append (\<Y> (\<Z> k u) (\<P> k u) k) k Y

goal (1 subgoal):
 1. p \<in> Append (\<X> k) k Y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
admissible p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
admissible p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prefix_of_empty_is_empty: "is_prefix q [] \<Longrightarrow> q = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix q [] \<Longrightarrow> q = []
[PROOF STEP]
by (metis  is_prefix_cons neq_Nil_conv)


[STATEMENT]
lemma subset_\
 :
  assumes leq: "k' < k \<or> (k' = k \<and> u' \<le> u)"
  shows "\
 k' u' \<subseteq> \
 k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
from leq
[PROOF STATE]
proof (chain)
picking this:
k' < k \<or> k' = k \<and> u' \<le> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k' < k \<or> k' = k \<and> u' \<le> u

goal (1 subgoal):
 1. \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
k' < k

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
have s1: "\
 k' u' \<subseteq> \<Q> k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \
 k' u' \<subseteq> \<Q> k'
[PROOF STEP]
by (rule_tac subset_\
\<Q>k)
[PROOF STATE]
proof (state)
this:
\
 k' u' \<subseteq> \<Q> k'

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
have s2: "\<Q> k' \<subseteq> \<Q> (k - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Q> k' \<subseteq> \<Q> (k - 1)
[PROOF STEP]
apply (rule_tac subset_\<Q>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' \<le> k - 1
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
k' < k

goal (1 subgoal):
 1. k' \<le> k - 1
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<Q> k' \<subseteq> \<Q> (k - 1)

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
from subset_\<Q>\
Suc[where k="k - 1"] 1
[PROOF STATE]
proof (chain)
picking this:
\<Q> (k - 1) \<subseteq> \
 (Suc (k - 1)) ?u
k' < k
[PROOF STEP]
have s3: "\<Q> (k - 1) \<subseteq> \
 k 0"
[PROOF STATE]
proof (prove)
using this:
\<Q> (k - 1) \<subseteq> \
 (Suc (k - 1)) ?u
k' < k

goal (1 subgoal):
 1. \<Q> (k - 1) \<subseteq> \
 k 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Q> (k - 1) \<subseteq> \
 k 0

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
have s4: "\
 k 0 \<subseteq> \
 k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \
 k 0 \<subseteq> \
 k u
[PROOF STEP]
by (rule_tac subset_\
k, simp)
[PROOF STATE]
proof (state)
this:
\
 k 0 \<subseteq> \
 k u

goal (2 subgoals):
 1. k' < k \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
 2. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
from s1 s2 s3 s4 subset_trans
[PROOF STATE]
proof (chain)
picking this:
\
 k' u' \<subseteq> \<Q> k'
\<Q> k' \<subseteq> \<Q> (k - 1)
\<Q> (k - 1) \<subseteq> \
 k 0
\
 k 0 \<subseteq> \
 k u
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?C\<rbrakk> \<Longrightarrow> ?A \<subseteq> ?C
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\
 k' u' \<subseteq> \<Q> k'
\<Q> k' \<subseteq> \<Q> (k - 1)
\<Q> (k - 1) \<subseteq> \
 k 0
\
 k 0 \<subseteq> \
 k u
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?C\<rbrakk> \<Longrightarrow> ?A \<subseteq> ?C

goal (1 subgoal):
 1. \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\
 k' u' \<subseteq> \
 k u

goal (1 subgoal):
 1. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
k' = k \<and> u' \<le> u

goal (1 subgoal):
 1. k' = k \<and> u' \<le> u \<Longrightarrow> \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
k' = k \<and> u' \<le> u

goal (1 subgoal):
 1. \
 k' u' \<subseteq> \
 k u
[PROOF STEP]
by (simp add : subset_\
k)
[PROOF STATE]
proof (state)
this:
\
 k' u' \<subseteq> \
 k u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\
 k' u' \<subseteq> \
 k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_path_is_elem[simp]: "[] \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> \<P> k u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<in> \<P> k u
[PROOF STEP]
have "[] \<in> \<P> 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> \<P> 0 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<in> \<P> 0 0

goal (1 subgoal):
 1. [] \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<in> \<P> 0 0
[PROOF STEP]
show "[] \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
[] \<in> \<P> 0 0

goal (1 subgoal):
 1. [] \<in> \<P> k u
[PROOF STEP]
by (metis le0 not_gr0 subsetCE subset_\<P>)
[PROOF STATE]
proof (state)
this:
[] \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_prefix_of_append:
  assumes "is_prefix p (a@b)"
  shows "is_prefix p a \<or> (\<exists> b'. b' \<noteq> [] \<and> is_prefix b' b \<and> p = a@b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix p a \<or> (\<exists>b'. b' \<noteq> [] \<and> is_prefix b' b \<and> p = a @ b')
[PROOF STEP]
apply (auto simp add: is_prefix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b'. b' = [] \<or> (\<forall>w. b' @ w \<noteq> b) \<or> p \<noteq> a @ b' \<Longrightarrow> \<exists>w. p @ w = a
[PROOF STEP]
by (metis append_Nil2 append_eq_append_conv2 assms is_prefix_cancel is_prefix_def)


[STATEMENT]
lemma prefix_is_continuation: "is_continuation k u p ts \<Longrightarrow> is_prefix ts' ts \<Longrightarrow>
  is_continuation k u p ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_continuation k u p ts; is_prefix ts' ts\<rbrakk> \<Longrightarrow> is_continuation k u p ts'
[PROOF STEP]
apply (auto simp add: is_continuation_def is_prefix_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>ts = ts' @ w; p \<in> \<P> (length (chars p)) u; k = length (chars p); admissible (p @ ts' @ w); \<forall>t\<in>set ts' \<union> set w. t \<in> \<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p)); \<forall>t\<in>set (butlast (ts' @ w)). chars_of_token t = []\<rbrakk> \<Longrightarrow> admissible (p @ ts')
 2. \<And>w a b. \<lbrakk>ts = ts' @ w; p \<in> \<P> (length (chars p)) u; k = length (chars p); admissible (p @ ts' @ w); \<forall>t\<in>set ts' \<union> set w. t \<in> \<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p)); \<forall>t\<in>set (butlast (ts' @ w)). chars_of_token t = []; (a, b) \<in> set (butlast ts')\<rbrakk> \<Longrightarrow> b = []
[PROOF STEP]
apply (metis \<L>\<^sub>P_split admissible_def append_assoc terminals_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w a b. \<lbrakk>ts = ts' @ w; p \<in> \<P> (length (chars p)) u; k = length (chars p); admissible (p @ ts' @ w); \<forall>t\<in>set ts' \<union> set w. t \<in> \<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p)); \<forall>t\<in>set (butlast (ts' @ w)). chars_of_token t = []; (a, b) \<in> set (butlast ts')\<rbrakk> \<Longrightarrow> b = []
[PROOF STEP]
using in_set_butlast_appendI
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (butlast ?xs) \<or> ?x \<in> set (butlast ?ys) \<Longrightarrow> ?x \<in> set (butlast (?xs @ ?ys))

goal (1 subgoal):
 1. \<And>w a b. \<lbrakk>ts = ts' @ w; p \<in> \<P> (length (chars p)) u; k = length (chars p); admissible (p @ ts' @ w); \<forall>t\<in>set ts' \<union> set w. t \<in> \<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p)); \<forall>t\<in>set (butlast (ts' @ w)). chars_of_token t = []; (a, b) \<in> set (butlast ts')\<rbrakk> \<Longrightarrow> b = []
[PROOF STEP]
by fastforce


[STATEMENT]
lemma charslength_0: "(\<forall> t \<in> set ts. chars_of_token t = []) = (charslength ts = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>t\<in>set ts. chars_of_token t = []) = (charslength ts = 0)
[PROOF STEP]
by (induct ts, auto)


[STATEMENT]
lemma is_continuation_in_\<P>: "is_continuation k u p ts \<Longrightarrow> p@ts \<in> \<P> k (Suc u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k u p ts \<Longrightarrow> p @ ts \<in> \<P> k (Suc u)
[PROOF STEP]
proof(induct ts rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_continuation k u p [] \<Longrightarrow> p @ [] \<in> \<P> k (Suc u)
 2. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_continuation k u p []

goal (2 subgoals):
 1. is_continuation k u p [] \<Longrightarrow> p @ [] \<in> \<P> k (Suc u)
 2. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p []

goal (1 subgoal):
 1. p @ [] \<in> \<P> k (Suc u)
[PROOF STEP]
apply (auto simp add: is_continuation_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> (length (chars p)) u; admissible p; k = length (chars p)\<rbrakk> \<Longrightarrow> p \<in> limit (Append (\<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p))) (length (chars p))) (\<P> (length (chars p)) u)
[PROOF STEP]
using subset_\<P>Suc
[PROOF STATE]
proof (prove)
using this:
\<P> ?k ?u \<subseteq> \<P> ?k (Suc ?u)

goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> (length (chars p)) u; admissible p; k = length (chars p)\<rbrakk> \<Longrightarrow> p \<in> limit (Append (\<Y> (\<Z> (length (chars p)) u) (\<P> (length (chars p)) u) (length (chars p))) (length (chars p))) (\<P> (length (chars p)) u)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p @ [] \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
case (snoc t ts)
[PROOF STATE]
proof (state)
this:
is_continuation k u p ts \<Longrightarrow> p @ ts \<in> \<P> k (Suc u)
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
from snoc(2)
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u p (ts @ [t])
[PROOF STEP]
have "is_continuation k u p ts"
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. is_continuation k u p ts
[PROOF STEP]
by (metis append_Nil2 is_prefix_cancel is_prefix_empty prefix_is_continuation)
[PROOF STATE]
proof (state)
this:
is_continuation k u p ts

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
note induct = snoc(1)[OF this]
[PROOF STATE]
proof (state)
this:
p @ ts \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p @ ts \<in> \<P> k (Suc u)
[PROOF STEP]
have pts: "p@ts \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)"
[PROOF STATE]
proof (prove)
using this:
p @ ts \<in> \<P> k (Suc u)

goal (1 subgoal):
 1. p @ ts \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p @ ts \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
note is_cont = snoc(2)
[PROOF STATE]
proof (state)
this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u p (ts @ [t])
[PROOF STEP]
have admissible: "admissible (p@ts@[t])"
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. admissible (p @ ts @ [t])
[PROOF STEP]
by (simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
admissible (p @ ts @ [t])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
from is_cont
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u p (ts @ [t])
[PROOF STEP]
have t: "t \<in> \<Z> k (Suc u)"
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. t \<in> \<Z> k (Suc u)
[PROOF STEP]
by (simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
t \<in> \<Z> k (Suc u)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
from is_cont
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u p (ts @ [t])
[PROOF STEP]
have "\<forall> t \<in> set ts. chars_of_token t = []"
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. \<forall>t\<in>set ts. chars_of_token t = []
[PROOF STEP]
by (simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. chars_of_token t = []

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set ts. chars_of_token t = []
[PROOF STEP]
have charslength_ts: "charslength ts = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. chars_of_token t = []

goal (1 subgoal):
 1. charslength ts = 0
[PROOF STEP]
by (simp only: charslength_0)
[PROOF STATE]
proof (state)
this:
charslength ts = 0

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
from is_cont
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u p (ts @ [t])
[PROOF STEP]
have plen: "charslength p = k"
[PROOF STATE]
proof (prove)
using this:
is_continuation k u p (ts @ [t])

goal (1 subgoal):
 1. charslength p = k
[PROOF STEP]
by (simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
charslength p = k

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>is_continuation k u p xs \<Longrightarrow> p @ xs \<in> \<P> k (Suc u); is_continuation k u p (xs @ [x])\<rbrakk> \<Longrightarrow> p @ xs @ [x] \<in> \<P> k (Suc u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ ts @ [t] \<in> \<P> k (Suc u)
[PROOF STEP]
apply (simp only: \<P>.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ ts @ [t] \<in> limit (Append (\<Z> k (Suc u)) k) (\<P> k u)
[PROOF STEP]
apply (rule_tac limit_step_pointwise[OF pts])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pointwise (Append (\<Z> k (Suc u)) k)
 2. p @ ts @ [t] \<in> Append (\<Z> k (Suc u)) k {p @ ts}
[PROOF STEP]
apply (simp add: pointwise_Append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ ts @ [t] \<in> Append (\<Z> k (Suc u)) k {p @ ts}
[PROOF STEP]
apply (auto simp add: Append_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b. t = (a, b) \<and> length (chars p) + length (chars ts) = k \<and> (a, b) \<in> \<Y> (\<Z> k u) (\<P> k u) k \<and> admissible (p @ ts @ [(a, b)])
[PROOF STEP]
apply (rule_tac x="fst t" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. t = (fst t, b) \<and> length (chars p) + length (chars ts) = k \<and> (fst t, b) \<in> \<Y> (\<Z> k u) (\<P> k u) k \<and> admissible (p @ ts @ [(fst t, b)])
[PROOF STEP]
apply (rule_tac x="snd t" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = (fst t, snd t) \<and> length (chars p) + length (chars ts) = k \<and> (fst t, snd t) \<in> \<Y> (\<Z> k u) (\<P> k u) k \<and> admissible (p @ ts @ [(fst t, snd t)])
[PROOF STEP]
apply (auto simp add: admissible)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (chars p) + length (chars ts) = k
 2. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
using charslength_ts
[PROOF STATE]
proof (prove)
using this:
charslength ts = 0

goal (2 subgoals):
 1. length (chars p) + length (chars ts) = k
 2. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. chars ts = [] \<Longrightarrow> length (chars p) = k
 2. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
using plen
[PROOF STATE]
proof (prove)
using this:
charslength p = k

goal (2 subgoals):
 1. chars ts = [] \<Longrightarrow> length (chars p) = k
 2. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
t \<in> \<Z> k (Suc u)

goal (1 subgoal):
 1. t \<in> \<Y> (\<Z> k u) (\<P> k u) k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p @ ts @ [t] \<in> \<P> k (Suc u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma indexlt_subset_\<P>: "indexlt k' u' k u \<Longrightarrow> \<P> k' (Suc u') \<subseteq> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indexlt k' u' k u \<Longrightarrow> \<P> k' (Suc u') \<subseteq> \<P> k u
[PROOF STEP]
apply (rule_tac subset_\<P>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indexlt k' u' k u \<Longrightarrow> k' < k \<or> k' = k \<and> Suc u' \<le> u
[PROOF STEP]
apply (simp add: indexlt_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < k \<or> k' = k \<and> u' < u \<Longrightarrow> k' < k \<or> k' = k \<and> Suc u' \<le> u
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prefixes_are_paths: "p \<in> \<P> k u \<Longrightarrow> is_prefix x p \<Longrightarrow> x \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k u; is_prefix x p\<rbrakk> \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
proof (induct arbitrary: x rule: \<P>_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u x. \<lbrakk>\<And>p' k' u' x. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; is_prefix x p'\<rbrakk> \<Longrightarrow> x \<in> \<P> k' u'; p \<in> \<P> k u; is_prefix x p\<rbrakk> \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
case (Induct p k u)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p' \<in> \<P> ?k' ?u'; indexlt ?k' ?u' k u; is_prefix ?x ?p'\<rbrakk> \<Longrightarrow> ?x \<in> \<P> ?k' ?u'
p \<in> \<P> k u
is_prefix x p

goal (1 subgoal):
 1. \<And>p k u x. \<lbrakk>\<And>p' k' u' x. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; is_prefix x p'\<rbrakk> \<Longrightarrow> x \<in> \<P> k' u'; p \<in> \<P> k u; is_prefix x p\<rbrakk> \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
proof (cases "p = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> x \<in> \<P> k u
 2. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> x \<in> \<P> k u
 2. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = []
[PROOF STEP]
have "x = []"
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. x = []
[PROOF STEP]
using Induct.prems prefix_of_empty_is_empty
[PROOF STATE]
proof (prove)
using this:
p = []
is_prefix x p
is_prefix ?q [] \<Longrightarrow> ?q = []

goal (1 subgoal):
 1. x = []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> x \<in> \<P> k u
 2. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = []
[PROOF STEP]
show "x \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
x = []

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k u

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> []

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
from final_step_of_path[OF Induct(2) False]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
[PROOF STEP]
obtain q ts k' u' where step: "p = q@ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. (\<And>q ts k' u'. p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
have subset: "\<P> k' u' \<subseteq> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<P> k' u' \<subseteq> \<P> k u
[PROOF STEP]
by (metis indexlt_simp less_or_eq_imp_le step subset_\<P>)
[PROOF STATE]
proof (state)
this:
\<P> k' u' \<subseteq> \<P> k u

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
have "is_prefix x q \<or> (\<exists> ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q@ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix x q \<or> (\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts')
[PROOF STEP]
apply (rule_tac is_prefix_of_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix x (q @ ts)
[PROOF STEP]
using Induct(3) step
[PROOF STATE]
proof (prove)
using this:
is_prefix x p
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. is_prefix x (q @ ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_prefix x q \<or> (\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts')

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_prefix x q \<or> (\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_prefix x q \<or> (\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts')

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_prefix x q \<Longrightarrow> x \<in> \<P> k u
 2. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
is_prefix x q

goal (2 subgoals):
 1. is_prefix x q \<Longrightarrow> x \<in> \<P> k u
 2. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
have x: "x \<in> \<P> k' u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<P> k' u'
[PROOF STEP]
using 1 Induct step
[PROOF STATE]
proof (prove)
using this:
is_prefix x q
\<lbrakk>?p' \<in> \<P> ?k' ?u'; indexlt ?k' ?u' k u; is_prefix ?x ?p'\<rbrakk> \<Longrightarrow> ?x \<in> \<P> ?k' ?u'
p \<in> \<P> k u
is_prefix x p
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. x \<in> \<P> k' u'
[PROOF STEP]
by (auto simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k' u'

goal (2 subgoals):
 1. is_prefix x q \<Longrightarrow> x \<in> \<P> k u
 2. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<P> k' u'
[PROOF STEP]
show "x \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<P> k' u'

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
using subset subsetCE
[PROOF STATE]
proof (prove)
using this:
x \<in> \<P> k' u'
\<P> k' u' \<subseteq> \<P> k u
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?A \<Longrightarrow> ?P; ?c \<in> ?B \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k u

goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts'

goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts'
[PROOF STEP]
obtain ts' where ts': "is_prefix ts' ts \<and> x = q@ts'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts'

goal (1 subgoal):
 1. (\<And>ts'. is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_prefix ts' ts \<and> x = q @ ts'

goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
have "is_continuation k' u' q ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k' u' q ts'
[PROOF STEP]
using step prefix_is_continuation ts'
[PROOF STATE]
proof (prove)
using this:
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts
\<lbrakk>is_continuation ?k ?u ?p ?ts; is_prefix ?ts' ?ts\<rbrakk> \<Longrightarrow> is_continuation ?k ?u ?p ?ts'
is_prefix ts' ts \<and> x = q @ ts'

goal (1 subgoal):
 1. is_continuation k' u' q ts'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_continuation k' u' q ts'

goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
with ts'
[PROOF STATE]
proof (chain)
picking this:
is_prefix ts' ts \<and> x = q @ ts'
is_continuation k' u' q ts'
[PROOF STEP]
have "x \<in> \<P> k' (Suc u')"
[PROOF STATE]
proof (prove)
using this:
is_prefix ts' ts \<and> x = q @ ts'
is_continuation k' u' q ts'

goal (1 subgoal):
 1. x \<in> \<P> k' (Suc u')
[PROOF STEP]
apply (simp only: ts')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True \<and> q @ ts' = q @ ts'; is_continuation k' u' q ts'\<rbrakk> \<Longrightarrow> q @ ts' \<in> \<P> k' (Suc u')
[PROOF STEP]
apply (rule_tac is_continuation_in_\<P>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True \<and> q @ ts' = q @ ts'; is_continuation k' u' q ts'\<rbrakk> \<Longrightarrow> is_continuation k' u' q ts'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k' (Suc u')

goal (1 subgoal):
 1. \<exists>ts'. ts' \<noteq> [] \<and> is_prefix ts' ts \<and> x = q @ ts' \<Longrightarrow> x \<in> \<P> k u
[PROOF STEP]
with subset
[PROOF STATE]
proof (chain)
picking this:
\<P> k' u' \<subseteq> \<P> k u
x \<in> \<P> k' (Suc u')
[PROOF STEP]
show "x \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
\<P> k' u' \<subseteq> \<P> k u
x \<in> \<P> k' (Suc u')

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
using indexlt_subset_\<P> step
[PROOF STATE]
proof (prove)
using this:
\<P> k' u' \<subseteq> \<P> k u
x \<in> \<P> k' (Suc u')
indexlt ?k' ?u' ?k ?u \<Longrightarrow> \<P> ?k' (Suc ?u') \<subseteq> \<P> ?k ?u
p = q @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' q ts

goal (1 subgoal):
 1. x \<in> \<P> k u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_or_last_of_suffix:
  assumes "q = q' @ [t]"
  assumes "q = p @ ts"
  shows "ts = [] \<or> (\<exists> ts'. q' = p @ ts' \<and> ts'@[t] = ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts = [] \<or> (\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts)
[PROOF STEP]
by (metis assms(1) assms(2) butlast_append last_appendR snoc_eq_iff_butlast)


[STATEMENT]
lemma is_prefix_butlast: "is_prefix q (butlast p) \<Longrightarrow> is_prefix q p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix q (butlast p) \<Longrightarrow> is_prefix q p
[PROOF STEP]
by (metis butlast_conv_take is_prefix_append is_prefix_def is_prefix_take)


[STATEMENT]
lemma last_step_of_path:
  "q \<in> \<P> k u \<Longrightarrow> q = q'@[t] \<Longrightarrow>
   \<exists> k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q \<in> \<P> k u; q = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
proof (induct arbitrary: q' t rule: \<P>_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
case (Induct q k u)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p' \<in> \<P> ?k' ?u'; indexlt ?k' ?u' k u; ?p' = ?q' @ [?t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' ?k' ?u' \<and> ?p' \<in> \<P> k' (Suc u') \<and> charslength ?q' = k' \<and> ?t \<in> \<Z> k' (Suc u')
q \<in> \<P> k u
q = q' @ [t]

goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
have "\<exists> p ts k' u'. q = p@ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p ts k' u'. q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
[PROOF STEP]
apply (rule_tac final_step_of_path)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q \<in> \<P> k u
 2. q \<noteq> []
[PROOF STEP]
apply (simp add: Induct(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> []
[PROOF STEP]
apply (simp add: Induct(3))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>p ts k' u'. q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts

goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p ts k' u'. q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
[PROOF STEP]
obtain p ts k' u' where pts: "q = p@ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>p ts k' u'. q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts

goal (1 subgoal):
 1. (\<And>p ts k' u'. q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts

goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
[PROOF STEP]
have indexlt: "indexlt k' u' k u"
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts

goal (1 subgoal):
 1. indexlt k' u' k u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indexlt k' u' k u

goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
from pts
[PROOF STATE]
proof (chain)
picking this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
[PROOF STEP]
have "ts = [] \<or> (\<exists> ts'. q' = p @ ts' \<and> ts'@[t] = ts)"
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts

goal (1 subgoal):
 1. ts = [] \<or> (\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts)
[PROOF STEP]
by (metis empty_or_last_of_suffix Induct(3))
[PROOF STATE]
proof (state)
this:
ts = [] \<or> (\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts)

goal (1 subgoal):
 1. \<And>p k u q' t. \<lbrakk>\<And>p' k' u' q' t. \<lbrakk>p' \<in> \<P> k' u'; indexlt k' u' k u; p' = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k'a u'a. indexlt k'a u'a k' u' \<and> p' \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a); p \<in> \<P> k u; p = q' @ [t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> p \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts = [] \<or> (\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts = [] \<or> (\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts)

goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ts = [] \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
 2. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
ts = []

goal (2 subgoals):
 1. ts = [] \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
 2. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
with pts
[PROOF STATE]
proof (chain)
picking this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
ts = []
[PROOF STEP]
have q: "q \<in> \<P> k' u'"
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
ts = []

goal (1 subgoal):
 1. q \<in> \<P> k' u'
[PROOF STEP]
by (auto simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k' u'

goal (2 subgoals):
 1. ts = [] \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
 2. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
from Induct(1)[OF this indexlt Induct(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'a u'a. indexlt k'a u'a k' u' \<and> q \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>k'a u'a. indexlt k'a u'a k' u' \<and> q \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a)

goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
using indexlt indexlt_trans
[PROOF STATE]
proof (prove)
using this:
\<exists>k'a u'a. indexlt k'a u'a k' u' \<and> q \<in> \<P> k'a (Suc u'a) \<and> charslength q' = k'a \<and> t \<in> \<Z> k'a (Suc u'a)
indexlt k' u' k u
\<lbrakk>indexlt ?k'' ?u'' ?k' ?u'; indexlt ?k' ?u' ?k ?u\<rbrakk> \<Longrightarrow> indexlt ?k'' ?u'' ?k ?u

goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts
[PROOF STEP]
obtain ts' where ts': "q' = p @ ts' \<and> ts'@[t] = ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. (\<And>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q' = p @ ts' \<and> ts' @ [t] = ts
[PROOF STEP]
have "is_prefix ts' ts"
[PROOF STATE]
proof (prove)
using this:
q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. is_prefix ts' ts
[PROOF STEP]
using is_prefix_def
[PROOF STATE]
proof (prove)
using this:
q' = p @ ts' \<and> ts' @ [t] = ts
is_prefix ?u ?v = (\<exists>w. ?u @ w = ?v)

goal (1 subgoal):
 1. is_prefix ts' ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_prefix ts' ts

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_prefix ts' ts
[PROOF STEP]
have "is_continuation k' u' p ts'"
[PROOF STATE]
proof (prove)
using this:
is_prefix ts' ts

goal (1 subgoal):
 1. is_continuation k' u' p ts'
[PROOF STEP]
by (metis prefix_is_continuation pts)
[PROOF STATE]
proof (state)
this:
is_continuation k' u' p ts'

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
have "charslength ts' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength ts' = 0
[PROOF STEP]
using charslength_0 is_continuation_def pts ts'
[PROOF STATE]
proof (prove)
using this:
(\<forall>t\<in>set ?ts. chars_of_token t = []) = (charslength ?ts = 0)
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. charslength ts' = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength ts' = 0

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
charslength ts' = 0
[PROOF STEP]
have q'len: "charslength q' = k'"
[PROOF STATE]
proof (prove)
using this:
charslength ts' = 0

goal (1 subgoal):
 1. charslength q' = k'
[PROOF STEP]
using is_continuation_def pts ts'
[PROOF STATE]
proof (prove)
using this:
charslength ts' = 0
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. charslength q' = k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength q' = k'

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
have "t \<in> set ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> set ts
[PROOF STEP]
using ts'
[PROOF STATE]
proof (prove)
using this:
q' = p @ ts' \<and> ts' @ [t] = ts

goal (1 subgoal):
 1. t \<in> set ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> set ts

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
with pts
[PROOF STATE]
proof (chain)
picking this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
t \<in> set ts
[PROOF STEP]
have t_in_\<Z>: "t \<in> \<Z> k' (Suc u')"
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
t \<in> set ts

goal (1 subgoal):
 1. t \<in> \<Z> k' (Suc u')
[PROOF STEP]
using is_continuation_def
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
t \<in> set ts
is_continuation ?k ?u ?q ?ts = (?q \<in> \<P> ?k ?u \<and> charslength ?q = ?k \<and> admissible (?q @ ?ts) \<and> (\<forall>t\<in>set ?ts. t \<in> \<Z> ?k (Suc ?u)) \<and> (\<forall>t\<in>set (butlast ?ts). chars_of_token t = []))

goal (1 subgoal):
 1. t \<in> \<Z> k' (Suc u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
have q_dom: "q \<in> \<P> k' (Suc u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> \<P> k' (Suc u')
[PROOF STEP]
using pts is_continuation_in_\<P>
[PROOF STATE]
proof (prove)
using this:
q = p @ ts \<and> indexlt k' u' k u \<and> is_continuation k' u' p ts
is_continuation ?k ?u ?p ?ts \<Longrightarrow> ?p @ ?ts \<in> \<P> ?k (Suc ?u)

goal (1 subgoal):
 1. q \<in> \<P> k' (Suc u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> \<P> k' (Suc u')

goal (1 subgoal):
 1. \<exists>ts'. q' = p @ ts' \<and> ts' @ [t] = ts \<Longrightarrow> \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
apply (rule_tac x=k' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
apply (rule_tac x=u' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
by (simp only: indexlt q'len t_in_\<Z> q_dom)
[PROOF STATE]
proof (state)
this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma charslength_of_butlast_0: "p \<in> \<P> k 0 \<Longrightarrow> p = q@[t] \<Longrightarrow> charslength q < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k 0; p = q @ [t]\<rbrakk> \<Longrightarrow> charslength q < k
[PROOF STEP]
using last_step_of_path LocalLexing_axioms indexlt_simp
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> \<P> ?k ?u; ?q = ?q' @ [?t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' ?k ?u \<and> ?q \<in> \<P> k' (Suc u') \<and> charslength ?q' = k' \<and> ?t \<in> \<Z> k' (Suc u')
LocalLexing \<NN> \<TT> \<RR> \<SS> Lex Sel
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)

goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k 0; p = q @ [t]\<rbrakk> \<Longrightarrow> charslength q < k
[PROOF STEP]
by blast


[STATEMENT]
lemma charslength_of_butlast: "p \<in> \<P> k u \<Longrightarrow> p = q@[t] \<Longrightarrow> charslength q \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k u; p = q @ [t]\<rbrakk> \<Longrightarrow> charslength q \<le> k
[PROOF STEP]
by (metis indexlt_simp last_step_of_path eq_imp_le less_imp_le_nat)


[STATEMENT]
lemma last_token_of_path:
  assumes "q \<in> \<P> k u"
  assumes "q = q'@[t]"
  assumes "charslength q' = k"
  shows "t \<in> \<Z> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
q \<in> \<P> k u
q = q' @ [t]
charslength q' = k
[PROOF STEP]
have "\<exists> k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and>
    t \<in> \<Z> k' (Suc u')"
[PROOF STATE]
proof (prove)
using this:
q \<in> \<P> k u
q = q' @ [t]
charslength q' = k

goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
using last_step_of_path
[PROOF STATE]
proof (prove)
using this:
q \<in> \<P> k u
q = q' @ [t]
charslength q' = k
\<lbrakk>?q \<in> \<P> ?k ?u; ?q = ?q' @ [?t]\<rbrakk> \<Longrightarrow> \<exists>k' u'. indexlt k' u' ?k ?u \<and> ?q \<in> \<P> k' (Suc u') \<and> charslength ?q' = k' \<and> ?t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. \<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
obtain k' u' where th: "indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and>
    t \<in> \<Z> k' (Suc u')"
[PROOF STATE]
proof (prove)
using this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. (\<And>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
charslength q' = k
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
[PROOF STEP]
have k': "k' = k"
[PROOF STATE]
proof (prove)
using this:
charslength q' = k
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')

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

goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
with th
[PROOF STATE]
proof (chain)
picking this:
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
k' = k
[PROOF STEP]
have "t \<in> \<Z> k' (Suc u') \<and> u' < u"
[PROOF STATE]
proof (prove)
using this:
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
k' = k

goal (1 subgoal):
 1. t \<in> \<Z> k' (Suc u') \<and> u' < u
[PROOF STEP]
using indexlt_simp
[PROOF STATE]
proof (prove)
using this:
indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength q' = k' \<and> t \<in> \<Z> k' (Suc u')
k' = k
indexlt ?k' ?u' ?k ?u = (?k' < ?k \<or> ?k' = ?k \<and> ?u' < ?u)

goal (1 subgoal):
 1. t \<in> \<Z> k' (Suc u') \<and> u' < u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> \<Z> k' (Suc u') \<and> u' < u

goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> \<Z> k' (Suc u') \<and> u' < u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<in> \<Z> k' (Suc u') \<and> u' < u

goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
by (metis (no_types, opaque_lifting) \<Z>_subset_Suc k' linorder_neqE_nat not_less_eq
      subsetCE subset_fSuc_strict)
[PROOF STATE]
proof (state)
this:
t \<in> \<Z> k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma final_step_of_path': "p \<in> \<P> k u \<Longrightarrow> p \<notin> \<P> k (u - 1) \<Longrightarrow>
  \<exists> q ts. u > 0 \<and> p = q@ts \<and> is_continuation k (u - 1) q ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k u; p \<notin> \<P> k (u - 1)\<rbrakk> \<Longrightarrow> \<exists>q ts. 0 < u \<and> p = q @ ts \<and> is_continuation k (u - 1) q ts
[PROOF STEP]
by (metis Suc_diff_1 \<P>.simps(2) diff_0_eq_0 limit_Append_path_nonelem_split' not_gr0)


[STATEMENT]
lemma is_continuation_continue:
  assumes "is_continuation k u q ts"
  assumes "charslength ts = 0"
  assumes "t \<in> \<Z> k (Suc u)"
  assumes "admissible (q @ ts @ [t])"
  shows "is_continuation k u q (ts@[t])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k u q (ts @ [t])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_continuation k u q (ts @ [t])
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_continuation k u q ts
charslength ts = 0
t \<in> \<Z> k (Suc u)
admissible (q @ ts @ [t])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_continuation k u q ts
charslength ts = 0
t \<in> \<Z> k (Suc u)
admissible (q @ ts @ [t])

goal (1 subgoal):
 1. is_continuation k u q (ts @ [t])
[PROOF STEP]
by (simp add: is_continuation_def charslength_0)
[PROOF STATE]
proof (state)
this:
is_continuation k u q (ts @ [t])

goal:
No subgoals!
[PROOF STEP]
qed