[STATEMENT]
lemma acceptI[intro?]: "\<lbrakk>is_run r; w = L o r\<rbrakk> \<Longrightarrow> accept w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_run r; w = L \<circ> r\<rbrakk> \<Longrightarrow> accept w
[PROOF STEP]
by (auto simp: accept_def)