[STATEMENT]
lemma fin_steps_plusI:
 "[| (start A,q) : steps A u; u \<noteq> []; fin A p |] 
 ==> (p,q) : steps (plus A) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply (case_tac "u")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = []\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
 2. \<And>a list. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(start A, q) \<in> step A a O steps A list; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> step (RegExp2NA.plus A) a O steps (RegExp2NA.plus A) list
[PROOF STEP]
apply (blast intro: steps_plusI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done