∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {o : Option Turing.PartrecToTM2.Γ'} {L₂ : List Turing.PartrecToTM2.Γ'}
  {S : Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'},
  Turing.PartrecToTM2.splitAtPred p (S k₁) = ([], o, L₂) →
    Relation.ReflTransGen (fun a b => b ∈ Turing.TM2.step Turing.PartrecToTM2.tr a)
      (bif (S k₁).head?.elim true p then { l := some q, var := (S k₁).head?, stk := Function.update S k₁ (S k₁).tail }
      else
        Turing.TM2.stepAux
          (Turing.PartrecToTM2.push' k₂ (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
          (S k₁).head? (Function.update S k₁ (S k₁).tail))
      { l := some q, var := o, stk := Function.update S k₁ L₂ }