Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case zero
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ TransGen (fun a b ↦ TM2.step tr a = some b) (TM2.stepAux (tr q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d }

Tactic:
convert! unrev_ok using 1

Goal state after:
case e'_2
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ { l := some q, var := none, stk := elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d } =
    { l := some q, var := none,
      stk :=
        update
          (update
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main))
            rev [])
          main
          ((update
                (update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
                main
                ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update
                    (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                    main
                    ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                      update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                        (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                    main)
                rev).reverseAux
            (update
              (update
                (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                  (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun x ↦ Γ'.bit1) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update
                  (update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                    (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun x ↦ Γ'.cons) ((fun x v ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main)
              main)) }