Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.pos.bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d } ∈
    TM2.step tr { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d }

Tactic:
simp

Goal state after:
case cons.succ.pos.bit1
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }
    { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
⊢ (bif decide ((trPosNum m.bit1.succ).head?.getD Γ'.cons = Γ'.bit0) then
      { l := some (q₁.pred q₂), var := some ((trPosNum m.bit1.succ).head?.getD Γ'.cons),
        stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit1 :: l₁) c d }
    else
      bif
          match (trPosNum m.bit1.succ).head?.getD Γ'.cons with
          | Γ'.consₗ => true
          | Γ'.cons => true
          | x => false then
        { l := some q₁, var := some ((trPosNum m.bit1.succ).head?.getD Γ'.cons),
          stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d }
      else
        bif
            match (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?.getD Γ'.consₗ with
            | Γ'.consₗ => true
            | Γ'.cons => true
            | x => false then
          { l := some (unrev q₂), var := (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?,
            stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d }
        else
          { l := some (unrev q₂), var := (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)[1]?,
            stk := elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit0 :: l₁) c d }) =
    { l := some (q₁.pred q₂), var := some Γ'.bit0,
      stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d }