∀ (x : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ x =
    match x with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => insert Q (Finset.univ.biUnion fun s => Turing.PartrecToTM2.trStmts₁ (q s))
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:q.copy => insert Q (Turing.PartrecToTM2.trStmts₁ q)
    | Q@h:q.succ => insert Q (insert (Turing.PartrecToTM2.unrev q) (Turing.PartrecToTM2.trStmts₁ q))
    | Q@h:(q₁.pred q₂) =>
      insert Q
        (Turing.PartrecToTM2.trStmts₁ q₁ ∪ insert (Turing.PartrecToTM2.unrev q₂) (Turing.PartrecToTM2.trStmts₁ q₂))
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => {Q}