-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
h :
  elim (Γ'.cons :: trList v) [] c d =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        ((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)).stk
          (Γ := fun (x : K') ↦ Γ'))
        rev [])
      main
      (((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)).stk
            (Γ := fun (x : K') ↦ Γ') rev).reverseAux
        ((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)).stk
          (Γ := fun (x : K') ↦ Γ') main))
⊢ 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))

Tactic:
convert! unrev_ok using 2

Premises used: Turing.PartrecToTM2.unrev_ok