[STATEMENT]
lemma ta_subset_trans: "ta_subset \<A> \<B> \<Longrightarrow> ta_subset \<B> \<CC> \<Longrightarrow> ta_subset \<A> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ta_subset \<A> \<B>; ta_subset \<B> \<CC>\<rbrakk> \<Longrightarrow> ta_subset \<A> \<CC>
[PROOF STEP]
unfolding ta_subset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rules \<A> |\<subseteq>| rules \<B> \<and> eps \<A> |\<subseteq>| eps \<B>; rules \<B> |\<subseteq>| rules \<CC> \<and> eps \<B> |\<subseteq>| eps \<CC>\<rbrakk> \<Longrightarrow> rules \<A> |\<subseteq>| rules \<CC> \<and> eps \<A> |\<subseteq>| eps \<CC>
[PROOF STEP]
by auto