[STATEMENT]
lemma rtranclp_closed: "rtranclp R q q' \<Longrightarrow> X = X \<union> {q'. \<exists>q \<in> X. R q q'} \<Longrightarrow>
  q \<in> X \<Longrightarrow> q' \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R\<^sup>*\<^sup>* q q'; X = X \<union> {q'. \<exists>q\<in>X. R q q'}; q \<in> X\<rbrakk> \<Longrightarrow> q' \<in> X
[PROOF STEP]
by (induction q q' rule: rtranclp.induct) auto


[STATEMENT]
lemma rtranclp_closed_sub: "rtranclp R q q' \<Longrightarrow> {q'. \<exists>q \<in> X. R q q'} \<subseteq> X \<Longrightarrow>
  q \<in> X \<Longrightarrow> q' \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R\<^sup>*\<^sup>* q q'; {q'. \<exists>q\<in>X. R q q'} \<subseteq> X; q \<in> X\<rbrakk> \<Longrightarrow> q' \<in> X
[PROOF STEP]
by (induction q q' rule: rtranclp.induct) auto


[STATEMENT]
lemma rtranclp_closed_sub': "rtranclp R q q' \<Longrightarrow> q' = q \<or> (\<exists>q''. R q q'' \<and> rtranclp R q'' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* q q' \<Longrightarrow> q' = q \<or> (\<exists>q''. R q q'' \<and> R\<^sup>*\<^sup>* q'' q')
[PROOF STEP]
using converse_rtranclpE
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r\<^sup>*\<^sup>* ?x ?z; ?x = ?z \<Longrightarrow> ?P; \<And>y. \<lbrakk>?r ?x y; ?r\<^sup>*\<^sup>* y ?z\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. R\<^sup>*\<^sup>* q q' \<Longrightarrow> q' = q \<or> (\<exists>q''. R q q'' \<and> R\<^sup>*\<^sup>* q'' q')
[PROOF STEP]
by force


[STATEMENT]
lemma rtranclp_step: "rtranclp R q q'' \<Longrightarrow> (\<And>q'. R q q' \<longleftrightarrow> q' \<in> X) \<Longrightarrow>
  q = q'' \<or> (\<exists>q' \<in> X. R q q' \<and> rtranclp R q' q'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R\<^sup>*\<^sup>* q q''; \<And>q'. R q q' = (q' \<in> X)\<rbrakk> \<Longrightarrow> q = q'' \<or> (\<exists>q'\<in>X. R q q' \<and> R\<^sup>*\<^sup>* q' q'')
[PROOF STEP]
by (induction q q'' rule: rtranclp.induct)
     (auto intro: rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma rtranclp_unfold: "rtranclp R x z \<Longrightarrow> x = z \<or> (\<exists>y. R x y \<and> rtranclp R y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* x z \<Longrightarrow> x = z \<or> (\<exists>y. R x y \<and> R\<^sup>*\<^sup>* y z)
[PROOF STEP]
by (induction x z rule: rtranclp.induct) auto


[STATEMENT]
lemma q_in_SQ[code_unfold]: "q \<in> SQ \<longleftrightarrow> q0 \<le> q \<and> q < q0 + length transs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> SQ) = (q0 \<le> q \<and> q < q0 + length transs)
[PROOF STEP]
by (auto simp: SQ_def)


[STATEMENT]
lemma finite_SQ: "finite SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite SQ
[PROOF STEP]
by (auto simp add: SQ_def)


[STATEMENT]
lemma transs_q_in_set: "q \<in> SQ \<Longrightarrow> transs ! (q - q0) \<in> set transs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> SQ \<Longrightarrow> transs ! (q - q0) \<in> set transs
[PROOF STEP]
by (auto simp add: SQ_def)


[STATEMENT]
lemma finite_Q: "finite Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Q
[PROOF STEP]
by (auto simp add: Q_def SQ_def)


[STATEMENT]
lemma SQ_sub_Q: "SQ \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SQ \<subseteq> Q
[PROOF STEP]
by (auto simp add: SQ_def Q_def)


[STATEMENT]
lemma step_eps_mono: "step_eps [] q q' \<Longrightarrow> step_eps bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps [] q q' \<Longrightarrow> step_eps bs q q'
[PROOF STEP]
by (auto simp: step_eps_def split: transition.splits)


[STATEMENT]
lemma step_eps_sucs_sound: "q' \<in> step_eps_sucs bs q \<longleftrightarrow> step_eps bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q' \<in> step_eps_sucs bs q) = step_eps bs q q'
[PROOF STEP]
by (auto simp add: step_eps_sucs_def step_eps_def split: transition.splits)


[STATEMENT]
lemma step_eps_set_sound: "step_eps_set bs R = {q'. \<exists>q \<in> R. step_eps bs q q'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_set bs R = {q'. \<exists>q\<in>R. step_eps bs q q'}
[PROOF STEP]
using step_eps_sucs_sound
[PROOF STATE]
proof (prove)
using this:
(?q' \<in> step_eps_sucs ?bs ?q) = step_eps ?bs ?q ?q'

goal (1 subgoal):
 1. step_eps_set bs R = {q'. \<exists>q\<in>R. step_eps bs q q'}
[PROOF STEP]
by (auto simp add: step_eps_set_def)


[STATEMENT]
lemma step_eps_set_mono: "R \<subseteq> S \<Longrightarrow> step_eps_set bs R \<subseteq> step_eps_set bs S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> S \<Longrightarrow> step_eps_set bs R \<subseteq> step_eps_set bs S
[PROOF STEP]
by (auto simp add: step_eps_set_def)


[STATEMENT]
lemma step_eps_closure_dest: "step_eps_closure bs q q' \<Longrightarrow> q \<noteq> q' \<Longrightarrow> q \<in> SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; q \<noteq> q'\<rbrakk> \<Longrightarrow> q \<in> SQ
[PROOF STEP]
unfolding step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q \<noteq> q'\<rbrakk> \<Longrightarrow> q \<in> SQ
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<noteq> a \<Longrightarrow> a \<in> SQ
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<noteq> b \<Longrightarrow> a \<in> SQ; step_eps bs b c; a \<noteq> c\<rbrakk> \<Longrightarrow> a \<in> SQ
[PROOF STEP]
using step_eps_dest
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs ?q ?q' \<Longrightarrow> ?q \<in> SQ

goal (2 subgoals):
 1. \<And>a. a \<noteq> a \<Longrightarrow> a \<in> SQ
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<noteq> b \<Longrightarrow> a \<in> SQ; step_eps bs b c; a \<noteq> c\<rbrakk> \<Longrightarrow> a \<in> SQ
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_refl: "R \<subseteq> step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> step_eps_closure_set R bs
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def step_eps_closure_def)


[STATEMENT]
lemma step_eps_closure_set_mono: "R \<subseteq> S \<Longrightarrow> step_eps_closure_set R bs \<subseteq> step_eps_closure_set S bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> S \<Longrightarrow> step_eps_closure_set R bs \<subseteq> step_eps_closure_set S bs
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def)


[STATEMENT]
lemma step_eps_closure_set_empty: "step_eps_closure_set {} bs = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set {} bs = {}
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def)


[STATEMENT]
lemma step_eps_closure_set_mono': "step_eps_closure_set R [] \<subseteq> step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set R [] \<subseteq> step_eps_closure_set R bs
[PROOF STEP]
by (auto simp: step_eps_closure_set_def step_eps_closure_def) (metis mono_rtranclp step_eps_mono)


[STATEMENT]
lemma step_eps_closure_set_split: "step_eps_closure_set (R \<union> S) bs =
  step_eps_closure_set R bs \<union> step_eps_closure_set S bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set (R \<union> S) bs = step_eps_closure_set R bs \<union> step_eps_closure_set S bs
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def)


[STATEMENT]
lemma step_eps_closure_set_Un: "step_eps_closure_set (\<Union>x \<in> X. R x) bs =
  (\<Union>x \<in> X. step_eps_closure_set (R x) bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set (\<Union> (R ` X)) bs = (\<Union>x\<in>X. step_eps_closure_set (R x) bs)
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def)


[STATEMENT]
lemma step_eps_closure_set_idem: "step_eps_closure_set (step_eps_closure_set R bs) bs =
  step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set (step_eps_closure_set R bs) bs = step_eps_closure_set R bs
[PROOF STEP]
unfolding step_eps_closure_set_def step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>q\<in>\<Union>q\<in>R. Collect ((step_eps bs)\<^sup>*\<^sup>* q). Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = (\<Union>q\<in>R. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_flip:
  assumes "step_eps_closure_set R bs = R \<union> S"
  shows "step_eps_closure_set S bs \<subseteq> R \<union> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set S bs \<subseteq> R \<union> S
[PROOF STEP]
using step_eps_closure_set_idem[of R bs, unfolded assms, unfolded step_eps_closure_set_split]
[PROOF STATE]
proof (prove)
using this:
step_eps_closure_set R bs \<union> step_eps_closure_set S bs = R \<union> S

goal (1 subgoal):
 1. step_eps_closure_set S bs \<subseteq> R \<union> S
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_unfold: "(\<And>q'. step_eps bs q q' \<longleftrightarrow> q' \<in> X) \<Longrightarrow>
  step_eps_closure_set {q} bs = {q} \<union> step_eps_closure_set X bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q'. step_eps bs q q' = (q' \<in> X)) \<Longrightarrow> step_eps_closure_set {q} bs = {q} \<union> step_eps_closure_set X bs
[PROOF STEP]
unfolding step_eps_closure_set_def step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q'. step_eps bs q q' = (q' \<in> X)) \<Longrightarrow> (\<Union>q\<in>{q}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = {q} \<union> (\<Union>q\<in>X. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
using rtranclp_step[of "step_eps bs" q]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q ?q''; \<And>q'. step_eps bs q q' = (q' \<in> ?X)\<rbrakk> \<Longrightarrow> q = ?q'' \<or> (\<exists>q'\<in>?X. step_eps bs q q' \<and> (step_eps bs)\<^sup>*\<^sup>* q' ?q'')

goal (1 subgoal):
 1. (\<And>q'. step_eps bs q q' = (q' \<in> X)) \<Longrightarrow> (\<Union>q\<in>{q}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = {q} \<union> (\<Union>q\<in>X. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
by (auto simp add: converse_rtranclp_into_rtranclp)


[STATEMENT]
lemma step_step_eps_closure: "step_eps bs q q' \<Longrightarrow> q \<in> R \<Longrightarrow> q' \<in> step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps bs q q'; q \<in> R\<rbrakk> \<Longrightarrow> q' \<in> step_eps_closure_set R bs
[PROOF STEP]
unfolding step_eps_closure_set_def step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps bs q q'; q \<in> R\<rbrakk> \<Longrightarrow> q' \<in> (\<Union>q\<in>R. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_code[code]:
  "step_eps_closure_set R bs =
    (let R' = R \<union> step_eps_set bs R in if R = R' then R else step_eps_closure_set R' bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set R bs = (let R' = R \<union> step_eps_set bs R in if R = R' then R else step_eps_closure_set R' bs)
[PROOF STEP]
using rtranclp_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R\<^sup>*\<^sup>* ?q ?q'; ?X = ?X \<union> {q'. \<exists>q\<in>?X. ?R q q'}; ?q \<in> ?X\<rbrakk> \<Longrightarrow> ?q' \<in> ?X

goal (1 subgoal):
 1. step_eps_closure_set R bs = (let R' = R \<union> step_eps_set bs R in if R = R' then R else step_eps_closure_set R' bs)
[PROOF STEP]
by (auto simp add: step_eps_closure_set_def step_eps_closure_def step_eps_set_sound Let_def)


[STATEMENT]
lemma step_eps_closure_empty: "step_eps_closure bs q q' \<Longrightarrow> (\<And>q'. \<not>step_eps bs q q') \<Longrightarrow> q = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; \<And>q'. \<not> step_eps bs q q'\<rbrakk> \<Longrightarrow> q = q'
[PROOF STEP]
unfolding step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; \<And>q'. \<not> step_eps bs q q'\<rbrakk> \<Longrightarrow> q = q'
[PROOF STEP]
by (induction q q' rule: rtranclp.induct) auto


[STATEMENT]
lemma step_eps_closure_set_step_id: "(\<And>q q'. q \<in> R \<Longrightarrow> \<not>step_eps bs q q') \<Longrightarrow>
  step_eps_closure_set R bs = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q q'. q \<in> R \<Longrightarrow> \<not> step_eps bs q q') \<Longrightarrow> step_eps_closure_set R bs = R
[PROOF STEP]
using step_eps_closure_empty step_eps_closure_set_refl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; \<And>q'. \<not> step_eps ?bs ?q q'\<rbrakk> \<Longrightarrow> ?q = ?q'
?R \<subseteq> step_eps_closure_set ?R ?bs

goal (1 subgoal):
 1. (\<And>q q'. q \<in> R \<Longrightarrow> \<not> step_eps bs q q') \<Longrightarrow> step_eps_closure_set R bs = R
[PROOF STEP]
unfolding step_eps_closure_set_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; \<And>q'. \<not> step_eps ?bs ?q q'\<rbrakk> \<Longrightarrow> ?q = ?q'
?R \<subseteq> (\<Union>q\<in>?R. Collect (step_eps_closure ?bs q))

goal (1 subgoal):
 1. (\<And>q q'. q \<in> R \<Longrightarrow> \<not> step_eps bs q q') \<Longrightarrow> (\<Union>q\<in>R. Collect (step_eps_closure bs q)) = R
[PROOF STEP]
by blast


[STATEMENT]
lemma step_symb_sucs_sound: "q' \<in> step_symb_sucs q \<longleftrightarrow> step_symb q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q' \<in> step_symb_sucs q) = step_symb q q'
[PROOF STEP]
by (auto simp add: step_symb_sucs_def step_symb_def split: transition.splits)


[STATEMENT]
lemma step_symb_set_mono: "R \<subseteq> S \<Longrightarrow> step_symb_set R \<subseteq> step_symb_set S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> S \<Longrightarrow> step_symb_set R \<subseteq> step_symb_set S
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma step_symb_set_empty: "step_symb_set {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {} = {}
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma step_symb_set_proj: "step_symb_set R = step_symb_set (R \<inter> SQ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set R = step_symb_set (R \<inter> SQ)
[PROOF STEP]
using step_symb_dest
[PROOF STATE]
proof (prove)
using this:
step_symb ?q ?q' \<Longrightarrow> ?q \<in> SQ

goal (1 subgoal):
 1. step_symb_set R = step_symb_set (R \<inter> SQ)
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma step_symb_set_split: "step_symb_set (R \<union> S) = step_symb_set R \<union> step_symb_set S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set (R \<union> S) = step_symb_set R \<union> step_symb_set S
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma step_symb_set_Un: "step_symb_set (\<Union>x \<in> X. R x) = (\<Union>x \<in> X. step_symb_set (R x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set (\<Union> (R ` X)) = (\<Union>x\<in>X. step_symb_set (R x))
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma step_symb_set_code[code]: "step_symb_set R = \<Union>(step_symb_sucs ` R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set R = \<Union> (step_symb_sucs ` R)
[PROOF STEP]
using step_symb_sucs_sound
[PROOF STATE]
proof (prove)
using this:
(?q' \<in> step_symb_sucs ?q) = step_symb ?q ?q'

goal (1 subgoal):
 1. step_symb_set R = \<Union> (step_symb_sucs ` R)
[PROOF STEP]
by (auto simp add: step_symb_set_def)


[STATEMENT]
lemma delta_eps: "delta (step_eps_closure_set R bs) bs = delta R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta (step_eps_closure_set R bs) bs = delta R bs
[PROOF STEP]
unfolding delta_def step_eps_closure_set_idem
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set R bs) = step_symb_set (step_eps_closure_set R bs)
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma delta_eps_split:
  assumes "step_eps_closure_set R bs = R \<union> S"
  shows "delta R bs = step_symb_set R \<union> delta S bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = step_symb_set R \<union> delta S bs
[PROOF STEP]
unfolding delta_def assms step_symb_set_split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set R \<union> step_symb_set S = step_symb_set R \<union> step_symb_set (step_eps_closure_set S bs)
[PROOF STEP]
using step_symb_set_mono[OF step_eps_closure_set_flip[OF assms], unfolded step_symb_set_split]
    step_symb_set_mono[OF step_eps_closure_set_refl]
[PROOF STATE]
proof (prove)
using this:
step_symb_set (step_eps_closure_set S bs) \<subseteq> step_symb_set R \<union> step_symb_set S
step_symb_set ?R \<subseteq> step_symb_set (step_eps_closure_set ?R ?bs1)

goal (1 subgoal):
 1. step_symb_set R \<union> step_symb_set S = step_symb_set R \<union> step_symb_set (step_eps_closure_set S bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma delta_split: "delta (R \<union> S) bs = delta R bs \<union> delta S bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta (R \<union> S) bs = delta R bs \<union> delta S bs
[PROOF STEP]
by (auto simp add: delta_def step_symb_set_split step_eps_closure_set_split)


[STATEMENT]
lemma delta_Un: "delta (\<Union>x \<in> X. R x) bs = (\<Union>x \<in> X. delta (R x) bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta (\<Union> (R ` X)) bs = (\<Union>x\<in>X. delta (R x) bs)
[PROOF STEP]
unfolding delta_def step_eps_closure_set_Un step_symb_set_Un
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>X. step_symb_set (step_eps_closure_set (R x) bs)) = (\<Union>x\<in>X. step_symb_set (step_eps_closure_set (R x) bs))
[PROOF STEP]
by simp


[STATEMENT]
lemma delta_step_symb_set_absorb: "delta R bs = delta R bs \<union> step_symb_set R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = delta R bs \<union> step_symb_set R
[PROOF STEP]
using step_eps_closure_set_refl
[PROOF STATE]
proof (prove)
using this:
?R \<subseteq> step_eps_closure_set ?R ?bs

goal (1 subgoal):
 1. delta R bs = delta R bs \<union> step_symb_set R
[PROOF STEP]
by (auto simp add: delta_def step_symb_set_def)


[STATEMENT]
lemma delta_sub_eps_mono:
  assumes "S \<subseteq> step_eps_closure_set R bs"
  shows "delta S bs \<subseteq> delta R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta S bs \<subseteq> delta R bs
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set S bs) \<subseteq> step_symb_set (step_eps_closure_set R bs)
[PROOF STEP]
using step_symb_set_mono[OF step_eps_closure_set_mono[OF assms, of bs,
        unfolded step_eps_closure_set_idem]]
[PROOF STATE]
proof (prove)
using this:
step_symb_set (step_eps_closure_set S bs) \<subseteq> step_symb_set (step_eps_closure_set R bs)

goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set S bs) \<subseteq> step_symb_set (step_eps_closure_set R bs)
[PROOF STEP]
by simp


[STATEMENT]
lemma run_eps_split:
  assumes "step_eps_closure_set R bs = R \<union> S" "step_symb_set R = {}"
  shows "run R (bs # bss) = run S (bs # bss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (bs # bss) = run S (bs # bss)
[PROOF STEP]
unfolding run_def foldl.simps delta_eps_split[OF assms(1), unfolded assms(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta ({} \<union> delta S bs) bss = foldl delta (delta S bs) bss
[PROOF STEP]
by auto


[STATEMENT]
lemma run_empty: "run {} bss = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run {} bss = {}
[PROOF STEP]
unfolding run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta {} bss = {}
[PROOF STEP]
by (induction bss)
     (auto simp add: delta_def step_symb_set_empty step_eps_closure_set_empty)


[STATEMENT]
lemma run_Nil: "run R [] = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R [] = R
[PROOF STEP]
by (auto simp add: run_def)


[STATEMENT]
lemma run_Cons: "run R (bs # bss) = run (delta R bs) bss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (bs # bss) = run (delta R bs) bss
[PROOF STEP]
unfolding run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta R (bs # bss) = foldl delta (delta R bs) bss
[PROOF STEP]
by simp


[STATEMENT]
lemma run_split: "run (R \<union> S) bss = run R bss \<union> run S bss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (R \<union> S) bss = run R bss \<union> run S bss
[PROOF STEP]
unfolding run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta (R \<union> S) bss = foldl delta R bss \<union> foldl delta S bss
[PROOF STEP]
by (induction bss arbitrary: R S) (auto simp add: delta_split)


[STATEMENT]
lemma run_Un: "run (\<Union>x \<in> X. R x) bss = (\<Union>x \<in> X. run (R x) bss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (\<Union> (R ` X)) bss = (\<Union>x\<in>X. run (R x) bss)
[PROOF STEP]
unfolding run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta (\<Union> (R ` X)) bss = (\<Union>x\<in>X. foldl delta (R x) bss)
[PROOF STEP]
by (induction bss arbitrary: R) (auto simp add: delta_Un)


[STATEMENT]
lemma run_comp: "run R (bss @ css) = run (run R bss) css"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (bss @ css) = run (run R bss) css
[PROOF STEP]
unfolding run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta R (bss @ css) = foldl delta (foldl delta R bss) css
[PROOF STEP]
by simp


[STATEMENT]
lemma step_eps_accept_eps: "step_eps bs q qf \<Longrightarrow> q \<in> R \<Longrightarrow> accept_eps R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps bs q qf; q \<in> R\<rbrakk> \<Longrightarrow> accept_eps R bs
[PROOF STEP]
unfolding accept_eps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps bs q qf; q \<in> R\<rbrakk> \<Longrightarrow> qf \<in> step_eps_closure_set R bs
[PROOF STEP]
using step_step_eps_closure
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps ?bs ?q ?q'; ?q \<in> ?R\<rbrakk> \<Longrightarrow> ?q' \<in> step_eps_closure_set ?R ?bs

goal (1 subgoal):
 1. \<lbrakk>step_eps bs q qf; q \<in> R\<rbrakk> \<Longrightarrow> qf \<in> step_eps_closure_set R bs
[PROOF STEP]
by simp


[STATEMENT]
lemma accept_eps_empty: "accept_eps {} bs \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps {} bs = False
[PROOF STEP]
by (auto simp add: accept_eps_def step_eps_closure_set_def)


[STATEMENT]
lemma accept_eps_split: "accept_eps (R \<union> S) bs \<longleftrightarrow> accept_eps R bs \<or> accept_eps S bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (R \<union> S) bs = (accept_eps R bs \<or> accept_eps S bs)
[PROOF STEP]
by (auto simp add: accept_eps_def step_eps_closure_set_split)


[STATEMENT]
lemma accept_eps_Un: "accept_eps (\<Union>x \<in> X. R x) bs \<longleftrightarrow> (\<exists>x \<in> X. accept_eps (R x) bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (\<Union> (R ` X)) bs = (\<exists>x\<in>X. accept_eps (R x) bs)
[PROOF STEP]
by (auto simp add: accept_eps_def step_eps_closure_set_def)


[STATEMENT]
lemma run_accept_eps_empty: "\<not>run_accept_eps {} bss bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> run_accept_eps {} bss bs
[PROOF STEP]
unfolding run_accept_eps_def run_empty accept_eps_empty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> False
[PROOF STEP]
by simp


[STATEMENT]
lemma run_accept_eps_Nil: "run_accept_eps R [] cs \<longleftrightarrow> accept_eps R cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R [] cs = accept_eps R cs
[PROOF STEP]
by (auto simp add: run_accept_eps_def run_Nil)


[STATEMENT]
lemma run_accept_eps_Cons: "run_accept_eps R (bs # bss) cs \<longleftrightarrow> run_accept_eps (delta R bs) bss cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R (bs # bss) cs = run_accept_eps (delta R bs) bss cs
[PROOF STEP]
by (auto simp add: run_accept_eps_def run_Cons)


[STATEMENT]
lemma run_accept_eps_Cons_delta_cong: "delta R bs = delta S bs \<Longrightarrow>
  run_accept_eps R (bs # bss) cs \<longleftrightarrow> run_accept_eps S (bs # bss) cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = delta S bs \<Longrightarrow> run_accept_eps R (bs # bss) cs = run_accept_eps S (bs # bss) cs
[PROOF STEP]
unfolding run_accept_eps_Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = delta S bs \<Longrightarrow> run_accept_eps (delta R bs) bss cs = run_accept_eps (delta S bs) bss cs
[PROOF STEP]
by auto


[STATEMENT]
lemma run_accept_eps_Nil_eps: "run_accept_eps (step_eps_closure_set R bs) [] bs \<longleftrightarrow> run_accept_eps R [] bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps (step_eps_closure_set R bs) [] bs = run_accept_eps R [] bs
[PROOF STEP]
unfolding run_accept_eps_Nil accept_eps_def step_eps_closure_set_idem
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qf \<in> step_eps_closure_set R bs) = (qf \<in> step_eps_closure_set R bs)
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma run_accept_eps_Cons_eps: "run_accept_eps (step_eps_closure_set R cs) (cs # css) bs \<longleftrightarrow>
  run_accept_eps R (cs # css) bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps (step_eps_closure_set R cs) (cs # css) bs = run_accept_eps R (cs # css) bs
[PROOF STEP]
unfolding run_accept_eps_Cons delta_eps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps (delta R cs) css bs = run_accept_eps (delta R cs) css bs
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma run_accept_eps_Nil_eps_split:
  assumes "step_eps_closure_set R bs = R \<union> S" "step_symb_set R = {}" "qf \<notin> R"
  shows "run_accept_eps R [] bs = run_accept_eps S [] bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R [] bs = run_accept_eps S [] bs
[PROOF STEP]
unfolding Nil run_accept_eps_Nil accept_eps_def assms(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qf \<in> R \<union> S) = (qf \<in> step_eps_closure_set S bs)
[PROOF STEP]
using assms(3) step_eps_closure_set_refl step_eps_closure_set_flip[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
qf \<notin> R
?R \<subseteq> step_eps_closure_set ?R ?bs
step_eps_closure_set S bs \<subseteq> R \<union> S

goal (1 subgoal):
 1. (qf \<in> R \<union> S) = (qf \<in> step_eps_closure_set S bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma run_accept_eps_Cons_eps_split:
  assumes "step_eps_closure_set R cs = R \<union> S" "step_symb_set R = {}" "qf \<notin> R"
  shows "run_accept_eps R (cs # css) bs = run_accept_eps S (cs # css) bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R (cs # css) bs = run_accept_eps S (cs # css) bs
[PROOF STEP]
unfolding run_accept_eps_def Cons run_eps_split[OF assms(1,2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (run S (cs # css)) bs = accept_eps (run S (cs # css)) bs
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma run_accept_eps_split: "run_accept_eps (R \<union> S) bss bs \<longleftrightarrow>
  run_accept_eps R bss bs \<or> run_accept_eps S bss bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps (R \<union> S) bss bs = (run_accept_eps R bss bs \<or> run_accept_eps S bss bs)
[PROOF STEP]
unfolding run_accept_eps_def run_split accept_eps_split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (accept_eps (run R bss) bs \<or> accept_eps (run S bss) bs) = (accept_eps (run R bss) bs \<or> accept_eps (run S bss) bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma run_accept_eps_Un: "run_accept_eps (\<Union>x \<in> X. R x) bss bs \<longleftrightarrow>
  (\<exists>x \<in> X. run_accept_eps (R x) bss bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps (\<Union> (R ` X)) bss bs = (\<exists>x\<in>X. run_accept_eps (R x) bss bs)
[PROOF STEP]
unfolding run_accept_eps_def run_Un accept_eps_Un
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>X. accept_eps (run (R x) bss) bs) = (\<exists>x\<in>X. accept_eps (run (R x) bss) bs)
[PROOF STEP]
by simp


[STATEMENT]
lemma step_eps_sucs'_sound: "q' \<in> step_eps_sucs' bs q \<longleftrightarrow> step_eps' bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q' \<in> step_eps_sucs' bs q) = step_eps' bs q q'
[PROOF STEP]
by (auto simp add: step_eps_sucs'_def step_eps'_def split: transition.splits)


[STATEMENT]
lemma step_eps_set'_sound: "step_eps_set' bs R = {q'. \<exists>q \<in> R. step_eps' bs q q'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_set' bs R = {q'. \<exists>q\<in>R. step_eps' bs q q'}
[PROOF STEP]
using step_eps_sucs'_sound
[PROOF STATE]
proof (prove)
using this:
(?q' \<in> step_eps_sucs' ?bs ?q) = step_eps' ?bs ?q ?q'

goal (1 subgoal):
 1. step_eps_set' bs R = {q'. \<exists>q\<in>R. step_eps' bs q q'}
[PROOF STEP]
by (auto simp add: step_eps_set'_def)


[STATEMENT]
lemma step_eps_closure_set'_code[code]:
  "step_eps_closure_set' R bs =
    (let R' = R \<union> step_eps_set' bs R in if R = R' then R else step_eps_closure_set' R' bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set' R bs = (let R' = R \<union> step_eps_set' bs R in if R = R' then R else step_eps_closure_set' R' bs)
[PROOF STEP]
using rtranclp_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R\<^sup>*\<^sup>* ?q ?q'; ?X = ?X \<union> {q'. \<exists>q\<in>?X. ?R q q'}; ?q \<in> ?X\<rbrakk> \<Longrightarrow> ?q' \<in> ?X

goal (1 subgoal):
 1. step_eps_closure_set' R bs = (let R' = R \<union> step_eps_set' bs R in if R = R' then R else step_eps_closure_set' R' bs)
[PROOF STEP]
by (auto simp add: step_eps_closure_set'_def step_eps_closure'_def step_eps_set'_sound Let_def)


[STATEMENT]
lemma q_in_SQ: "q \<in> NFA.SQ 0 transs \<longleftrightarrow> q < len"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> NFA.SQ 0 transs) = (q < len)
[PROOF STEP]
using len_def
[PROOF STATE]
proof (prove)
using this:
len = length transs

goal (1 subgoal):
 1. (q \<in> NFA.SQ 0 transs) = (q < len)
[PROOF STEP]
by (auto simp: NFA.SQ_def)


[STATEMENT]
lemma step_eps'_eq: "bs' = IArray bs \<Longrightarrow> step_eps bs q q' \<longleftrightarrow> step_eps' bs' q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps bs q q' = step_eps' bs' q q'
[PROOF STEP]
by (auto simp: NFA.step_eps_def NFA.step_eps'_def q_in_SQ transs_eq split: transition.splits)


[STATEMENT]
lemma step_eps_closure'_eq: "bs' = IArray bs \<Longrightarrow> step_eps_closure bs q q' \<longleftrightarrow> step_eps_closure' bs' q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_closure bs q q' = step_eps_closure' bs' q q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_closure bs q q' = step_eps_closure' bs' q q'
[PROOF STEP]
assume lassm: "bs' = IArray bs"
[PROOF STATE]
proof (state)
this:
bs' = IArray bs

goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_closure bs q q' = step_eps_closure' bs' q q'
[PROOF STEP]
have step_eps_eq_folded: "step_eps bs = step_eps' bs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps bs = step_eps' bs'
[PROOF STEP]
using step_eps'_eq[OF lassm]
[PROOF STATE]
proof (prove)
using this:
step_eps bs ?q ?q' = step_eps' bs' ?q ?q'

goal (1 subgoal):
 1. step_eps bs = step_eps' bs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step_eps bs = step_eps' bs'

goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_closure bs q q' = step_eps_closure' bs' q q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure bs q q' = step_eps_closure' bs' q q'
[PROOF STEP]
by (auto simp: NFA.step_eps_closure_def NFA.step_eps_closure'_def step_eps_eq_folded)
[PROOF STATE]
proof (state)
this:
step_eps_closure bs q q' = step_eps_closure' bs' q q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_eps_sucs'_eq: "bs' = IArray bs \<Longrightarrow> step_eps_sucs bs q = step_eps_sucs' bs' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_sucs bs q = step_eps_sucs' bs' q
[PROOF STEP]
by (auto simp: NFA.step_eps_sucs_def NFA.step_eps_sucs'_def q_in_SQ transs_eq
      split: transition.splits)


[STATEMENT]
lemma step_eps_set'_eq: "bs' = IArray bs \<Longrightarrow> step_eps_set bs R = step_eps_set' bs' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_set bs R = step_eps_set' bs' R
[PROOF STEP]
by (auto simp: NFA.step_eps_set_def NFA.step_eps_set'_def step_eps_sucs'_eq)


[STATEMENT]
lemma step_eps_closure_set'_eq: "bs' = IArray bs \<Longrightarrow> step_eps_closure_set R bs = step_eps_closure_set' R bs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_eps_closure_set R bs = step_eps_closure_set' R bs'
[PROOF STEP]
by (auto simp: NFA.step_eps_closure_set_def NFA.step_eps_closure_set'_def step_eps_closure'_eq)


[STATEMENT]
lemma step_symb_sucs'_eq: "bs' = IArray bs \<Longrightarrow> step_symb_sucs R = step_symb_sucs' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_symb_sucs R = step_symb_sucs' R
[PROOF STEP]
by (auto simp: NFA.step_symb_sucs_def NFA.step_symb_sucs'_def q_in_SQ transs_eq
      split: transition.splits)


[STATEMENT]
lemma step_symb_set'_eq: "bs' = IArray bs \<Longrightarrow> step_symb_set R = step_symb_set' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> step_symb_set R = step_symb_set' R
[PROOF STEP]
by (auto simp: step_symb_set_code NFA.step_symb_set'_def step_symb_sucs'_eq)


[STATEMENT]
lemma delta'_eq: "bs' = IArray bs \<Longrightarrow> delta R bs = delta' R bs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> delta R bs = delta' R bs'
[PROOF STEP]
by (auto simp: NFA.delta_def NFA.delta'_def step_eps_closure_set'_eq step_symb_set'_eq)


[STATEMENT]
lemma accept_eps'_eq: "bs' = IArray bs \<Longrightarrow> accept_eps R bs = accept_eps' R bs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs' = IArray bs \<Longrightarrow> accept_eps R bs = accept_eps' R bs'
[PROOF STEP]
by (auto simp: NFA.accept_eps_def NFA.accept_eps'_def step_eps_closure_set'_eq)


[STATEMENT]
lemma accept'_eq: "accept R = accept' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept R = accept' R
[PROOF STEP]
by (auto simp: NFA.accept_def NFA.accept'_def accept_eps'_eq iarray_of_list_def)


[STATEMENT]
lemma run'_eq: "bss' = map IArray bss \<Longrightarrow> run R bss = run' R bss'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bss' = map IArray bss \<Longrightarrow> run R bss = run' R bss'
[PROOF STEP]
by (induction bss arbitrary: R bss') (auto simp: NFA.run_def NFA.run'_def delta'_eq)


[STATEMENT]
lemma run_accept_eps'_eq: "bss' = map IArray bss \<Longrightarrow> bs' = IArray bs \<Longrightarrow>
  run_accept_eps R bss bs \<longleftrightarrow> run_accept_eps' R bss' bs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bss' = map IArray bss; bs' = IArray bs\<rbrakk> \<Longrightarrow> run_accept_eps R bss bs = run_accept_eps' R bss' bs'
[PROOF STEP]
by (auto simp: NFA.run_accept_eps_def NFA.run_accept_eps'_def accept_eps'_eq run'_eq)


[STATEMENT]
lemma run_accept'_eq: "bss' = map IArray bss \<Longrightarrow>
  run_accept R bss \<longleftrightarrow> run_accept' R bss'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bss' = map IArray bss \<Longrightarrow> run_accept R bss = run_accept' R bss'
[PROOF STEP]
by (auto simp: NFA.run_accept_def NFA.run_accept'_def run'_eq accept'_eq)


[STATEMENT]
lemma Q_diff_qf_SQ: "Q - {qf} = SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q - {qf} = SQ
[PROOF STEP]
using qf_not_in_SQ
[PROOF STATE]
proof (prove)
using this:
qf \<notin> SQ

goal (1 subgoal):
 1. Q - {qf} = SQ
[PROOF STEP]
by (auto simp add: NFA.Q_def)


[STATEMENT]
lemma q0_sub_SQ: "{q0} \<subseteq> SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q0} \<subseteq> SQ
[PROOF STEP]
using transs_not_Nil
[PROOF STATE]
proof (prove)
using this:
transs \<noteq> []

goal (1 subgoal):
 1. {q0} \<subseteq> SQ
[PROOF STEP]
by (auto simp add: NFA.SQ_def)


[STATEMENT]
lemma q0_sub_Q: "{q0} \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q0} \<subseteq> Q
[PROOF STEP]
using q0_sub_SQ SQ_sub_Q
[PROOF STATE]
proof (prove)
using this:
{q0} \<subseteq> SQ
NFA.SQ ?q0.0 ?transs \<subseteq> NFA.Q ?q0.0 ?qf ?transs

goal (1 subgoal):
 1. {q0} \<subseteq> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closed: "step_eps bs q q' \<Longrightarrow> q' \<in> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps bs q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
using transs_q_in_set state_closed
[PROOF STATE]
proof (prove)
using this:
?q \<in> NFA.SQ ?q0.0 ?transs \<Longrightarrow> ?transs ! (?q - ?q0.0) \<in> set ?transs
?t \<in> set transs \<Longrightarrow> state_set ?t \<subseteq> Q

goal (1 subgoal):
 1. step_eps bs q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
by (fastforce simp add: NFA.step_eps_def split: transition.splits)


[STATEMENT]
lemma step_eps_set_closed: "step_eps_set bs R \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_set bs R \<subseteq> Q
[PROOF STEP]
using step_eps_closed
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> Q

goal (1 subgoal):
 1. step_eps_set bs R \<subseteq> Q
[PROOF STEP]
by (auto simp add: step_eps_set_sound)


[STATEMENT]
lemma step_eps_closure_closed: "step_eps_closure bs q q' \<Longrightarrow> q \<noteq> q' \<Longrightarrow> q' \<in> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; q \<noteq> q'\<rbrakk> \<Longrightarrow> q' \<in> Q
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q \<noteq> q'\<rbrakk> \<Longrightarrow> q' \<in> Q
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<noteq> a \<Longrightarrow> a \<in> Q
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<noteq> b \<Longrightarrow> b \<in> Q; step_eps bs b c; a \<noteq> c\<rbrakk> \<Longrightarrow> c \<in> Q
[PROOF STEP]
using step_eps_closed
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> Q

goal (2 subgoals):
 1. \<And>a. a \<noteq> a \<Longrightarrow> a \<in> Q
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<noteq> b \<Longrightarrow> b \<in> Q; step_eps bs b c; a \<noteq> c\<rbrakk> \<Longrightarrow> c \<in> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_closed_union: "step_eps_closure_set R bs \<subseteq> R \<union> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set R bs \<subseteq> R \<union> Q
[PROOF STEP]
using step_eps_closure_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q \<noteq> ?q'\<rbrakk> \<Longrightarrow> ?q' \<in> Q

goal (1 subgoal):
 1. step_eps_closure_set R bs \<subseteq> R \<union> Q
[PROOF STEP]
by (auto simp add: NFA.step_eps_closure_set_def NFA.step_eps_closure_def)


[STATEMENT]
lemma step_eps_closure_set_closed: "R \<subseteq> Q \<Longrightarrow> step_eps_closure_set R bs \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> Q \<Longrightarrow> step_eps_closure_set R bs \<subseteq> Q
[PROOF STEP]
using step_eps_closure_set_closed_union
[PROOF STATE]
proof (prove)
using this:
step_eps_closure_set ?R ?bs \<subseteq> ?R \<union> Q

goal (1 subgoal):
 1. R \<subseteq> Q \<Longrightarrow> step_eps_closure_set R bs \<subseteq> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma step_symb_set_closed: "step_symb_set R \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set R \<subseteq> Q
[PROOF STEP]
using step_symb_closed
[PROOF STATE]
proof (prove)
using this:
step_symb ?q ?q' \<Longrightarrow> ?q' \<in> Q

goal (1 subgoal):
 1. step_symb_set R \<subseteq> Q
[PROOF STEP]
by (auto simp add: NFA.step_symb_set_def)


[STATEMENT]
lemma step_symb_set_qf: "step_symb_set {qf} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {qf} = {}
[PROOF STEP]
using qf_not_in_SQ step_symb_set_proj[of _ _ "{qf}"] step_symb_set_empty
[PROOF STATE]
proof (prove)
using this:
qf \<notin> SQ
NFA.step_symb_set ?q0.0 ?transs {qf} = NFA.step_symb_set ?q0.0 ?transs ({qf} \<inter> NFA.SQ ?q0.0 ?transs)
NFA.step_symb_set ?q0.0 ?transs {} = {}

goal (1 subgoal):
 1. step_symb_set {qf} = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma delta_closed: "delta R bs \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs \<subseteq> Q
[PROOF STEP]
using step_symb_set_closed
[PROOF STATE]
proof (prove)
using this:
step_symb_set ?R \<subseteq> Q

goal (1 subgoal):
 1. delta R bs \<subseteq> Q
[PROOF STEP]
by (auto simp add: NFA.delta_def)


[STATEMENT]
lemma run_closed_Cons: "run R (bs # bss) \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (bs # bss) \<subseteq> Q
[PROOF STEP]
unfolding NFA.run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl delta R (bs # bss) \<subseteq> Q
[PROOF STEP]
using delta_closed
[PROOF STATE]
proof (prove)
using this:
delta ?R ?bs \<subseteq> Q

goal (1 subgoal):
 1. foldl delta R (bs # bss) \<subseteq> Q
[PROOF STEP]
by (induction bss arbitrary: R bs) auto


[STATEMENT]
lemma run_closed: "R \<subseteq> Q \<Longrightarrow> run R bss \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> Q \<Longrightarrow> run R bss \<subseteq> Q
[PROOF STEP]
using run_Nil run_closed_Cons
[PROOF STATE]
proof (prove)
using this:
NFA.run ?q0.0 ?transs ?R [] = ?R
run ?R (?bs # ?bss) \<subseteq> Q

goal (1 subgoal):
 1. R \<subseteq> Q \<Longrightarrow> run R bss \<subseteq> Q
[PROOF STEP]
by (cases bss) auto


[STATEMENT]
lemma step_eps_qf: "step_eps bs qf q \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps bs qf q = False
[PROOF STEP]
using qf_not_in_SQ step_eps_dest
[PROOF STATE]
proof (prove)
using this:
qf \<notin> SQ
NFA.step_eps ?q0.0 ?transs ?bs ?q ?q' \<Longrightarrow> ?q \<in> NFA.SQ ?q0.0 ?transs

goal (1 subgoal):
 1. step_eps bs qf q = False
[PROOF STEP]
by force


[STATEMENT]
lemma step_symb_qf: "step_symb qf q \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb qf q = False
[PROOF STEP]
using qf_not_in_SQ step_symb_dest
[PROOF STATE]
proof (prove)
using this:
qf \<notin> SQ
NFA.step_symb ?q0.0 ?transs ?q ?q' \<Longrightarrow> ?q \<in> NFA.SQ ?q0.0 ?transs

goal (1 subgoal):
 1. step_symb qf q = False
[PROOF STEP]
by force


[STATEMENT]
lemma step_eps_closure_qf: "step_eps_closure bs q q' \<Longrightarrow> q = qf \<Longrightarrow> q = q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; q = qf\<rbrakk> \<Longrightarrow> q = q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q = qf\<rbrakk> \<Longrightarrow> q = q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a = qf \<Longrightarrow> a = a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a = qf \<Longrightarrow> a = b; step_eps bs b c; a = qf\<rbrakk> \<Longrightarrow> a = c
[PROOF STEP]
using step_eps_qf
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs qf ?q = False

goal (2 subgoals):
 1. \<And>a. a = qf \<Longrightarrow> a = a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a = qf \<Longrightarrow> a = b; step_eps bs b c; a = qf\<rbrakk> \<Longrightarrow> a = c
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_qf: "step_eps_closure_set {qf} bs = {qf}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set {qf} bs = {qf}
[PROOF STEP]
using step_eps_closure_qf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q = qf\<rbrakk> \<Longrightarrow> ?q = ?q'

goal (1 subgoal):
 1. step_eps_closure_set {qf} bs = {qf}
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q = qf\<rbrakk> \<Longrightarrow> ?q = ?q'

goal (1 subgoal):
 1. (\<Union>q\<in>{qf}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = {qf}
[PROOF STEP]
by auto


[STATEMENT]
lemma delta_qf: "delta {qf} bs = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta {qf} bs = {}
[PROOF STEP]
using step_eps_closure_qf step_symb_qf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q = qf\<rbrakk> \<Longrightarrow> ?q = ?q'
step_symb qf ?q = False

goal (1 subgoal):
 1. delta {qf} bs = {}
[PROOF STEP]
by (auto simp add: NFA.delta_def NFA.step_symb_set_def NFA.step_eps_closure_set_def)


[STATEMENT]
lemma run_qf_many: "run {qf} (bs # bss) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run {qf} (bs # bss) = {}
[PROOF STEP]
unfolding run_Cons delta_qf run_empty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = {}
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma run_accept_eps_qf_many: "run_accept_eps {qf} (bs # bss) cs \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps {qf} (bs # bss) cs = False
[PROOF STEP]
unfolding NFA.run_accept_eps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (run {qf} (bs # bss)) cs = False
[PROOF STEP]
using run_qf_many accept_eps_empty
[PROOF STATE]
proof (prove)
using this:
run {qf} (?bs # ?bss) = {}
NFA.accept_eps ?q0.0 ?qf ?transs {} ?bs = False

goal (1 subgoal):
 1. accept_eps (run {qf} (bs # bss)) cs = False
[PROOF STEP]
by simp


[STATEMENT]
lemma run_accept_eps_qf_one: "run_accept_eps {qf} [] bs \<longleftrightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps {qf} [] bs = True
[PROOF STEP]
unfolding NFA.run_accept_eps_def NFA.accept_eps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qf \<in> step_eps_closure_set (run {qf} []) bs) = True
[PROOF STEP]
using run_Nil step_eps_closure_set_refl
[PROOF STATE]
proof (prove)
using this:
NFA.run ?q0.0 ?transs ?R [] = ?R
?R \<subseteq> NFA.step_eps_closure_set ?q0.0 ?transs ?R ?bs

goal (1 subgoal):
 1. (qf \<in> step_eps_closure_set (run {qf} []) bs) = True
[PROOF STEP]
by force


[STATEMENT]
lemma q_Q_SQ_nfa'_SQ:  "q \<in> nfa'.Q \<Longrightarrow> q \<in> SQ \<longleftrightarrow> q \<in> nfa'.SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> (q \<in> SQ) = (q \<in> nfa'.SQ)
[PROOF STEP]
using SQ_sub qf_not_in_SQ qf_eq
[PROOF STATE]
proof (prove)
using this:
nfa'.SQ \<subseteq> SQ
qf \<notin> SQ
qf = qf'

goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> (q \<in> SQ) = (q \<in> nfa'.SQ)
[PROOF STEP]
by (auto simp add: NFA.Q_def)


[STATEMENT]
lemma step_eps_cong: "q \<in> nfa'.Q \<Longrightarrow> step_eps bs q q' \<longleftrightarrow> nfa'.step_eps bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> step_eps bs q q' = nfa'.step_eps bs q q'
[PROOF STEP]
using q_Q_SQ_nfa'_SQ transs_eq
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.Q \<Longrightarrow> (?q \<in> SQ) = (?q \<in> nfa'.SQ)
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> step_eps bs q q' = nfa'.step_eps bs q q'
[PROOF STEP]
by (auto simp add: NFA.step_eps_def)


[STATEMENT]
lemma eps_nfa'_step_eps_closure: "step_eps_closure bs q q' \<Longrightarrow> q \<in> nfa'.Q \<Longrightarrow>
  q' \<in> nfa'.Q \<and> nfa'.step_eps_closure bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> nfa'.step_eps_closure bs q q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a b; step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
using nfa'.step_eps_closure_closed step_eps_cong
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<noteq> ?q'\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q
?q \<in> nfa'.Q \<Longrightarrow> step_eps ?bs ?q ?q' = nfa'.step_eps ?bs ?q ?q'

goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a b; step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
by (auto simp add: NFA.step_eps_closure_def)


[STATEMENT]
lemma nfa'_eps_step_eps_closure: "nfa'.step_eps_closure bs q q' \<Longrightarrow> q \<in> nfa'.Q \<Longrightarrow>
  q' \<in> nfa'.Q \<and> step_eps_closure bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nfa'.step_eps_closure bs q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> step_eps_closure bs q q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* q q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
using nfa'.step_eps_closed step_eps_cong
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> nfa'.Q
?q \<in> nfa'.Q \<Longrightarrow> step_eps ?bs ?q ?q' = nfa'.step_eps ?bs ?q ?q'

goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
by (auto simp add: NFA.step_eps_closure_def intro: rtranclp.intros(2))


[STATEMENT]
lemma step_eps_closure_set_cong: "R \<subseteq> nfa'.Q \<Longrightarrow> step_eps_closure_set R bs =
  nfa'.step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs
[PROOF STEP]
using eps_nfa'_step_eps_closure nfa'_eps_step_eps_closure
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> nfa'.step_eps_closure ?bs ?q ?q'
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> step_eps_closure ?bs ?q ?q'

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs
[PROOF STEP]
by (fastforce simp add: NFA.step_eps_closure_set_def)


[STATEMENT]
lemma step_symb_cong: "q \<in> nfa'.Q \<Longrightarrow> step_symb q q' \<longleftrightarrow> nfa'.step_symb q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> step_symb q q' = nfa'.step_symb q q'
[PROOF STEP]
using q_Q_SQ_nfa'_SQ transs_eq
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.Q \<Longrightarrow> (?q \<in> SQ) = (?q \<in> nfa'.SQ)
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. q \<in> nfa'.Q \<Longrightarrow> step_symb q q' = nfa'.step_symb q q'
[PROOF STEP]
by (auto simp add: NFA.step_symb_def)


[STATEMENT]
lemma step_symb_set_cong: "R \<subseteq> nfa'.Q \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R
[PROOF STEP]
using step_symb_cong
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.Q \<Longrightarrow> step_symb ?q ?q' = nfa'.step_symb ?q ?q'

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R
[PROOF STEP]
by (auto simp add: NFA.step_symb_set_def)


[STATEMENT]
lemma delta_cong: "R \<subseteq> nfa'.Q \<Longrightarrow> delta R bs = nfa'.delta R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> delta R bs = nfa'.delta R bs
[PROOF STEP]
using step_symb_set_cong nfa'.step_eps_closure_set_closed
[PROOF STATE]
proof (prove)
using this:
?R \<subseteq> nfa'.Q \<Longrightarrow> step_symb_set ?R = nfa'.step_symb_set ?R
?R \<subseteq> nfa'.Q \<Longrightarrow> nfa'.step_eps_closure_set ?R ?bs \<subseteq> nfa'.Q

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> delta R bs = nfa'.delta R bs
[PROOF STEP]
by (auto simp add: NFA.delta_def step_eps_closure_set_cong)


[STATEMENT]
lemma run_cong: "R \<subseteq> nfa'.Q \<Longrightarrow> run R bss = nfa'.run R bss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> run R bss = nfa'.run R bss
[PROOF STEP]
unfolding NFA.run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> foldl delta R bss = foldl nfa'.delta R bss
[PROOF STEP]
using nfa'.delta_closed delta_cong
[PROOF STATE]
proof (prove)
using this:
nfa'.delta ?R ?bs \<subseteq> nfa'.Q
?R \<subseteq> nfa'.Q \<Longrightarrow> delta ?R ?bs = nfa'.delta ?R ?bs

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> foldl delta R bss = foldl nfa'.delta R bss
[PROOF STEP]
by (induction bss arbitrary: R) auto


[STATEMENT]
lemma accept_eps_cong: "R \<subseteq> nfa'.Q \<Longrightarrow> accept_eps R bs \<longleftrightarrow> nfa'.accept_eps R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> accept_eps R bs = nfa'.accept_eps R bs
[PROOF STEP]
unfolding NFA.accept_eps_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> (qf \<in> step_eps_closure_set R bs) = (qf' \<in> nfa'.step_eps_closure_set R bs)
[PROOF STEP]
using step_eps_closure_set_cong qf_eq
[PROOF STATE]
proof (prove)
using this:
?R \<subseteq> nfa'.Q \<Longrightarrow> step_eps_closure_set ?R ?bs = nfa'.step_eps_closure_set ?R ?bs
qf = qf'

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> (qf \<in> step_eps_closure_set R bs) = (qf' \<in> nfa'.step_eps_closure_set R bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma run_accept_eps_cong:
  assumes "R \<subseteq> nfa'.Q"
  shows "run_accept_eps R bss bs \<longleftrightarrow> nfa'.run_accept_eps R bss bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R bss bs = nfa'.run_accept_eps R bss bs
[PROOF STEP]
unfolding NFA.run_accept_eps_def run_cong[OF assms]
    accept_eps_cong[OF nfa'.run_closed[OF assms]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.accept_eps (nfa'.run R bss) bs = nfa'.accept_eps (nfa'.run R bss) bs
[PROOF STEP]
by simp


[STATEMENT]
lemma list_split_unfold: "(\<Union>(ys, zs) \<in> list_split (x # xs). f ys zs) =
  f [] (x # xs) \<union> (\<Union>(ys, zs) \<in> list_split xs. f (x # ys) zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>(ys, zs)\<in>list_split (x # xs). f ys zs) = f [] (x # xs) \<union> (\<Union>(ys, zs)\<in>list_split xs. f (x # ys) zs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma list_split_def: "list_split xs = (\<Union>n < length xs. {(take n xs, drop n xs)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_split xs = (\<Union>n<length xs. {(take n xs, drop n xs)})
[PROOF STEP]
using less_Suc_eq_0_disj
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m = 0 \<or> (\<exists>j. ?m = Suc j \<and> j < ?n))

goal (1 subgoal):
 1. list_split xs = (\<Union>n<length xs. {(take n xs, drop n xs)})
[PROOF STEP]
by (induction xs rule: list_split.induct) auto+


[STATEMENT]
lemma nfa'_Q_sub_Q: "nfa'.Q \<subseteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.Q \<subseteq> Q
[PROOF STEP]
unfolding NFA.Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.SQ \<union> {qf'} \<subseteq> SQ \<union> {qf}
[PROOF STEP]
using SQ_sub qf'_in_SQ
[PROOF STATE]
proof (prove)
using this:
nfa'.SQ \<subseteq> SQ
qf' \<in> SQ

goal (1 subgoal):
 1. nfa'.SQ \<union> {qf'} \<subseteq> SQ \<union> {qf}
[PROOF STEP]
by auto


[STATEMENT]
lemma q_SQ_SQ_nfa'_SQ:  "q \<in> nfa'.SQ \<Longrightarrow> q \<in> SQ \<longleftrightarrow> q \<in> nfa'.SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> (q \<in> SQ) = (q \<in> nfa'.SQ)
[PROOF STEP]
using SQ_sub
[PROOF STATE]
proof (prove)
using this:
nfa'.SQ \<subseteq> SQ

goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> (q \<in> SQ) = (q \<in> nfa'.SQ)
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_cong_SQ: "q \<in> nfa'.SQ \<Longrightarrow> step_eps bs q q' \<longleftrightarrow> nfa'.step_eps bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> step_eps bs q q' = nfa'.step_eps bs q q'
[PROOF STEP]
using q_SQ_SQ_nfa'_SQ transs_eq
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.SQ \<Longrightarrow> (?q \<in> SQ) = (?q \<in> nfa'.SQ)
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> step_eps bs q q' = nfa'.step_eps bs q q'
[PROOF STEP]
by (auto simp add: NFA.step_eps_def)


[STATEMENT]
lemma step_eps_cong_Q: "q \<in> nfa'.Q \<Longrightarrow> nfa'.step_eps bs q q' \<Longrightarrow> step_eps bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q \<in> nfa'.Q; nfa'.step_eps bs q q'\<rbrakk> \<Longrightarrow> step_eps bs q q'
[PROOF STEP]
using SQ_sub transs_eq
[PROOF STATE]
proof (prove)
using this:
nfa'.SQ \<subseteq> SQ
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. \<lbrakk>q \<in> nfa'.Q; nfa'.step_eps bs q q'\<rbrakk> \<Longrightarrow> step_eps bs q q'
[PROOF STEP]
by (auto simp add: NFA.step_eps_def)


[STATEMENT]
lemma nfa'_step_eps_closure_cong: "nfa'.step_eps_closure bs q q' \<Longrightarrow> q \<in> nfa'.Q \<Longrightarrow>
  step_eps_closure bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nfa'.step_eps_closure bs q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> step_eps_closure bs q q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* q q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
using NFA.Q_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
using this:
NFA.Q ?q0.0 ?qf ?transs = NFA.SQ ?q0.0 ?transs \<union> {?qf}
NFA.step_eps_closure ?q0.0 ?transs ?bs = (NFA.step_eps ?q0.0 ?transs ?bs)\<^sup>*\<^sup>*

goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
by (auto simp add: rtranclp.rtrancl_into_rtrancl step_eps_cong_SQ step_eps_dest)


[STATEMENT]
lemma nfa'_step_eps_closure_set_sub: "R \<subseteq> nfa'.Q \<Longrightarrow> nfa'.step_eps_closure_set R bs \<subseteq>
  step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> nfa'.step_eps_closure_set R bs \<subseteq> step_eps_closure_set R bs
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> (\<Union>q\<in>R. Collect (nfa'.step_eps_closure bs q)) \<subseteq> (\<Union>q\<in>R. Collect (step_eps_closure bs q))
[PROOF STEP]
using nfa'_step_eps_closure_cong
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> step_eps_closure ?bs ?q ?q'

goal (1 subgoal):
 1. R \<subseteq> nfa'.Q \<Longrightarrow> (\<Union>q\<in>R. Collect (nfa'.step_eps_closure bs q)) \<subseteq> (\<Union>q\<in>R. Collect (step_eps_closure bs q))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma eps_nfa'_step_eps_closure_cong: "step_eps_closure bs q q' \<Longrightarrow> q \<in> nfa'.Q \<Longrightarrow>
  (q' \<in> nfa'.Q \<and> nfa'.step_eps_closure bs q q') \<or>
  (nfa'.step_eps_closure bs q qf' \<and> step_eps_closure bs qf' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_eps_closure bs q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> nfa'.step_eps_closure bs q q' \<or> nfa'.step_eps_closure bs q qf' \<and> step_eps_closure bs qf' q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q q' \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* q qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a a \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a b \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' b; step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a c \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' c
[PROOF STEP]
using nfa'.step_eps_closure_closed nfa'.step_eps_closed step_eps_cong_SQ NFA.Q_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<noteq> ?q'\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q
nfa'.step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> nfa'.Q
?q \<in> nfa'.SQ \<Longrightarrow> step_eps ?bs ?q ?q' = nfa'.step_eps ?bs ?q ?q'
NFA.Q ?q0.0 ?qf ?transs = NFA.SQ ?q0.0 ?transs \<union> {?qf}

goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a a \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a b \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' b; step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* a c \<or> (nfa'.step_eps bs)\<^sup>*\<^sup>* a qf' \<and> (step_eps bs)\<^sup>*\<^sup>* qf' c
[PROOF STEP]
by (auto simp add: intro: rtranclp.rtrancl_into_rtrancl) fastforce+


[STATEMENT]
lemma nfa'_eps_step_eps_closure_cong: "nfa'.step_eps_closure bs q q' \<Longrightarrow> q \<in> nfa'.Q \<Longrightarrow>
  q' \<in> nfa'.Q \<and> step_eps_closure bs q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nfa'.step_eps_closure bs q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> step_eps_closure bs q q'
[PROOF STEP]
unfolding NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* q q'; q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> q' \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* q q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
using nfa'.step_eps_closed step_eps_cong_Q
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> nfa'.Q
\<lbrakk>?q \<in> nfa'.Q; nfa'.step_eps ?bs ?q ?q'\<rbrakk> \<Longrightarrow> step_eps ?bs ?q ?q'

goal (2 subgoals):
 1. \<And>a. a \<in> nfa'.Q \<Longrightarrow> a \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>(nfa'.step_eps bs)\<^sup>*\<^sup>* a b; a \<in> nfa'.Q \<Longrightarrow> b \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a b; nfa'.step_eps bs b c; a \<in> nfa'.Q\<rbrakk> \<Longrightarrow> c \<in> nfa'.Q \<and> (step_eps bs)\<^sup>*\<^sup>* a c
[PROOF STEP]
by (auto intro: rtranclp.intros(2))


[STATEMENT]
lemma step_eps_closure_set_cong_reach: "R \<subseteq> nfa'.Q \<Longrightarrow> qf' \<in> nfa'.step_eps_closure_set R bs \<Longrightarrow>
  step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs \<union> step_eps_closure_set {qf'} bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<in> nfa'.step_eps_closure_set R bs\<rbrakk> \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs \<union> step_eps_closure_set {qf'} bs
[PROOF STEP]
using eps_nfa'_step_eps_closure_cong nfa'_eps_step_eps_closure_cong
    rtranclp_trans[of "step_eps bs"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> nfa'.step_eps_closure ?bs ?q ?q' \<or> nfa'.step_eps_closure ?bs ?q qf' \<and> step_eps_closure ?bs qf' ?q'
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> step_eps_closure ?bs ?q ?q'
\<lbrakk>(step_eps bs)\<^sup>*\<^sup>* ?x ?y; (step_eps bs)\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<in> nfa'.step_eps_closure_set R bs\<rbrakk> \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs \<union> step_eps_closure_set {qf'} bs
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> (nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q ?q' \<or> (nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q qf' \<and> (step_eps ?bs)\<^sup>*\<^sup>* qf' ?q'
\<lbrakk>(nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> (step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'
\<lbrakk>(step_eps bs)\<^sup>*\<^sup>* ?x ?y; (step_eps bs)\<^sup>*\<^sup>* ?y ?z\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* ?x ?z

goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<in> (\<Union>q\<in>R. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q))\<rbrakk> \<Longrightarrow> (\<Union>q\<in>R. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = (\<Union>q\<in>R. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q)) \<union> (\<Union>q\<in>{qf'}. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
by auto blast+


[STATEMENT]
lemma step_eps_closure_set_cong_unreach: "R \<subseteq> nfa'.Q \<Longrightarrow> qf' \<notin> nfa'.step_eps_closure_set R bs \<Longrightarrow>
  step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<notin> nfa'.step_eps_closure_set R bs\<rbrakk> \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs
[PROOF STEP]
using eps_nfa'_step_eps_closure_cong nfa'_eps_step_eps_closure_cong
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> nfa'.step_eps_closure ?bs ?q ?q' \<or> nfa'.step_eps_closure ?bs ?q qf' \<and> step_eps_closure ?bs qf' ?q'
\<lbrakk>nfa'.step_eps_closure ?bs ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> step_eps_closure ?bs ?q ?q'

goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<notin> nfa'.step_eps_closure_set R bs\<rbrakk> \<Longrightarrow> step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> (nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q ?q' \<or> (nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q qf' \<and> (step_eps ?bs)\<^sup>*\<^sup>* qf' ?q'
\<lbrakk>(nfa'.step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q \<in> nfa'.Q\<rbrakk> \<Longrightarrow> ?q' \<in> nfa'.Q \<and> (step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'

goal (1 subgoal):
 1. \<lbrakk>R \<subseteq> nfa'.Q; qf' \<notin> (\<Union>q\<in>R. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q))\<rbrakk> \<Longrightarrow> (\<Union>q\<in>R. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = (\<Union>q\<in>R. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
by auto blast+


[STATEMENT]
lemma step_symb_cong_SQ: "q \<in> nfa'.SQ \<Longrightarrow> step_symb q q' \<longleftrightarrow> nfa'.step_symb q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> step_symb q q' = nfa'.step_symb q q'
[PROOF STEP]
using q_SQ_SQ_nfa'_SQ transs_eq
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.SQ \<Longrightarrow> (?q \<in> SQ) = (?q \<in> nfa'.SQ)
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. q \<in> nfa'.SQ \<Longrightarrow> step_symb q q' = nfa'.step_symb q q'
[PROOF STEP]
by (auto simp add: NFA.step_symb_def)


[STATEMENT]
lemma step_symb_cong_Q: "nfa'.step_symb q q' \<Longrightarrow> step_symb q q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.step_symb q q' \<Longrightarrow> step_symb q q'
[PROOF STEP]
using SQ_sub transs_eq
[PROOF STATE]
proof (prove)
using this:
nfa'.SQ \<subseteq> SQ
?q \<in> nfa'.SQ \<Longrightarrow> transs ! (?q - q0) = transs' ! (?q - q0')

goal (1 subgoal):
 1. nfa'.step_symb q q' \<Longrightarrow> step_symb q q'
[PROOF STEP]
by (auto simp add: NFA.step_symb_def)


[STATEMENT]
lemma step_symb_set_cong_SQ: "R \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R
[PROOF STEP]
using step_symb_cong_SQ
[PROOF STATE]
proof (prove)
using this:
?q \<in> nfa'.SQ \<Longrightarrow> step_symb ?q ?q' = nfa'.step_symb ?q ?q'

goal (1 subgoal):
 1. R \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set R = nfa'.step_symb_set R
[PROOF STEP]
by (auto simp add: NFA.step_symb_set_def)


[STATEMENT]
lemma step_symb_set_cong_Q: "nfa'.step_symb_set R \<subseteq> step_symb_set R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.step_symb_set R \<subseteq> step_symb_set R
[PROOF STEP]
using step_symb_cong_Q
[PROOF STATE]
proof (prove)
using this:
nfa'.step_symb ?q ?q' \<Longrightarrow> step_symb ?q ?q'

goal (1 subgoal):
 1. nfa'.step_symb_set R \<subseteq> step_symb_set R
[PROOF STEP]
by (auto simp add: NFA.step_symb_set_def)


[STATEMENT]
lemma delta_cong_unreach:
  assumes "R \<subseteq> nfa'.Q" "\<not>nfa'.accept_eps R bs"
  shows "delta R bs = nfa'.delta R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = nfa'.delta R bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. delta R bs = nfa'.delta R bs
[PROOF STEP]
have "nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ
[PROOF STEP]
using nfa'.step_eps_closure_set_closed[OF assms(1), unfolded NFA.Q_def]
      assms(2)[unfolded NFA.accept_eps_def]
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps_closure_set R ?bs \<subseteq> nfa'.SQ \<union> {qf'}
qf' \<notin> nfa'.step_eps_closure_set R bs

goal (1 subgoal):
 1. nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ

goal (1 subgoal):
 1. delta R bs = nfa'.delta R bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ

goal (1 subgoal):
 1. delta R bs = nfa'.delta R bs
[PROOF STEP]
unfolding NFA.accept_eps_def NFA.delta_def
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ

goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set R bs) = nfa'.step_symb_set (nfa'.step_eps_closure_set R bs)
[PROOF STEP]
using step_symb_set_cong_SQ
      step_eps_closure_set_cong_unreach[OF assms(1) assms(2)[unfolded NFA.accept_eps_def]]
[PROOF STATE]
proof (prove)
using this:
nfa'.step_eps_closure_set R bs \<subseteq> nfa'.SQ
?R \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set ?R = nfa'.step_symb_set ?R
step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs

goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set R bs) = nfa'.step_symb_set (nfa'.step_eps_closure_set R bs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
delta R bs = nfa'.delta R bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nfa'_delta_sub_delta:
  assumes "R \<subseteq> nfa'.Q"
  shows "nfa'.delta R bs \<subseteq> delta R bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.delta R bs \<subseteq> delta R bs
[PROOF STEP]
unfolding NFA.delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.step_symb_set (nfa'.step_eps_closure_set R bs) \<subseteq> step_symb_set (step_eps_closure_set R bs)
[PROOF STEP]
using step_symb_set_mono[OF nfa'_step_eps_closure_set_sub[OF assms]] step_symb_set_cong_Q
[PROOF STATE]
proof (prove)
using this:
NFA.step_symb_set ?q0.0 ?transs (nfa'.step_eps_closure_set R ?bs1) \<subseteq> NFA.step_symb_set ?q0.0 ?transs (step_eps_closure_set R ?bs1)
nfa'.step_symb_set ?R \<subseteq> step_symb_set ?R

goal (1 subgoal):
 1. nfa'.step_symb_set (nfa'.step_eps_closure_set R bs) \<subseteq> step_symb_set (step_eps_closure_set R bs)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma delta_cong_reach:
  assumes "R \<subseteq> nfa'.Q" "nfa'.accept_eps R bs"
  shows "delta R bs = nfa'.delta R bs \<union> delta {qf'} bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta R bs = nfa'.delta R bs \<union> delta {qf'} bs
[PROOF STEP]
proof (rule set_eqI, rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
assume assm: "q \<in> delta R bs"
[PROOF STATE]
proof (state)
this:
q \<in> delta R bs

goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
have nfa'_eps_diff_Un: "nfa'.step_eps_closure_set R bs =
    nfa'.step_eps_closure_set R bs - {qf'} \<union> {qf'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfa'.step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs - {qf'} \<union> {qf'}
[PROOF STEP]
using assms(2)[unfolded NFA.accept_eps_def]
[PROOF STATE]
proof (prove)
using this:
qf' \<in> nfa'.step_eps_closure_set R bs

goal (1 subgoal):
 1. nfa'.step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs - {qf'} \<union> {qf'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nfa'.step_eps_closure_set R bs = nfa'.step_eps_closure_set R bs - {qf'} \<union> {qf'}

goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
from assm
[PROOF STATE]
proof (chain)
picking this:
q \<in> delta R bs
[PROOF STEP]
have "q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union>
    step_symb_set {qf'} \<union> delta {qf'} bs"
[PROOF STATE]
proof (prove)
using this:
q \<in> delta R bs

goal (1 subgoal):
 1. q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set {qf'} \<union> delta {qf'} bs
[PROOF STEP]
unfolding NFA.delta_def step_eps_closure_set_cong_reach[OF assms(1)
      assms(2)[unfolded NFA.accept_eps_def]] step_symb_set_split[symmetric]
      nfa'_eps_diff_Un[symmetric]
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs \<union> step_eps_closure_set {qf'} bs)

goal (1 subgoal):
 1. q \<in> step_symb_set (nfa'.step_eps_closure_set R bs \<union> step_eps_closure_set {qf'} bs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set {qf'} \<union> delta {qf'} bs

goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set {qf'} \<union> delta {qf'} bs
[PROOF STEP]
have "q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs"
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set {qf'} \<union> delta {qf'} bs

goal (1 subgoal):
 1. q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs
[PROOF STEP]
using step_symb_set_mono[of "{qf'}" "step_eps_closure_set {qf'} bs",
      OF step_eps_closure_set_refl, unfolded NFA.delta_def[symmetric]]
    delta_step_symb_set_absorb
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set {qf'} \<union> delta {qf'} bs
NFA.step_symb_set ?q0.0 ?transs {qf'} \<subseteq> NFA.step_symb_set ?q0.0 ?transs (step_eps_closure_set {qf'} bs)
NFA.delta ?q0.0 ?transs ?R ?bs = NFA.delta ?q0.0 ?transs ?R ?bs \<union> NFA.step_symb_set ?q0.0 ?transs ?R

goal (1 subgoal):
 1. q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs

goal (2 subgoals):
 1. \<And>x. x \<in> delta R bs \<Longrightarrow> x \<in> nfa'.delta R bs \<union> delta {qf'} bs
 2. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs
[PROOF STEP]
show "q \<in> nfa'.delta R bs \<union> delta {qf'} bs"
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> delta {qf'} bs

goal (1 subgoal):
 1. q \<in> nfa'.delta R bs \<union> delta {qf'} bs
[PROOF STEP]
unfolding NFA.delta_def
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set (step_eps_closure_set {qf'} bs)

goal (1 subgoal):
 1. q \<in> nfa'.step_symb_set (nfa'.step_eps_closure_set R bs) \<union> step_symb_set (step_eps_closure_set {qf'} bs)
[PROOF STEP]
using nfa'.step_eps_closure_set_closed[OF assms(1), unfolded NFA.Q_def]
      step_symb_set_cong_SQ[of "nfa'.step_eps_closure_set R bs - {qf'}"]
      step_symb_set_mono
[PROOF STATE]
proof (prove)
using this:
q \<in> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) \<union> step_symb_set (step_eps_closure_set {qf'} bs)
nfa'.step_eps_closure_set R ?bs \<subseteq> nfa'.SQ \<union> {qf'}
nfa'.step_eps_closure_set R bs - {qf'} \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set (nfa'.step_eps_closure_set R bs - {qf'}) = nfa'.step_symb_set (nfa'.step_eps_closure_set R bs - {qf'})
?R \<subseteq> ?S \<Longrightarrow> NFA.step_symb_set ?q0.0 ?transs ?R \<subseteq> NFA.step_symb_set ?q0.0 ?transs ?S

goal (1 subgoal):
 1. q \<in> nfa'.step_symb_set (nfa'.step_eps_closure_set R bs) \<union> step_symb_set (step_eps_closure_set {qf'} bs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> nfa'.delta R bs \<union> delta {qf'} bs

goal (1 subgoal):
 1. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
assume "q \<in> nfa'.delta R bs \<union> delta {qf'} bs"
[PROOF STATE]
proof (state)
this:
q \<in> nfa'.delta R bs \<union> delta {qf'} bs

goal (1 subgoal):
 1. \<And>x. x \<in> nfa'.delta R bs \<union> delta {qf'} bs \<Longrightarrow> x \<in> delta R bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> nfa'.delta R bs \<union> delta {qf'} bs
[PROOF STEP]
show "q \<in> delta R bs"
[PROOF STATE]
proof (prove)
using this:
q \<in> nfa'.delta R bs \<union> delta {qf'} bs

goal (1 subgoal):
 1. q \<in> delta R bs
[PROOF STEP]
using nfa'_delta_sub_delta[OF assms(1)] delta_sub_eps_mono[of "{qf'}" _ _ R bs]
      assms(2)[unfolded NFA.accept_eps_def] nfa'_step_eps_closure_set_sub[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
q \<in> nfa'.delta R bs \<union> delta {qf'} bs
nfa'.delta R ?bs \<subseteq> delta R ?bs
{qf'} \<subseteq> NFA.step_eps_closure_set ?q0.0 ?transs R bs \<Longrightarrow> NFA.delta ?q0.0 ?transs {qf'} bs \<subseteq> NFA.delta ?q0.0 ?transs R bs
qf' \<in> nfa'.step_eps_closure_set R bs
nfa'.step_eps_closure_set R ?bs \<subseteq> step_eps_closure_set R ?bs

goal (1 subgoal):
 1. q \<in> delta R bs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
q \<in> delta R bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma run_cong:
  assumes "R \<subseteq> nfa'.Q"
  shows "run R bss = nfa'.run R bss \<union> (\<Union>(css, css') \<in> list_split bss.
    if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R bss = nfa'.run R bss \<union> (\<Union>(css, css')\<in>list_split bss. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> nfa'.Q

goal (1 subgoal):
 1. run R bss = nfa'.run R bss \<union> (\<Union>(css, css')\<in>list_split bss. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
proof (induction bss arbitrary: R rule: list_split.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R [] = nfa'.run R [] \<union> (\<Union>(css, css')\<in>list_split []. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
 2. \<And>x xs R. \<lbrakk>\<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R xs = nfa'.run R xs \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {}); R \<subseteq> nfa'.Q\<rbrakk> \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>(css, css')\<in>list_split (x # xs). if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
R \<subseteq> nfa'.Q

goal (2 subgoals):
 1. \<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R [] = nfa'.run R [] \<union> (\<Union>(css, css')\<in>list_split []. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
 2. \<And>x xs R. \<lbrakk>\<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R xs = nfa'.run R xs \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {}); R \<subseteq> nfa'.Q\<rbrakk> \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>(css, css')\<in>list_split (x # xs). if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R \<subseteq> nfa'.Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> nfa'.Q

goal (1 subgoal):
 1. run R [] = nfa'.run R [] \<union> (\<Union>a\<in>list_split []. case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
using run_Nil
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> nfa'.Q
NFA.run ?q0.0 ?transs ?R [] = ?R

goal (1 subgoal):
 1. run R [] = nfa'.run R [] \<union> (\<Union>a\<in>list_split []. case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run R [] = nfa'.run R [] \<union> (\<Union>a\<in>list_split []. case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})

goal (1 subgoal):
 1. \<And>x xs R. \<lbrakk>\<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R xs = nfa'.run R xs \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {}); R \<subseteq> nfa'.Q\<rbrakk> \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>(css, css')\<in>list_split (x # xs). if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs R. \<lbrakk>\<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R xs = nfa'.run R xs \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {}); R \<subseteq> nfa'.Q\<rbrakk> \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>(css, css')\<in>list_split (x # xs). if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
case (2 x xs)
[PROOF STATE]
proof (state)
this:
?R \<subseteq> nfa'.Q \<Longrightarrow> run ?R xs = nfa'.run ?R xs \<union> (\<Union>a\<in>list_split xs. case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps ?R css (hd css') then run {qf'} css' else {})
R \<subseteq> nfa'.Q

goal (1 subgoal):
 1. \<And>x xs R. \<lbrakk>\<And>R. R \<subseteq> nfa'.Q \<Longrightarrow> run R xs = nfa'.run R xs \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {}); R \<subseteq> nfa'.Q\<rbrakk> \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>(css, css')\<in>list_split (x # xs). if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>a\<in>list_split (x # xs). case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
apply (cases "nfa'.accept_eps R x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nfa'.accept_eps R x \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>a\<in>list_split (x # xs). case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
 2. \<not> nfa'.accept_eps R x \<Longrightarrow> run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>a\<in>list_split (x # xs). case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})
[PROOF STEP]
unfolding run_Cons delta_cong_reach[OF 2(2)]
      delta_cong_unreach[OF 2(2)] run_split run_accept_eps_Nil run_accept_eps_Cons
      list_split_unfold[of "\<lambda>ys zs. if nfa'.run_accept_eps R ys (hd zs)
      then run {qf'} zs else {}" x xs]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nfa'.accept_eps R x \<Longrightarrow> run (nfa'.delta R x) xs \<union> run (delta {qf'} x) xs = nfa'.run (nfa'.delta R x) xs \<union> ((if nfa'.accept_eps R (hd (x # xs)) then run (delta {qf'} x) xs else {}) \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps (nfa'.delta R x) css (hd css') then run {qf'} css' else {}))
 2. \<not> nfa'.accept_eps R x \<Longrightarrow> run (nfa'.delta R x) xs = nfa'.run (nfa'.delta R x) xs \<union> ((if nfa'.accept_eps R (hd (x # xs)) then run (delta {qf'} x) xs else {}) \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps (nfa'.delta R x) css (hd css') then run {qf'} css' else {}))
[PROOF STEP]
using 2(1)[of "nfa'.delta R x",
    OF nfa'.delta_closed, unfolded run_accept_eps_Nil]
[PROOF STATE]
proof (prove)
using this:
run (nfa'.delta R x) xs = nfa'.run (nfa'.delta R x) xs \<union> (\<Union>a\<in>list_split xs. case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps (nfa'.delta R x) css (hd css') then run {qf'} css' else {})

goal (2 subgoals):
 1. nfa'.accept_eps R x \<Longrightarrow> run (nfa'.delta R x) xs \<union> run (delta {qf'} x) xs = nfa'.run (nfa'.delta R x) xs \<union> ((if nfa'.accept_eps R (hd (x # xs)) then run (delta {qf'} x) xs else {}) \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps (nfa'.delta R x) css (hd css') then run {qf'} css' else {}))
 2. \<not> nfa'.accept_eps R x \<Longrightarrow> run (nfa'.delta R x) xs = nfa'.run (nfa'.delta R x) xs \<union> ((if nfa'.accept_eps R (hd (x # xs)) then run (delta {qf'} x) xs else {}) \<union> (\<Union>(css, css')\<in>list_split xs. if nfa'.run_accept_eps (nfa'.delta R x) css (hd css') then run {qf'} css' else {}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
run R (x # xs) = nfa'.run R (x # xs) \<union> (\<Union>a\<in>list_split (x # xs). case a of (css, css') \<Rightarrow> if nfa'.run_accept_eps R css (hd css') then run {qf'} css' else {})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma run_cong_Cons_sub:
  assumes "R \<subseteq> nfa'.Q" "delta {qf'} bs \<subseteq> nfa'.delta R bs"
  shows "run R (bs # bss) = nfa'.run R (bs # bss) \<union>
    (\<Union>(css, css') \<in> list_split bss.
    if nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') then run {qf'} css' else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run R (bs # bss) = nfa'.run R (bs # bss) \<union> (\<Union>(css, css')\<in>list_split bss. if nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') then run {qf'} css' else {})
[PROOF STEP]
unfolding run_Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (delta R bs) bss = nfa'.run (nfa'.delta R bs) bss \<union> (\<Union>(css, css')\<in>list_split bss. if nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') then run {qf'} css' else {})
[PROOF STEP]
using run_cong[OF nfa'.delta_closed]
    delta_cong_reach[OF assms(1)] delta_cong_unreach[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
run (nfa'.delta ?R1 ?bs1) ?bss = nfa'.run (nfa'.delta ?R1 ?bs1) ?bss \<union> (\<Union>(css, css')\<in>list_split ?bss. if nfa'.run_accept_eps (nfa'.delta ?R1 ?bs1) css (hd css') then run {qf'} css' else {})
nfa'.accept_eps R ?bs \<Longrightarrow> delta R ?bs = nfa'.delta R ?bs \<union> delta {qf'} ?bs
\<not> nfa'.accept_eps R ?bs \<Longrightarrow> delta R ?bs = nfa'.delta R ?bs

goal (1 subgoal):
 1. run (delta R bs) bss = nfa'.run (nfa'.delta R bs) bss \<union> (\<Union>(css, css')\<in>list_split bss. if nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') then run {qf'} css' else {})
[PROOF STEP]
by (cases "nfa'.accept_eps R bs") (auto simp add: Un_absorb2[OF assms(2)])


[STATEMENT]
lemma accept_eps_nfa'_run:
  assumes "R \<subseteq> nfa'.Q"
  shows "accept_eps (nfa'.run R bss) bs \<longleftrightarrow>
    nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (nfa'.run R bss) bs = (nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs)
[PROOF STEP]
unfolding NFA.accept_eps_def run_Nil
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qf \<in> step_eps_closure_set (nfa'.run R bss) bs) = (qf' \<in> nfa'.step_eps_closure_set (nfa'.run R bss) bs \<and> qf \<in> step_eps_closure_set {qf'} bs)
[PROOF STEP]
using step_eps_closure_set_cong_reach[OF nfa'.run_closed[OF assms]]
    step_eps_closure_set_cong_unreach[OF nfa'.run_closed[OF assms]] qf_not_in_SQ
    qf'_in_SQ nfa'.step_eps_closure_set_closed[OF nfa'.run_closed[OF assms],
    unfolded NFA.Q_def] SQ_sub
[PROOF STATE]
proof (prove)
using this:
qf' \<in> nfa'.step_eps_closure_set (nfa'.run R ?bss1) ?bs \<Longrightarrow> step_eps_closure_set (nfa'.run R ?bss1) ?bs = nfa'.step_eps_closure_set (nfa'.run R ?bss1) ?bs \<union> step_eps_closure_set {qf'} ?bs
qf' \<notin> nfa'.step_eps_closure_set (nfa'.run R ?bss1) ?bs \<Longrightarrow> step_eps_closure_set (nfa'.run R ?bss1) ?bs = nfa'.step_eps_closure_set (nfa'.run R ?bss1) ?bs
qf \<notin> SQ
qf' \<in> SQ
nfa'.step_eps_closure_set (nfa'.run R ?bss1) ?bs \<subseteq> nfa'.SQ \<union> {qf'}
nfa'.SQ \<subseteq> SQ

goal (1 subgoal):
 1. (qf \<in> step_eps_closure_set (nfa'.run R bss) bs) = (qf' \<in> nfa'.step_eps_closure_set (nfa'.run R bss) bs \<and> qf \<in> step_eps_closure_set {qf'} bs)
[PROOF STEP]
by (cases "qf' \<in> nfa'.step_eps_closure_set (nfa'.run R bss) bs") fastforce+


[STATEMENT]
lemma run_accept_eps_cong:
  assumes "R \<subseteq> nfa'.Q"
  shows "run_accept_eps R bss bs \<longleftrightarrow> (nfa'.run_accept_eps R bss bs \<and> run_accept_eps {qf'} [] bs) \<or>
    (\<exists>(css, css') \<in> list_split bss. nfa'.run_accept_eps R css (hd css') \<and>
    run_accept_eps {qf'} css' bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R bss bs = (nfa'.run_accept_eps R bss bs \<and> run_accept_eps {qf'} [] bs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.run_accept_eps R css (hd css') \<and> run_accept_eps {qf'} css' bs))
[PROOF STEP]
unfolding NFA.run_accept_eps_def run_cong[OF assms] accept_eps_split
    accept_eps_Un accept_eps_nfa'_run[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs \<or> (\<exists>x\<in>list_split bss. accept_eps (case x of (css, css') \<Rightarrow> if nfa'.accept_eps (nfa'.run R css) (hd css') then run {qf'} css' else {}) bs)) = (nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.accept_eps (nfa'.run R css) (hd css') \<and> accept_eps (run {qf'} css') bs))
[PROOF STEP]
using accept_eps_empty
[PROOF STATE]
proof (prove)
using this:
NFA.accept_eps ?q0.0 ?qf ?transs {} ?bs = False

goal (1 subgoal):
 1. (nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs \<or> (\<exists>x\<in>list_split bss. accept_eps (case x of (css, css') \<Rightarrow> if nfa'.accept_eps (nfa'.run R css) (hd css') then run {qf'} css' else {}) bs)) = (nfa'.accept_eps (nfa'.run R bss) bs \<and> accept_eps (run {qf'} []) bs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.accept_eps (nfa'.run R css) (hd css') \<and> accept_eps (run {qf'} css') bs))
[PROOF STEP]
by (auto split: if_splits)+


[STATEMENT]
lemma run_accept_eps_cong_Cons_sub:
  assumes "R \<subseteq> nfa'.Q" "delta {qf'} bs \<subseteq> nfa'.delta R bs"
  shows "run_accept_eps R (bs # bss) cs \<longleftrightarrow>
    (nfa'.run_accept_eps R (bs # bss) cs \<and> run_accept_eps {qf'} [] cs) \<or>
    (\<exists>(css, css') \<in> list_split bss. nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') \<and>
    run_accept_eps {qf'} css' cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps R (bs # bss) cs = (nfa'.run_accept_eps R (bs # bss) cs \<and> run_accept_eps {qf'} [] cs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.run_accept_eps (nfa'.delta R bs) css (hd css') \<and> run_accept_eps {qf'} css' cs))
[PROOF STEP]
unfolding NFA.run_accept_eps_def run_cong_Cons_sub[OF assms]
    accept_eps_split accept_eps_Un accept_eps_nfa'_run[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nfa'.accept_eps (nfa'.run R (bs # bss)) cs \<and> accept_eps (run {qf'} []) cs \<or> (\<exists>x\<in>list_split bss. accept_eps (case x of (css, css') \<Rightarrow> if nfa'.accept_eps (nfa'.run (nfa'.delta R bs) css) (hd css') then run {qf'} css' else {}) cs)) = (nfa'.accept_eps (nfa'.run R (bs # bss)) cs \<and> accept_eps (run {qf'} []) cs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.accept_eps (nfa'.run (nfa'.delta R bs) css) (hd css') \<and> accept_eps (run {qf'} css') cs))
[PROOF STEP]
using accept_eps_empty
[PROOF STATE]
proof (prove)
using this:
NFA.accept_eps ?q0.0 ?qf ?transs {} ?bs = False

goal (1 subgoal):
 1. (nfa'.accept_eps (nfa'.run R (bs # bss)) cs \<and> accept_eps (run {qf'} []) cs \<or> (\<exists>x\<in>list_split bss. accept_eps (case x of (css, css') \<Rightarrow> if nfa'.accept_eps (nfa'.run (nfa'.delta R bs) css) (hd css') then run {qf'} css' else {}) cs)) = (nfa'.accept_eps (nfa'.run R (bs # bss)) cs \<and> accept_eps (run {qf'} []) cs \<or> (\<exists>(css, css')\<in>list_split bss. nfa'.accept_eps (nfa'.run (nfa'.delta R bs) css) (hd css') \<and> accept_eps (run {qf'} css') cs))
[PROOF STEP]
by (auto split: if_splits)+


[STATEMENT]
lemma step_symb_set_q0: "step_symb_set {q0} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {q0} = {}
[PROOF STEP]
unfolding NFA.step_symb_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0}. step_symb q q'} = {}
[PROOF STEP]
using step_symb_q0
[PROOF STATE]
proof (prove)
using this:
\<not> step_symb q0 ?q

goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0}. step_symb q q'} = {}
[PROOF STEP]
by simp