[STATEMENT]
lemma heap_upds_ok_invariant:
  "invariant step heap_upds_ok_conf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant (\<Rightarrow>) heap_upds_ok_conf
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
fix c c'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
assume "c \<Rightarrow> c'" and "heap_upds_ok_conf c"
[PROOF STATE]
proof (state)
this:
c \<Rightarrow> c'
heap_upds_ok_conf c

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
thus "heap_upds_ok_conf c'"
[PROOF STATE]
proof (prove)
using this:
c \<Rightarrow> c'
heap_upds_ok_conf c

goal (1 subgoal):
 1. heap_upds_ok_conf c'
[PROOF STEP]
by (induction rule: step.induct) auto
[PROOF STATE]
proof (state)
this:
heap_upds_ok_conf c'

goal:
No subgoals!
[PROOF STEP]
qed