[STATEMENT]
lemma step_invariant_mono:
  assumes "step_invariant (ws, ps, N) = (ws', ps', N')"
  shows "snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')

goal (1 subgoal):
 1. snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'
[PROOF STEP]
proof (intro subsetI, elim UnE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
assume "x \<in> snd `set ws"
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws

goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set ws
[PROOF STEP]
show "x \<in> snd ` set ws' \<union> set ps'"
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set ws

goal (1 subgoal):
 1. x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
proof (cases "x = snd (hd ws)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> snd (hd ws)

goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with \<open>x \<in> image snd (set ws)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> snd ` set ws
x \<noteq> snd (hd ws)
[PROOF STEP]
have "x \<in> snd ` set (tl ws)"
[PROOF STATE]
proof (prove)
using this:
x \<in> snd ` set ws
x \<noteq> snd (hd ws)

goal (1 subgoal):
 1. x \<in> snd ` set (tl ws)
[PROOF STEP]
by (cases ws) auto
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set (tl ws)

goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set (tl ws)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set (tl ws)

goal (1 subgoal):
 1. x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
by (auto split: prod.splits simp: Let_def)
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws' \<union> set ps'

goal (1 subgoal):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
qed (auto split: prod.splits simp: Let_def)
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws' \<union> set ps'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
qed (auto split: prod.splits simp: Let_def)