[STATEMENT]
lemma doesnt_modify_annos:
  "doesnt_modify c x \<Longrightarrow> doesnt_modify (c \<otimes> annos) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doesnt_modify c x \<Longrightarrow> doesnt_modify (c \<otimes> annos) x
[PROOF STEP]
unfolding doesnt_modify_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x \<Longrightarrow> \<forall>mds mem c' mds' mem'. \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply (induct annos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> [], mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
 2. \<And>a annos mds mem c' mds' mem'. \<lbrakk>\<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> (a # annos), mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a annos mds mem c' mds' mem'. \<lbrakk>\<And>mds mem c' mds' mem'. \<lbrakk>\<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> annos, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<forall>mds mem c' mds' mem'. \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x; \<langle>c \<otimes> (a # annos), mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>\<rbrakk> \<Longrightarrow> mem x = mem' x \<and> dma mem x = dma mem' x
[PROOF STEP]
by (metis annotate.simps(2) upd_elim)