section ‹Minsky machines›

theory Minsky
  imports Recursive_Inseparability "Abstract-Rewriting.Abstract_Rewriting" "Pure-ex.Guess"
begin

text ‹We formalize Minksy machines, and relate them to recursive functions. In our flavor of
  machines, a machine has a set of registers and a set of labels, and a program is a set of
  operations. There are two operations, @{term Inc} and @{term Dec}; the former takes a
  and a label, and the latter takes a register and two labels. When an @{term Inc}
  is executed, the register is incremented and execution continues at the provided label.
  @{term Dec} instruction checks the register. If it is non-zero, the register and continues
  at the first label. Otherwise, the register remains at zero and execution continues at
  second label.

  continue to show that Minksy machines can implement any primitive recursive function. Based on
 , we encode recursively enumerable sets as Minsky machines, and finally show that
 begin{enumerate}
 item The set of Minsky configurations such that from state $1$, state $0$ can be reached,
 is undecidable;
 item There is a deterministic Minsky machine $U$ such that the set of values $x$ such that
 $(2, \lambda n.\, \text{if $n = 0$ then $x$ else $0$})$ reach state $0$ is recursively
 inseparable from those that reach state $1$; and
 item As a corollary, the set of Minsky configurations that reach state $0$ but not state $1$ is
 recursively inseparable from the configurations that reach state $1$ but not state $0$.
 end{enumerate}›

subsection ‹Deterministic relations›

text ‹A relation $\to$ is \emph{deterministic} if $t \from s \to u'$ implies $t = u$.
  abstract rewriting notion is useful for talking about deterministic Minsky machines.›

definition
  "deterministic R ⟷ R^-1 O R ⊆ Id"

lemma deterministicD:
  "deterministic R ==> (x, y) ∈ R ==> (x, z) ∈ R ==> y = z"
  by (auto simp: deterministic_def)

lemma deterministic_empty [simp]:
  "deterministic {}"
  by (auto simp: deterministic_def)

lemma deterministic_singleton [simp]:
  "deterministic {p}"
  by (auto simp: deterministic_def)

lemma deterministic_imp_weak_diamond [intro]:
  "deterministic R ==> w♢ R"
  by (auto simp: weak_diamond_def deterministic_def)

lemmas deterministic_imp_CR = deterministic_imp_weak_diamond[THEN weak_diamond_imp_CR]

lemma deterministic_union:
  "fst ` S ∩ fst ` R = {} ==> deterministic S ==> deterministic R ==> deterministic (S ∪ R)"
  by (fastforce simp add: deterministic_def disjoint_iff_not_equal)

lemma deterministic_map:
  "inj_on f (fst ` R) ==> deterministic R ==> deterministic (map_prod f g ` R)"
  by (auto simp add: deterministic_def dest!: inj_onD; force)


subsection ‹Minsky machine definition›

text ‹A Minsky operation either decrements a register (testing for zero, with two possible
  states), or increments a register (with one successor state). A Minsky machine is a
  of pairs of states and operations.›

datatype ('s, 'v) Op = Dec (op_var: 'v) 's 's | Inc (op_var: 'v) 's

type_synonym ('s, 'v) minsky = "('s × ('s, 'v) Op) set"

text ‹Semantics: A Minsky machine operates on pairs consisting of a state and an assignment of
  registers; in each step, either a register is incremented, or a register is decremented,
  it is non-zero. We write $\alpha$ for assignments; $\alpha[v]$ for the value of the
  $v$ in $\alpha$ and $\alpha[v := n]$ for the update of $v$ to $n$. Thus, the semantics
  as follows:
 begin{enumerate}
 item if $(s, Inc\ v\ s') \in M$ then $(s, \alpha) \to (s', \alpha[v := \alpha[v] + 1]$);
 item if $(s, Dec\ v\ s_n\ s_z) \in M$ and $\alpha[v] > 0$ then $(s, \alpha) \to (s_n, \alpha[v := \alpha[v] - 1]$); and
 item if $(s, Dec\ v\ s_n\ s_z) \in M$ and $\alpha[v] = 0$ then $(s, \alpha) \to (s_z, \alpha)$.
 end{enumerate}
  state is finite if there is no operation associated with it.›

inductive_set step :: "('s, 'v) minsky → ('s × ('v → nat)) rel" for M :: "('s, 'v) minsky" where
  inc: "(s, Inc v s') ∈ M ==> ((s, vs), (s', λx. if x = v then Suc (vs v) else vs x)) ∈ step M"
| decn: "(s, Dec v sn sz) ∈ M ==> vs v = Suc n ==> ((s, vs), (sn, λx. if x = v then n else vs x)) ∈ step M"
| decz: "(s, Dec v sn sz) ∈ M ==> vs v = 0 ==> ((s, vs), (sz, vs)) ∈ step M"

lemma step_mono:
  "M ⊆ M' ==> step M ⊆ step M'"
  by (auto elim: step.cases intro: step.intros)

lemmas steps_mono = rtrancl_mono[OF step_mono]

text ‹A Minsky machine has deterministic steps if its defining relation between states and
  is deterministic.›

lemma deterministic_stepI [intro]:
  assumes "deterministic M" shows "deterministic (step M)"
proof -
  { fix s vs s1 vs1 s2 vs2
    assume s: "((s, vs), (s1, vs1)) ∈ step M" "((s, vs), (s2, vs2)) ∈ step M"
    have "(s1, vs1) = (s2, vs2)" using deterministicD[OF assms]
      by (cases rule: step.cases[OF s(1)]; cases rule: step.cases[OF s(2)]) fastforce+ }
  then show ?thesis by (auto simp: deterministic_def)
qed

text ‹A Minksy machine halts when it reaches a state with no associated operation.›

lemma NF_stepI [intro]:
  "s ∉ fst ` M ==> (s, vs) ∈ NF (step M)"
  by (auto intro!: no_step elim!: step.cases simp: rev_image_eqI)

text ‹Deterministic Minsky machines enjoy unique normal forms.›

lemmas deterministic_minsky_UN =
  join_NF_imp_eq[OF CR_divergence_imp_join[OF deterministic_imp_CR[OF deterministic_stepI]] NF_stepI NF_stepI]

text ‹We will rename states and variables.›

definition map_minsky where
  "map_minsky f g M = map_prod f (map_Op f g) ` M"

lemma map_minsky_id:
  "map_minsky id id M = M"
  by (simp add: map_minsky_def Op.map_id0 map_prod.id)

lemma map_minsky_comp:
  "map_minsky f g (map_minsky f' g' M) = map_minsky (f ∘ f') (g ∘ g') M"
  unfolding map_minsky_def image_comp Op.map_comp map_prod.comp comp_def[of "map_Op _ _"] ..

text ‹When states and variables are renamed, computations carry over from the original machine,
  that variables are renamed injectively.›

lemma map_step:
  assumes "inj g" "vs = vs' ∘ g" "((s, vs), (t, ws)) ∈ step M"
  shows "((f s, vs'), (f t, λx. if x ∈ range g then ws (inv g x) else vs' x)) ∈ step (map_minsky f g M)"
  using assms(3)
proof (cases rule: step.cases)
  case (inc v) note [simp] = inc(1)
  let ?ws' = "λw. if w = g v then Suc (vs' (g v)) else vs' w"
  have "((f s, vs'), (f t, ?ws')) ∈ step (map_minsky f g M)"
    using inc(2) step.inc[of "f s" "g v" "f t" "map_minsky f g M" vs']
    by (force simp: map_minsky_def)
  moreover have "(λx. if x ∈ range g then ws (inv g x) else vs' x) = ?ws'"
    using assms(1,2) by (auto intro!: ext simp: injD image_def)
  ultimately show ?thesis by auto
next
  case (decn v sz n) note [simp] = decn(1)
  let ?ws' = "λx. if x = g v then n else vs' x"
  have "((f s, vs'), (f t, ?ws')) ∈ step (map_minsky f g M)"
    using assms(2) decn(2-) step.decn[of "f s" "g v" "f t" "f sz" "map_minsky f g M" vs' n]
    by (force simp: map_minsky_def)
  moreover have "(λx. if x ∈ range g then ws (inv g x) else vs' x) = ?ws'"
    using assms(1,2) by (auto intro!: ext simp: injD image_def)
  ultimately show ?thesis by auto
next
  case (decz v sn) note [simp] = decz(1)
  have "((f s, vs'), (f t, vs')) ∈ step (map_minsky f g M)"
    using assms(2) decz(2-) step.decz[of "f s" "g v" "f sn" "f t" "map_minsky f g M" vs']
    by (force simp: map_minsky_def)
  moreover have "(λx. if x ∈ range g then ws (inv g x) else vs' x) = vs'"
    using assms(1,2) by (auto intro!: ext simp: injD image_def)
  ultimately show ?thesis by auto
qed

lemma map_steps:
  assumes "inj g" "vs = ws ∘ g" "((s, vs), (t, vs')) ∈ (step M)^*"
  shows "((f s, ws), (f t, λx. if x ∈ range g then vs' (inv g x) else ws x)) ∈ (step (map_minsky f g M))^*"
  using assms(3,2)
proof (induct "(s, vs)" arbitrary: s vs ws rule: converse_rtrancl_induct)
  case base
  then have "(λx. if x ∈ range g then vs' (inv g x) else ws x) = ws"
    using assms(1) by (auto intro!: ext simp: injD image_def)
  then show ?case by auto
next
  case (step y)
  have "snd y = (λx. if x ∈ range g then snd y (inv g x) else ws x) ∘ g" (is "_ = ?ys' ∘ _")
    using assms(1) by auto
  then show ?case  using map_step[OF assms(1) step(4), of s "fst y" "snd y" M f] step(1)
    step(3)[OF prod.collapse[symmetric], of ?ys'] by (auto cong: if_cong)
qed

subsection ‹Concrete Minsky machines›

text ‹The following definition expresses when a Minsky machine $M$ implements a specification $P$.
  adopt the convention that computations always start out in state $1$ and end in state $0$, which
  be a final state. The specification $P$ relates initial assignments to final assignments.›

definition mk_minsky_wit :: "(nat, nat) minsky → ((nat → nat) → (nat → nat) → bool) → bool" where
  "mk_minsky_wit M P ≡ finite M ∧ deterministic M ∧ 0 ∉ fst ` M ∧
     (∀vs. ∃vs'. ((Suc 0, vs), (0, vs')) ∈ (step M)^* ∧ P vs vs')"

abbreviation mk_minsky :: "((nat → nat) → (nat → nat) → bool) → bool" where
  "mk_minsky P ≡ ∃M. mk_minsky_wit M P"

lemmas mk_minsky_def = mk_minsky_wit_def

lemma mk_minsky_mono:
  shows "mk_minsky P ==> (∧vs vs'. P vs vs' ==> Q vs vs') ==> mk_minsky Q"
  unfolding mk_minsky_def by meson

lemma mk_minsky_sound:
  assumes "mk_minsky_wit M P" "((Suc 0, vs), (0, vs')) ∈ (step M)^*"
  shows "P vs vs'"
proof -
  have M: "deterministic M" "0 ∉ fst ` M" "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step M)^* ∧ P vs vs'"
    using assms(1) by (auto simp: mk_minsky_wit_def)
  obtain vs'' where vs'': "((Suc 0, vs), (0, vs'')) ∈ (step M)^*" "P vs vs''" using M(3) by blast
  have "(0 :: nat, vs') = (0, vs'')" using M(1,2)
    by (intro deterministic_minsky_UN[OF _ assms(2) vs''(1)])
  then show ?thesis using vs''(2) by simp
qed

text ‹Realizability of $n$-ary functions for $n = 1 \dots 3$. Here we use the convention that the
  are passed in registers $1 \dots 3$, and the result is stored in register $0$.›

abbreviation mk_minsky1 where
  "mk_minsky1 f ≡ mk_minsky (λvs vs'. vs' 0 = f (vs 1))"

abbreviation mk_minsky2 where
  "mk_minsky2 f ≡ mk_minsky (λvs vs'. vs' 0 = f (vs 1) (vs 2))"

abbreviation mk_minsky3 where
  "mk_minsky3 f ≡ mk_minsky (λvs vs'. vs' 0 = f (vs 1) (vs 2) (vs 3))"

subsection ‹Trivial building blocks›

text ‹We can increment and decrement any register.›

lemma mk_minsky_inc:
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then Suc (vs v) else vs x))"
  using step.inc[of "Suc 0" v 0]
  by (auto simp: deterministic_def mk_minsky_def intro!: exI[of _ "{(1, Inc v 0)} :: (nat, nat) minsky"])

lemma mk_minsky_dec:
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then vs v - 1 else vs x))"
proof -
  let ?M = "{(1, Dec v 0 0)} :: (nat, nat) minsky"
  show ?thesis unfolding mk_minsky_def
  proof (intro exI[of _ ?M] allI conjI, goal_cases)
    case (4 vs)
    have [simp]: "vs v = 0 ==> (λx. if x = v then 0 else vs x) = vs" by auto
    show ?case using step.decz[of "Suc 0" v 0 0 ?M] step.decn[of "Suc 0" v 0 0 ?M]
      by (cases "vs v") (auto cong: if_cong)
  qed auto
qed

subsection ‹Sequential composition›

text ‹The following lemma has two useful corollaries (which we prove simultaneously because they
  much of the proof structure): First, if $P$ and $Q$ are realizable, then so is $P \circ Q$.
 , if we rename variables by an injective function $f$ in a Minksy machine, then the
  outside the range of $f$ remain unchanged.›

lemma mk_minsky_seq_map:
  assumes "mk_minsky P" "mk_minsky Q" "inj g"
    "∧vs vs' vs''. P vs vs' ==> Q vs' vs'' ==> R vs vs''"
  shows "mk_minsky (λvs vs'. R (vs ∘ g) (vs' ∘ g) ∧ (∀x. x ∉ range g ⟶ vs x = vs' x))"
proof -
  obtain M where M: "finite M" "deterministic M" "0 ∉ fst ` M"
    "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step M)<sup>*</sup> ∧ P vs vs'"
    using assms(1) by (auto simp: mk_minsky_def)
  obtain N where N: "finite N" "deterministic N" "0 ∉ fst ` N"
    "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step N)^* ∧ Q vs vs'"
    using assms(2) by (auto simp: mk_minsky_def)
  let ?fM = "λs. if s = 0 then 2 else if s = 1 then 1 else 2 * s + 1" ― ‹M: from 1 to 2›
  let ?fN = "λs. 2 * s"                                               ― ‹N: from 2 to 0›
  let ?M = "map_minsky ?fM g M ∪ map_minsky ?fN g N"
  show ?thesis unfolding mk_minsky_def
  proof (intro exI[of _ ?M] conjI allI, goal_cases)
    case 1 show ?case using M(1) N(1) by (auto simp: map_minsky_def)
  next
    case 2 show ?case using M(2,3) N(2) unfolding map_minsky_def
      by (intro deterministic_union deterministic_map)
        (auto simp: inj_on_def rev_image_eqI Suc_double_not_eq_double split: if_splits)
  next
    case 3 show ?case using N(3) by (auto simp: rev_image_eqI map_minsky_def split: if_splits)
  next
    case (4 vs)
    obtain vsM where M': "((Suc 0, vs ∘ g), 0, vsM) ∈ (step M)^*" "P (vs ∘ g) vsM"
      using M(4) by blast
    obtain vsN where N': "((Suc 0, vsM), 0, vsN) ∈ (step N)^*" "Q vsM vsN"
      using N(4) by blast
    note * = subsetD[OF steps_mono, of _ ?M]
      map_steps[OF _ _ M'(1), of g vs ?fM, simplified]
      map_steps[OF _ _ N'(1), of g _ ?fN, simplified]
    show ?case
      using assms(3,4) M'(2) N'(2) rtrancl_trans[OF *(1)[OF _ *(2)] *(1)[OF _ *(3)]]
      by (auto simp: comp_def)
  qed
qed

text ‹Sequential composition.›

lemma mk_minsky_seq:
  assumes "mk_minsky P" "mk_minsky Q"
    "∧vs vs' vs''. P vs vs' ==> Q vs' vs'' ==> R vs vs''"
  shows "mk_minsky R"
  using mk_minsky_seq_map[OF assms(1,2), of id] assms(3) by simp

lemma mk_minsky_seq':
  assumes "mk_minsky P" "mk_minsky Q"
  shows "mk_minsky (λvs vs''. (∃vs'. P vs vs' ∧ Q vs' vs''))"
  by (intro mk_minsky_seq[OF assms]) blast

text ‹We can do nothing (besides transitioning from state 1 to state 0).›

lemma mk_minsky_nop:
  "mk_minsky (λvs vs'. vs = vs')"
  by (intro mk_minsky_seq[OF mk_minsky_inc mk_minsky_dec]) auto

text ‹Renaming variables.›

lemma mk_minsky_map:
  assumes "mk_minsky P" "inj f"
  shows "mk_minsky (λvs vs'. P (vs ∘ f) (vs' ∘ f) ∧ (∀x. x ∉ range f ⟶ vs x = vs' x))"
  using mk_minsky_seq_map[OF assms(1) mk_minsky_nop assms(2)] by simp

lemma inj_shift [simp]:
  fixes a b :: nat
  assumes "a < b"
  shows "inj (λx. if x = 0 then a else x + b)"
  using assms by (auto simp: inj_on_def)

subsection ‹Bounded loop›

text ‹In the following lemma, $P$ is the specification of a loop body, and $Q$ the specification
  the loop itself (a loop invariant). The loop variable is $v$. $Q$ can be realized provided that
 begin{enumerate}
 item $P$ can be realized;
 item $P$ ensures that the loop variable is not changed by the loop body; and
 item $Q$ follows by induction on the loop variable:
 \begin{enumerate}
 \item $\alpha\,Q\,\alpha$ holds when $\alpha[v] = 0$; and
 \item $\alpha[v := n]\,P\,\alpha'$ and $\alpha'\,Q\,\alpha''$ imply $\alpha\,Q\,alpha''$
 when $\alpha[v] = n+1$.
 \end{enumerate}
 end{enumerate}›

lemma mk_minsky_loop:
  assumes "mk_minsky P"
    "∧vs vs'. P vs vs' ==> vs' v = vs v"
    "∧vs. vs v = 0 ==> Q vs vs"
    "∧n vs vs' vs''. vs v = Suc n ==> P (λx. if x = v then n else vs x) vs' ==> Q vs' vs'' ==> Q vs vs''"
  shows "mk_minsky Q"
proof -
  obtain M where M: "finite M" "deterministic M" "0 ∉ fst ` M"
    "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step M)^* ∧ P vs vs'"
    using assms(1) by (auto simp: mk_minsky_def)
  let ?M = "{(1, Dec v 2 0)} ∪ map_minsky Suc id M"
  show ?thesis unfolding mk_minsky_def
  proof (intro exI[of _ ?M] conjI allI, goal_cases)
    case 1 show ?case using M(1) by (auto simp: map_minsky_def)
  next
    case 2 show ?case using M(2,3) unfolding map_minsky_def
      by (intro deterministic_union deterministic_map) (auto simp: rev_image_eqI)
  next
    case 3 show ?case by (auto simp: map_minsky_def)
  next
    case (4 vs) show ?case
    proof (induct "vs v" arbitrary: vs)
      case 0 then show ?case using assms(3)[of vs] step.decz[of 1 v 2 0 ?M vs]
        by (auto simp: id_def)
    next
      case (Suc n)
      obtain vs' where M': "((Suc 0, λx. if x = v then n else vs x), 0, vs') ∈ (step M)^*"
        "P (λx. if x = v then n else vs x) vs'" using M(4) by blast
      obtain vs'' where D: "((Suc 0, vs'), 0, vs'') ∈ (step ?M)^*" "Q vs' vs''"
        using Suc(1)[of vs'] assms(2)[OF M'(2)] by auto
      note * = subsetD[OF steps_mono, of _ ?M]
        r_into_rtrancl[OF decn[of "Suc 0" v 2 0 ?M vs n]]
        map_steps[OF _ _ M'(1), of id _ Suc, simplified, OF refl, simplified, folded numeral_2_eq_2]
      show ?case using rtrancl_trans[OF rtrancl_trans, OF *(2) *(1)[OF _ *(3)] D(1)]
        D(2) Suc(2) assms(4)[OF _ M'(2), of vs''] by auto
    qed
  qed
qed

subsection ‹Copying values›

text ‹We work up to copying values in several steps.
 begin{enumerate}
 item Clear a register. This is a loop that decrements the register until it reaches $0$.
 item Add a register to another one. This is a loop that decrements one register, and increments
 the other register, until the first register reaches 0.
 item Add a register to two others. This is the same, except that two registers are incremented.
 item Move a register: set a register to 0, then add another register to it.
 item Copy a register destructively: clear two registers, then add another register to them.
 end{enumerate}›

lemma mk_minsky_zero:
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then 0 else vs x))"
  by (intro mk_minsky_loop[where v = v, OF ― ‹ while v[v]$--$: ›
    mk_minsky_nop]) auto                   ― ‹ pass ›

lemma mk_minsky_add1:
  assumes "v ≠ w"
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then 0 else if x = w then vs v + vs w else vs x))"
  using assms by (intro mk_minsky_loop[where v = v, OF ― ‹ while v[v]$--$: ›
    mk_minsky_inc[of w]]) auto                         ― ‹ v[w]++ ›

lemma mk_minsky_add2:
  assumes "u ≠ v" "u ≠ w" "v ≠ w"
  shows "mk_minsky (λvs vs'. vs' =
    (λx. if x = u then 0 else if x = v then vs u + vs v else if x = w then vs u + vs w else vs x))"
  using assms by (intro mk_minsky_loop[where v = u, OF mk_minsky_seq'[OF ― ‹ while v[u]$--$: ›
    mk_minsky_inc[of v]                                                  ― ‹ v[v]++ ›
    mk_minsky_inc[of w]]]) auto                                          ― ‹ v[w]++ ›

lemma mk_minsky_copy1:
  assumes "v ≠ w"
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then 0 else if x = w then vs v else vs x))"
  using assms by (intro mk_minsky_seq[OF
    mk_minsky_zero[of w]          ― ‹ v[w] := 0 ›
    mk_minsky_add1[of v w]]) auto ― ‹ v[w] := v[w] + v[v], v[v] := 0 ›

lemma mk_minsky_copy2:
  assumes "u ≠ v" "u ≠ w" "v ≠ w"
  shows "mk_minsky (λvs vs'. vs' =
    (λx. if x = u then 0 else if x = v then vs u else if x = w then vs u else vs x))"
  using assms by (intro mk_minsky_seq[OF mk_minsky_seq', OF
    mk_minsky_zero[of v]            ― ‹ v[v] := 0 ›
    mk_minsky_zero[of w]            ― ‹ v[w] := 0 ›
    mk_minsky_add2[of u v w]]) auto ― ‹ v[v] := v[v] + v[u], v[w] := v[w] + v[u], v[u] := 0 ›

lemma mk_minsky_copy:
  assumes "u ≠ v" "u ≠ w" "v ≠ w"
  shows "mk_minsky (λvs vs'. vs' = (λx. if x = v then vs u else if x = w then 0 else vs x))"
  using assms by (intro mk_minsky_seq[OF
    mk_minsky_copy2[of u v w]      ― ‹ v[v] := v[u], v[w] := v[u], v[u] := 0 ›
    mk_minsky_copy1[of w u]]) auto ― ‹ v[u] := v[w], v[w] := 0 ›

subsection ‹Primitive recursive functions›

text ‹Nondestructive apply: compute $f$ on arguments $\alpha[u]$, $\alpha[v]$, $\alpha[w]$,
  the result in $\alpha[t]$ and preserving all other registers below $k$. This is easy
  that we can copy values.›

lemma mk_minsky_apply3:
  assumes "mk_minsky3 f" "t < k" "u < k" "v < k" "w < k"
  shows "mk_minsky (λvs vs'. ∀x < k. vs' x = (if x = t then f (vs u) (vs v) (vs w) else vs x))"
  using assms(2-)
  by (intro mk_minsky_seq[OF mk_minsky_seq'[OF mk_minsky_seq'], OF
    mk_minsky_copy[of u "1 + k" k] ― ‹ v[1+k] := v[u] ›
    mk_minsky_copy[of v "2 + k" k] ― ‹ v[2+k] := v[v] ›
    mk_minsky_copy[of w "3 + k" k] ― ‹ v[3+k] := v[w] ›
    mk_minsky_map[OF assms(1), of "λx. if x = 0 then t else x + k"]]) (auto 0 2)
                                   ― ‹ v[t] := f v[1+k] v[2+k] v[3+k] ›

text ‹Composition is just four non-destructive applies.›

lemma mk_minsky_comp3_3:
  assumes "mk_minsky3 f" "mk_minsky3 g" "mk_minsky3 h" "mk_minsky3 k"
  shows "mk_minsky3 (λx y z. f (g x y z) (h x y z) (k x y z))"
  by (rule mk_minsky_seq[OF mk_minsky_seq'[OF mk_minsky_seq'], OF
    mk_minsky_apply3[OF assms(2), of 4 7 1 2 3]        ― ‹ v[4] := g v[1] v[2] v[3] ›
    mk_minsky_apply3[OF assms(3), of 5 7 1 2 3]        ― ‹ v[5] := h v[1] v[2] v[3] ›
    mk_minsky_apply3[OF assms(4), of 6 7 1 2 3]        ― ‹ v[6] := k v[1] v[2] v[3] ›
    mk_minsky_apply3[OF assms(1), of 0 7 4 5 6]]) auto ― ‹ v[0] := f v[4] v[5] v[6] ›

text ‹Primitive recursion is a non-destructive apply followed by a loop with another
 -destructive apply. The key to the proof is the loop invariant, which we can specify
  part of composing the various ‹mk_minsky_*› lemmas.›

lemma mk_minsky_prim_rec:
  assumes "mk_minsky1 g" "mk_minsky3 h"
  shows "mk_minsky2 (PrimRecOp g h)"
  by (intro mk_minsky_seq[OF mk_minsky_seq', OF
    mk_minsky_apply3[OF assms(1), of 0 4 2 2 2]       ― ‹ v[0] := g v[2] ›
    mk_minsky_zero[of 3]                              ― ‹ v[3] := 0 ›
    mk_minsky_loop[where v = 1, OF mk_minsky_seq', OF ― ‹ while v[1]$--$: ›
      mk_minsky_apply3[OF assms(2), of 0 4 3 0 2]     ― ‹ v[0] := h v[3] v[0] v[2] ›
      mk_minsky_inc[of 3],                            ― ‹ v[3]++ ›
      of "λvs vs'. vs 0 = PrimRecOp g h (vs 3) (vs 2) ⟶ vs' 0 = PrimRecOp g h (vs 3 + vs 1) (vs 2)"
    ]]) auto

text ‹With these building blocks we can easily show that all primitive recursive functions can
  realized by a Minsky machine.›

lemma mk_minsky_PrimRec:
  "f ∈ PrimRec1 ==> mk_minsky1 f"
  "g ∈ PrimRec2 ==> mk_minsky2 g"
  "h ∈ PrimRec3 ==> mk_minsky3 h"
proof (goal_cases)
  have *: "(f ∈ PrimRec1 ⟶ mk_minsky1 f) ∧ (g ∈ PrimRec2 ⟶ mk_minsky2 g) ∧ (h ∈ PrimRec3 ⟶ mk_minsky3 h)"
  proof (induction rule: PrimRec1_PrimRec2_PrimRec3.induct)
    case zero show ?case by (intro mk_minsky_mono[OF mk_minsky_zero]) auto
  next
    case suc show ?case by (intro mk_minsky_seq[OF mk_minsky_copy1[of 1 0] mk_minsky_inc[of 0]]) auto
  next
    case id1_1 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 1 0]]) auto
  next
    case id2_1 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 1 0]]) auto
  next
    case id2_2 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 2 0]]) auto
  next
    case id3_1 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 1 0]]) auto
  next
    case id3_2 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 2 0]]) auto
  next
    case id3_3 show ?case by (intro mk_minsky_mono[OF mk_minsky_copy1[of 3 0]]) auto
  next
    case (comp1_1 f g) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp1_2 f g) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp1_3 f g) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp2_1 f g h) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp3_1 f g h k) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp2_2 f g h) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp2_3 f g h) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp3_2 f g h k) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (comp3_3 f g h k) then show ?case using mk_minsky_comp3_3 by fast
  next
    case (prim_rec g h) then show ?case using mk_minsky_prim_rec by blast
  qed
  { case 1 thus ?case using * by blast next
    case 2 thus ?case using * by blast next
    case 3 thus ?case using * by blast }
qed

subsection ‹Recursively enumerable sets as Minsky machines›

text ‹The following is the most complicated lemma of this theory: Given two r.e.\ sets $A$ and $B$
  want to construct a Minsky machine that reaches the final state $0$ for input $x$ if $x \in A$
  final state $1$ if $x \in B$, and never reaches either of these states if $x \notin A \cup B$.
 If $x \in A \cap B$, then either state $0$ or state $1$ may be reached.) We consider two
 .e.\ sets rather than one because we target recursive inseparability.

  the r.e.\ set $A$, there is a primitive recursive function $f$ such that
 x \in A \iff \exists y.\, f(x,y) = 0$. Similarly there is a primitive recursive function $g$ for
 B$ such that $x \in B \iff \exists y.\, f(x,y) = 0$. Our Minsky machine takes $x$ in register
 0$ and $y$ in register $1$ (initially $0$) and works as follows.
 begin{enumerate}
 item evaluate $f(x,y)$; if the result is $0$, transition to state $0$; otherwise,
 item evaluate $g(x,y)$; if the result is $0$, transition to state $1$; otherwise,
 item increment $y$ and start over.
 end{enumerate}›

lemma ce_set_pair_by_minsky:
  assumes "A ∈ ce_sets" "B ∈ ce_sets"
  obtains M :: "(nat, nat) minsky" where
    "finite M" "deterministic M" "0 ∉ fst ` M" "Suc 0 ∉ fst ` M"
    "∧x vs. vs 0 = x ==> vs 1 = 0 ==> x ∈ A ∪ B ==>
     ∃vs'. ((2, vs), (0, vs')) ∈ (step M)^* ∨ ((2, vs), (Suc 0, vs')) ∈ (step M)^*"
    "∧x vs vs'. vs 0 = x ==> vs 1 = 0 ==> ((2, vs), (0, vs')) ∈ (step M)^* ==> x ∈ A"
    "∧x vs vs'. vs 0 = x ==> vs 1 = 0 ==> ((2, vs), (Suc 0, vs')) ∈ (step M)^* ==> x ∈ B"
proof -
  obtain g where g: "g ∈ PrimRec2" "∧x. x ∈ A ⟷ (∃y. g x y = 0)"
    using assms(1) by (auto simp: ce_sets_def fn_to_set_def)
  obtain h where h: "h ∈ PrimRec2" "∧x. x ∈ B ⟷ (∃y. h x y = 0)"
    using assms(2) by (auto simp: ce_sets_def fn_to_set_def)
  have "mk_minsky (λvs vs'. vs' 0 = vs 0 ∧ vs' 1 = vs 1 ∧ vs' 2 = g (vs 0) (vs 1))"
    using mk_minsky_seq[OF
      mk_minsky_apply3[OF mk_minsky_PrimRec(2)[OF g(1)], of 2 3 0 1 0] ― ‹ v[2] := g v[0] v[1] ›
      mk_minsky_nop] by auto                                           ― ‹ pass ›
  then obtain M :: "(nat, nat) minsky" where M: "finite M" "deterministic M" "0 ∉ fst ` M"
    "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step M)<sup>*</sup> ∧
    vs' 0 = vs 0 ∧ vs' 1 = vs 1 ∧ vs' 2 = g (vs 0) (vs 1)"
    unfolding mk_minsky_def by blast
  have "mk_minsky (λvs vs'. vs' 0 = vs 0 ∧ vs' 1 = vs 1 + 1 ∧ vs' 2 = h (vs 0) (vs 1))"
    using mk_minsky_seq[OF
      mk_minsky_apply3[OF mk_minsky_PrimRec(2)[OF h(1)], of 2 3 0 1 0] ― ‹ v[2] := h v[0] v[1] ›
      mk_minsky_inc[of 1]] by auto                                     ― ‹ v[1] := v[1] + 1 ›
  then obtain N :: "(nat, nat) minsky" where N: "finite N" "deterministic N" "0 ∉ fst ` N"
    "∧vs. ∃vs'. ((Suc 0, vs), 0, vs') ∈ (step N)^* ∧
    vs' 0 = vs 0 ∧ vs' 1 = vs 1 + 1 ∧ vs' 2 = h (vs 0) (vs 1)"
    unfolding mk_minsky_def by blast
  let ?f = "λs. if s = 0 then 3 else 2 * s" ― ‹M: from state 4 to state 3›
  let ?g = "λs. 2 * s + 5"                  ― ‹N: from state 7 to state 5›
  define X where "X = map_minsky ?f id M ∪ map_minsky ?g id N ∪ {(3, Dec 2 7 0)} ∪ {(5, Dec 2 2 1)}"
  have MX: "map_minsky ?f id M ⊆ X" by (auto simp: X_def)
  have NX: "map_minsky ?g id N ⊆ X" by (auto simp: X_def)
  have DX: "(3, Dec 2 7 0) ∈ X" "(5, Dec 2 2 1) ∈ X" by (auto simp: X_def)
  have X1: "finite X" using M(1) N(1) by (auto simp: map_minsky_def X_def)
  have X2: "deterministic X" unfolding X_def using M(2,3) N(2,3)
    apply (intro deterministic_union)
    by (auto simp: map_minsky_def rev_image_eqI inj_on_def split: if_splits
      intro!: deterministic_map) presburger+
  have X3: "0 ∉ fst ` X" "Suc 0 ∉ fst ` X" using M(3) N(3)
    by (auto simp: X_def map_minsky_def split: if_splits)
  have X4: "∃vs'. g (vs 0) (vs 1) = 0 ∧ ((2, vs), (0, vs')) ∈ (step X)^* ∨
    h (vs 0) (vs 1) = 0 ∧ ((2, vs), (1, vs')) ∈ (step X)^* ∨
    g (vs 0) (vs 1) ≠ 0 ∧ h (vs 0) (vs 1) ≠ 0 ∧ vs' 0 = vs 0 ∧ vs' 1 = vs 1 + 1 ∧
    ((2, vs), (2, vs')) ∈ (step X)⁺" for vs
  proof -
    guess vs' using M(4)[of vs] by (elim exE conjE) note vs' = this
    have 1: "((2, vs), (3, vs')) ∈ (step X)^*"
      using subsetD[OF steps_mono[OF MX], OF map_steps[OF _ _ vs'(1), of id vs ?f]] by simp
    show ?thesis
    proof (cases "vs' 2")
      case 0 then show ?thesis using decz[OF DX(1), of vs'] vs' 1
        by (auto intro: rtrancl_into_rtrancl)
    next
      case (Suc n) note Suc' = Suc
      let ?vs = "λx. if x = 2 then n else vs' x"
      have 2: "((2, vs), (7, ?vs)) ∈ (step X)^*"
        using 1 decn[OF DX(1), of vs'] Suc by (auto intro: rtrancl_into_rtrancl)
      guess vs'' using N(4)[of "?vs"] by (elim exE conjE) note vs'' = this
      have 3: "((2, vs), (5, vs'')) ∈ (step X)^*"
        using 2 subsetD[OF steps_mono[OF NX], OF map_steps[OF _ _ vs''(1), of id ?vs ?g]] by simp
      show ?thesis
      proof (cases "vs'' 2")
        case 0 then show ?thesis using 3 decz[OF DX(2), of vs''] vs''(2-) vs'(2-)
          by (auto intro: rtrancl_into_rtrancl)
      next
        case (Suc m)
        let ?vs = "λx. if x = 2 then m else vs'' x"
        have 4: "((2, vs), (2, ?vs)) ∈ (step X)⁺" using 3 decn[OF DX(2), of vs'' m] Suc by auto
        then show ?thesis using vs''(2-) vs'(2-) Suc Suc' by (auto intro!: exI[of _ ?vs])
      qed
    qed
  qed
  have *: "vs 1 ≤ y ==> g (vs 0) y = 0 ∨ h (vs 0) y = 0 ==>
    ∃vs'. ((2, vs), (0, vs')) ∈ (step X)^* ∨ ((2, vs), (1, vs')) ∈ (step X)^*" for vs y
  proof (induct "vs 1" arbitrary: vs rule: inc_induct, goal_cases base step)
    case (base vs) then show ?case using X4[of vs] by auto
  next
    case (step vs)
    guess vs' using X4[of vs] by (elim exE)
    then show ?case unfolding ex_disj_distrib using step(4) step(3)[of vs']
      by (auto dest!: trancl_into_rtrancl) (meson rtrancl_trans)+
  qed
  have **: "((s, vs), (t, ws)) ∈ (step X)^* ==> t ∈ {0, 1} ==> ((s, vs), (2, ws')) ∈ (step X)^* ==>
    ∃y. if t = 0 then g (ws' 0) y = 0 else h (ws' 0) y = 0" for s t vs ws' ws
  proof (induct arbitrary: ws' rule: converse_rtrancl_induct2)
    case refl show ?case using refl(1) NF_not_suc[OF refl(2) NF_stepI] X3 by auto
  next
    case (step s vs s' vs')
    show ?case using step(5)
    proof (cases rule: converse_rtranclE[case_names base' step'])
      case base'
      note *** = deterministic_minsky_UN[OF X2 _ _ X3]
      show ?thesis using X4[of ws']
      proof (elim exE disjE conjE, goal_cases)
        case (1 vs'') then show ?case using step(1,2,4) ***[of "(2,ws')" vs'' ws]
          by (auto simp: base' intro: converse_rtrancl_into_rtrancl)
      next
        case (2 vs'') then show ?case using step(1,2,4) ***[of "(2,ws')" ws vs'']
          by (auto simp: base' intro: converse_rtrancl_into_rtrancl)
      next
        case (3 vs'') then show ?case using step(2) step(3)[of vs'', OF step(4)]
          deterministicD[OF deterministic_stepI[OF X2], OF _ step(1)]
          by (auto simp: base' if_bool_eq_conj trancl_unfold_left)
      qed
    next
      case (step' y) then show ?thesis
        by (metis deterministicD[OF deterministic_stepI[OF X2]] step(1) step(3)[OF step(4)])
    qed
  qed
  show ?thesis
  proof (intro that[of X] X1 X2 X3, goal_cases)
    case (1 x vs) then show ?case using *[of vs] by (auto simp: g(2) h(2))
  next
    case (2 x vs vs') then show ?case using **[of 2 vs 0 vs' vs] by (auto simp: g(2) h(2))
  next
    case (3 x vs vs') then show ?case using **[of 2 vs 1 vs' vs] by (auto simp: g(2) h(2))
  qed
qed

text ‹For r.e.\ sets we obtain the following lemma as a special case (taking $B = \varnothing$,
  swapping states $1$ and $2$).›

lemma ce_set_by_minsky:
  assumes "A ∈ ce_sets"
  obtains M :: "(nat, nat) minsky" where
    "finite M" "deterministic M" "0 ∉ fst ` M"
    "∧x vs. vs 0 = x ==> vs 1 = 0 ==> x ∈ A ==> ∃vs'. ((Suc 0, vs), (0, vs')) ∈ (step M)^*"
    "∧x vs vs'. vs 0 = x ==> vs 1 = 0 ==> ((Suc 0, vs), (0, vs')) ∈ (step M)^* ==> x ∈ A"
proof -
  guess M using ce_set_pair_by_minsky[OF assms(1) ce_empty] . note M = this
  let ?f = "λs. if s = 1 then 2 else if s = 2 then 1 else s" ― ‹swap states 1 and 2›
  have "?f ∘ ?f = id" by auto
  define N where "N = map_minsky ?f id M"
  have M_def: "M = map_minsky ?f id N"
    unfolding N_def map_minsky_comp ‹?f ∘ ?f = id› map_minsky_id o_id ..
  show ?thesis using M(1-3)
  proof (intro that[of N], goal_cases)
    case (4 x vs) show ?case using M(5)[OF 4(4,5)] 4(6) M(7)[OF 4(4,5)]
      map_steps[of id vs vs 2 0 _ M ?f] by (auto simp: N_def)
  next
    case (5 x vs vs') show ?case
      using M(6)[OF 5(4,5)] 5(6) map_steps[of id vs vs 1 0 _ N ?f] by (auto simp: M_def)
  qed (auto simp: N_def map_minsky_def inj_on_def rev_image_eqI deterministic_map split: if_splits)
qed

subsection ‹Encoding of Minsky machines›

text ‹So far, Minsky machines have been sets of pairs of states and operations. We now provide an
  of Minsky machines as natural numbers, so that we can talk about them as r.e.\ or
  sets. First we encode operations.›

primrec encode_Op :: "(nat, nat) Op → nat" where
  "encode_Op (Dec v s s') = c_pair 0 (c_pair v (c_pair s s'))"
| "encode_Op (Inc v s) = c_pair 1 (c_pair v s)"

definition decode_Op :: "nat → (nat, nat) Op" where
  "decode_Op n = (if c_fst n = 0
   then Dec (c_fst (c_snd n)) (c_fst (c_snd (c_snd n))) (c_snd (c_snd (c_snd n)))
   else Inc (c_fst (c_snd n)) (c_snd (c_snd n)))"

lemma encode_Op_inv [simp]:
  "decode_Op (encode_Op x) = x"
  by (cases x) (auto simp: decode_Op_def)

text ‹Minsky machines are encoded via lists of pairs of states and operations.›

definition encode_minsky :: "(nat × (nat, nat) Op) list → nat" where
  "encode_minsky M = list_to_nat (map (λx. c_pair (fst x) (encode_Op (snd x))) M)"

definition decode_minsky :: "nat → (nat × (nat, nat) Op) list" where
  "decode_minsky n = map (λn. (c_fst n, decode_Op (c_snd n))) (nat_to_list n)"

lemma encode_minsky_inv [simp]:
  "decode_minsky (encode_minsky M) = M"
  by (auto simp: encode_minsky_def decode_minsky_def comp_def)

text ‹Assignments are stored as lists (starting with register 0).›

definition decode_regs :: "nat → (nat → nat)" where
  "decode_regs n = (λi. let xs = nat_to_list n in if i < length xs then nat_to_list n ! i else 0)"

text ‹The undecidability results talk about Minsky configurations (pairs of Minsky machines and
 ). This means that we do not have to construct any recursive functions that modify
  machines (for example in order to initialize variables), keeping the proofs simple.›

definition decode_minsky_state :: "nat → ((nat, nat) minsky × (nat → nat))" where
  "decode_minsky_state n = (set (decode_minsky (c_fst n)), (decode_regs (c_snd n)))"

subsection ‹Undecidablity results›

text ‹We conclude with some undecidability results. First we show that it is undecidable whether
  Minksy machine starting at state 1 terminates in state 0.›

definition minsky_reaching_0 where
  "minsky_reaching_0 = {n |n M vs vs'. (M, vs) = decode_minsky_state n ∧ ((Suc 0, vs), (0, vs')) ∈ (step M)^*}"

lemma minsky_reaching_0_not_computable:
  "¬ computable minsky_reaching_0"
proof -
  guess U using ce_set_by_minsky[OF univ_is_ce] . note U = this
  obtain us where [simp]: "set us = U" using finite_list[OF U(1)] by blast
  let ?f = "λn. c_pair (encode_minsky us) (c_cons n 0)"
  have "?f ∈ PrimRec1"
    using comp2_1[OF c_pair_is_pr const_is_pr comp2_1[OF c_cons_is_pr id1_1 const_is_pr]] by simp
  moreover have "?f x ∈ minsky_reaching_0 ⟷ x ∈ univ_ce" for x
    using U(4,5)[of "λi. if i = 0 then x else 0"]
    by (auto simp: minsky_reaching_0_def decode_minsky_state_def decode_regs_def c_cons_def cong: if_cong)
  ultimately have "many_reducible_to univ_ce minsky_reaching_0"
    by (auto simp: many_reducible_to_def many_reducible_to_via_def dest: pr_is_total_rec)
  then show ?thesis by (rule many_reducible_lm_1)
qed

text ‹The remaining results are resursive inseparability results. We start be showing that there
  a Minksy machine $U$ with final states $0$ and $1$ such that it is not possible to recursively
  inputs reaching state $0$ from inputs reaching state $1$.›

lemma rec_inseparable_0not1_1not0:
  "rec_inseparable {p. 0 ∈ nat_to_ce_set p ∧ 1 ∉ nat_to_ce_set p} {p. 0 ∉ nat_to_ce_set p ∧ 1 ∈ nat_to_ce_set p}"
proof -
  obtain n where n: "nat_to_ce_set n = {0}" using nat_to_ce_set_srj[OF ce_finite[of "{0}"]] by auto
  obtain m where m: "nat_to_ce_set m = {1}" using nat_to_ce_set_srj[OF ce_finite[of "{1}"]] by auto
  show ?thesis by (rule rec_inseparable_mono[OF Rice_rec_inseparable[of n m]]) (auto simp: n m)
qed

lemma ce_sets_containing_n_ce:
  "{p. n ∈ nat_to_ce_set p} ∈ ce_sets"
  using ce_set_lm_5[OF univ_is_ce comp2_1[OF c_pair_is_pr id1_1 const_is_pr[of n]]]
  by (auto simp: univ_ce_lm_1)

lemma rec_inseparable_fixed_minsky_reaching_0_1:
  obtains U :: "(nat, nat) minsky" where
    "finite U" "deterministic U" "0 ∉ fst ` U" "1 ∉ fst ` U"
    "rec_inseparable {x |x vs'. ((2, (λn. if n = 0 then x else 0)), (0, vs')) ∈ (step U)^*}
      {x |x vs'. ((2, (λn. if n = 0 then x else 0)), (1, vs')) ∈ (step U)^*}"
proof -
  guess U using ce_set_pair_by_minsky[OF ce_sets_containing_n_ce ce_sets_containing_n_ce, of 0 1] .
  from this(1-4) this(5-7)[of "λn. if n = 0 then _ else 0"]
  show ?thesis by (auto 0 0 intro!: that[of U] rec_inseparable_mono[OF rec_inseparable_0not1_1not0]
      pr_is_total_rec simp: rev_image_eqI cong: if_cong) meson+
qed

text ‹Consequently, it is impossible to separate Minsky configurations with determistic machines
  final states $0$ and $1$ that reach state $0$ from those that reach state $1$.›

definition minsky_reaching_s where
  "minsky_reaching_s s = {m |M m vs vs'. (M, vs) = decode_minsky_state m ∧
    deterministic M ∧ 0 ∉ fst ` M ∧ 1 ∉ fst ` M ∧ ((2, vs), (s, vs')) ∈ (step M)^*}"

lemma rec_inseparable_minsky_reaching_0_1:
  "rec_inseparable (minsky_reaching_s 0) (minsky_reaching_s 1)"
proof -
  guess U using rec_inseparable_fixed_minsky_reaching_0_1 . note U = this
  obtain us where [simp]: "set us = U" using finite_list[OF U(1)] by blast
  let ?f = "λn. c_pair (encode_minsky us) (c_cons n 0)"
  have "?f ∈ PrimRec1"
    using comp2_1[OF c_pair_is_pr const_is_pr comp2_1[OF c_cons_is_pr id1_1 const_is_pr]] by simp
  then show ?thesis
    using U(1-4) rec_inseparable_many_reducible[of ?f, OF _ rec_inseparable_mono[OF U(5)]]
    by (auto simp: pr_is_total_rec minsky_reaching_s_def decode_minsky_state_def rev_image_eqI
      decode_regs_def c_cons_def cong: if_cong)
qed

text ‹As a corollary, it is impossible to separate Minsky configurations that reach state 0 but not
  1 from those that reach state 1 but not state 0.›

definition minsky_reaching_s_not_t where
  "minsky_reaching_s_not_t s t = {m |M m vs vs'. (M, vs) = decode_minsky_state m ∧
    ((2, vs), (s, vs')) ∈ (step M)^* ∧ ((2, vs), (t, vs')) ∉ (step M)^*}"

lemma minsky_reaching_s_imp_minsky_reaching_s_not_t:
  assumes "s ∈ {0,1}" "t ∈ {0,1}" "s ≠ t"
  shows "minsky_reaching_s s ⊆ minsky_reaching_s_not_t s t"
proof -
  have [dest!]: "((2, vs), (0, vs')) ∉ (step M)^* ∨ ((2, vs), (1, vs')) ∉ (step M)^*"
    if "deterministic M" "0 ∉ fst ` M" "1 ∉ fst ` M" for M :: "(nat, nat) minsky" and vs vs'
    using deterministic_minsky_UN[OF that(1) _ _ that(2,3)] by auto
  show ?thesis using assms
    by (auto simp: minsky_reaching_s_def minsky_reaching_s_not_t_def rev_image_eqI)
qed

lemma rec_inseparable_minsky_reaching_0_not_1_1_not_0:
  "rec_inseparable (minsky_reaching_s_not_t 0 1) (minsky_reaching_s_not_t 1 0)"
  by (intro rec_inseparable_mono[OF rec_inseparable_minsky_reaching_0_1]
    minsky_reaching_s_imp_minsky_reaching_s_not_t) simp_all

end