-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q))
      ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
            (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
          main
          ((fun (x : Option Γ') ↦ Γ'.cons)
              ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
            update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
              (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
        main
        ((fun (x : Option Γ') ↦ Γ'.bit1)
            ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
          update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
              (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
            main
            ((fun (x : Option Γ') ↦ Γ'.cons)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
            main)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
            main
            ((fun (x : Option Γ') ↦ Γ'.bit1)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                main))
          rev [])
        main
        ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
              main
              ((fun (x : Option Γ') ↦ Γ'.bit1)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                  (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                  main
                  ((fun (x : Option Γ') ↦ Γ'.cons)
                      ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                    update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d) main
                      (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                  main)
              rev).reverseAux
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
            (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
              (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
              main
              ((fun (x : Option Γ') ↦ Γ'.cons)
                  ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main))
            main
            ((fun (x : Option Γ') ↦ Γ'.bit1)
                ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
              update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
                (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                  main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail)
                main
                ((fun (x : Option Γ') ↦ Γ'.cons)
                    ((fun (x v : Option Γ') ↦ v) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).head?) ::
                  update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trNum Num.zero ++ [Γ'.cons]) [] c d)
                    main (elim (trNum Num.zero ++ [Γ'.cons]) [] c d main).tail main)
                main)
            main))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok