[STATEMENT]
theorem thmD11_helper:
  "p \<in> \<PP> \<Longrightarrow>
   charslength p = k \<Longrightarrow>
   X \<in> T \<Longrightarrow>
   T \<subseteq> \<X> k \<Longrightarrow>
   q = p @ [X] \<Longrightarrow>
   (N, \<alpha>@\<beta>) \<in> \<RR> \<Longrightarrow>
   r \<le> length q \<Longrightarrow>
   LeftDerivation [\<SS>] D ((terminals (take r q))@[N]@\<gamma>) \<Longrightarrow>
   leftderives \<alpha> (terminals (drop r q)) \<Longrightarrow>
   k' = k + length (chars_of_token X) \<Longrightarrow>
   x = Item (N, \<alpha>@\<beta>) (length \<alpha>) (charslength (take r q)) k' \<Longrightarrow>
   I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p)))) \<Longrightarrow>
   x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
proof (induct "length D" arbitrary: D r N \<gamma> \<alpha> \<beta> x rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>D r N \<gamma> \<alpha> \<beta> x. \<lbrakk>\<And>Da r N \<gamma> \<alpha> \<beta> x. \<lbrakk>length Da < length D; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] Da (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?D < length D; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (?N, ?\<alpha> @ ?\<beta>) \<in> \<RR>; ?r \<le> length q; LeftDerivation [\<SS>] ?D (terminals (take ?r q) @ [?N] @ ?\<gamma>); leftderives ?\<alpha> (terminals (drop ?r q)); k' = k + length (chars_of_token X); ?x = Item (?N, ?\<alpha> @ ?\<beta>) (length ?\<alpha>) (charslength (take ?r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> ?x \<in> I
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

goal (1 subgoal):
 1. \<And>D r N \<gamma> \<alpha> \<beta> x. \<lbrakk>\<And>Da r N \<gamma> \<alpha> \<beta> x. \<lbrakk>length Da < length D; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] Da (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
have "D = [] \<or> D \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D = [] \<or> D \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D = [] \<or> D \<noteq> []

goal (1 subgoal):
 1. \<And>D r N \<gamma> \<alpha> \<beta> x. \<lbrakk>\<And>Da r N \<gamma> \<alpha> \<beta> x. \<lbrakk>length Da < length D; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] Da (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (N, \<alpha> @ \<beta>) \<in> \<RR>; r \<le> length q; LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>); leftderives \<alpha> (terminals (drop r q)); k' = k + length (chars_of_token X); x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D = [] \<or> D \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
D = [] \<or> D \<noteq> []

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
D = []

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D = []
[PROOF STEP]
have r: "r = 0"
[PROOF STATE]
proof (prove)
using this:
D = []

goal (1 subgoal):
 1. r = 0
[PROOF STEP]
by (metis LeftDerivation.simps(1) diff_add_0 diff_add_inverse2 le_0_eq length_0_conv
            length_append length_terminals less.prems(7) less.prems(8) list.size(4) take_eq_Nil)
[PROOF STATE]
proof (state)
this:
r = 0

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
D = []
r = 0
[PROOF STEP]
have \<gamma>: "\<gamma> = []"
[PROOF STATE]
proof (prove)
using this:
D = []
r = 0

goal (1 subgoal):
 1. \<gamma> = []
[PROOF STEP]
using LeftDerivation.simps(1) append_Cons append_self_conv2 less.prems(8) list.inject
            take_eq_Nil terminals_empty
[PROOF STATE]
proof (prove)
using this:
D = []
r = 0
LeftDerivation ?a [] ?b = (?a = ?b)
(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys
(?xs @ ?ys = ?ys) = (?xs = [])
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
(?x21.0 # ?x22.0 = ?y21.0 # ?y22.0) = (?x21.0 = ?y21.0 \<and> ?x22.0 = ?y22.0)
(take ?n ?xs = []) = (?n = 0 \<or> ?xs = [])
terminals [] = []

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

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
from r \<gamma> 1
[PROOF STATE]
proof (chain)
picking this:
r = 0
\<gamma> = []
D = []
[PROOF STEP]
have start_is_N: "\<SS> = N"
[PROOF STATE]
proof (prove)
using this:
r = 0
\<gamma> = []
D = []

goal (1 subgoal):
 1. \<SS> = N
[PROOF STEP]
using LeftDerivation.simps(1) append_eq_Cons_conv less.prems(8) list.inject take_eq_Nil
            terminals_empty
[PROOF STATE]
proof (prove)
using this:
r = 0
\<gamma> = []
D = []
LeftDerivation ?a [] ?b = (?a = ?b)
(?ys @ ?zs = ?x # ?xs) = (?ys = [] \<and> ?zs = ?x # ?xs \<or> (\<exists>ys'. ?ys = ?x # ys' \<and> ys' @ ?zs = ?xs))
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
(?x21.0 # ?x22.0 = ?y21.0 # ?y22.0) = (?x21.0 = ?y21.0 \<and> ?x22.0 = ?y22.0)
(take ?n ?xs = []) = (?n = 0 \<or> ?xs = [])
terminals [] = []

goal (1 subgoal):
 1. \<SS> = N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<SS> = N

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
have h1: "r \<le> length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> length p
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
r = 0

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

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
have h2: "leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)
[PROOF STEP]
by (simp add: r \<gamma> start_is_N)
[PROOF STATE]
proof (state)
this:
leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
have h3: "leftderives \<alpha> (terminals (drop r p @ [X]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives \<alpha> (terminals (drop r p @ [X]))
[PROOF STEP]
using "less.prems"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

goal (1 subgoal):
 1. leftderives \<alpha> (terminals (drop r p @ [X]))
[PROOF STEP]
by (simp add: r "less.prems")
[PROOF STATE]
proof (state)
this:
leftderives \<alpha> (terminals (drop r p @ [X]))

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
have h4: "x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'
[PROOF STEP]
using "less.prems"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

goal (1 subgoal):
 1. x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'
[PROOF STEP]
by (simp add: r "less.prems")
[PROOF STATE]
proof (state)
this:
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'

goal (2 subgoals):
 1. D = [] \<Longrightarrow> x \<in> I
 2. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
from thmD10[OF "less.prems"(1, 2, 3, 4, 6) h1 h2 h3 "less.prems"(10) h4  "less.prems"(12)]
[PROOF STATE]
proof (chain)
picking this:
x \<in> I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (1 subgoal):
 1. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
D \<noteq> []

goal (1 subgoal):
 1. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
note D_non_empty = 2
[PROOF STATE]
proof (state)
this:
D \<noteq> []

goal (1 subgoal):
 1. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
have "r < length q \<or> r = length q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r < length q \<or> r = length q
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?D < length D; p \<in> \<PP>; charslength p = k; X \<in> T; T \<subseteq> \<X> k; q = p @ [X]; (?N, ?\<alpha> @ ?\<beta>) \<in> \<RR>; ?r \<le> length q; LeftDerivation [\<SS>] ?D (terminals (take ?r q) @ [?N] @ ?\<gamma>); leftderives ?\<alpha> (terminals (drop ?r q)); k' = k + length (chars_of_token X); ?x = Item (?N, ?\<alpha> @ ?\<beta>) (length ?\<alpha>) (charslength (take ?r q)) k'; I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))\<rbrakk> \<Longrightarrow> ?x \<in> I
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

goal (1 subgoal):
 1. r < length q \<or> r = length q
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
r < length q \<or> r = length q

goal (1 subgoal):
 1. D \<noteq> [] \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r < length q \<or> r = length q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r < length q \<or> r = length q

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
r < length q

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have h1: "r \<le> length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> length p
[PROOF STEP]
using less.prems 1
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))
r < length q

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

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have take_q_p: "take r q = take r p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take r q = take r p
[PROOF STEP]
using 1 less.prems
[PROOF STATE]
proof (prove)
using this:
r < length q
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

goal (1 subgoal):
 1. take r q = take r p
[PROOF STEP]
by (simp add: drop_keep_last le_neq_implies_less nat_le_linear not_less_eq not_less_eq_eq)
[PROOF STATE]
proof (state)
this:
take r q = take r p

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have h2: "leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)
[PROOF STEP]
apply (simp only: take_q_p[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives [\<SS>] (terminals (take r q) @ [N] @ \<gamma>)
[PROOF STEP]
using less.prems LeftDerivation_implies_leftderives
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))
LeftDerivation ?a ?D ?b \<Longrightarrow> leftderives ?a ?b

goal (1 subgoal):
 1. leftderives [\<SS>] (terminals (take r q) @ [N] @ \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
leftderives [\<SS>] (terminals (take r p) @ [N] @ \<gamma>)

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have h3: "leftderives \<alpha> (terminals (drop r p @ [X]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives \<alpha> (terminals (drop r p @ [X]))
[PROOF STEP]
using less.prems(5, 9) h1
[PROOF STATE]
proof (prove)
using this:
q = p @ [X]
leftderives \<alpha> (terminals (drop r q))
r \<le> length p

goal (1 subgoal):
 1. leftderives \<alpha> (terminals (drop r p @ [X]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
leftderives \<alpha> (terminals (drop r p @ [X]))

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have h4: "k' = k + length (chars_of_token X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' = k + length (chars_of_token X)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

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

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have h5: "x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'
[PROOF STEP]
using less.prems take_q_p
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))
take r q = take r p

goal (1 subgoal):
 1. x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r p)) k'

goal (2 subgoals):
 1. r < length q \<Longrightarrow> x \<in> I
 2. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
from thmD10[OF "less.prems"(1, 2, 3, 4, 6) h1 h2 h3 h4 h5 less.prems(12)]
[PROOF STATE]
proof (chain)
picking this:
x \<in> I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> I

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
r = length q

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
r = length q
[PROOF STEP]
have ld: "LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
r = length q

goal (1 subgoal):
 1. LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
using less.prems(8)
[PROOF STATE]
proof (prove)
using this:
r = length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)

goal (1 subgoal):
 1. LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
r = length q
[PROOF STEP]
have \<alpha>_derives_empty: "derives \<alpha> []"
[PROOF STATE]
proof (prove)
using this:
r = length q

goal (1 subgoal):
 1. derives \<alpha> []
[PROOF STEP]
using less.prems(9)
[PROOF STATE]
proof (prove)
using this:
r = length q
leftderives \<alpha> (terminals (drop r q))

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

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_sentence_p: "is_sentence (terminals p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence (terminals p)
[PROOF STEP]
using less.prems(1) \<L>\<^sub>P_derives \<PP>_are_admissible admissible_def is_derivation_def
                is_derivation_is_sentence is_sentence_concat
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
?a \<in> \<L>\<^sub>P \<Longrightarrow> \<exists>b. derives [\<SS>] (?a @ b)
?p \<in> \<PP> \<Longrightarrow> admissible ?p
admissible ?ts = (terminals ?ts \<in> \<L>\<^sub>P)
is_derivation ?u = derives [\<SS>] ?u
is_derivation ?s \<Longrightarrow> is_sentence ?s
is_sentence (?x @ ?y) = (is_sentence ?x \<and> is_sentence ?y)

goal (1 subgoal):
 1. is_sentence (terminals p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sentence (terminals p)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_symbol_X: "is_symbol (terminal_of_token X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_symbol (terminal_of_token X)
[PROOF STEP]
using less.prems(3, 4) \<X>_are_terminals is_symbol_def rev_subsetD
[PROOF STATE]
proof (prove)
using this:
X \<in> T
T \<subseteq> \<X> k
?u \<in> \<X> ?k \<Longrightarrow> is_terminal (terminal_of_token ?u)
is_symbol ?s = (is_terminal ?s \<or> is_nonterminal ?s)
\<lbrakk>?c \<in> ?A; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> ?c \<in> ?B

goal (1 subgoal):
 1. is_symbol (terminal_of_token X)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_symbol (terminal_of_token X)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_sentence_q: "is_sentence (terminals q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence (terminals q)
[PROOF STEP]
using is_sentence_p is_symbol_X
              less.prems LeftDerivation_implies_leftderives is_derivation_def
              is_derivation_is_sentence is_sentence_concat ld leftderives_implies_derives
[PROOF STATE]
proof (prove)
using this:
is_sentence (terminals p)
is_symbol (terminal_of_token X)
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))
LeftDerivation ?a ?D ?b \<Longrightarrow> leftderives ?a ?b
is_derivation ?u = derives [\<SS>] ?u
is_derivation ?s \<Longrightarrow> is_sentence ?s
is_sentence (?x @ ?y) = (is_sentence ?x \<and> is_sentence ?y)
LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)
leftderives ?u ?v \<Longrightarrow> derives ?u ?v

goal (1 subgoal):
 1. is_sentence (terminals q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sentence (terminals q)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_symbol_N: "is_symbol N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_symbol N
[PROOF STEP]
using less.prems(6) is_symbol_def rule_nonterminal_type
[PROOF STATE]
proof (prove)
using this:
(N, \<alpha> @ \<beta>) \<in> \<RR>
is_symbol ?s = (is_terminal ?s \<or> is_nonterminal ?s)
(?N, ?\<alpha>) \<in> \<RR> \<Longrightarrow> is_nonterminal ?N

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

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_sentence_\<gamma>: "is_sentence \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence \<gamma>
[PROOF STEP]
by (meson LeftDerivation_implies_leftderives is_derivation_def is_derivation_is_sentence
                is_sentence_concat ld leftderives_implies_derives)
[PROOF STATE]
proof (state)
this:
is_sentence \<gamma>

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have ld_exists_h1: "is_sentence (terminals q @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
using is_sentence_q is_sentence_\<gamma> is_symbol_N is_sentence_concat
                LeftDerivation_implies_leftderives is_derivation_def is_derivation_is_sentence ld
                leftderives_implies_derives
[PROOF STATE]
proof (prove)
using this:
is_sentence (terminals q)
is_sentence \<gamma>
is_symbol N
is_sentence (?x @ ?y) = (is_sentence ?x \<and> is_sentence ?y)
LeftDerivation ?a ?D ?b \<Longrightarrow> leftderives ?a ?b
is_derivation ?u = derives [\<SS>] ?u
is_derivation ?s \<Longrightarrow> is_sentence ?s
LeftDerivation [\<SS>] D (terminals q @ [N] @ \<gamma>)
leftderives ?u ?v \<Longrightarrow> derives ?u ?v

goal (1 subgoal):
 1. is_sentence (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sentence (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have ld_exists_h2: "length q < length (terminals q @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length q < length (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length q < length (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
from LeftDerivationLadder_exists[OF ld ld_exists_h1 ld_exists_h2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>L. LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>) \<and> ladder_last_j L = length q
[PROOF STEP]
obtain L where
              L: "LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)" and
              L_last_j: "ladder_last_j L = length q"
[PROOF STATE]
proof (prove)
using this:
\<exists>L. LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>) \<and> ladder_last_j L = length q

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>); ladder_last_j L = length q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)
ladder_last_j L = length q

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
note r_eq_length_q = 2
[PROOF STATE]
proof (state)
this:
r = length q

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have ladder_i_0_eq_0: "ladder_i L 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_i L 0 = 0
[PROOF STEP]
using L append_Nil ladder_i_0_bound
              length_append_singleton less_Suc0 list.size(3)
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)
[] @ ?ys = ?ys
LeftDerivationLadder ?\<alpha> ?D ?L ?\<gamma> \<Longrightarrow> ladder_i ?L 0 < length ?\<alpha>
length (?xs @ [?x]) = Suc (length ?xs)
(?n < Suc 0) = (?n = 0)
length [] = 0

goal (1 subgoal):
 1. ladder_i L 0 = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ladder_i L 0 = 0

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
have "length L = 1 \<or> length L > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length L = 1 \<or> 1 < length L
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. length L = 1 \<or> 1 < length L
[PROOF STEP]
by (metis LeftDerivationLadder_def Suc_eq_plus1 Suc_eq_plus1_left butlast_conv_take
                butlast_snoc diff_add_inverse2 is_ladder_def le_add1 le_neq_implies_less
                length_append_singleton old.nat.exhaust take_0)
[PROOF STATE]
proof (state)
this:
length L = 1 \<or> 1 < length L

goal (1 subgoal):
 1. r = length q \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length L = 1 \<or> 1 < length L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length L = 1 \<or> 1 < length L

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length L = 1 \<Longrightarrow> x \<in> I
 2. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
length L = 1

goal (2 subgoals):
 1. length L = 1 \<Longrightarrow> x \<in> I
 2. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
from LeftDerivationLadder_length_1[OF L 1] ladder_i_0_eq_0
[PROOF STATE]
proof (chain)
picking this:
LeftDerivationFix [\<SS>] (ladder_i L 0) D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)
ladder_i L 0 = 0
[PROOF STEP]
have ldfix: "LeftDerivationFix [\<SS>] 0 D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix [\<SS>] (ladder_i L 0) D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)
ladder_i L 0 = 0

goal (1 subgoal):
 1. LeftDerivationFix [\<SS>] 0 D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LeftDerivationFix [\<SS>] 0 D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)

goal (2 subgoals):
 1. length L = 1 \<Longrightarrow> x \<in> I
 2. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with LeftDerivationFix_from_singleton
[PROOF STATE]
proof (chain)
picking this:
LeftDerivationFix [?A] ?i ?D ?j ?\<gamma> \<Longrightarrow> ?D = []
LeftDerivationFix [\<SS>] 0 D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)
[PROOF STEP]
have "D = []"
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix [?A] ?i ?D ?j ?\<gamma> \<Longrightarrow> ?D = []
LeftDerivationFix [\<SS>] 0 D (ladder_last_j L) (terminals q @ [N] @ \<gamma>)

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

goal (2 subgoals):
 1. length L = 1 \<Longrightarrow> x \<in> I
 2. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with D_non_empty
[PROOF STATE]
proof (chain)
picking this:
D \<noteq> []
D = []
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
D \<noteq> []
D = []

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

goal (2 subgoals):
 1. length L = 1 \<Longrightarrow> x \<in> I
 2. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
1 < length L

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain a where a: "a = ladder_\<alpha> [\<SS>] D L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. a = ladder_\<alpha> [\<SS>] D L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = ladder_\<alpha> [\<SS>] D L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = ladder_\<alpha> [\<SS>] D L (length L - 1)
[PROOF STEP]
have a_as_\<gamma>: "a = ladder_\<gamma> [\<SS>] D L (length L - 2)"
[PROOF STATE]
proof (prove)
using this:
a = ladder_\<alpha> [\<SS>] D L (length L - 1)

goal (1 subgoal):
 1. a = ladder_\<gamma> [\<SS>] D L (length L - 2)
[PROOF STEP]
using 2 ladder_\<alpha>_def
[PROOF STATE]
proof (prove)
using this:
a = ladder_\<alpha> [\<SS>] D L (length L - 1)
1 < length L
ladder_\<alpha> ?a ?D ?L ?index = (if ?index = 0 then ?a else ladder_\<gamma> ?a ?D ?L (?index - 1))

goal (1 subgoal):
 1. a = ladder_\<gamma> [\<SS>] D L (length L - 2)
[PROOF STEP]
by (metis diff_diff_left diff_is_0_eq not_le one_add_one)
[PROOF STATE]
proof (state)
this:
a = ladder_\<gamma> [\<SS>] D L (length L - 2)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have introsAt: "LeftDerivationIntrosAt [\<SS>] D L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivationIntrosAt [\<SS>] D L (length L - 1)
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. LeftDerivationIntrosAt [\<SS>] D L (length L - 1)
[PROOF STEP]
by (metis "2.hyps" LeftDerivationIntros_def LeftDerivationLadder_def One_nat_def
                    Suc_leI Suc_lessD diff_less less_not_refl not_less_eq zero_less_diff)
[PROOF STATE]
proof (state)
this:
LeftDerivationIntrosAt [\<SS>] D L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain i where i: "i = ladder_i L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i = ladder_i L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i = ladder_i L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain j where j: "j = ladder_j L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. j = ladder_j L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j = ladder_j L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain ix where ix: "ix = ladder_ix L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ix. ix = ladder_ix L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ix = ladder_ix L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain c where c: "c = ladder_\<gamma> [\<SS>] D L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c = ladder_\<gamma> [\<SS>] D L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = ladder_\<gamma> [\<SS>] D L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain n where n: "n = ladder_n L (length L - 1 - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n = ladder_n L (length L - 1 - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n = ladder_n L (length L - 1 - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain m where m: "m = ladder_n L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m = ladder_n L (length L - 1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m = ladder_n L (length L - 1)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain e where e: "e = D ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. e = D ! n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e = D ! n

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain E where E: "E = drop (Suc n) (take m D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E. E = drop (Suc n) (take m D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
E = drop (Suc n) (take m D)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
from iffD1[OF LeftDerivationIntrosAt_def introsAt]
[PROOF STATE]
proof (chain)
picking this:
let \<alpha> = ladder_\<alpha> [\<SS>] D L (length L - 1); i = ladder_i L (length L - 1); j = ladder_j L (length L - 1); ix = ladder_ix L (length L - 1); \<gamma> = ladder_\<gamma> [\<SS>] D L (length L - 1); n = ladder_n L (length L - 1 - 1); m = ladder_n L (length L - 1); e = D ! n; E = drop (Suc n) (take m D) in i = fst e \<and> LeftDerivationIntro \<alpha> i (snd e) ix E j \<gamma>
[PROOF STEP]
have "i = fst e \<and> LeftDerivationIntro a i (snd e) ix E j c"
[PROOF STATE]
proof (prove)
using this:
let \<alpha> = ladder_\<alpha> [\<SS>] D L (length L - 1); i = ladder_i L (length L - 1); j = ladder_j L (length L - 1); ix = ladder_ix L (length L - 1); \<gamma> = ladder_\<gamma> [\<SS>] D L (length L - 1); n = ladder_n L (length L - 1 - 1); m = ladder_n L (length L - 1); e = D ! n; E = drop (Suc n) (take m D) in i = fst e \<and> LeftDerivationIntro \<alpha> i (snd e) ix E j \<gamma>

goal (1 subgoal):
 1. i = fst e \<and> LeftDerivationIntro a i (snd e) ix E j c
[PROOF STEP]
by (metis E a c e i ix j m n)
[PROOF STATE]
proof (state)
this:
i = fst e \<and> LeftDerivationIntro a i (snd e) ix E j c

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = fst e \<and> LeftDerivationIntro a i (snd e) ix E j c
[PROOF STEP]
have i_eq_fst_e: "i = fst e" and
                  ldintro: "LeftDerivationIntro a i (snd e) ix E j c"
[PROOF STATE]
proof (prove)
using this:
i = fst e \<and> LeftDerivationIntro a i (snd e) ix E j c

goal (1 subgoal):
 1. i = fst e &&& LeftDerivationIntro a i (snd e) ix E j c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = fst e
LeftDerivationIntro a i (snd e) ix E j c

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have c_def: "c = terminals q @ [N] @ \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = terminals q @ [N] @ \<gamma>
[PROOF STEP]
using c L LeftDerivationLadder_ladder_\<gamma>_last
[PROOF STATE]
proof (prove)
using this:
c = ladder_\<gamma> [\<SS>] D L (length L - 1)
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)
LeftDerivationLadder ?\<alpha> ?D ?L ?\<gamma> \<Longrightarrow> ?\<gamma> = ladder_\<gamma> ?\<alpha> ?D ?L (length ?L - 1)

goal (1 subgoal):
 1. c = terminals q @ [N] @ \<gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c = terminals q @ [N] @ \<gamma>

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
from iffD1[OF LeftDerivationIntro_def ldintro]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<beta>. LeftDerives1 a i (snd e) \<beta> \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix \<beta> (i + ix) E j c
[PROOF STEP]
obtain b where b:
                  "LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and>
                   snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<beta>. LeftDerives1 a i (snd e) \<beta> \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix \<beta> (i + ix) E j c

goal (1 subgoal):
 1. (\<And>b. LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain M \<omega> where M\<omega>: "(M, \<omega>) = snd e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M \<omega>. (M, \<omega>) = snd e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>M \<omega>. (M, \<omega>) = snd e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(M, \<omega>) = snd e

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have j_q: "j = length q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = length q
[PROOF STEP]
using L_last_j j ladder_last_j_def
[PROOF STATE]
proof (prove)
using this:
ladder_last_j L = length q
j = ladder_j L (length L - 1)
ladder_last_j ?L = ladder_j ?L (length ?L - 1)

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with c_def
[PROOF STATE]
proof (chain)
picking this:
c = terminals q @ [N] @ \<gamma>
j = length q
[PROOF STEP]
have c_at_j: "c ! j = N"
[PROOF STATE]
proof (prove)
using this:
c = terminals q @ [N] @ \<gamma>
j = length q

goal (1 subgoal):
 1. c ! j = N
[PROOF STEP]
by (metis append_Cons length_terminals nth_append_length)
[PROOF STATE]
proof (state)
this:
c ! j = N

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with b M\<omega>
[PROOF STATE]
proof (chain)
picking this:
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c
(M, \<omega>) = snd e
c ! j = N
[PROOF STEP]
have \<omega>_at_ix: "\<omega> ! ix = N"
[PROOF STATE]
proof (prove)
using this:
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c
(M, \<omega>) = snd e
c ! j = N

goal (1 subgoal):
 1. \<omega> ! ix = N
[PROOF STEP]
by (metis snd_conv)
[PROOF STATE]
proof (state)
this:
\<omega> ! ix = N

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain \<mu>1 \<mu>2 where split_\<omega>: "splits_at \<omega> ix \<mu>1 N \<mu>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<mu>1 \<mu>2. splits_at \<omega> ix \<mu>1 N \<mu>2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis M\<omega> \<omega>_at_ix b snd_conv splits_at_def)
[PROOF STATE]
proof (state)
this:
splits_at \<omega> ix \<mu>1 N \<mu>2

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain a1 a2 where split_a: "splits_at a i a1 M a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a1 a2. splits_at a i a1 M a2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c

goal (1 subgoal):
 1. (\<And>a1 a2. splits_at a i a1 M a2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis LeftDerivationIntro_bounds_ij LeftDerivationIntro_examine_rule M\<omega>
                   fst_conv ldintro splits_at_def)
[PROOF STATE]
proof (state)
this:
splits_at a i a1 M a2

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
splits_at a i a1 M a2
[PROOF STEP]
have is_word_a1: "is_word a1"
[PROOF STATE]
proof (prove)
using this:
splits_at a i a1 M a2

goal (1 subgoal):
 1. is_word a1
[PROOF STEP]
using LeftDerives1_splits_at_is_word b
[PROOF STATE]
proof (prove)
using this:
splits_at a i a1 M a2
\<lbrakk>LeftDerives1 ?\<delta> ?i ?r ?s; splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta>\<rbrakk> \<Longrightarrow> is_word ?\<alpha>
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "b = a1 @ \<omega> @ a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = a1 @ \<omega> @ a2
[PROOF STEP]
using split_a b M\<omega>
[PROOF STATE]
proof (prove)
using this:
splits_at a i a1 M a2
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c
(M, \<omega>) = snd e

goal (1 subgoal):
 1. b = a1 @ \<omega> @ a2
[PROOF STEP]
by (metis LeftDerives1_implies_Derives1 snd_conv splits_at_combine_dest)
[PROOF STATE]
proof (state)
this:
b = a1 @ \<omega> @ a2

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a1 @ \<omega> @ a2
[PROOF STEP]
have b_def: "b = a1 @ \<mu>1 @ [N] @ \<mu>2 @ a2"
[PROOF STATE]
proof (prove)
using this:
b = a1 @ \<omega> @ a2

goal (1 subgoal):
 1. b = a1 @ \<mu>1 @ [N] @ \<mu>2 @ a2
[PROOF STEP]
using split_\<omega> splits_at_combine
[PROOF STATE]
proof (prove)
using this:
b = a1 @ \<omega> @ a2
splits_at \<omega> ix \<mu>1 N \<mu>2
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> \<Longrightarrow> ?\<delta> = ?\<alpha> @ [?N] @ ?\<beta>

goal (1 subgoal):
 1. b = a1 @ \<mu>1 @ [N] @ \<mu>2 @ a2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = a1 @ \<mu>1 @ [N] @ \<mu>2 @ a2

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_nonterminal_N: "is_nonterminal N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nonterminal N
[PROOF STEP]
using less.prems(6) rule_nonterminal_type
[PROOF STATE]
proof (prove)
using this:
(N, \<alpha> @ \<beta>) \<in> \<RR>
(?N, ?\<alpha>) \<in> \<RR> \<Longrightarrow> is_nonterminal ?N

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with LeftDerivationFix_splits_at_nonterminal split_a b
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>LeftDerivationFix ?a ?i ?D ?j ?b; is_nonterminal (?a ! ?i)\<rbrakk> \<Longrightarrow> \<exists>U a1 a2 b1. splits_at ?a ?i a1 U a2 \<and> splits_at ?b ?j b1 U a2 \<and> LeftDerivation a1 ?D b1
splits_at a i a1 M a2
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c
is_nonterminal N
[PROOF STEP]
have "\<exists> U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and>
                  LeftDerivation b1 E c1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>LeftDerivationFix ?a ?i ?D ?j ?b; is_nonterminal (?a ! ?i)\<rbrakk> \<Longrightarrow> \<exists>U a1 a2 b1. splits_at ?a ?i a1 U a2 \<and> splits_at ?b ?j b1 U a2 \<and> LeftDerivation a1 ?D b1
splits_at a i a1 M a2
LeftDerives1 a i (snd e) b \<and> ix < length (snd (snd e)) \<and> snd (snd e) ! ix = c ! j \<and> LeftDerivationFix b (i + ix) E j c
is_nonterminal N

goal (1 subgoal):
 1. \<exists>U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and> LeftDerivation b1 E c1
[PROOF STEP]
by (simp add: LeftDerivationFix_def c_at_j)
[PROOF STATE]
proof (state)
this:
\<exists>U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and> LeftDerivation b1 E c1

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and> LeftDerivation b1 E c1
[PROOF STEP]
obtain b1 b2 c1 where b1b2c1:
                  "splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and>
                   LeftDerivation b1 E c1"
[PROOF STATE]
proof (prove)
using this:
\<exists>U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and> LeftDerivation b1 E c1

goal (1 subgoal):
 1. (\<And>b1 b2 c1. splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using c_at_j splits_at_def
[PROOF STATE]
proof (prove)
using this:
\<exists>U b1 b2 c1. splits_at b (i + ix) b1 U b2 \<and> splits_at c j c1 U b2 \<and> LeftDerivation b1 E c1
c ! j = 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>)

goal (1 subgoal):
 1. (\<And>b1 b2 c1. splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1
[PROOF STEP]
have c1_q: "c1 = terminals q"
[PROOF STATE]
proof (prove)
using this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1

goal (1 subgoal):
 1. c1 = terminals q
[PROOF STEP]
using c_def j_q
[PROOF STATE]
proof (prove)
using this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1
c = terminals q @ [N] @ \<gamma>
j = length q

goal (1 subgoal):
 1. c1 = terminals q
[PROOF STEP]
by (simp add: append_eq_conv_conj splits_at_def)
[PROOF STATE]
proof (state)
this:
c1 = terminals q

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have length_a1_eq_i: "length a1 = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length a1 = i
[PROOF STEP]
using split_a splits_at_def
[PROOF STATE]
proof (prove)
using this:
splits_at a i a1 M a2
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>)

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have length_\<mu>1_eq_ix: "length \<mu>1 = ix"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<mu>1 = ix
[PROOF STEP]
using split_\<omega> splits_at_def
[PROOF STATE]
proof (prove)
using this:
splits_at \<omega> ix \<mu>1 N \<mu>2
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>)

goal (1 subgoal):
 1. length \<mu>1 = ix
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length \<mu>1 = ix

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "b1 = take (i + ix) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b1 = take (i + ix) b
[PROOF STEP]
using b1b2c1 splits_at_def
[PROOF STATE]
proof (prove)
using this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1
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>)

goal (1 subgoal):
 1. b1 = take (i + ix) b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b1 = take (i + ix) b

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b1 = take (i + ix) b
[PROOF STEP]
have b1_eq_a1_\<mu>1: "b1 = a1 @ \<mu>1"
[PROOF STATE]
proof (prove)
using this:
b1 = take (i + ix) b

goal (1 subgoal):
 1. b1 = a1 @ \<mu>1
[PROOF STEP]
using b_def length_a1_eq_i length_\<mu>1_eq_ix
[PROOF STATE]
proof (prove)
using this:
b1 = take (i + ix) b
b = a1 @ \<mu>1 @ [N] @ \<mu>2 @ a2
length a1 = i
length \<mu>1 = ix

goal (1 subgoal):
 1. b1 = a1 @ \<mu>1
[PROOF STEP]
by (simp add: append_eq_conv_conj take_add)
[PROOF STATE]
proof (state)
this:
b1 = a1 @ \<mu>1

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "LeftDerivation (a1 @ \<mu>1) E c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivation (a1 @ \<mu>1) E c1
[PROOF STEP]
using b1b2c1 b1_eq_a1_\<mu>1
[PROOF STATE]
proof (prove)
using this:
splits_at b (i + ix) b1 N b2 \<and> splits_at c j c1 N b2 \<and> LeftDerivation b1 E c1
b1 = a1 @ \<mu>1

goal (1 subgoal):
 1. LeftDerivation (a1 @ \<mu>1) E c1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivation (a1 @ \<mu>1) E c1

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
from LeftDerivation_skip_prefixword_ex[OF this is_word_a1]
[PROOF STATE]
proof (chain)
picking this:
\<exists>w'. c1 = a1 @ w' \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w'
[PROOF STEP]
obtain w where w: "c1 = a1 @ w \<and>
                  LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>w'. c1 = a1 @ w' \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w'

goal (1 subgoal):
 1. (\<And>w. c1 = a1 @ w \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c1 = a1 @ w \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have a1_eq_take_i: "a1 = take i (terminals q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a1 = take i (terminals q)
[PROOF STEP]
using w c1_q split_a append_eq_conv_conj length_a1_eq_i
[PROOF STATE]
proof (prove)
using this:
c1 = a1 @ w \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w
c1 = terminals q
splits_at a i a1 M a2
(?xs @ ?ys = ?zs) = (?xs = take (length ?xs) ?zs \<and> ?ys = drop (length ?xs) ?zs)
length a1 = i

goal (1 subgoal):
 1. a1 = take i (terminals q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a1 = take i (terminals q)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have \<mu>1_leftderives: "leftderives \<mu>1 (terminals (drop i q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives \<mu>1 (terminals (drop i q))
[PROOF STEP]
using w c1_q split_a
                  LeftDerivation_implies_leftderives append_eq_conv_conj length_a1_eq_i
[PROOF STATE]
proof (prove)
using this:
c1 = a1 @ w \<and> LeftDerivation \<mu>1 (derivation_shift E (length a1) 0) w
c1 = terminals q
splits_at a i a1 M a2
LeftDerivation ?a ?D ?b \<Longrightarrow> leftderives ?a ?b
(?xs @ ?ys = ?zs) = (?xs = take (length ?xs) ?zs \<and> ?ys = drop (length ?xs) ?zs)
length a1 = i

goal (1 subgoal):
 1. leftderives \<mu>1 (terminals (drop i q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
leftderives \<mu>1 (terminals (drop i q))

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "LeftDerivation [\<SS>] (take n D) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivation [\<SS>] (take n D) a
[PROOF STEP]
by (metis "2.hyps" L LeftDerivationLadder_implies_LeftDerivation_at_index
                    One_nat_def Suc_lessD a_as_\<gamma> diff_Suc_eq_diff_pred diff_Suc_less n numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] (take n D) a

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LeftDerivation [\<SS>] (take n D) a
[PROOF STEP]
have LD_to_M: "LeftDerivation [\<SS>] (take n D) ((terminals (take i q))@[M]@a2)"
[PROOF STATE]
proof (prove)
using this:
LeftDerivation [\<SS>] (take n D) a

goal (1 subgoal):
 1. LeftDerivation [\<SS>] (take n D) (terminals (take i q) @ [M] @ a2)
[PROOF STEP]
using split_a splits_at_combine a1_eq_take_i terminals_take
[PROOF STATE]
proof (prove)
using this:
LeftDerivation [\<SS>] (take n D) a
splits_at a i a1 M a2
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> \<Longrightarrow> ?\<delta> = ?\<alpha> @ [?N] @ ?\<beta>
a1 = take i (terminals q)
terminals (take ?n ?p) = take ?n (terminals ?p)

goal (1 subgoal):
 1. LeftDerivation [\<SS>] (take n D) (terminals (take i q) @ [M] @ a2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] (take n D) (terminals (take i q) @ [M] @ a2)

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have is_ladder: "is_ladder D L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ladder D L
[PROOF STEP]
using L
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder [\<SS>] D L (terminals q @ [N] @ \<gamma>)

goal (1 subgoal):
 1. is_ladder D L
[PROOF STEP]
by (simp add: LeftDerivationLadder_def)
[PROOF STATE]
proof (state)
this:
is_ladder D L

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ladder D L
[PROOF STEP]
have n_less_m: "n < m"
[PROOF STATE]
proof (prove)
using this:
is_ladder D L

goal (1 subgoal):
 1. n < m
[PROOF STEP]
using n m is_ladder_def
[PROOF STATE]
proof (prove)
using this:
is_ladder D L
n = ladder_n L (length L - 1 - 1)
m = ladder_n L (length L - 1)
is_ladder ?D ?L = (?L \<noteq> [] \<and> (\<forall>u<length ?L. ladder_n ?L u \<le> length ?D) \<and> (\<forall>u v. u < v \<and> v < length ?L \<longrightarrow> ladder_n ?L u < ladder_n ?L v) \<and> ladder_last_n ?L = length ?D)

goal (1 subgoal):
 1. n < m
[PROOF STEP]
by (metis (no_types, lifting) "2.hyps" One_nat_def diff_Suc_less
                    length_greater_0_conv zero_less_diff)
[PROOF STATE]
proof (state)
this:
n < m

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have m_le_D: "m \<le> length D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> length D
[PROOF STEP]
using m is_ladder_def is_ladder dual_order.refl
                  ladder_n_last_is_length
[PROOF STATE]
proof (prove)
using this:
m = ladder_n L (length L - 1)
is_ladder ?D ?L = (?L \<noteq> [] \<and> (\<forall>u<length ?L. ladder_n ?L u \<le> length ?D) \<and> (\<forall>u v. u < v \<and> v < length ?L \<longrightarrow> ladder_n ?L u < ladder_n ?L v) \<and> ladder_last_n ?L = length ?D)
is_ladder D L
?a \<le> ?a
is_ladder ?D ?L \<Longrightarrow> ladder_n ?L (length ?L - 1) = length ?D

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "length (take n D) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (take n D) = n
[PROOF STEP]
using  n_less_m m_le_D
[PROOF STATE]
proof (prove)
using this:
n < m
m \<le> length D

goal (1 subgoal):
 1. length (take n D) = n
[PROOF STEP]
using length_take less_irrefl less_le_trans linear min.absorb2
[PROOF STATE]
proof (prove)
using this:
n < m
m \<le> length D
length (take ?n ?xs) = min (length ?xs) ?n
\<not> ?x < ?x
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
?x \<le> ?y \<or> ?y \<le> ?x
?b \<le> ?a \<Longrightarrow> min ?a ?b = ?b

goal (1 subgoal):
 1. length (take n D) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (take n D) = n

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (take n D) = n
[PROOF STEP]
have length_take_n_D: "length (take n D) < length D"
[PROOF STATE]
proof (prove)
using this:
length (take n D) = n

goal (1 subgoal):
 1. length (take n D) < length D
[PROOF STEP]
using n_less_m m_le_D less_le_trans
[PROOF STATE]
proof (prove)
using this:
length (take n D) = n
n < m
m \<le> length D
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. length (take n D) < length D
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length (take n D) < length D

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have \<omega>_decompose: "\<omega> = \<mu>1@(N#\<mu>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> = \<mu>1 @ N # \<mu>2
[PROOF STEP]
using split_\<omega> splits_at_combine
[PROOF STATE]
proof (prove)
using this:
splits_at \<omega> ix \<mu>1 N \<mu>2
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> \<Longrightarrow> ?\<delta> = ?\<alpha> @ [?N] @ ?\<beta>

goal (1 subgoal):
 1. \<omega> = \<mu>1 @ N # \<mu>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<omega> = \<mu>1 @ N # \<mu>2

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "(M, \<omega>) \<in> \<RR>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, \<omega>) \<in> \<RR>
[PROOF STEP]
by (metis Derives1_rule LeftDerives1_implies_Derives1 M\<omega> b)
[PROOF STATE]
proof (state)
this:
(M, \<omega>) \<in> \<RR>

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with \<omega>_decompose
[PROOF STATE]
proof (chain)
picking this:
\<omega> = \<mu>1 @ N # \<mu>2
(M, \<omega>) \<in> \<RR>
[PROOF STEP]
have M_rule: "(M, \<mu>1@(N#\<mu>2)) \<in> \<RR>"
[PROOF STATE]
proof (prove)
using this:
\<omega> = \<mu>1 @ N # \<mu>2
(M, \<omega>) \<in> \<RR>

goal (1 subgoal):
 1. (M, \<mu>1 @ N # \<mu>2) \<in> \<RR>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(M, \<mu>1 @ N # \<mu>2) \<in> \<RR>

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have i_le_q: "i \<le> length q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> length q
[PROOF STEP]
using a1_eq_take_i length_a1_eq_i
[PROOF STATE]
proof (prove)
using this:
a1 = take i (terminals q)
length a1 = i

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain y where
                  y: "y = Item (M, \<mu>1 @ N # \<mu>2) (length \<mu>1) (charslength (take i q)) k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. y = Item (M, \<mu>1 @ N # \<mu>2) (length \<mu>1) (charslength (take i q)) k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y = Item (M, \<mu>1 @ N # \<mu>2) (length \<mu>1) (charslength (take i q)) k'

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
from less.hyps[OF length_take_n_D less.prems(1, 2, 3, 4, 5) M_rule i_le_q LD_to_M
                   \<mu>1_leftderives less.prems(10) y less.prems(12)]
[PROOF STATE]
proof (chain)
picking this:
y \<in> I
[PROOF STEP]
have y_in_I: "y \<in> I"
[PROOF STATE]
proof (prove)
using this:
y \<in> I

goal (1 subgoal):
 1. y \<in> I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> I

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
obtain z where z: "z = Item (N, \<alpha>@\<beta>) 0 k' k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. z = Item (N, \<alpha> @ \<beta>) 0 k' k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z = Item (N, \<alpha> @ \<beta>) 0 k' k'

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z = Item (N, \<alpha> @ \<beta>) 0 k' k'
[PROOF STEP]
have z_is_init_item: "z = init_item (N, \<alpha>@\<beta>) k'"
[PROOF STATE]
proof (prove)
using this:
z = Item (N, \<alpha> @ \<beta>) 0 k' k'

goal (1 subgoal):
 1. z = init_item (N, \<alpha> @ \<beta>) k'
[PROOF STEP]
by (simp add: init_item_def)
[PROOF STATE]
proof (state)
this:
z = init_item (N, \<alpha> @ \<beta>) k'

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "z \<in> Predict k' {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> Predict k' {y}
[PROOF STEP]
apply (simp add: z_is_init_item)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init_item (N, \<alpha> @ \<beta>) k' \<in> Predict k' {y}
[PROOF STEP]
apply (rule next_symbol_predicts)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. next_symbol y = Some N
 2. (N, \<alpha> @ \<beta>) \<in> \<RR>
 3. k' = item_end y
[PROOF STEP]
apply (simp add: is_complete_def next_symbol_def y)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (N, \<alpha> @ \<beta>) \<in> \<RR>
 2. k' = item_end y
[PROOF STEP]
apply (simp add: less.prems(6))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' = item_end y
[PROOF STEP]
apply (simp add: y item_end_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
z \<in> Predict k' {y}

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> Predict k' {y}
[PROOF STEP]
have "z \<in> Predict k' I"
[PROOF STATE]
proof (prove)
using this:
z \<in> Predict k' {y}

goal (1 subgoal):
 1. z \<in> Predict k' I
[PROOF STEP]
using Predict_def bin_def y_in_I
[PROOF STATE]
proof (prove)
using this:
z \<in> Predict k' {y}
Predict ?k ?I = ?I \<union> {uu_. \<exists>r x. uu_ = init_item r ?k \<and> r \<in> \<RR> \<and> x \<in> bin ?I ?k \<and> next_symbol x = Some (fst r)}
bin ?I ?k = {x \<in> ?I. item_end x = ?k}
y \<in> I

goal (1 subgoal):
 1. z \<in> Predict k' I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> Predict k' I

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> Predict k' I
[PROOF STEP]
have z_in_I: "z \<in> I"
[PROOF STATE]
proof (prove)
using this:
z \<in> Predict k' I

goal (1 subgoal):
 1. z \<in> I
[PROOF STEP]
by (metis Predict_\<pi>_fix items_le_Predict less.prems(12))
[PROOF STATE]
proof (state)
this:
z \<in> I

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have length_chars_q: "length (chars q) = k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars q) = k'
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
p \<in> \<PP>
charslength p = k
X \<in> T
T \<subseteq> \<X> k
q = p @ [X]
(N, \<alpha> @ \<beta>) \<in> \<RR>
r \<le> length q
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
leftderives \<alpha> (terminals (drop r q))
k' = k + length (chars_of_token X)
x = Item (N, \<alpha> @ \<beta>) (length \<alpha>) (charslength (take r q)) k'
I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have x_is_inc_dot: "x = inc_dot (length \<alpha>) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = inc_dot (length \<alpha>) z
[PROOF STEP]
by (simp add: less.prems(11) r_eq_length_q length_chars_q z inc_dot_def)
[PROOF STATE]
proof (state)
this:
x = inc_dot (length \<alpha>) z

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have wellformed_items_I: "wellformed_items I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_items I
[PROOF STEP]
apply (subst less.prems(12))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_items (items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p)))))
[PROOF STEP]
by (meson LocalLexing.items_le_is_filter LocalLexing.wellformed_items_Gen
                    LocalLexing_axioms empty_subsetI less.prems(4) subsetCE wellformed_items_Scan
                    wellformed_items_\<pi> wellformed_items_def)
[PROOF STATE]
proof (state)
this:
wellformed_items I

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
with z_in_I
[PROOF STATE]
proof (chain)
picking this:
z \<in> I
wellformed_items I
[PROOF STEP]
have wellformed_z: "wellformed_item z"
[PROOF STATE]
proof (prove)
using this:
z \<in> I
wellformed_items I

goal (1 subgoal):
 1. wellformed_item z
[PROOF STEP]
using wellformed_items_def
[PROOF STATE]
proof (prove)
using this:
z \<in> I
wellformed_items I
wellformed_items ?X = Ball ?X wellformed_item

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

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have item_\<beta>_z: "item_\<beta> z = \<alpha>@\<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<beta> z = \<alpha> @ \<beta>
[PROOF STEP]
by (simp add: z_is_init_item)
[PROOF STATE]
proof (state)
this:
item_\<beta> z = \<alpha> @ \<beta>

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have item_end_z: "item_end z = k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end z = k'
[PROOF STEP]
by (simp add: z_is_init_item)
[PROOF STATE]
proof (state)
this:
item_end z = k'

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
have "x \<in> \<pi> k' {} {z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<pi> k' {} {z}
[PROOF STEP]
apply (simp add: x_is_inc_dot)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inc_dot (length \<alpha>) z \<in> \<pi> k' {} {z}
[PROOF STEP]
apply (rule thmD6)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. wellformed_item z
 2. item_\<beta> z = \<alpha> @ ?\<omega>1
 3. item_end z = k'
 4. derives \<alpha> []
[PROOF STEP]
apply (rule wellformed_z)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. item_\<beta> z = \<alpha> @ ?\<omega>1
 2. item_end z = k'
 3. derives \<alpha> []
[PROOF STEP]
apply (rule item_\<beta>_z)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. item_end z = k'
 2. derives \<alpha> []
[PROOF STEP]
apply (rule item_end_z)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives \<alpha> []
[PROOF STEP]
by (simp add: \<alpha>_derives_empty)
[PROOF STATE]
proof (state)
this:
x \<in> \<pi> k' {} {z}

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<pi> k' {} {z}
[PROOF STEP]
have "x \<in> \<pi> k' {} I"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<pi> k' {} {z}

goal (1 subgoal):
 1. x \<in> \<pi> k' {} I
[PROOF STEP]
using z_in_I
[PROOF STATE]
proof (prove)
using this:
x \<in> \<pi> k' {} {z}
z \<in> I

goal (1 subgoal):
 1. x \<in> \<pi> k' {} I
[PROOF STEP]
by (meson contra_subsetD empty_subsetI insert_subset monoD mono_\<pi>)
[PROOF STATE]
proof (state)
this:
x \<in> \<pi> k' {} I

goal (1 subgoal):
 1. 1 < length L \<Longrightarrow> x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<pi> k' {} I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> \<pi> k' {} I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
by (metis (no_types, lifting) LocalLexing.wellformed_item_def LocalLexing_axioms
                    \<pi>_subset_elem_trans item.sel(3) item.sel(4) items_le_def items_le_is_filter
                    less.prems(11) less.prems(12) mem_Collect_eq wellformed_z z)
[PROOF STATE]
proof (state)
this:
x \<in> I

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem thmD11:
  assumes p_dom: "p \<in> \<PP>"
  assumes p_charslength: "charslength p = k"
  assumes X_dom: "X \<in> T"
  assumes T_dom: "T \<subseteq> \<X> k"
  assumes q_def: "q = p @ [X]"
  assumes rule_dom: "(N, \<alpha>@\<beta>) \<in> \<RR>"
  assumes r: "r \<le> length q"
  assumes leftderives_start: "leftderives [\<SS>] ((terminals (take r q))@[N]@\<gamma>)"
  assumes leftderives_\<alpha>: "leftderives \<alpha> (terminals (drop r q))"
  assumes k': "k' = k + length (chars_of_token X)"
  assumes item_def: "x = Item (N, \<alpha>@\<beta>) (length \<alpha>) (charslength (take r q)) k'"
  assumes I: "I = items_le k' (\<pi> k' {} (Scan T k (Gen (Prefixes p))))"
  shows "x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
have "\<exists> D. LeftDerivation  [\<SS>] D ((terminals (take r q))@[N]@\<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
[PROOF STEP]
using leftderives_start leftderives_implies_LeftDerivation
[PROOF STATE]
proof (prove)
using this:
leftderives [\<SS>] (terminals (take r q) @ [N] @ \<gamma>)
leftderives ?a ?b \<Longrightarrow> \<exists>D. LeftDerivation ?a D ?b

goal (1 subgoal):
 1. \<exists>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)
[PROOF STEP]
obtain D where D: "LeftDerivation  [\<SS>] D ((terminals (take r q))@[N]@\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)

goal (1 subgoal):
 1. (\<And>D. LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivation [\<SS>] D (terminals (take r q) @ [N] @ \<gamma>)

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
from thmD11_helper[OF assms(1, 2, 3, 4, 5, 6, 7) D assms(9, 10, 11, 12)]
[PROOF STATE]
proof (chain)
picking this:
x \<in> I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> I

goal (1 subgoal):
 1. x \<in> I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma elim_interleave'[pred_set_conv]: "interleave' xs ys zs \<longleftrightarrow> zs \<in> xs \<otimes> ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interleave' xs ys zs = (zs \<in> xs \<otimes> ys)
[PROOF STEP]
unfolding interleave_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interleave' xs ys zs = (zs \<in> Collect (interleave' xs ys))
[PROOF STEP]
by simp


[STATEMENT]
lemma interleave_comm: "xs \<in> ys \<otimes> zs \<Longrightarrow> xs \<in> zs \<otimes> ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> ys \<otimes> zs \<Longrightarrow> xs \<in> zs \<otimes> ys
[PROOF STEP]
by (induction rule: interleave_induct) (auto intro: interleave_intros)


[STATEMENT]
lemma interleave_Nil1[simp]: "[] \<otimes> xs = {xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<otimes> xs = {xs}
[PROOF STEP]
by (induction xs) (auto intro: interleave_intros elim: interleave_cases)


[STATEMENT]
lemma interleave_Nil2[simp]: "xs \<otimes> [] = {xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<otimes> [] = {xs}
[PROOF STEP]
by (induction xs) (auto intro: interleave_intros elim: interleave_cases)


[STATEMENT]
lemma interleave_nil_simp[simp]: "[] \<in> xs \<otimes> ys \<longleftrightarrow> xs = [] \<and> ys = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([] \<in> xs \<otimes> ys) = (xs = [] \<and> ys = [])
[PROOF STEP]
by (auto elim: interleave_cases)


[STATEMENT]
lemma append_interleave: "xs @ ys \<in> xs \<otimes> ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ ys \<in> xs \<otimes> ys
[PROOF STEP]
by (induction xs) (auto intro: interleave_intros)


[STATEMENT]
lemma interleave_assoc1: "a \<in> xs \<otimes> ys \<Longrightarrow> b \<in> a \<otimes> zs \<Longrightarrow> \<exists> c. c \<in> ys \<otimes> zs \<and>  b \<in> xs  \<otimes> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> xs \<otimes> ys; b \<in> a \<otimes> zs\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> ys \<otimes> zs \<and> b \<in> xs \<otimes> c
[PROOF STEP]
by (induction b arbitrary: a  xs ys zs)
     (simp, fastforce del: interleave_ConsE elim!: interleave_ConsE  intro: interleave_intros)


[STATEMENT]
lemma interleave_assoc2: "a \<in> ys \<otimes> zs \<Longrightarrow> b \<in> xs \<otimes> a \<Longrightarrow> \<exists> c. c \<in> xs \<otimes> ys \<and>  b \<in> c \<otimes> zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> ys \<otimes> zs; b \<in> xs \<otimes> a\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> xs \<otimes> ys \<and> b \<in> c \<otimes> zs
[PROOF STEP]
by (induction b arbitrary: a  xs ys zs )
     (simp, fastforce del: interleave_ConsE elim!: interleave_ConsE  intro: interleave_intros)


[STATEMENT]
lemma interleave_set: "zs \<in> xs \<otimes> ys \<Longrightarrow> set zs = set xs \<union> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs \<in> xs \<otimes> ys \<Longrightarrow> set zs = set xs \<union> set ys
[PROOF STEP]
by(induction rule:interleave_induct) auto


[STATEMENT]
lemma interleave_tl: "xs \<in> ys \<otimes> zs \<Longrightarrow> tl xs \<in> tl ys \<otimes> zs \<or> tl xs \<in> ys \<otimes> (tl zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> ys \<otimes> zs \<Longrightarrow> tl xs \<in> tl ys \<otimes> zs \<or> tl xs \<in> ys \<otimes> tl zs
[PROOF STEP]
by(induction rule:interleave_induct) auto


[STATEMENT]
lemma interleave_butlast: "xs \<in> ys \<otimes> zs \<Longrightarrow> butlast xs \<in> butlast ys \<otimes> zs \<or> butlast xs \<in> ys \<otimes> (butlast zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> ys \<otimes> zs \<Longrightarrow> butlast xs \<in> butlast ys \<otimes> zs \<or> butlast xs \<in> ys \<otimes> butlast zs
[PROOF STEP]
by (induction rule:interleave_induct) (auto intro: interleave_intros)


[STATEMENT]
lemma interleave_take: "zs \<in> xs \<otimes> ys \<Longrightarrow> \<exists> n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and>  take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs \<in> xs \<otimes> ys \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys
[PROOF STEP]
apply(induction arbitrary: n rule:interleave_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n [] \<in> take n\<^sub>1 [] \<otimes> take n\<^sub>2 []
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 (x # xs) \<otimes> take n\<^sub>2 ys
 3. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 (x # xs) \<otimes> take n\<^sub>2 ys
 3. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 (x # xs) \<otimes> take n\<^sub>2 ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (case_tac n, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n nat. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 (x # xs) \<otimes> take n\<^sub>2 ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (drule_tac x = nat in meta_spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n nat. \<lbrakk>zs \<in> xs \<otimes> ys; n = Suc nat; \<exists>n\<^sub>1 n\<^sub>2. nat = n\<^sub>1 + n\<^sub>2 \<and> take nat zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 (x # xs) \<otimes> take n\<^sub>2 ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1' n\<^sub>2'. Suc (n\<^sub>1 + n\<^sub>2) = n\<^sub>1' + n\<^sub>2' \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1' (x # xs) \<otimes> take n\<^sub>2' ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (rule_tac x = "Suc n\<^sub>1" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>2'. Suc (n\<^sub>1 + n\<^sub>2) = Suc n\<^sub>1 + n\<^sub>2' \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take (Suc n\<^sub>1) (x # xs) \<otimes> take n\<^sub>2' ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (rule_tac x = "n\<^sub>2" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> Suc (n\<^sub>1 + n\<^sub>2) = Suc n\<^sub>1 + n\<^sub>2 \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take (Suc n\<^sub>1) (x # xs) \<otimes> take n\<^sub>2 ys
 2. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (auto intro: interleave_intros)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (case_tac n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n nat. \<lbrakk>zs \<in> xs \<otimes> ys; \<And>n. \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply (drule_tac x = nat in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n nat. \<lbrakk>zs \<in> xs \<otimes> ys; n = Suc nat; \<exists>n\<^sub>1 n\<^sub>2. nat = n\<^sub>1 + n\<^sub>2 \<and> take nat zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1 n\<^sub>2. n = n\<^sub>1 + n\<^sub>2 \<and> take n (x # zs) \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 (x # ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>1' n\<^sub>2'. Suc (n\<^sub>1 + n\<^sub>2) = n\<^sub>1' + n\<^sub>2' \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1' xs \<otimes> take n\<^sub>2' (x # ys)
[PROOF STEP]
apply (rule_tac x = "n\<^sub>1" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> \<exists>n\<^sub>2'. Suc (n\<^sub>1 + n\<^sub>2) = n\<^sub>1 + n\<^sub>2' \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2' (x # ys)
[PROOF STEP]
apply (rule_tac x = "Suc n\<^sub>2" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys zs x n\<^sub>1 n\<^sub>2. \<lbrakk>zs \<in> xs \<otimes> ys; take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take n\<^sub>2 ys\<rbrakk> \<Longrightarrow> Suc (n\<^sub>1 + n\<^sub>2) = n\<^sub>1 + Suc n\<^sub>2 \<and> x # take (n\<^sub>1 + n\<^sub>2) zs \<in> take n\<^sub>1 xs \<otimes> take (Suc n\<^sub>2) (x # ys)
[PROOF STEP]
apply (auto intro: interleave_intros)[1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma filter_interleave: "xs \<in> ys \<otimes> zs \<Longrightarrow> filter P xs \<in> filter P ys \<otimes> filter P zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> ys \<otimes> zs \<Longrightarrow> filter P xs \<in> filter P ys \<otimes> filter P zs
[PROOF STEP]
by (induction rule: interleave_induct)  (auto intro: interleave_intros)


[STATEMENT]
lemma interleave_filtered: "xs \<in> interleave (filter P xs)  (filter (\<lambda>x'. \<not> P x') xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> filter P xs \<otimes> filter (\<lambda>x'. \<not> P x') xs
[PROOF STEP]
by (induction xs) (auto intro: interleave_intros)