[STATEMENT]
theorem compatibility_def:
  assumes p_in_dom: "p \<in> \<P> k u"
  assumes q_in_dom: "q \<in> \<P> k u"
  assumes p_charslength: "charslength p = k"
  assumes q_split: "q = q'@[t]"
  assumes q'len: "charslength q' = k"
  assumes admissible: "admissible (p @ [t])"
  shows "p @ [t] \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
have u: "u > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u
[PROOF STEP]
proof (cases "u = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = 0

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = 0
[PROOF STEP]
have "charslength q' < k"
[PROOF STATE]
proof (prove)
using this:
u = 0

goal (1 subgoal):
 1. charslength q' < k
[PROOF STEP]
using charslength_of_butlast_0 q_in_dom q_split
[PROOF STATE]
proof (prove)
using this:
u = 0
\<lbrakk>?p \<in> \<P> ?k 0; ?p = ?q @ [?t]\<rbrakk> \<Longrightarrow> charslength ?q < ?k
q \<in> \<P> k u
q = q' @ [t]

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

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < u
[PROOF STEP]
with q'len
[PROOF STATE]
proof (chain)
picking this:
charslength q' = k
charslength q' < k
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
charslength q' = k
charslength q' < k

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

goal (2 subgoals):
 1. u = 0 \<Longrightarrow> 0 < u
 2. u \<noteq> 0 \<Longrightarrow> 0 < u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

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

goal (1 subgoal):
 1. u \<noteq> 0 \<Longrightarrow> 0 < u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < u

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
have t_dom: "t \<in> \<Z> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \<Z> k u
[PROOF STEP]
using last_token_of_path q'len q_in_dom q_split
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> \<P> ?k ?u; ?q = ?q' @ [?t]; charslength ?q' = ?k\<rbrakk> \<Longrightarrow> ?t \<in> \<Z> ?k ?u
charslength q' = k
q \<in> \<P> k u
q = q' @ [t]

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

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
have "p \<in> \<P> k (u - 1) \<or> p \<notin> \<P> k (u - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> k (u - 1) \<or> p \<notin> \<P> k (u - 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k (u - 1) \<or> p \<notin> \<P> k (u - 1)

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> k (u - 1) \<or> p \<notin> \<P> k (u - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> k (u - 1) \<or> p \<notin> \<P> k (u - 1)

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
 2. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p \<in> \<P> k (u - 1)

goal (2 subgoals):
 1. p \<in> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
 2. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
with t_dom p_charslength admissible u
[PROOF STATE]
proof (chain)
picking this:
t \<in> \<Z> k u
charslength p = k
admissible (p @ [t])
0 < u
p \<in> \<P> k (u - 1)
[PROOF STEP]
have "is_continuation k (u - 1) p [t]"
[PROOF STATE]
proof (prove)
using this:
t \<in> \<Z> k u
charslength p = k
admissible (p @ [t])
0 < u
p \<in> \<P> k (u - 1)

goal (1 subgoal):
 1. is_continuation k (u - 1) p [t]
[PROOF STEP]
by (auto simp add: is_continuation_def)
[PROOF STATE]
proof (state)
this:
is_continuation k (u - 1) p [t]

goal (2 subgoals):
 1. p \<in> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
 2. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
with u
[PROOF STATE]
proof (chain)
picking this:
0 < u
is_continuation k (u - 1) p [t]
[PROOF STEP]
show "p@[t] \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
0 < u
is_continuation k (u - 1) p [t]

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
by (metis One_nat_def Suc_pred is_continuation_in_\<P>)
[PROOF STATE]
proof (state)
this:
p @ [t] \<in> \<P> k u

goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p \<notin> \<P> k (u - 1)

goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
from final_step_of_path'[OF p_in_dom 2]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q ts. 0 < u \<and> p = q @ ts \<and> is_continuation k (u - 1) q ts
[PROOF STEP]
obtain p' ts where p': "p = p' @ ts \<and> is_continuation k (u - 1) p' ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>q ts. 0 < u \<and> p = q @ ts \<and> is_continuation k (u - 1) q ts

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

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

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

goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
from u
[PROOF STATE]
proof (chain)
picking this:
0 < u
[PROOF STEP]
have u': "Suc (u - 1) = u"
[PROOF STATE]
proof (prove)
using this:
0 < u

goal (1 subgoal):
 1. Suc (u - 1) = u
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
Suc (u - 1) = u

goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
have "is_continuation k (u - 1) p' (ts@[t])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_continuation k (u - 1) p' (ts @ [t])
[PROOF STEP]
apply (rule_tac is_continuation_continue)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. is_continuation k (u - 1) p' ts
 2. charslength ts = 0
 3. t \<in> \<Z> k (Suc (u - 1))
 4. admissible (p' @ ts @ [t])
[PROOF STEP]
using p'
[PROOF STATE]
proof (prove)
using this:
p = p' @ ts \<and> is_continuation k (u - 1) p' ts

goal (4 subgoals):
 1. is_continuation k (u - 1) p' ts
 2. charslength ts = 0
 3. t \<in> \<Z> k (Suc (u - 1))
 4. admissible (p' @ ts @ [t])
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. charslength ts = 0
 2. t \<in> \<Z> k (Suc (u - 1))
 3. admissible (p' @ ts @ [t])
[PROOF STEP]
using charslength_ts
[PROOF STATE]
proof (prove)
using this:
charslength ts = 0

goal (3 subgoals):
 1. charslength ts = 0
 2. t \<in> \<Z> k (Suc (u - 1))
 3. admissible (p' @ ts @ [t])
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. t \<in> \<Z> k (Suc (u - 1))
 2. admissible (p' @ ts @ [t])
[PROOF STEP]
apply (simp only: u' t_dom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible (p' @ ts @ [t])
[PROOF STEP]
using admissible p'
[PROOF STATE]
proof (prove)
using this:
admissible (p @ [t])
p = p' @ ts \<and> is_continuation k (u - 1) p' ts

goal (1 subgoal):
 1. admissible (p' @ ts @ [t])
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
is_continuation k (u - 1) p' (ts @ [t])

goal (1 subgoal):
 1. p \<notin> \<P> k (u - 1) \<Longrightarrow> p @ [t] \<in> \<P> k u
[PROOF STEP]
from is_continuation_in_\<P>[OF this]
[PROOF STATE]
proof (chain)
picking this:
p' @ ts @ [t] \<in> \<P> k (Suc (u - 1))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p' @ ts @ [t] \<in> \<P> k (Suc (u - 1))

goal (1 subgoal):
 1. p @ [t] \<in> \<P> k u
[PROOF STEP]
by (simp only: p' u', simp)
[PROOF STATE]
proof (state)
this:
p @ [t] \<in> \<P> k u

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_prefix_admissible:
  assumes "is_prefix a b"
  assumes "admissible b"
  shows "admissible a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admissible a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. admissible a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_prefix a b
admissible b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_prefix a b
admissible b

goal (1 subgoal):
 1. admissible a
[PROOF STEP]
by (auto simp add: is_prefix_def admissible_def \<L>\<^sub>P_def)
[PROOF STATE]
proof (state)
this:
admissible a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_\<P>_charslength:
  assumes p_dom: "p \<in> \<P> k u"
  shows "\<exists> v. p \<in> \<P> (charslength p) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
proof (cases "charslength p \<ge> k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
 2. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<le> charslength p

goal (2 subgoals):
 1. k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
 2. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
apply (rule_tac x=u in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<P> (charslength p) u
[PROOF STEP]
by (metis True le_neq_implies_less p_dom subsetCE subset_\<P>)
[PROOF STATE]
proof (state)
this:
\<exists>v. p \<in> \<P> (charslength p) v

goal (1 subgoal):
 1. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k \<le> charslength p

goal (1 subgoal):
 1. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> k \<le> charslength p
[PROOF STEP]
have charslength: "charslength p < k"
[PROOF STATE]
proof (prove)
using this:
\<not> k \<le> charslength p

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

goal (1 subgoal):
 1. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
have "p = [] \<or> p \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<or> p \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. \<not> k \<le> charslength p \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = [] \<or> p \<noteq> []

goal (1 subgoal):
 1. \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
 2. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
 2. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>v. p \<in> \<P> (charslength p) v

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
p \<noteq> []

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

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

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

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

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

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

goal (1 subgoal):
 1. charslength q \<le> charslength p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
charslength q \<le> charslength p

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
with k'
[PROOF STATE]
proof (chain)
picking this:
charslength q = k'
charslength q \<le> charslength p
[PROOF STEP]
have k': "k' \<le> charslength p"
[PROOF STATE]
proof (prove)
using this:
charslength q = k'
charslength q \<le> charslength p

goal (1 subgoal):
 1. k' \<le> charslength p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' \<le> charslength p

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

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

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

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
with k'
[PROOF STATE]
proof (chain)
picking this:
k' \<le> charslength p
p \<in> \<P> k' (Suc u')
[PROOF STEP]
have "p \<in> \<P> (charslength p) (Suc u')"
[PROOF STATE]
proof (prove)
using this:
k' \<le> charslength p
p \<in> \<P> k' (Suc u')

goal (1 subgoal):
 1. p \<in> \<P> (charslength p) (Suc u')
[PROOF STEP]
by (metis le_neq_implies_less subsetCE subset_\<P>)
[PROOF STATE]
proof (state)
this:
p \<in> \<P> (charslength p) (Suc u')

goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<P> (charslength p) (Suc u')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> \<P> (charslength p) (Suc u')

goal (1 subgoal):
 1. \<exists>v. p \<in> \<P> (charslength p) v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v. p \<in> \<P> (charslength p) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>v. p \<in> \<P> (charslength p) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem general_compatibility:
  "p \<in> \<P> k u \<Longrightarrow> q \<in> \<P> k u \<Longrightarrow> charslength p = charslength (take n q)
    \<Longrightarrow> charslength p \<le> k \<Longrightarrow> admissible (p @ (drop n q)) \<Longrightarrow> p @ (drop n q) \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
proof (induct "length q - n" arbitrary: p q n k u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q n p k u. \<lbrakk>0 = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = length q - n
p \<in> \<P> k u
q \<in> \<P> k u
charslength p = charslength (take n q)
charslength p \<le> k
admissible (p @ drop n q)

goal (2 subgoals):
 1. \<And>q n p k u. \<lbrakk>0 = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
0 = length q - n
p \<in> \<P> k u
q \<in> \<P> k u
charslength p = charslength (take n q)
charslength p \<le> k
admissible (p @ drop n q)
[PROOF STEP]
have "0 = length q - n"
[PROOF STATE]
proof (prove)
using this:
0 = length q - n
p \<in> \<P> k u
q \<in> \<P> k u
charslength p = charslength (take n q)
charslength p \<le> k
admissible (p @ drop n q)

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

goal (2 subgoals):
 1. \<And>q n p k u. \<lbrakk>0 = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = length q - n
[PROOF STEP]
have n: "n \<ge> length q"
[PROOF STATE]
proof (prove)
using this:
0 = length q - n

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

goal (2 subgoals):
 1. \<And>q n p k u. \<lbrakk>0 = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length q \<le> n
[PROOF STEP]
have "drop n q = []"
[PROOF STATE]
proof (prove)
using this:
length q \<le> n

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

goal (2 subgoals):
 1. \<And>q n p k u. \<lbrakk>0 = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
drop n q = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
drop n q = []

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
by (simp add: "0.prems"(1))
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal (1 subgoal):
 1. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l = length ?q - ?n; ?p \<in> \<P> ?k ?u; ?q \<in> \<P> ?k ?u; charslength ?p = charslength (take ?n ?q); charslength ?p \<le> ?k; admissible (?p @ drop ?n ?q)\<rbrakk> \<Longrightarrow> ?p @ drop ?n ?q \<in> \<P> ?k ?u
Suc l = length q - n
p \<in> \<P> k u
q \<in> \<P> k u
charslength p = charslength (take n q)
charslength p \<le> k
admissible (p @ drop n q)

goal (1 subgoal):
 1. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have "n \<ge> length q \<or> n < length q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length q \<le> n \<or> n < length q
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length q \<le> n \<or> n < length q

goal (1 subgoal):
 1. \<And>x q n p k u. \<lbrakk>\<And>q n p k u. \<lbrakk>x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u; Suc x = length q - n; p \<in> \<P> k u; q \<in> \<P> k u; charslength p = charslength (take n q); charslength p \<le> k; admissible (p @ drop n q)\<rbrakk> \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length q \<le> n \<or> n < length q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length q \<le> n \<or> n < length q

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length q \<le> n \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
length q \<le> n

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

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

goal (2 subgoals):
 1. length q \<le> n \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
drop n q = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
drop n q = []

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
by (simp add: Suc.prems(1))
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
n < length q

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < length q
[PROOF STEP]
have "length q > 0"
[PROOF STATE]
proof (prove)
using this:
n < length q

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

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < length q
[PROOF STEP]
have q_nonempty: "q \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < length q

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

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
let ?q' = "butlast q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from q_nonempty Suc(2)
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> []
Suc l = length q - n
[PROOF STEP]
have h1: "l = length ?q' - n"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []
Suc l = length q - n

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

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have h2: "?q' \<in> \<P> k u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast q \<in> \<P> k u
[PROOF STEP]
by (metis Suc.prems(2) butlast_conv_take is_prefix_take prefixes_are_paths)
[PROOF STATE]
proof (state)
this:
butlast q \<in> \<P> k u

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have h3: "charslength p = charslength (take n ?q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength p = charslength (take n (butlast q))
[PROOF STEP]
using "2.hyps" Suc.prems(3) take_butlast
[PROOF STATE]
proof (prove)
using this:
n < length q
charslength p = charslength (take n q)
?n < length ?xs \<Longrightarrow> take ?n (butlast ?xs) = take ?n ?xs

goal (1 subgoal):
 1. charslength p = charslength (take n (butlast q))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
charslength p = charslength (take n (butlast q))

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have "is_prefix (p @ drop n ?q') (p @ drop n q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_prefix (p @ drop n (butlast q)) (p @ drop n q)
[PROOF STEP]
by (simp add: butlast_conv_take drop_take)
[PROOF STATE]
proof (state)
this:
is_prefix (p @ drop n (butlast q)) (p @ drop n q)

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
note h4 = is_prefix_admissible[OF this Suc.prems(5)]
[PROOF STATE]
proof (state)
this:
admissible (p @ drop n (butlast q))

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
note induct = Suc(1)[OF h1 Suc(3) h2 h3 Suc.prems(4) h4]
[PROOF STATE]
proof (state)
this:
p @ drop n (butlast q) \<in> \<P> k u

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
let ?p' = "p @ (drop n (butlast q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from induct
[PROOF STATE]
proof (chain)
picking this:
p @ drop n (butlast q) \<in> \<P> k u
[PROOF STEP]
have "?p' \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
p @ drop n (butlast q) \<in> \<P> k u

goal (1 subgoal):
 1. p @ drop n (butlast q) \<in> \<P> k u
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p @ drop n (butlast q) \<in> \<P> k u

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
let ?i = "charslength ?p'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have charslength_i[symmetric]: "charslength ?q' = ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength (butlast q) = charslength (p @ drop n (butlast q))
[PROOF STEP]
using Suc.prems(3)
[PROOF STATE]
proof (prove)
using this:
charslength p = charslength (take n q)

goal (1 subgoal):
 1. charslength (butlast q) = charslength (p @ drop n (butlast q))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p) = length (chars (take n q)) \<Longrightarrow> length (chars (butlast q)) = length (chars (take n q)) + length (chars (drop n (butlast q)))
[PROOF STEP]
apply (subst butlast_split[OF 2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (chars p) = length (chars (take n q)) \<Longrightarrow> length (chars (take n q @ drop n (butlast q))) = length (chars (take n q)) + length (chars (drop n (butlast q)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
charslength (p @ drop n (butlast q)) = charslength (butlast q)

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have q_split: "q = ?q'@[last q]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = butlast q @ [last q]
[PROOF STEP]
by (simp add: q_nonempty)
[PROOF STATE]
proof (state)
this:
q = butlast q @ [last q]

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
with Suc.prems(2) charslength_of_butlast
[PROOF STATE]
proof (chain)
picking this:
q \<in> \<P> k u
\<lbrakk>?p \<in> \<P> ?k ?u; ?p = ?q @ [?t]\<rbrakk> \<Longrightarrow> charslength ?q \<le> ?k
q = butlast q @ [last q]
[PROOF STEP]
have charslength_q': "charslength ?q' \<le> k"
[PROOF STATE]
proof (prove)
using this:
q \<in> \<P> k u
\<lbrakk>?p \<in> \<P> ?k ?u; ?p = ?q @ [?t]\<rbrakk> \<Longrightarrow> charslength ?q \<le> ?k
q = butlast q @ [last q]

goal (1 subgoal):
 1. charslength (butlast q) \<le> k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
charslength (butlast q) \<le> k

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from q_nonempty
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> []
[PROOF STEP]
have p'last: "?p'@[last q] = p@(drop n q)"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> []

goal (1 subgoal):
 1. (p @ drop n (butlast q)) @ [last q] = p @ drop n q
[PROOF STEP]
by (metis "2.hyps" append_assoc drop_eq_Nil drop_keep_last not_le q_split)
[PROOF STATE]
proof (state)
this:
(p @ drop n (butlast q)) @ [last q] = p @ drop n q

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have "?i \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) \<le> k
[PROOF STEP]
by (simp only: charslength_i charslength_q')
[PROOF STATE]
proof (state)
this:
charslength (p @ drop n (butlast q)) \<le> k

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
charslength (p @ drop n (butlast q)) \<le> k
[PROOF STEP]
have "?i = k \<or> ?i < k"
[PROOF STATE]
proof (prove)
using this:
charslength (p @ drop n (butlast q)) \<le> k

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) = k \<or> charslength (p @ drop n (butlast q)) < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
charslength (p @ drop n (butlast q)) = k \<or> charslength (p @ drop n (butlast q)) < k

goal (1 subgoal):
 1. n < length q \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
charslength (p @ drop n (butlast q)) = k \<or> charslength (p @ drop n (butlast q)) < k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
charslength (p @ drop n (butlast q)) = k \<or> charslength (p @ drop n (butlast q)) < k

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
proof (induct rule: disjCases2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. charslength (p @ drop n (butlast q)) = k \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
charslength (p @ drop n (butlast q)) = k

goal (2 subgoals):
 1. charslength (p @ drop n (butlast q)) = k \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have charslength_q': "charslength ?q' = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. charslength (butlast q) = k
[PROOF STEP]
using charslength_i[symmetric] 1
[PROOF STATE]
proof (prove)
using this:
charslength (butlast q) = charslength (p @ drop n (butlast q))
charslength (p @ drop n (butlast q)) = k

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

goal (2 subgoals):
 1. charslength (p @ drop n (butlast q)) = k \<Longrightarrow> p @ drop n q \<in> \<P> k u
 2. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from compatibility_def[OF induct Suc.prems(2) 1 q_split charslength_q']
[PROOF STATE]
proof (chain)
picking this:
admissible ((p @ drop n (butlast q)) @ [last q]) \<Longrightarrow> (p @ drop n (butlast q)) @ [last q] \<in> \<P> k u
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
admissible ((p @ drop n (butlast q)) @ [last q]) \<Longrightarrow> (p @ drop n (butlast q)) @ [last q] \<in> \<P> k u

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
by (simp only: p'last Suc.prems(5))
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
charslength (p @ drop n (butlast q)) < k

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from in_\<P>_charslength[OF induct]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v
[PROOF STEP]
obtain v1 where v1: "?p' \<in> \<P> ?i v1"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v

goal (1 subgoal):
 1. (\<And>v1. p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v1

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from last_step_of_path[OF Suc.prems(2) q_split]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength (butlast q) = k' \<and> last q \<in> \<Z> k' (Suc u')
[PROOF STEP]
have "\<exists> u. q \<in> \<P> ?i u"
[PROOF STATE]
proof (prove)
using this:
\<exists>k' u'. indexlt k' u' k u \<and> q \<in> \<P> k' (Suc u') \<and> charslength (butlast q) = k' \<and> last q \<in> \<Z> k' (Suc u')

goal (1 subgoal):
 1. \<exists>u. q \<in> \<P> (charslength (p @ drop n (butlast q))) u
[PROOF STEP]
by (metis charslength_i)
[PROOF STATE]
proof (state)
this:
\<exists>u. q \<in> \<P> (charslength (p @ drop n (butlast q))) u

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. q \<in> \<P> (charslength (p @ drop n (butlast q))) u
[PROOF STEP]
obtain v2 where v2: "q \<in> \<P> ?i v2"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. q \<in> \<P> (charslength (p @ drop n (butlast q))) u

goal (1 subgoal):
 1. (\<And>v2. q \<in> \<P> (charslength (p @ drop n (butlast q))) v2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> \<P> (charslength (p @ drop n (butlast q))) v2

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
let ?v = "max v1 v2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have "v1 \<le> ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<le> max v1 v2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v1 \<le> max v1 v2

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
with v1
[PROOF STATE]
proof (chain)
picking this:
p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v1
v1 \<le> max v1 v2
[PROOF STEP]
have dom1: "?p' \<in> \<P> ?i ?v"
[PROOF STATE]
proof (prove)
using this:
p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) v1
v1 \<le> max v1 v2

goal (1 subgoal):
 1. p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)
[PROOF STEP]
by (metis (no_types, opaque_lifting) subsetCE subset_\<P>k)
[PROOF STATE]
proof (state)
this:
p @ drop n (butlast q) \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
have "v2 \<le> ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v2 \<le> max v1 v2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v2 \<le> max v1 v2

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
with v2
[PROOF STATE]
proof (chain)
picking this:
q \<in> \<P> (charslength (p @ drop n (butlast q))) v2
v2 \<le> max v1 v2
[PROOF STEP]
have dom2: "q \<in> \<P> ?i ?v"
[PROOF STATE]
proof (prove)
using this:
q \<in> \<P> (charslength (p @ drop n (butlast q))) v2
v2 \<le> max v1 v2

goal (1 subgoal):
 1. q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)
[PROOF STEP]
by (metis (no_types, opaque_lifting) subsetCE subset_\<P>k)
[PROOF STATE]
proof (state)
this:
q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
from compatibility_def[OF dom1 dom2 _ q_split]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>charslength (p @ drop n (butlast q)) = charslength (p @ drop n (butlast q)); charslength (butlast q) = charslength (p @ drop n (butlast q)); admissible ((p @ drop n (butlast q)) @ [last q])\<rbrakk> \<Longrightarrow> (p @ drop n (butlast q)) @ [last q] \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)
[PROOF STEP]
have "p @ drop n q \<in> \<P> ?i ?v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>charslength (p @ drop n (butlast q)) = charslength (p @ drop n (butlast q)); charslength (butlast q) = charslength (p @ drop n (butlast q)); admissible ((p @ drop n (butlast q)) @ [last q])\<rbrakk> \<Longrightarrow> (p @ drop n (butlast q)) @ [last q] \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)
[PROOF STEP]
by (simp only: p'last charslength_i[symmetric] Suc.prems(5))
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)

goal (1 subgoal):
 1. charslength (p @ drop n (butlast q)) < k \<Longrightarrow> p @ drop n q \<in> \<P> k u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p @ drop n q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)
[PROOF STEP]
show "p @ drop n q \<in> \<P> k u"
[PROOF STATE]
proof (prove)
using this:
p @ drop n q \<in> \<P> (charslength (p @ drop n (butlast q))) (max v1 v2)

goal (1 subgoal):
 1. p @ drop n q \<in> \<P> k u
[PROOF STEP]
by (meson "2.hyps" subsetCE subset_\<P>)
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p @ drop n q \<in> \<P> k u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wellformed_item_derives:
  assumes wellformed: "wellformed_item x"
  shows "derives [item_nonterminal x] (item_rhs x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives [item_nonterminal x] (item_rhs x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. derives [item_nonterminal x] (item_rhs x)
[PROOF STEP]
from wellformed
[PROOF STATE]
proof (chain)
picking this:
wellformed_item x
[PROOF STEP]
have "(item_nonterminal x, item_rhs x) \<in> \<RR>"
[PROOF STATE]
proof (prove)
using this:
wellformed_item x

goal (1 subgoal):
 1. (item_nonterminal x, item_rhs x) \<in> \<RR>
[PROOF STEP]
by (simp add: item_nonterminal_def item_rhs_def wellformed_item_def)
[PROOF STATE]
proof (state)
this:
(item_nonterminal x, item_rhs x) \<in> \<RR>

goal (1 subgoal):
 1. derives [item_nonterminal x] (item_rhs x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(item_nonterminal x, item_rhs x) \<in> \<RR>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(item_nonterminal x, item_rhs x) \<in> \<RR>

goal (1 subgoal):
 1. derives [item_nonterminal x] (item_rhs x)
[PROOF STEP]
by (metis append_Nil2 derives1_def derives1_implies_derives is_sentence_concat
        rule_\<alpha>_type self_append_conv2)
[PROOF STATE]
proof (state)
this:
derives [item_nonterminal x] (item_rhs x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wellformed_complete_item_\<beta>:
  assumes wellformed: "wellformed_item x"
  assumes complete: "is_complete x"
  shows "item_\<beta> x = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<beta> x = []
[PROOF STEP]
using complete is_complete_def item_\<beta>_def
[PROOF STATE]
proof (prove)
using this:
is_complete x
is_complete ?x = (length (item_rhs ?x) \<le> item_dot ?x)
item_\<beta> ?x = drop (item_dot ?x) (item_rhs ?x)

goal (1 subgoal):
 1. item_\<beta> x = []
[PROOF STEP]
by auto


[STATEMENT]
lemma wellformed_complete_item_derives:
  assumes wellformed: "wellformed_item x"
  assumes complete: "is_complete x"
  shows "derives [item_nonterminal x] (item_\<alpha> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives [item_nonterminal x] (item_\<alpha> x)
[PROOF STEP]
using complete is_complete_def item_\<alpha>_def wellformed wellformed_item_derives
[PROOF STATE]
proof (prove)
using this:
is_complete x
is_complete ?x = (length (item_rhs ?x) \<le> item_dot ?x)
item_\<alpha> ?x = take (item_dot ?x) (item_rhs ?x)
wellformed_item x
wellformed_item ?x \<Longrightarrow> derives [item_nonterminal ?x] (item_rhs ?x)

goal (1 subgoal):
 1. derives [item_nonterminal x] (item_\<alpha> x)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_derivation_implies_admissible:
  "is_derivation (terminals p @ \<delta>) \<Longrightarrow> is_word (terminals p) \<Longrightarrow> admissible p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derivation (terminals p @ \<delta>); is_word (terminals p)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
using \<L>\<^sub>P_def admissible_def
[PROOF STATE]
proof (prove)
using this:
\<L>\<^sub>P = {uu_. \<exists>u v. uu_ = u \<and> is_word u \<and> is_derivation (u @ v)}
admissible ?ts = (terminals ?ts \<in> \<L>\<^sub>P)

goal (1 subgoal):
 1. \<lbrakk>is_derivation (terminals p @ \<delta>); is_word (terminals p)\<rbrakk> \<Longrightarrow> admissible p
[PROOF STEP]
by blast


[STATEMENT]
lemma item_rhs_of_inc_item[simp]: "item_rhs (inc_item x k) = item_rhs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_rhs (inc_item x k) = item_rhs x
[PROOF STEP]
by (auto simp add: inc_item_def item_rhs_def)


[STATEMENT]
lemma item_rule_of_inc_item[simp]: "item_rule (inc_item x k) = item_rule x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_rule (inc_item x k) = item_rule x
[PROOF STEP]
by (simp add: inc_item_def)


[STATEMENT]
lemma item_origin_of_inc_item[simp]: "item_origin (inc_item x k) = item_origin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_origin (inc_item x k) = item_origin x
[PROOF STEP]
by (simp add: inc_item_def)


[STATEMENT]
lemma item_end_of_inc_item[simp]: "item_end (inc_item x k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_end (inc_item x k) = k
[PROOF STEP]
by (simp add: inc_item_def)


[STATEMENT]
lemma item_dot_of_inc_item[simp]: "item_dot (inc_item x k) = (item_dot x) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_dot (inc_item x k) = item_dot x + 1
[PROOF STEP]
by (simp add: inc_item_def)


[STATEMENT]
lemma item_nonterminal_of_inc_item[simp]: "item_nonterminal (inc_item x k) = item_nonterminal x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_nonterminal (inc_item x k) = item_nonterminal x
[PROOF STEP]
by (simp add: inc_item_def item_nonterminal_def)


[STATEMENT]
lemma wellformed_inc_item:
  assumes wellformed: "wellformed_item x"
  assumes next_symbol: "next_symbol x = Some s"
  assumes k_upper_bound: "k \<le> length Doc"
  assumes k_lower_bound: "k \<ge> item_end x"
  shows "wellformed_item (inc_item x k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item (inc_item x k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wellformed_item (inc_item x k)
[PROOF STEP]
have k_lower_bound': "k \<ge> item_origin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_origin x \<le> k
[PROOF STEP]
using k_lower_bound wellformed wellformed_item_def
[PROOF STATE]
proof (prove)
using this:
item_end x \<le> k
wellformed_item x
wellformed_item ?x = (item_rule ?x \<in> \<RR> \<and> item_origin ?x \<le> item_end ?x \<and> item_end ?x \<le> length Doc \<and> item_dot ?x \<le> length (item_rhs ?x))

goal (1 subgoal):
 1. item_origin x \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
item_origin x \<le> k

goal (1 subgoal):
 1. wellformed_item (inc_item x k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item (inc_item x k)
[PROOF STEP]
apply (auto simp add: wellformed_item_def k_upper_bound k_lower_bound')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. item_rule x \<in> \<RR>
 2. Suc (item_dot x) \<le> length (item_rhs x)
[PROOF STEP]
using wellformed wellformed_item_def
[PROOF STATE]
proof (prove)
using this:
wellformed_item x
wellformed_item ?x = (item_rule ?x \<in> \<RR> \<and> item_origin ?x \<le> item_end ?x \<and> item_end ?x \<le> length Doc \<and> item_dot ?x \<le> length (item_rhs ?x))

goal (2 subgoals):
 1. item_rule x \<in> \<RR>
 2. Suc (item_dot x) \<le> length (item_rhs x)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (item_dot x) \<le> length (item_rhs x)
[PROOF STEP]
using is_complete_def next_symbol next_symbol_not_complete not_less_eq_eq
[PROOF STATE]
proof (prove)
using this:
is_complete ?x = (length (item_rhs ?x) \<le> item_dot ?x)
next_symbol x = Some s
next_symbol ?x = Some ?t \<Longrightarrow> \<not> is_complete ?x
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. Suc (item_dot x) \<le> length (item_rhs x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wellformed_item (inc_item x k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma item_\<alpha>_of_inc_item:
  assumes wellformed: "wellformed_item x"
  assumes next_symbol: "next_symbol x = Some s"
  shows "item_\<alpha> (inc_item x k) = item_\<alpha> x @ [s]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. item_\<alpha> (inc_item x k) = item_\<alpha> x @ [s]
[PROOF STEP]
by (metis (mono_tags, lifting) item_dot_of_inc_item item_rhs_of_inc_item
  One_nat_def add.right_neutral add_Suc_right is_complete_def item_\<alpha>_def item_\<beta>_def
  le_neq_implies_less list.sel(1) next_symbol next_symbol_not_complete next_symbol_starts_item_\<beta>
  take_hd_drop wellformed wellformed_item_def)


[STATEMENT]
lemma derives1_pad:
  assumes derives1: "derives1 \<alpha> \<beta>"
  assumes u: "is_sentence u"
  assumes v: "is_sentence v"
  shows "derives1 (u@\<alpha>@v) (u@\<beta>@v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
from derives1
[PROOF STATE]
proof (chain)
picking this:
derives1 \<alpha> \<beta>
[PROOF STEP]
have
   "\<exists>x y N \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>"
[PROOF STATE]
proof (prove)
using this:
derives1 \<alpha> \<beta>

goal (1 subgoal):
 1. \<exists>x y N \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>
[PROOF STEP]
by (auto simp add: derives1_def)
[PROOF STATE]
proof (state)
this:
\<exists>x y N \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>

goal (1 subgoal):
 1. derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x y N \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>
[PROOF STEP]
obtain x y N \<delta> where
   1: "\<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>"
[PROOF STATE]
proof (prove)
using this:
\<exists>x y N \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>

goal (1 subgoal):
 1. (\<And>x N y \<delta>. \<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>

goal (1 subgoal):
 1. derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
apply (simp only: derives1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y N \<alpha>'. u @ \<alpha> @ v = x @ [N] @ y \<and> u @ \<beta> @ v = x @ \<alpha>' @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<alpha>') \<in> \<RR>
[PROOF STEP]
apply (rule_tac x="u@x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y N \<alpha>'. u @ \<alpha> @ v = (u @ x) @ [N] @ y \<and> u @ \<beta> @ v = (u @ x) @ \<alpha>' @ y \<and> is_sentence (u @ x) \<and> is_sentence y \<and> (N, \<alpha>') \<in> \<RR>
[PROOF STEP]
apply (rule_tac x="y@v" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N \<alpha>'. u @ \<alpha> @ v = (u @ x) @ [N] @ y @ v \<and> u @ \<beta> @ v = (u @ x) @ \<alpha>' @ y @ v \<and> is_sentence (u @ x) \<and> is_sentence (y @ v) \<and> (N, \<alpha>') \<in> \<RR>
[PROOF STEP]
apply (rule_tac x=N in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha>'. u @ \<alpha> @ v = (u @ x) @ [N] @ y @ v \<and> u @ \<beta> @ v = (u @ x) @ \<alpha>' @ y @ v \<and> is_sentence (u @ x) \<and> is_sentence (y @ v) \<and> (N, \<alpha>') \<in> \<RR>
[PROOF STEP]
apply (rule_tac x=\<delta> in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u @ \<alpha> @ v = (u @ x) @ [N] @ y @ v \<and> u @ \<beta> @ v = (u @ x) @ \<delta> @ y @ v \<and> is_sentence (u @ x) \<and> is_sentence (y @ v) \<and> (N, \<delta>) \<in> \<RR>
[PROOF STEP]
using 1 u v is_sentence_concat
[PROOF STATE]
proof (prove)
using this:
\<alpha> = x @ [N] @ y \<and> \<beta> = x @ \<delta> @ y \<and> is_sentence x \<and> is_sentence y \<and> (N, \<delta>) \<in> \<RR>
is_sentence u
is_sentence v
is_sentence (?x @ ?y) = (is_sentence ?x \<and> is_sentence ?y)

goal (1 subgoal):
 1. u @ \<alpha> @ v = (u @ x) @ [N] @ y @ v \<and> u @ \<beta> @ v = (u @ x) @ \<delta> @ y @ v \<and> is_sentence (u @ x) \<and> is_sentence (y @ v) \<and> (N, \<delta>) \<in> \<RR>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derives1 (u @ \<alpha> @ v) (u @ \<beta> @ v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derives_pad:
  "derives \<alpha> \<beta> \<Longrightarrow> is_sentence u \<Longrightarrow> is_sentence v \<Longrightarrow> derives (u@\<alpha>@v) (u@\<beta>@v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>derives \<alpha> \<beta>; is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ \<beta> @ v)
[PROOF STEP]
proof (induct rule: derives_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ \<alpha> @ v)
 2. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:
is_sentence u
is_sentence v

goal (2 subgoals):
 1. \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ \<alpha> @ v)
 2. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_sentence u
is_sentence v

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
case (Step y z)
[PROOF STATE]
proof (state)
this:
derives \<alpha> y
derives1 y z
\<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v)
is_sentence u
is_sentence v

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
from Step
[PROOF STATE]
proof (chain)
picking this:
derives \<alpha> y
derives1 y z
\<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v)
is_sentence u
is_sentence v
[PROOF STEP]
have 1: "derives (u@\<alpha>@v) (u@y@v)"
[PROOF STATE]
proof (prove)
using this:
derives \<alpha> y
derives1 y z
\<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v)
is_sentence u
is_sentence v

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
from Step
[PROOF STATE]
proof (chain)
picking this:
derives \<alpha> y
derives1 y z
\<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v)
is_sentence u
is_sentence v
[PROOF STEP]
have 2: "derives1 y z"
[PROOF STATE]
proof (prove)
using this:
derives \<alpha> y
derives1 y z
\<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v)
is_sentence u
is_sentence v

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
derives1 y z
[PROOF STEP]
have "derives1 (u@y@v) (u@z@v)"
[PROOF STATE]
proof (prove)
using this:
derives1 y z

goal (1 subgoal):
 1. derives1 (u @ y @ v) (u @ z @ v)
[PROOF STEP]
by (simp add: Step.prems derives1_pad)
[PROOF STATE]
proof (state)
this:
derives1 (u @ y @ v) (u @ z @ v)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<lbrakk>is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ y @ v); is_sentence u; is_sentence v\<rbrakk> \<Longrightarrow> derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
derives1 (u @ y @ v) (u @ z @ v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
derives1 (u @ y @ v) (u @ z @ v)

goal (1 subgoal):
 1. derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
using "1" derives1_implies_derives derives_trans
[PROOF STATE]
proof (prove)
using this:
derives1 (u @ y @ v) (u @ z @ v)
derives (u @ \<alpha> @ v) (u @ y @ v)
derives1 ?a ?b \<Longrightarrow> derives ?a ?b
\<lbrakk>derives ?a ?b; derives ?b ?c\<rbrakk> \<Longrightarrow> derives ?a ?c

goal (1 subgoal):
 1. derives (u @ \<alpha> @ v) (u @ z @ v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derives (u @ \<alpha> @ v) (u @ z @ v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derives1_is_sentence: "derives1 \<alpha> \<beta> \<Longrightarrow> is_sentence \<alpha> \<and> is_sentence \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives1 \<alpha> \<beta> \<Longrightarrow> is_sentence \<alpha> \<and> is_sentence \<beta>
[PROOF STEP]
using Derives1_sentence1 Derives1_sentence2 derives1_implies_Derives1
[PROOF STATE]
proof (prove)
using this:
Derives1 ?a ?i ?r ?b \<Longrightarrow> is_sentence ?a
Derives1 ?a ?i ?r ?b \<Longrightarrow> is_sentence ?b
derives1 ?u ?v \<Longrightarrow> \<exists>i r. Derives1 ?u i r ?v

goal (1 subgoal):
 1. derives1 \<alpha> \<beta> \<Longrightarrow> is_sentence \<alpha> \<and> is_sentence \<beta>
[PROOF STEP]
by blast


[STATEMENT]
lemma derives_is_sentence: "derives \<alpha> \<beta> \<Longrightarrow> (\<alpha> = \<beta>) \<or> (is_sentence \<alpha> \<and> is_sentence \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives \<alpha> \<beta> \<Longrightarrow> \<alpha> = \<beta> \<or> is_sentence \<alpha> \<and> is_sentence \<beta>
[PROOF STEP]
proof (induct rule: derives_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<alpha> = \<alpha> \<or> is_sentence \<alpha> \<and> is_sentence \<alpha>
 2. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y\<rbrakk> \<Longrightarrow> \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
case Base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<alpha> = \<alpha> \<or> is_sentence \<alpha> \<and> is_sentence \<alpha>
 2. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y\<rbrakk> \<Longrightarrow> \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = \<alpha> \<or> is_sentence \<alpha> \<and> is_sentence \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> = \<alpha> \<or> is_sentence \<alpha> \<and> is_sentence \<alpha>

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y\<rbrakk> \<Longrightarrow> \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y\<rbrakk> \<Longrightarrow> \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
case (Step y z)
[PROOF STATE]
proof (state)
this:
derives \<alpha> y
derives1 y z
\<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>derives \<alpha> y; derives1 y z; \<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y\<rbrakk> \<Longrightarrow> \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
using Step.hyps(2) Step.hyps(3) derives1_is_sentence
[PROOF STATE]
proof (prove)
using this:
derives1 y z
\<alpha> = y \<or> is_sentence \<alpha> \<and> is_sentence y
derives1 ?\<alpha> ?\<beta> \<Longrightarrow> is_sentence ?\<alpha> \<and> is_sentence ?\<beta>

goal (1 subgoal):
 1. \<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> = z \<or> is_sentence \<alpha> \<and> is_sentence z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derives_append:
  assumes au: "derives a u"
  assumes bv: "derives b v"
  assumes is_sentence_a: "is_sentence a"
  assumes is_sentence_b: "is_sentence b"
  shows "derives (a@b) (u@v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
from au
[PROOF STATE]
proof (chain)
picking this:
derives a u
[PROOF STEP]
have "a = u \<or> (is_sentence a \<and> is_sentence u)"
[PROOF STATE]
proof (prove)
using this:
derives a u

goal (1 subgoal):
 1. a = u \<or> is_sentence a \<and> is_sentence u
[PROOF STEP]
using derives_is_sentence
[PROOF STATE]
proof (prove)
using this:
derives a u
derives ?\<alpha> ?\<beta> \<Longrightarrow> ?\<alpha> = ?\<beta> \<or> is_sentence ?\<alpha> \<and> is_sentence ?\<beta>

goal (1 subgoal):
 1. a = u \<or> is_sentence a \<and> is_sentence u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = u \<or> is_sentence a \<and> is_sentence u

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = u \<or> is_sentence a \<and> is_sentence u
[PROOF STEP]
have au_sentences: "is_sentence a \<and> is_sentence u"
[PROOF STATE]
proof (prove)
using this:
a = u \<or> is_sentence a \<and> is_sentence u

goal (1 subgoal):
 1. is_sentence a \<and> is_sentence u
[PROOF STEP]
using is_sentence_a
[PROOF STATE]
proof (prove)
using this:
a = u \<or> is_sentence a \<and> is_sentence u
is_sentence a

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

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
from bv
[PROOF STATE]
proof (chain)
picking this:
derives b v
[PROOF STEP]
have "b = v \<or> (is_sentence b \<and> is_sentence v)"
[PROOF STATE]
proof (prove)
using this:
derives b v

goal (1 subgoal):
 1. b = v \<or> is_sentence b \<and> is_sentence v
[PROOF STEP]
using derives_is_sentence
[PROOF STATE]
proof (prove)
using this:
derives b v
derives ?\<alpha> ?\<beta> \<Longrightarrow> ?\<alpha> = ?\<beta> \<or> is_sentence ?\<alpha> \<and> is_sentence ?\<beta>

goal (1 subgoal):
 1. b = v \<or> is_sentence b \<and> is_sentence v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = v \<or> is_sentence b \<and> is_sentence v

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = v \<or> is_sentence b \<and> is_sentence v
[PROOF STEP]
have bv_sentences: "is_sentence b \<and> is_sentence v"
[PROOF STATE]
proof (prove)
using this:
b = v \<or> is_sentence b \<and> is_sentence v

goal (1 subgoal):
 1. is_sentence b \<and> is_sentence v
[PROOF STEP]
using is_sentence_b
[PROOF STATE]
proof (prove)
using this:
b = v \<or> is_sentence b \<and> is_sentence v
is_sentence b

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

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
have 1: "derives (a@b) (u@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (a @ b) (u @ b)
[PROOF STEP]
apply (rule_tac derives_pad[OF au, where u="[]", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence b
[PROOF STEP]
using is_sentence_b
[PROOF STATE]
proof (prove)
using this:
is_sentence b

goal (1 subgoal):
 1. is_sentence b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
derives (a @ b) (u @ b)

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
have 2: "derives (u@b) (u@v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derives (u @ b) (u @ v)
[PROOF STEP]
apply (rule_tac derives_pad[OF bv, where v="[]", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sentence u
[PROOF STEP]
apply (simp add: au_sentences)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
derives (u @ b) (u @ v)

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
from 1 2 derives_trans
[PROOF STATE]
proof (chain)
picking this:
derives (a @ b) (u @ b)
derives (u @ b) (u @ v)
\<lbrakk>derives ?a ?b; derives ?b ?c\<rbrakk> \<Longrightarrow> derives ?a ?c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
derives (a @ b) (u @ b)
derives (u @ b) (u @ v)
\<lbrakk>derives ?a ?b; derives ?b ?c\<rbrakk> \<Longrightarrow> derives ?a ?c

goal (1 subgoal):
 1. derives (a @ b) (u @ v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
derives (a @ b) (u @ v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_sentence_item_\<alpha>: "wellformed_item x \<Longrightarrow> is_sentence (item_\<alpha> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item x \<Longrightarrow> is_sentence (item_\<alpha> x)
[PROOF STEP]
by (metis is_sentence_take item_\<alpha>_def item_rhs_def prod.collapse rule_\<alpha>_type wellformed_item_def)


[STATEMENT]
lemma is_nonterminal_item_nonterminal:  "wellformed_item x \<Longrightarrow> is_nonterminal (item_nonterminal x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed_item x \<Longrightarrow> is_nonterminal (item_nonterminal x)
[PROOF STEP]
by (metis item_nonterminal_def prod.collapse rule_nonterminal_type wellformed_item_def)