Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
        stk :=
          update
            (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            rev
            (Γ'.bit1 ::
              update (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
        { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
          stk :=
            update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
      else
        TM2.stepAux
          (peek' main
            (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
              (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
convert! unrev_ok using 2

Goal state after:
case e'_2
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ elim (Γ'.cons :: trList v) [] c d =
    update
      (update
        (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
            { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
              stk :=
                update
                  (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                  rev
                  (Γ'.bit1 ::
                    update (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
              { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                stk :=
                  update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
            else
              TM2.stepAux
                (peek' main
                  (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                    (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂))))
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
        rev [])
      main
      (((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
                { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                  stk :=
                    update
                      (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                      rev
                      (Γ'.bit1 ::
                        update (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
                  { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                    stk :=
                      update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
                else
                  TM2.stepAux
                    (peek' main
                      (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                        (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂))))
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                    (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
            rev).reverseAux
        ((bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
              { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                stk :=
                  update
                    (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
                    rev
                    (Γ'.bit1 ::
                      update (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
                { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
                  stk :=
                    update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                      (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
              else
                TM2.stepAux
                  (peek' main
                    (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                      (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂))))
                  (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
                  (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                    (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)).stk
          main))