[STATEMENT]
lemma is_pod_ta_eps_empty:
  "is_ta_eps_free (ta R) \<Longrightarrow> is_ta_eps_free (ta L) \<Longrightarrow> is_ta_eps_free (ta (reg_intersect R L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ta_eps_free (ta R); is_ta_eps_free (ta L)\<rbrakk> \<Longrightarrow> is_ta_eps_free (ta (reg_intersect R L))
[PROOF STEP]
by (auto simp: reg_intersect_def prod_ta_def prod_epsRp_def prod_epsLp_def is_ta_eps_free_def)