Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₁.refine_2.refine_5
fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (move₂ (fun x ↦ false) aux stack (trNormal fs (trCont k).cons₂)), var := none,
      stk :=
        update
          (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
            ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
          main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) }
    s'

Tactic:
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_

Goal state after:
case cons₁.refine_2.refine_5.refine_1
fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ update
      (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
        ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
      main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) rev =
    []

case cons₁.refine_2.refine_5.refine_2
fs : Code
as : List ℕ
k : Cont
a_ih✝ :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (trNormal fs (trCont k).cons₂), var := none,
      stk :=
        update
          (update
            (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main))
            aux (none.elim id List.cons []))
          stack
          (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) aux ++
            update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) stack) }
    s'