Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case false
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (false :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif false then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

pp: case true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (true :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif true then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
<;>

Goal state after:
case false
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (false :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif false then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

case true
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, ⋯⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (true :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ (bif true then
      stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun v ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))) =
    stepAux (readAux l₂.length fun v ↦ f (true ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))