-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
          rev
          (Γ'.bit1 ::
            update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev))
    else
      bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
      else
        TM2.stepAux (Γ := fun (x : K') ↦ Γ')
          (peek' main
            (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
              (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit0))
          (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit1)
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁.pred q₂))
          (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁)
            (peek' main
              (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                  (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))

Tactic:
simp only [pop', TM2.stepAux]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.pop'