[STATEMENT]
lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 \<union> supp e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Alts e1 e2) = supp e1 \<union> supp e2
[PROOF STEP]
unfolding supp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> Alts e1 e2 \<noteq> Alts e1 e2}} = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> e1 \<noteq> e1}} \<union> {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> e2 \<noteq> e2}}
[PROOF STEP]
by (auto simp add: Collect_imp_eq Collect_neg_eq)