[STATEMENT]
lemma is_symbol_distinct: "is_symbol x \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_symbol x \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x
[PROOF STEP]
apply (insert disjunct_symbols)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_symbol x; \<NN> \<inter> \<TT> = {}\<rbrakk> \<Longrightarrow> is_terminal x \<noteq> is_nonterminal x
[PROOF STEP]
apply (auto simp add: is_symbol_def is_terminal_def is_nonterminal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done