-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
h :
  Eq (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
    (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))))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ TM2.step (Γ := fun (x : K') ↦ Γ') tr a = some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))

Tactic:
convert! unrev_ok using 1

Premises used: Turing.PartrecToTM2.unrev_ok