[STATEMENT]
lemma map_step:
  assumes "inj g" "vs = vs' \<circ> g" "((s, vs), (t, ws)) \<in> step M"
  shows "((f s, vs'), (f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x)) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
((s, vs), t, ws) \<in> step M

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
proof (cases rule: step.cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (inc v)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then Suc (vs v) else vs x)
(s, Inc v t) \<in> M

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = inc(1)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then Suc (vs v) else vs x)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
let ?ws' = "\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, ?ws')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
[PROOF STEP]
using inc(2) step.inc[of "f s" "g v" "f t" "map_minsky f g M" vs']
[PROOF STATE]
proof (prove)
using this:
(s, Inc v t) \<in> M
(f s, Inc (g v) (f t)) \<in> map_minsky f g M \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x = g v then Suc (vs' (g v)) else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = ?ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)

goal (3 subgoals):
 1. \<And>v. \<lbrakk>ws = (\<lambda>x. if x = v then Suc (vs v) else vs x); (s, Inc v t) \<in> M\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 3. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, \<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>w. if w = g v then Suc (vs' (g v)) else vs' w)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (decn v sz n)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then n else vs x)
(s, Dec v t sz) \<in> M
vs v = Suc n

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = decn(1)
[PROOF STATE]
proof (state)
this:
ws = (\<lambda>x. if x = v then n else vs x)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
let ?ws' = "\<lambda>x. if x = g v then n else vs' x"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, ?ws')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(2) decn(2-) step.decn[of "f s" "g v" "f t" "f sz" "map_minsky f g M" vs' n]
[PROOF STATE]
proof (prove)
using this:
vs = vs' \<circ> g
(s, Dec v t sz) \<in> M
vs v = Suc n
\<lbrakk>(f s, Dec (g v) (f t) (f sz)) \<in> map_minsky f g M; vs' (g v) = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = ?ws'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)

goal (2 subgoals):
 1. \<And>v sz n. \<lbrakk>ws = (\<lambda>x. if x = v then n else vs x); (s, Dec v t sz) \<in> M; vs v = Suc n\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
 2. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, \<lambda>x. if x = g v then n else vs' x) \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = (\<lambda>x. if x = g v then n else vs' x)

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
case (decz v sn)
[PROOF STATE]
proof (state)
this:
ws = vs
(s, Dec v sn t) \<in> M
vs v = 0

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
note [simp] = decz(1)
[PROOF STATE]
proof (state)
this:
ws = vs

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "((f s, vs'), (f t, vs')) \<in> step (map_minsky f g M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
[PROOF STEP]
using assms(2) decz(2-) step.decz[of "f s" "g v" "f sn" "f t" "map_minsky f g M" vs']
[PROOF STATE]
proof (prove)
using this:
vs = vs' \<circ> g
(s, Dec v sn t) \<in> M
vs v = 0
\<lbrakk>(f s, Dec (g v) (f sn) (f t)) \<in> map_minsky f g M; vs' (g v) = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. ((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
[PROOF STEP]
by (force simp: map_minsky_def)
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
have "(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
inj g
vs = vs' \<circ> g

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
by (auto intro!: ext simp: injD image_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'

goal (1 subgoal):
 1. \<And>v sn. \<lbrakk>ws = vs; (s, Dec v sn t) \<in> M; vs v = 0\<rbrakk> \<Longrightarrow> ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((f s, vs'), f t, vs') \<in> step (map_minsky f g M)
(\<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) = vs'

goal (1 subgoal):
 1. ((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((f s, vs'), f t, \<lambda>x. if x \<in> range g then ws (inv g x) else vs' x) \<in> step (map_minsky f g M)

goal:
No subgoals!
[PROOF STEP]
qed