[STATEMENT]
lemma Lact_Ract_noStateChange_set:
assumes "set al \<subseteq> Lact ` UNIV \<union> Ract ` UNIV"
shows "snd (sstep s al) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (sstep s al) = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set al \<subseteq> range Lact \<union> range Ract

goal (1 subgoal):
 1. snd (sstep s al) = s
[PROOF STEP]
by (induct al) (auto split: prod.splits)