-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
      ((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)).var
        (Γ := fun (x : K') ↦ Γ'))
      ((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') ↦ Γ')))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (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))))

Tactic:
unrev_ok

Premises used: Turing.PartrecToTM2.unrev_ok