[STATEMENT]
lemma mk_minsky_copy2:
  assumes "u \<noteq> v" "u \<noteq> w" "v \<noteq> w"
  shows "mk_minsky (\<lambda>vs vs'. vs' =
    (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_minsky (\<lambda>vs vs'. vs' = (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v
u \<noteq> w
v \<noteq> w

goal (1 subgoal):
 1. mk_minsky (\<lambda>vs vs'. vs' = (\<lambda>x. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))
[PROOF STEP]
by (intro mk_minsky_seq[OF mk_minsky_seq', OF
    mk_minsky_zero[of v]            \<comment> \<open> v[v] := 0                                           \<close>
    mk_minsky_zero[of w]            \<comment> \<open> v[w] := 0                                           \<close>
    mk_minsky_add2[of u v w]]) auto \<comment> \<open> v[v] := v[v] + v[u], v[w] := v[w] + v[u], v[u] := 0 \<close>