mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}

Tactic:
;

Goal state after:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case nil.refl
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append (enc a).1 R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)

Tactic:
;

Goal state after:
case nil.refl
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L'✝ R'✝ : ListBlank Bool
⊢ (Tape.move Dir.left)^[[].length] (Tape.mk' (ListBlank.append [] L'✝) (ListBlank.append (enc a).1 R'✝)) =
    Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [].flatten ∧ ∀ t ∈ [], t ≠ [] ∧ P.rmatch t = true

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [].flatten ∧ ∀ t ∈ [], t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [] ∧ ∀ t ∈ [], ¬t = [] ∧ P.rmatch t = true

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
IH :
  ∀ (t : List α),
    t.length < [].length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
_h : P.star.rmatch [] = true
⊢ [] = [] ∧ ∀ t ∈ [], ¬t = [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch f q₁ q₂)
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch f q₁ q₂)
⊢ SupportsStmt S (branch f q₁ q₂)

pp: case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

pp: case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
;

Goal state after:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch f q₁ q₂)
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch f q₁ q₂)
⊢ SupportsStmt S (branch f q₁ q₂)

case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt S (goto l)

Tactic:
;

Goal state after:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt S (goto l)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Tactic:
;

Goal state after:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case nil.refl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
e : [].length = [].length
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
;

Goal state after:
case nil.refl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
e : [].length = [].length
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₂ : SupportsStmt S (M l₁)
h₁ : stepAux (M l₁) v T = c'
⊢ c'.l ∈ Finset.insertNone S

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
c' : Cfg Γ Λ σ
h₂ : SupportsStmt S (M l₁)
h₁ : stepAux (M l₁) v T = c'
⊢ c'.l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
⊢ SupportsStmt S (M l₁) → (stepAux (M l₁) v T).l ∈ Finset.insertNone S

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : (k : K) → List (Γ k)
⊢ SupportsStmt S (M l₁) → (stepAux (M l₁) v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif p v then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
;

Goal state after:
case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : Inhabited Λ
inst✝ : DecidableEq K
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₁' → (stepAux q₁' v T).l ∈ Finset.insertNone S
IH₂ : ∀ (v : σ) (T : (k : K) → List (Γ k)), SupportsStmt S q₂' → (stepAux q₂' v T).l ∈ Finset.insertNone S
v : σ
T : (k : K) → List (Γ k)
hs : SupportsStmt S (branch p q₁' q₂')
⊢ (bif p v then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) =
    ListBlank.mk l

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
L L' : ListBlank ((k : K) → Option (Γ k))
l : List ((k : K) → Option (Γ k))
⊢ ListBlank.map { f := Prod.snd, map_pt' := ⋯ } (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.mk l)) =
    ListBlank.mk l
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) =
    ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail)

Tactic:
;

Goal state after:
case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail) =
    ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) =
    ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)

Tactic:
;

Goal state after:
case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } (ListBlank.modifyNth f n✝ L.tail) =
    ListBlank.modifyNth (fun a ↦ (a.1, f a.2)) n✝ (ListBlank.map { f := Prod.mk false, map_pt' := ⋯ } L.tail)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ∀ (x : (k : K) → Option (Γ k)),
    { f := Prod.mk false, map_pt' := ⋯ }.f (f x) =
      (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)

Tactic:
;

Goal state after:
case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
⊢ ∀ (x : (k : K) → Option (Γ k)),
    { f := Prod.mk false, map_pt' := ⋯ }.f (f x) =
      (({ f := Prod.mk false, map_pt' := ⋯ }.f x).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x).2)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)

Tactic:
;

Goal state after:
case e_l
K : Type u_1
Γ : K → Type u_2
f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
n✝ : ℕ
x✝ : (k : K) → Option (Γ k)
⊢ { f := Prod.mk false, map_pt' := ⋯ }.f (f x✝) =
    (({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).1, f ({ f := Prod.mk false, map_pt' := ⋯ }.f x✝).2)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
| L.nth n

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
| L.nth n
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (stWrite v (S k) o) k_1)).reverse) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o) ((Tape.move Dir.right)^[(stWrite v (S k) o).length] (Tape.mk' ∅ (addBottom L')))

Tactic:
;

Goal state after:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
⊢ ∃ L',
    (∀ (k_1 : K),
        ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (stWrite v (S k) o) k_1)).reverse) ∧
      TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) =
        TM1.stepAux q (stVar v (S k) o) ((Tape.move Dir.right)^[(stWrite v (S k) o).length] (Tape.mk' ∅ (addBottom L')))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ tm.k₀)

Tactic:
;

Goal state after:
tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ tm.k₀)
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ tm.k₁)

Tactic:
;

Goal state after:
tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ tm.k₁)
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) v.headI = Part.some [v.headI - 1]

Tactic:
;

Goal state after:
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x ↦ Part.some [y]) v.headI = Part.some [v.headI - 1]
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil

Tactic:
;

Goal state after:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
x✝ : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property✝ : (a :: as).length = n.succ
⊢ Part.some [a] = pure <$> Part.some (List.Vector.head ⟨a :: as, property✝⟩)

Tactic:
;

Goal state after:
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
x✝ : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property✝ : (a :: as).length = n.succ
⊢ Part.some [a] = pure <$> Part.some (List.Vector.head ⟨a :: as, property✝⟩)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
;

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q✝ : Λ' Γ Λ σ
h : q✝ ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝

Tactic:
;

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝).div2 = m✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝) / 2 = m✝

Tactic:
;

Goal state after:
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
m✝ : ℕ
⊢ (m✝ + m✝) / 2 = m✝
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
;

Goal state after:
case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
;

Goal state after:
case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case none
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M) { l := bif none.isSome then some (Λ'.normal q) else none, var := (), Tape := T }
    (Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      none)

Tactic:
;

Goal state after:
case none
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M) { l := bif none.isSome then some (Λ'.normal q) else none, var := (), Tape := T }
    (Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      none)