Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.one
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail✝

pp: case cons.succ.bit1
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit1)).tail ++ Γ'.cons :: trList tail✝

pp: case cons.succ.bit0
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit0)).tail ++ Γ'.cons :: trList tail✝

Tactic:
<;>

Goal state after:
case cons.succ.one
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail✝

case cons.succ.bit1
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit1) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit1)).tail ++ Γ'.cons :: trList tail✝

case cons.succ.bit0
f : Code
k : Cont
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₂
s : Option Γ'
tail✝ : List ℕ
n : ℕ
a✝ : PosNum
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = true ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail = trList tail✝
  else
    natEnd ((trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).head?.getD default) = false ∧
      (trNum (Num.pos a✝.bit0) ++ Γ'.cons :: trList tail✝).tail =
        (trNum (Num.pos a✝.bit0)).tail ++ Γ'.cons :: trList tail✝