[STATEMENT]
lemma Derives1_X_is_part_of_rule[consumes 2, case_names Suffix Prefix]:
  assumes aXb: "Derives1 \<delta> i r (a@[X]@b)"
  assumes split: "splits_at \<delta> i \<alpha> N \<beta>"
  assumes prefix: "\<And> \<beta>. \<delta> = a @ [X] @ \<beta> \<Longrightarrow> length a < i \<Longrightarrow>
                     Derives1 \<beta> (i - length a - 1) r b \<Longrightarrow> False"
  assumes suffix: "\<And> \<alpha>. \<delta> = \<alpha> @ [X] @ b \<Longrightarrow> Derives1 \<alpha> i r a \<Longrightarrow> False"
  shows "\<exists> u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> (snd r) = u@[X]@v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
have prefix_or: "is_prefix \<alpha> a \<or> is_proper_prefix a \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix \<alpha> a \<or> is_proper_prefix a \<alpha>
[PROOF STEP]
by (metis Derives1_prefix split aXb is_prefix_eq_proper_prefix)
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a \<or> is_proper_prefix a \<alpha>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
have "is_proper_prefix a \<alpha> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
assume proper:"is_proper_prefix a \<alpha>"
[PROOF STATE]
proof (state)
this:
is_proper_prefix a \<alpha>

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_proper_prefix a \<alpha>
[PROOF STEP]
have "\<exists> u. u \<noteq> [] \<and> \<alpha> = a@u"
[PROOF STATE]
proof (prove)
using this:
is_proper_prefix a \<alpha>

goal (1 subgoal):
 1. \<exists>u. u \<noteq> [] \<and> \<alpha> = a @ u
[PROOF STEP]
by (metis is_proper_prefix_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<noteq> [] \<and> \<alpha> = a @ u

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. u \<noteq> [] \<and> \<alpha> = a @ u
[PROOF STEP]
obtain u where u: "u \<noteq> [] \<and> \<alpha> = a@u"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. u \<noteq> [] \<and> \<alpha> = a @ u

goal (1 subgoal):
 1. (\<And>u. u \<noteq> [] \<and> \<alpha> = a @ u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<noteq> [] \<and> \<alpha> = a @ u

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
note splits_at = splits_at_\<alpha>[OF aXb split] splits_at_combine[OF split]
[PROOF STATE]
proof (state)
this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have \<alpha>1: "\<alpha> = take i \<delta>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<alpha> = take i \<delta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> = take i \<delta>

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have \<alpha>2: "\<alpha> = take i (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<alpha> = take i (a @ [X] @ b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> = take i (a @ [X] @ b)

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have len\<alpha>: "length \<alpha> = i"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. length \<alpha> = i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length \<alpha> = i

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
with proper
[PROOF STATE]
proof (chain)
picking this:
is_proper_prefix a \<alpha>
length \<alpha> = i
[PROOF STEP]
have lena: "length a < i"
[PROOF STATE]
proof (prove)
using this:
is_proper_prefix a \<alpha>
length \<alpha> = i

goal (1 subgoal):
 1. length a < i
[PROOF STEP]
using append_eq_conv_conj drop_eq_Nil leI u
[PROOF STATE]
proof (prove)
using this:
is_proper_prefix a \<alpha>
length \<alpha> = i
(?xs @ ?ys = ?zs) = (?xs = take (length ?xs) ?zs \<and> ?ys = drop (length ?xs) ?zs)
(drop ?n ?xs = []) = (length ?xs \<le> ?n)
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x
u \<noteq> [] \<and> \<alpha> = a @ u

goal (1 subgoal):
 1. length a < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length a < i

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
from u \<alpha>2
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> [] \<and> \<alpha> = a @ u
\<alpha> = take i (a @ [X] @ b)
[PROOF STEP]
have "a@u = take i (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> [] \<and> \<alpha> = a @ u
\<alpha> = take i (a @ [X] @ b)

goal (1 subgoal):
 1. a @ u = take i (a @ [X] @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a @ u = take i (a @ [X] @ b)

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
with lena
[PROOF STATE]
proof (chain)
picking this:
length a < i
a @ u = take i (a @ [X] @ b)
[PROOF STEP]
have "u = take (i - length a) ([X]@b)"
[PROOF STATE]
proof (prove)
using this:
length a < i
a @ u = take i (a @ [X] @ b)

goal (1 subgoal):
 1. u = take (i - length a) ([X] @ b)
[PROOF STEP]
by (simp add: less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
u = take (i - length a) ([X] @ b)

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
with lena
[PROOF STATE]
proof (chain)
picking this:
length a < i
u = take (i - length a) ([X] @ b)
[PROOF STEP]
have uX: "u = [X]@(take (i - length a - 1) b)"
[PROOF STATE]
proof (prove)
using this:
length a < i
u = take (i - length a) ([X] @ b)

goal (1 subgoal):
 1. u = [X] @ take (i - length a - 1) b
[PROOF STEP]
by (simp add: not_less take_Cons')
[PROOF STATE]
proof (state)
this:
u = [X] @ take (i - length a - 1) b

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
let ?\<beta> = "(take (i - length a - 1) b) @ [N] @ \<beta>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have f1: "\<delta> = \<alpha> @ [N] @ \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
with u uX
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> [] \<and> \<alpha> = a @ u
u = [X] @ take (i - length a - 1) b
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have f2: "\<delta> = a @ [X] @ ?\<beta>"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> [] \<and> \<alpha> = a @ u
u = [X] @ take (i - length a - 1) b
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<delta> = a @ [X] @ take (i - length a - 1) b @ [N] @ \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> = a @ [X] @ take (i - length a - 1) b @ [N] @ \<beta>

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
note skip = Derives1_skip_prefix[where a = "a @ [X]" and b = "?\<beta>" and
      r = r and i = i and c = b]
[PROOF STATE]
proof (state)
this:
\<lbrakk>length (a @ [X]) \<le> i; Derives1 ((a @ [X]) @ take (i - length a - 1) b @ [N] @ \<beta>) i r ((a @ [X]) @ b)\<rbrakk> \<Longrightarrow> Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length (a @ [X])) r b

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length (a @ [X]) \<le> i; Derives1 ((a @ [X]) @ take (i - length a - 1) b @ [N] @ \<beta>) i r ((a @ [X]) @ b)\<rbrakk> \<Longrightarrow> Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length (a @ [X])) r b
[PROOF STEP]
have D: "Derives1 ?\<beta> (i - length a - 1) r b"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length (a @ [X]) \<le> i; Derives1 ((a @ [X]) @ take (i - length a - 1) b @ [N] @ \<beta>) i r ((a @ [X]) @ b)\<rbrakk> \<Longrightarrow> Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length (a @ [X])) r b

goal (1 subgoal):
 1. Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length a - 1) r b
[PROOF STEP]
using One_nat_def Suc_leI aXb append_assoc diff_diff_left f2 lena length_Cons
        length_append length_append_singleton list.size(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length (a @ [X]) \<le> i; Derives1 ((a @ [X]) @ take (i - length a - 1) b @ [N] @ \<beta>) i r ((a @ [X]) @ b)\<rbrakk> \<Longrightarrow> Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length (a @ [X])) r b
1 = Suc 0
?m < ?n \<Longrightarrow> Suc ?m \<le> ?n
Derives1 \<delta> i r (a @ [X] @ b)
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs
?i - ?j - ?k = ?i - (?j + ?k)
\<delta> = a @ [X] @ take (i - length a - 1) b @ [N] @ \<beta>
length a < i
length (?x # ?xs) = Suc (length ?xs)
length (?xs @ ?ys) = length ?xs + length ?ys
length (?xs @ [?x]) = Suc (length ?xs)
length [] = 0

goal (1 subgoal):
 1. Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length a - 1) r b
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Derives1 (take (i - length a - 1) b @ [N] @ \<beta>) (i - length a - 1) r b

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
note prefix[OF f2 lena D]
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_proper_prefix a \<alpha> \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
with prefix_or
[PROOF STATE]
proof (chain)
picking this:
is_prefix \<alpha> a \<or> is_proper_prefix a \<alpha>
is_proper_prefix a \<alpha> \<Longrightarrow> False
[PROOF STEP]
have is_prefix: "is_prefix \<alpha> a"
[PROOF STATE]
proof (prove)
using this:
is_prefix \<alpha> a \<or> is_proper_prefix a \<alpha>
is_proper_prefix a \<alpha> \<Longrightarrow> False

goal (1 subgoal):
 1. is_prefix \<alpha> a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_prefix \<alpha> a

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from aXb
[PROOF STATE]
proof (chain)
picking this:
Derives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
have aXb': "Derives1 \<delta> i r ((a@[X])@b)"
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. Derives1 \<delta> i r ((a @ [X]) @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Derives1 \<delta> i r ((a @ [X]) @ b)

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
note  Derives1_suffix[OF aXb' split]
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b \<or> is_suffix b \<beta>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_suffix \<beta> b \<or> is_suffix b \<beta>
[PROOF STEP]
have suffix_or: "is_suffix \<beta> b \<or> is_proper_suffix b \<beta>"
[PROOF STATE]
proof (prove)
using this:
is_suffix \<beta> b \<or> is_suffix b \<beta>

goal (1 subgoal):
 1. is_suffix \<beta> b \<or> is_proper_suffix b \<beta>
[PROOF STEP]
by (metis is_suffix_eq_proper_suffix)
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b \<or> is_proper_suffix b \<beta>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
have "is_proper_suffix b \<beta> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
assume proper: "is_proper_suffix b \<beta>"
[PROOF STATE]
proof (state)
this:
is_proper_suffix b \<beta>

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_proper_suffix b \<beta>
[PROOF STEP]
have "\<exists> u. u \<noteq> [] \<and> \<beta> = u@b"
[PROOF STATE]
proof (prove)
using this:
is_proper_suffix b \<beta>

goal (1 subgoal):
 1. \<exists>u. u \<noteq> [] \<and> \<beta> = u @ b
[PROOF STEP]
by (metis is_proper_suffix_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<noteq> [] \<and> \<beta> = u @ b

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. u \<noteq> [] \<and> \<beta> = u @ b
[PROOF STEP]
obtain u where u: "u \<noteq> [] \<and> \<beta> = u@b"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. u \<noteq> [] \<and> \<beta> = u @ b

goal (1 subgoal):
 1. (\<And>u. u \<noteq> [] \<and> \<beta> = u @ b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<noteq> [] \<and> \<beta> = u @ b

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
note splits_at = splits_at_\<beta>[OF aXb split] splits_at_combine[OF split]
[PROOF STATE]
proof (state)
this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have \<beta>1: "\<beta> = drop (Suc i) \<delta>"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<beta> = drop (Suc i) \<delta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<beta> = drop (Suc i) \<delta>

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have \<beta>2: "\<beta> = drop (i + length (snd r)) (a @ [X] @ b)"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<beta> = drop (i + length (snd r)) (a @ [X] @ b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<beta> = drop (i + length (snd r)) (a @ [X] @ b)

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have len\<beta>: "length \<beta> = length \<delta> - i - 1"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. length \<beta> = length \<delta> - i - 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length \<beta> = length \<delta> - i - 1

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
with proper
[PROOF STATE]
proof (chain)
picking this:
is_proper_suffix b \<beta>
length \<beta> = length \<delta> - i - 1
[PROOF STEP]
have lenb: "length b < length \<beta>"
[PROOF STATE]
proof (prove)
using this:
is_proper_suffix b \<beta>
length \<beta> = length \<delta> - i - 1

goal (1 subgoal):
 1. length b < length \<beta>
[PROOF STEP]
by (metis is_proper_suffix_length_cmp)
[PROOF STATE]
proof (state)
this:
length b < length \<beta>

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from u \<beta>2
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> [] \<and> \<beta> = u @ b
\<beta> = drop (i + length (snd r)) (a @ [X] @ b)
[PROOF STEP]
have "u@b = drop (i + length (snd r)) ((a @ [X]) @ b)"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> [] \<and> \<beta> = u @ b
\<beta> = drop (i + length (snd r)) (a @ [X] @ b)

goal (1 subgoal):
 1. u @ b = drop (i + length (snd r)) ((a @ [X]) @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u @ b = drop (i + length (snd r)) ((a @ [X]) @ b)

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
hence "u = drop (i + length (snd r)) (a @ [X])"
[PROOF STATE]
proof (prove)
using this:
u @ b = drop (i + length (snd r)) ((a @ [X]) @ b)

goal (1 subgoal):
 1. u = drop (i + length (snd r)) (a @ [X])
[PROOF STEP]
by (metis drop_cancel_suffix)
[PROOF STATE]
proof (state)
this:
u = drop (i + length (snd r)) (a @ [X])

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
hence uX: "u = drop (i + length (snd r)) a @ [X]"
[PROOF STATE]
proof (prove)
using this:
u = drop (i + length (snd r)) (a @ [X])

goal (1 subgoal):
 1. u = drop (i + length (snd r)) a @ [X]
[PROOF STEP]
by (metis drop_keep_last u)
[PROOF STATE]
proof (state)
this:
u = drop (i + length (snd r)) a @ [X]

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
let ?\<alpha> = "\<alpha> @ [N] @ (drop (i + length (snd r)) a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from splits_at
[PROOF STATE]
proof (chain)
picking this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have f1: "\<delta> = \<alpha> @ [N] @ \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<beta> = drop (Suc i) \<delta> \<and> \<beta> = drop (i + length (snd r)) (a @ [X] @ b) \<and> length \<beta> = length \<delta> - i - 1
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
with u uX
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> [] \<and> \<beta> = u @ b
u = drop (i + length (snd r)) a @ [X]
\<delta> = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
have f2: "\<delta> = ?\<alpha> @ [X] @ b"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> [] \<and> \<beta> = u @ b
u = drop (i + length (snd r)) a @ [X]
\<delta> = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. \<delta> = (\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> = (\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
note skip = Derives1_skip_suffix[where a = "?\<alpha>" and c = "[X]@b" and b="a" and
      r = r and i = i]
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a); Derives1 ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) i r (a @ [X] @ b)\<rbrakk> \<Longrightarrow> Derives1 (\<alpha> @ [N] @ drop (i + length (snd r)) a) i r a

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
have f3: "i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
have f1: "1 + i + length b = length [X] + length b + i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + i + length b = length [X] + length b + i
[PROOF STEP]
by (metis Groups.add_ac(2) Suc_eq_plus1_left length_Cons list.size(3) list.size(4) semiring_normalization_rules(22))
[PROOF STATE]
proof (state)
this:
1 + i + length b = length [X] + length b + i

goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
have f2: "length \<delta> - i - 1 = length ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) - Suc i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<delta> - i - 1 = length ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) - Suc i
[PROOF STEP]
by (metis f2 length_drop splits_at(1))
[PROOF STATE]
proof (state)
this:
length \<delta> - i - 1 = length ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) - Suc i

goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
have "length ([]::symbol list) \<noteq> length \<delta> - i - 1 - length b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [] \<noteq> length \<delta> - i - 1 - length b
[PROOF STEP]
by (metis add_diff_cancel_right' append_Nil2 append_eq_append_conv len\<beta> length_append u)
[PROOF STATE]
proof (state)
this:
length [] \<noteq> length \<delta> - i - 1 - length b

goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [] \<noteq> length \<delta> - i - 1 - length b
[PROOF STEP]
have "length ([]::symbol list) \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i"
[PROOF STATE]
proof (prove)
using this:
length [] \<noteq> length \<delta> - i - 1 - length b

goal (1 subgoal):
 1. length [] \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i
[PROOF STEP]
using f2 f1
[PROOF STATE]
proof (prove)
using this:
length [] \<noteq> length \<delta> - i - 1 - length b
length \<delta> - i - 1 = length ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) - Suc i
1 + i + length b = length [X] + length b + i

goal (1 subgoal):
 1. length [] \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i
[PROOF STEP]
by (metis Suc_eq_plus1_left add_diff_cancel_right' diff_diff_left length_append)
[PROOF STATE]
proof (state)
this:
length [] \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i

goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [] \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length [] \<noteq> length \<alpha> + length ([N] @ drop (i + length (snd r)) a) - i

goal (1 subgoal):
 1. i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < length (\<alpha> @ [N] @ drop (i + length (snd r)) a)

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
from aXb f2
[PROOF STATE]
proof (chain)
picking this:
Derives1 \<delta> i r (a @ [X] @ b)
\<delta> = (\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b
[PROOF STEP]
have D: "Derives1 (?\<alpha> @ [X] @ b) i r (a@[X]@b)"
[PROOF STATE]
proof (prove)
using this:
Derives1 \<delta> i r (a @ [X] @ b)
\<delta> = (\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b

goal (1 subgoal):
 1. Derives1 ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) i r (a @ [X] @ b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Derives1 ((\<alpha> @ [N] @ drop (i + length (snd r)) a) @ [X] @ b) i r (a @ [X] @ b)

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
note skip[OF f3 D]
[PROOF STATE]
proof (state)
this:
Derives1 (\<alpha> @ [N] @ drop (i + length (snd r)) a) i r a

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
note suffix[OF f2  skip[OF f3 D]]
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_proper_suffix b \<beta> \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
with suffix_or
[PROOF STATE]
proof (chain)
picking this:
is_suffix \<beta> b \<or> is_proper_suffix b \<beta>
is_proper_suffix b \<beta> \<Longrightarrow> False
[PROOF STEP]
have is_suffix: "is_suffix \<beta> b"
[PROOF STATE]
proof (prove)
using this:
is_suffix \<beta> b \<or> is_proper_suffix b \<beta>
is_proper_suffix b \<beta> \<Longrightarrow> False

goal (1 subgoal):
 1. is_suffix \<beta> b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_suffix \<beta> b

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from is_prefix
[PROOF STATE]
proof (chain)
picking this:
is_prefix \<alpha> a
[PROOF STEP]
have "\<exists> u. a = \<alpha> @ u"
[PROOF STATE]
proof (prove)
using this:
is_prefix \<alpha> a

goal (1 subgoal):
 1. \<exists>u. a = \<alpha> @ u
[PROOF STEP]
by (auto simp add: is_prefix_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. a = \<alpha> @ u

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. a = \<alpha> @ u
[PROOF STEP]
obtain u where u: "a = \<alpha> @ u"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. a = \<alpha> @ u

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

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from is_suffix
[PROOF STATE]
proof (chain)
picking this:
is_suffix \<beta> b
[PROOF STEP]
have "\<exists> v. b = v @ \<beta>"
[PROOF STATE]
proof (prove)
using this:
is_suffix \<beta> b

goal (1 subgoal):
 1. \<exists>v. b = v @ \<beta>
[PROOF STEP]
by (auto simp add: is_suffix_def)
[PROOF STATE]
proof (state)
this:
\<exists>v. b = v @ \<beta>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. b = v @ \<beta>
[PROOF STEP]
obtain v where v: "b = v @ \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. b = v @ \<beta>

goal (1 subgoal):
 1. (\<And>v. b = v @ \<beta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = v @ \<beta>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from u v splits_at_combine[OF split] aXb
[PROOF STATE]
proof (chain)
picking this:
a = \<alpha> @ u
b = v @ \<beta>
\<delta> = \<alpha> @ [N] @ \<beta>
Derives1 \<delta> i r (a @ [X] @ b)
[PROOF STEP]
have D:"Derives1 (\<alpha>@[N]@\<beta>) i r (\<alpha>@(u@[X]@v)@\<beta>)"
[PROOF STATE]
proof (prove)
using this:
a = \<alpha> @ u
b = v @ \<beta>
\<delta> = \<alpha> @ [N] @ \<beta>
Derives1 \<delta> i r (a @ [X] @ b)

goal (1 subgoal):
 1. Derives1 (\<alpha> @ [N] @ \<beta>) i r (\<alpha> @ (u @ [X] @ v) @ \<beta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Derives1 (\<alpha> @ [N] @ \<beta>) i r (\<alpha> @ (u @ [X] @ v) @ \<beta>)

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from splits_at_\<alpha>[OF aXb split]
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i
[PROOF STEP]
have i: "length \<alpha> = i"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = take i \<delta> \<and> \<alpha> = take i (a @ [X] @ b) \<and> length \<alpha> = i

goal (1 subgoal):
 1. length \<alpha> = i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length \<alpha> = i

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
length \<alpha> = i
[PROOF STEP]
have i1: "length \<alpha> \<le> i" and i2: "i \<le> length \<alpha>"
[PROOF STATE]
proof (prove)
using this:
length \<alpha> = i

goal (1 subgoal):
 1. length \<alpha> \<le> i &&& i \<le> length \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length \<alpha> \<le> i
i \<le> length \<alpha>

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
note Derives1_skip_suffix[OF _ Derives1_skip_prefix[OF i1 D], simplified, OF i2]
[PROOF STATE]
proof (state)
this:
Derives1 [N] 0 r (u @ X # v)

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Derives1 [N] 0 r (u @ X # v)
[PROOF STEP]
have "Derives1 [N] 0 r (u @ [X] @ v)"
[PROOF STATE]
proof (prove)
using this:
Derives1 [N] 0 r (u @ X # v)

goal (1 subgoal):
 1. Derives1 [N] 0 r (u @ [X] @ v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Derives1 [N] 0 r (u @ [X] @ v)

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Derives1 [N] 0 r (u @ [X] @ v)
[PROOF STEP]
have r: "snd r = u @ [X] @ v"
[PROOF STATE]
proof (prove)
using this:
Derives1 [N] 0 r (u @ [X] @ v)

goal (1 subgoal):
 1. snd r = u @ [X] @ v
[PROOF STEP]
by (metis Derives1_split append_Cons append_Nil length_0_conv list.inject self_append_conv)
[PROOF STATE]
proof (state)
this:
snd r = u @ [X] @ v

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
using u v r
[PROOF STATE]
proof (prove)
using this:
a = \<alpha> @ u
b = v @ \<beta>
snd r = u @ [X] @ v

goal (1 subgoal):
 1. \<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u v. a = \<alpha> @ u \<and> b = v @ \<beta> \<and> snd r = u @ [X] @ v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<L>\<^sub>P_derives: "a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists> b. derives [\<SS>] (a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists>b. derives [\<SS>] (a @ b)
[PROOF STEP]
by (simp add: \<L>\<^sub>P_def is_derivation_def)


[STATEMENT]
lemma \<L>\<^sub>P_leftderives: "a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists> b. leftderives [\<SS>] (a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists>b. leftderives [\<SS>] (a @ b)
[PROOF STEP]
by (metis \<L>\<^sub>P_derives \<L>\<^sub>P_is_word derives_implies_leftderives_gen)


[STATEMENT]
lemma Derives1_rule: "Derives1 a i r b \<Longrightarrow> r \<in> \<RR>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 a i r b \<Longrightarrow> r \<in> \<RR>
[PROOF STEP]
by (auto simp add: Derives1_def)


[STATEMENT]
lemma is_prefix_empty[simp]: "is_prefix [] a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix [] a
[PROOF STEP]
by (simp add: is_prefix_def)


[STATEMENT]
lemma is_prefix_cons: "is_prefix (x # a) b = (\<exists> c. b = x # c \<and> is_prefix a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix (x # a) b = (\<exists>c. b = x # c \<and> is_prefix a c)
[PROOF STEP]
by (metis append_Cons is_prefix_def)


[STATEMENT]
lemma is_prefix_cancel[simp]: "is_prefix (a@b) (a@c) = is_prefix b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix (a @ b) (a @ c) = is_prefix b c
[PROOF STEP]
by (metis append_assoc is_prefix_def same_append_eq)


[STATEMENT]
lemma is_prefix_chars: "is_prefix a b \<Longrightarrow> is_prefix (chars a) (chars b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix a b \<Longrightarrow> is_prefix (chars a) (chars b)
[PROOF STEP]
proof (induct a arbitrary: b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. is_prefix [] b \<Longrightarrow> is_prefix (chars []) (chars b)
 2. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_prefix [] b

goal (2 subgoals):
 1. \<And>b. is_prefix [] b \<Longrightarrow> is_prefix (chars []) (chars b)
 2. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_prefix [] b

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

goal (1 subgoal):
 1. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
case (Cons x a)
[PROOF STATE]
proof (state)
this:
is_prefix a ?b \<Longrightarrow> is_prefix (chars a) (chars ?b)
is_prefix (x # a) b

goal (1 subgoal):
 1. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
is_prefix (x # a) b
[PROOF STEP]
have "\<exists> c. b = x # c \<and> is_prefix a c"
[PROOF STATE]
proof (prove)
using this:
is_prefix (x # a) b

goal (1 subgoal):
 1. \<exists>c. b = x # c \<and> is_prefix a c
[PROOF STEP]
by (simp add: is_prefix_cons)
[PROOF STATE]
proof (state)
this:
\<exists>c. b = x # c \<and> is_prefix a c

goal (1 subgoal):
 1. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. b = x # c \<and> is_prefix a c
[PROOF STEP]
obtain c where c: "b = x # c \<and> is_prefix a c"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. b = x # c \<and> is_prefix a c

goal (1 subgoal):
 1. (\<And>c. b = x # c \<and> is_prefix a c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = x # c \<and> is_prefix a c

goal (1 subgoal):
 1. \<And>a1 a2 b. \<lbrakk>\<And>b. is_prefix a2 b \<Longrightarrow> is_prefix (chars a2) (chars b); is_prefix (a1 # a2) b\<rbrakk> \<Longrightarrow> is_prefix (chars (a1 # a2)) (chars b)
[PROOF STEP]
from c Cons(1)
[PROOF STATE]
proof (chain)
picking this:
b = x # c \<and> is_prefix a c
is_prefix a ?b \<Longrightarrow> is_prefix (chars a) (chars ?b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
b = x # c \<and> is_prefix a c
is_prefix a ?b \<Longrightarrow> is_prefix (chars a) (chars ?b)

goal (1 subgoal):
 1. is_prefix (chars (x # a)) (chars b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_prefix (chars (x # a)) (chars b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_prefix_length: "is_prefix a b \<Longrightarrow> length a \<le> length b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix a b \<Longrightarrow> length a \<le> length b
[PROOF STEP]
by (auto simp add: is_prefix_def)


[STATEMENT]
lemma is_prefix_take[simp]: "is_prefix (take n a) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix (take n a) a
[PROOF STEP]
apply (auto simp add: is_prefix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>w. take n a @ w = a
[PROOF STEP]
apply (rule_tac x="drop n a" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take n a @ drop n a = a
[PROOF STEP]
by simp


[STATEMENT]
lemma doc_tokens_length: "doc_tokens p \<Longrightarrow> length (chars p) \<le> length Doc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doc_tokens p \<Longrightarrow> length (chars p) \<le> length Doc
[PROOF STEP]
by (metis doc_tokens_def is_prefix_length)


[STATEMENT]
lemma count_terminals_upper_bound: "count_terminals p \<le> length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals p \<le> length p
[PROOF STEP]
by (induct p, auto)


[STATEMENT]
lemma count_terminals_append[simp]: "count_terminals (a@b) = count_terminals a + count_terminals b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals (a @ b) = count_terminals a + count_terminals b
[PROOF STEP]
by (induct a arbitrary: b, auto)


[STATEMENT]
lemma Derives1_count_terminals:
  assumes D: "Derives1 a i r b"
  shows "count_terminals b = count_terminals a + count_terminals (snd r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
have "\<exists> \<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>
[PROOF STEP]
using D splits_at_ex
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r b
Derives1 ?\<delta> ?i ?r ?s \<Longrightarrow> \<exists>\<alpha> N \<beta>. splits_at ?\<delta> ?i \<alpha> N \<beta>

goal (1 subgoal):
 1. \<exists>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>
[PROOF STEP]
obtain \<alpha> N \<beta> where split: "splits_at a i \<alpha> N \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. (\<And>\<alpha> N \<beta>. splits_at a i \<alpha> N \<beta> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
from D split
[PROOF STATE]
proof (chain)
picking this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>
[PROOF STEP]
have N: "is_nonterminal N"
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. is_nonterminal N
[PROOF STEP]
by (simp add: Derives1_nonterminal)
[PROOF STATE]
proof (state)
this:
is_nonterminal N

goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
have a: "a = \<alpha> @ [N] @ \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = \<alpha> @ [N] @ \<beta>
[PROOF STEP]
by (metis split splits_at_combine)
[PROOF STATE]
proof (state)
this:
a = \<alpha> @ [N] @ \<beta>

goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
from D split
[PROOF STATE]
proof (chain)
picking this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>
[PROOF STEP]
have b: "b = \<alpha> @ (snd r) @ \<beta>"
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>

goal (1 subgoal):
 1. b = \<alpha> @ snd r @ \<beta>
[PROOF STEP]
using splits_at_combine_dest
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r b
splits_at a i \<alpha> N \<beta>
\<lbrakk>Derives1 ?a ?i ?r ?b; splits_at ?a ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> ?b = ?\<alpha> @ snd ?r @ ?\<beta>

goal (1 subgoal):
 1. b = \<alpha> @ snd r @ \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = \<alpha> @ snd r @ \<beta>

goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals b = count_terminals a + count_terminals (snd r)
[PROOF STEP]
apply (simp add: a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_terminal N
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
is_nonterminal N

goal (1 subgoal):
 1. \<not> is_terminal N
[PROOF STEP]
by (metis is_terminal_nonterminal)
[PROOF STATE]
proof (state)
this:
count_terminals b = count_terminals a + count_terminals (snd r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Derives1_count_terminals_leq:
  assumes D: "Derives1 a i r b"
  shows "count_terminals a \<le> count_terminals b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals a \<le> count_terminals b
[PROOF STEP]
by (metis Derives1_count_terminals assms le_less_linear not_add_less1)


[STATEMENT]
lemma Derivation_count_terminals_leq:
  "Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b
[PROOF STEP]
proof (induct E arbitrary: a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. Derivation a [] b \<Longrightarrow> count_terminals a \<le> count_terminals b
 2. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
Derivation a [] b

goal (2 subgoals):
 1. \<And>a. Derivation a [] b \<Longrightarrow> count_terminals a \<le> count_terminals b
 2. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Derivation a [] b

goal (1 subgoal):
 1. count_terminals a \<le> count_terminals b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
count_terminals a \<le> count_terminals b

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
case (Cons e E)
[PROOF STATE]
proof (state)
this:
Derivation ?a E b \<Longrightarrow> count_terminals ?a \<le> count_terminals b
Derivation a (e # E) b

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Derivation ?a E b \<Longrightarrow> count_terminals ?a \<le> count_terminals b
Derivation a (e # E) b
[PROOF STEP]
have "\<exists> x i r. Derives1 a i r x \<and> Derivation x E b"
[PROOF STATE]
proof (prove)
using this:
Derivation ?a E b \<Longrightarrow> count_terminals ?a \<le> count_terminals b
Derivation a (e # E) b

goal (1 subgoal):
 1. \<exists>x i r. Derives1 a i r x \<and> Derivation x E b
[PROOF STEP]
using Derivation.simps(2)
[PROOF STATE]
proof (prove)
using this:
Derivation ?a E b \<Longrightarrow> count_terminals ?a \<le> count_terminals b
Derivation a (e # E) b
Derivation ?a (?d # ?D) ?b = (\<exists>x. Derives1 ?a (fst ?d) (snd ?d) x \<and> Derivation x ?D ?b)

goal (1 subgoal):
 1. \<exists>x i r. Derives1 a i r x \<and> Derivation x E b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x i r. Derives1 a i r x \<and> Derivation x E b

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x i r. Derives1 a i r x \<and> Derivation x E b
[PROOF STEP]
obtain x i r where axb: "Derives1 a i r x \<and> Derivation x E b"
[PROOF STATE]
proof (prove)
using this:
\<exists>x i r. Derives1 a i r x \<and> Derivation x E b

goal (1 subgoal):
 1. (\<And>i r x. Derives1 a i r x \<and> Derivation x E b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Derives1 a i r x \<and> Derivation x E b

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
from axb
[PROOF STATE]
proof (chain)
picking this:
Derives1 a i r x \<and> Derivation x E b
[PROOF STEP]
have ax: "count_terminals a \<le> count_terminals x"
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r x \<and> Derivation x E b

goal (1 subgoal):
 1. count_terminals a \<le> count_terminals x
[PROOF STEP]
using Derives1_count_terminals_leq
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r x \<and> Derivation x E b
Derives1 ?a ?i ?r ?b \<Longrightarrow> count_terminals ?a \<le> count_terminals ?b

goal (1 subgoal):
 1. count_terminals a \<le> count_terminals x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
count_terminals a \<le> count_terminals x

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
from axb
[PROOF STATE]
proof (chain)
picking this:
Derives1 a i r x \<and> Derivation x E b
[PROOF STEP]
have xb: "count_terminals x \<le> count_terminals b"
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r x \<and> Derivation x E b

goal (1 subgoal):
 1. count_terminals x \<le> count_terminals b
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
Derives1 a i r x \<and> Derivation x E b
Derivation ?a E b \<Longrightarrow> count_terminals ?a \<le> count_terminals b
Derivation a (e # E) b

goal (1 subgoal):
 1. count_terminals x \<le> count_terminals b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_terminals x \<le> count_terminals b

goal (1 subgoal):
 1. \<And>a E aa. \<lbrakk>\<And>a. Derivation a E b \<Longrightarrow> count_terminals a \<le> count_terminals b; Derivation aa (a # E) b\<rbrakk> \<Longrightarrow> count_terminals aa \<le> count_terminals b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals a \<le> count_terminals b
[PROOF STEP]
using ax xb
[PROOF STATE]
proof (prove)
using this:
count_terminals a \<le> count_terminals x
count_terminals x \<le> count_terminals b

goal (1 subgoal):
 1. count_terminals a \<le> count_terminals b
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
count_terminals a \<le> count_terminals b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derives_count_terminals_leq: "derives a b \<Longrightarrow> count_terminals a \<le> count_terminals b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives a b \<Longrightarrow> count_terminals a \<le> count_terminals b
[PROOF STEP]
using Derivation_count_terminals_leq derives_implies_Derivation
[PROOF STATE]
proof (prove)
using this:
Derivation ?a ?E ?b \<Longrightarrow> count_terminals ?a \<le> count_terminals ?b
derives ?a ?b \<Longrightarrow> \<exists>D. Derivation ?a D ?b

goal (1 subgoal):
 1. derives a b \<Longrightarrow> count_terminals a \<le> count_terminals b
[PROOF STEP]
by force


[STATEMENT]
lemma is_word_cons[simp]: "is_word (x#xs) = (is_terminal x \<and> is_word xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_word (x # xs) = (is_terminal x \<and> is_word xs)
[PROOF STEP]
by (simp add: is_word_def)


[STATEMENT]
lemma count_terminals_of_word: "is_word w \<Longrightarrow> count_terminals w = length w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_word w \<Longrightarrow> count_terminals w = length w
[PROOF STEP]
by (induct w, auto)


[STATEMENT]
lemma length_terminals[simp]: "length (terminals p) = length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (terminals p) = length p
[PROOF STEP]
by (auto simp add: terminals_def)


[STATEMENT]
lemma path_length_is_upper_bound:
  assumes p: "wellformed_tokens p"
  assumes \<alpha>: "is_word \<alpha>"
  assumes derives: "derives (\<alpha>@u) (terminals p)"
  shows "length \<alpha> \<le> length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
have counts: "count_terminals \<alpha> \<le> count_terminals (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_terminals \<alpha> \<le> count_terminals (terminals p)
[PROOF STEP]
using derives derives_count_terminals_leq
[PROOF STATE]
proof (prove)
using this:
derives (\<alpha> @ u) (terminals p)
derives ?a ?b \<Longrightarrow> count_terminals ?a \<le> count_terminals ?b

goal (1 subgoal):
 1. count_terminals \<alpha> \<le> count_terminals (terminals p)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
count_terminals \<alpha> \<le> count_terminals (terminals p)

goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
have len1: "length \<alpha> = count_terminals \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<alpha> = count_terminals \<alpha>
[PROOF STEP]
by (simp add: \<alpha> count_terminals_of_word)
[PROOF STATE]
proof (state)
this:
length \<alpha> = count_terminals \<alpha>

goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
have len2: "length (terminals p) = count_terminals (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (terminals p) = count_terminals (terminals p)
[PROOF STEP]
by (simp add: count_terminals_of_word is_word_terminals p)
[PROOF STATE]
proof (state)
this:
length (terminals p) = count_terminals (terminals p)

goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
using counts len1 len2
[PROOF STATE]
proof (prove)
using this:
count_terminals \<alpha> \<le> count_terminals (terminals p)
length \<alpha> = count_terminals \<alpha>
length (terminals p) = count_terminals (terminals p)

goal (1 subgoal):
 1. length \<alpha> \<le> length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length \<alpha> \<le> length p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_word_Derives1_index:
  assumes w: "is_word w"
  assumes derives1: "Derives1 (w@a) i r b"
  shows "i \<ge> length w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
from derives1
[PROOF STATE]
proof (chain)
picking this:
Derives1 (w @ a) i r b
[PROOF STEP]
have n: "is_nonterminal ((w@a) ! i)"
[PROOF STATE]
proof (prove)
using this:
Derives1 (w @ a) i r b

goal (1 subgoal):
 1. is_nonterminal ((w @ a) ! i)
[PROOF STEP]
using Derives1_nonterminal splits_at_def splits_at_ex
[PROOF STATE]
proof (prove)
using this:
Derives1 (w @ a) i r b
\<lbrakk>Derives1 ?a ?i ?r ?b; splits_at ?a ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> fst ?r = ?N \<and> is_nonterminal ?N
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> = (?i < length ?\<delta> \<and> ?\<alpha> = take ?i ?\<delta> \<and> ?N = ?\<delta> ! ?i \<and> ?\<beta> = drop (Suc ?i) ?\<delta>)
Derives1 ?\<delta> ?i ?r ?s \<Longrightarrow> \<exists>\<alpha> N \<beta>. splits_at ?\<delta> ?i \<alpha> N \<beta>

goal (1 subgoal):
 1. is_nonterminal ((w @ a) ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_nonterminal ((w @ a) ! i)

goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
from w
[PROOF STATE]
proof (chain)
picking this:
is_word w
[PROOF STEP]
have t: "i < length w \<Longrightarrow> is_terminal ((w@a) ! i)"
[PROOF STATE]
proof (prove)
using this:
is_word w

goal (1 subgoal):
 1. i < length w \<Longrightarrow> is_terminal ((w @ a) ! i)
[PROOF STEP]
by (simp add: is_word_is_terminal nth_append)
[PROOF STATE]
proof (state)
this:
i < length w \<Longrightarrow> is_terminal ((w @ a) ! i)

goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
by (metis t n is_terminal_nonterminal less_le_not_le nat_le_linear)
[PROOF STATE]
proof (state)
this:
length w \<le> i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_word_Derivation_derivation_ge:
  assumes w: "is_word w"
  assumes D: "Derivation (w@a) D b"
  shows "derivation_ge D (length w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derivation_ge D (length w)
[PROOF STEP]
by (metis D Derivation_leftmost derivation_ge_empty leftmost_Derivation leftmost_append w)


[STATEMENT]
lemma derives_word_is_prefix:
  assumes w: "is_word w"
  assumes derives: "derives (w@a) b"
  shows "is_prefix w b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix w b
[PROOF STEP]
by (metis Derivation_take append_eq_conv_conj derives derives_implies_Derivation
    is_prefix_take is_word_Derivation_derivation_ge w)


[STATEMENT]
lemma terminals_take[simp]: "terminals (take n p) = take n (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. terminals (take n p) = take n (terminals p)
[PROOF STEP]
by (simp add: take_map terminals_def)


[STATEMENT]
lemma terminals_drop[simp]: "terminals (drop n p) = drop n (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. terminals (drop n p) = drop n (terminals p)
[PROOF STEP]
by (simp add: drop_map terminals_def)


[STATEMENT]
lemma take_prefix[simp]: "is_prefix a b \<Longrightarrow> take (length a) b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix a b \<Longrightarrow> take (length a) b = a
[PROOF STEP]
by (metis append_eq_conv_conj is_prefix_unsplit)


[STATEMENT]
lemma Derives1_drop_prefixword:
  assumes w: "is_word w"
  assumes wa_b: "Derives1 (w@a) i r b"
  shows "Derives1 a (i - length w) r (drop (length w) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
have i: "length w \<le> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
using wa_b is_word_Derives1_index w
[PROOF STATE]
proof (prove)
using this:
Derives1 (w @ a) i r b
\<lbrakk>is_word ?w; Derives1 (?w @ ?a) ?i ?r ?b\<rbrakk> \<Longrightarrow> length ?w \<le> ?i
is_word w

goal (1 subgoal):
 1. length w \<le> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length w \<le> i

goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
have "is_prefix w b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix w b
[PROOF STEP]
by (metis append_eq_conv_conj i is_prefix_take le_Derives1_take wa_b)
[PROOF STATE]
proof (state)
this:
is_prefix w b

goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_prefix w b
[PROOF STEP]
have b: "b = w @ (drop (length w) b)"
[PROOF STATE]
proof (prove)
using this:
is_prefix w b

goal (1 subgoal):
 1. b = w @ drop (length w) b
[PROOF STEP]
by (simp add: is_prefix_unsplit)
[PROOF STATE]
proof (state)
this:
b = w @ drop (length w) b

goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 a (i - length w) r (drop (length w) b)
[PROOF STEP]
apply (rule_tac Derives1_skip_prefix[OF i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Derives1 (w @ a) i r (w @ drop (length w) b)
[PROOF STEP]
by (simp add: b[symmetric] wa_b)
[PROOF STATE]
proof (state)
this:
Derives1 a (i - length w) r (drop (length w) b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derives1_drop_prefixword:
  assumes w: "is_word w"
  assumes wa_b: "derives1 (w@a) b"
  shows "derives1 a (drop (length w) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives1 a (drop (length w) b)
[PROOF STEP]
by (metis Derives1_drop_prefixword Derives1_implies_derives1 derives1_implies_Derives1 w wa_b)


[STATEMENT]
lemma derives1_is_word_is_prefix_drop:
  assumes w: "is_word w"
  assumes w_a: "is_prefix w a"
  assumes ab: "derives1 a b"
  shows "derives1 (drop (length w) a) (drop (length w) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives1 (drop (length w) a) (drop (length w) b)
[PROOF STEP]
by (metis ab append_take_drop_id derives1_drop_prefixword take_prefix w w_a)


[STATEMENT]
lemma derives_drop_prefixword_helper:
  "derives a b \<Longrightarrow> is_word w \<Longrightarrow> is_prefix w a \<Longrightarrow> derives (drop (length w) a) (drop (length w) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>derives a b; is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) b)
[PROOF STEP]
proof (induct rule: derives_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) a)
 2. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:
is_word w
is_prefix w a

goal (2 subgoals):
 1. \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) a)
 2. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_word w
is_prefix w a

goal (1 subgoal):
 1. derives (drop (length w) a) (drop (length w) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derives (drop (length w) a) (drop (length w) a)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
case (Step y z)
[PROOF STATE]
proof (state)
this:
derives a y
derives1 y z
\<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y)
is_word w
is_prefix w a

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
have is_prefix_w_y: "is_prefix w y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix w y
[PROOF STEP]
by (metis Step.hyps(1) Step.prems(1) Step.prems(2) derives_word_is_prefix is_prefix_def)
[PROOF STATE]
proof (state)
this:
is_prefix w y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives a y; derives1 y z; \<lbrakk>is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) y); is_word w; is_prefix w a\<rbrakk> \<Longrightarrow> derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_prefix w y

goal (1 subgoal):
 1. derives (drop (length w) a) (drop (length w) z)
[PROOF STEP]
by (metis Step.hyps(2) Step.hyps(3) Step.prems(1) Step.prems(2) derives1_implies_derives
        derives1_is_word_is_prefix_drop derives_trans)
[PROOF STATE]
proof (state)
this:
derives (drop (length w) a) (drop (length w) z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derive_drop_prefixword:
  "is_word w \<Longrightarrow> derives (w@a) b \<Longrightarrow> derives a (drop (length w) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_word w; derives (w @ a) b\<rbrakk> \<Longrightarrow> derives a (drop (length w) b)
[PROOF STEP]
by (metis append_eq_conv_conj derives_drop_prefixword_helper is_prefix_take)