[STATEMENT]
lemma apply_guards_append:
  "apply_guards (a@a') s = (apply_guards a s \<and> apply_guards a' s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_guards (a @ a') s = (apply_guards a s \<and> apply_guards a' s)
[PROOF STEP]
using apply_guards_def
[PROOF STATE]
proof (prove)
using this:
apply_guards ?G ?s = (\<forall>g\<in>set (map (\<lambda>g. gval g ?s) ?G). g = true)

goal (1 subgoal):
 1. apply_guards (a @ a') s = (apply_guards a s \<and> apply_guards a' s)
[PROOF STEP]
by auto