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

Goal state before:
pp: case zero
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
L : ListBlank Γ
⊢ map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)

pp: case succ
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n✝ : ℕ
a✝ : ∀ (L : ListBlank Γ), map F (modifyNth f n✝ L) = modifyNth f' n✝ (map F L)
L : ListBlank Γ
⊢ map F (modifyNth f (n✝ + 1) L) = modifyNth f' (n✝ + 1) (map F L)

Tactic:
<;>

Goal state after:
case zero
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
L : ListBlank Γ
⊢ map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)

case succ
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n✝ : ℕ
a✝ : ∀ (L : ListBlank Γ), map F (modifyNth f n✝ L) = modifyNth f' n✝ (map F L)
L : ListBlank Γ
⊢ map F (modifyNth f (n✝ + 1) L) = modifyNth f' (n✝ + 1) (map F L)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case nil
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
⊢ append [] (mk l₂) = mk ([] ++ l₂)

pp: case cons
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
head✝ : Γ
tail✝ : List Γ
tail_ih✝ : append tail✝ (mk l₂) = mk (tail✝ ++ l₂)
⊢ append (head✝ :: tail✝) (mk l₂) = mk (head✝ :: tail✝ ++ l₂)

Tactic:
<;>

Goal state after:
case nil
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
⊢ append [] (mk l₂) = mk ([] ++ l₂)

case cons
Γ : Type u_1
inst✝ : Inhabited Γ
l₂ : List Γ
head✝ : Γ
tail✝ : List Γ
tail_ih✝ : append tail✝ (mk l₂) = mk (tail✝ ++ l₂)
⊢ append (head✝ :: tail✝) (mk l₂) = mk (head✝ :: tail✝ ++ l₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

pp: case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ}, (q', s) ∈ M q a → q ∈ Set.univ → q' ∈ Set.univ

Tactic:
<;>

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ ∀ {q : Λ} {a : Γ} {q' : Λ} {s : Stmt Γ}, (q', s) ∈ M q a → q ∈ Set.univ → q' ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

pp: case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
q✝ : Λ
a✝² : Γ
q'✝ : Λ
s✝ : Stmt Γ
a✝¹ : (q'✝, s✝) ∈ M q✝ a✝²
a✝ : q✝ ∈ Set.univ
⊢ q'✝ ∈ Set.univ

Tactic:
<;>

Goal state after:
case left
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
⊢ default ∈ Set.univ

case right
Γ : Type u_1
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine Γ Λ
q✝ : Λ
a✝² : Γ
q'✝ : Λ
s✝ : Stmt Γ
a✝¹ : (q'✝, s✝) ∈ M q✝ a✝²
a✝ : q✝ ∈ Set.univ
⊢ q'✝ ∈ Set.univ
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case head
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Γ

pp: case left
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ

pp: case right
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ

Tactic:
<;>

Goal state after:
case head
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ Γ

case left
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ

case right
Γ : Type ?u.6
inst✝ : Inhabited Γ
⊢ ListBlank Γ
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ T.right₀.nth 0 = T.nth ↑0

pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n✝ : ℕ
⊢ T.right₀.nth (n✝ + 1) = T.nth ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ T.right₀.nth 0 = T.nth ↑0

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n✝ : ℕ
⊢ T.right₀.nth (n✝ + 1) = T.nth ↑(n✝ + 1)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))

pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n✝ : ℕ
a✝ :
  ∀ (L R : ListBlank Γ),
    write (f (R.nth n✝)) ((move Dir.right)^[n✝] (mk' L R)) = (move Dir.right)^[n✝] (mk' L (ListBlank.modifyNth f n✝ R))
L R : ListBlank Γ
⊢ write (f (R.nth (n✝ + 1))) ((move Dir.right)^[n✝ + 1] (mk' L R)) =
    (move Dir.right)^[n✝ + 1] (mk' L (ListBlank.modifyNth f (n✝ + 1) R))

Tactic:
<;>

Goal state after:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
⊢ write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n✝ : ℕ
a✝ :
  ∀ (L R : ListBlank Γ),
    write (f (R.nth n✝)) ((move Dir.right)^[n✝] (mk' L R)) = (move Dir.right)^[n✝] (mk' L (ListBlank.modifyNth f n✝ R))
L R : ListBlank Γ
⊢ write (f (R.nth (n✝ + 1))) ((move Dir.right)^[n✝ + 1] (mk' L R)) =
    (move Dir.right)^[n✝ + 1] (mk' L (ListBlank.modifyNth f (n✝ + 1) R))
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case mk.left
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.left { head := head✝, left := left✝, right := right✝ }) =
    move Dir.left (map f { head := head✝, left := left✝, right := right✝ })

pp: case mk.right
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.right { head := head✝, left := left✝, right := right✝ }) =
    move Dir.right (map f { head := head✝, left := left✝, right := right✝ })

Tactic:
<;>

Goal state after:
case mk.left
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.left { head := head✝, left := left✝, right := right✝ }) =
    move Dir.left (map f { head := head✝, left := left✝, right := right✝ })

case mk.right
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move Dir.right { head := head✝, left := left✝, right := right✝ }) =
    move Dir.right (map f { head := head✝, left := left✝, right := right✝ })
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Dir
a✝ : Stmt Γ Λ σ
⊢ move a✝¹ a✝ ∈ stmts₁ (move a✝¹ a✝)

pp: case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → Γ
a✝ : Stmt Γ Λ σ
⊢ write a✝¹ a✝ ∈ stmts₁ (write a✝¹ a✝)

pp: case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

pp: case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

pp: case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝ : Γ → σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
⊢ halt ∈ stmts₁ halt

Tactic:
<;>

Goal state after:
case move
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Dir
a✝ : Stmt Γ Λ σ
⊢ move a✝¹ a✝ ∈ stmts₁ (move a✝¹ a✝)

case write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → Γ
a✝ : Stmt Γ Λ σ
⊢ write a✝¹ a✝ ∈ stmts₁ (write a✝¹ a✝)

case load
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝¹ : Γ → σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

case branch
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

case goto
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
a✝ : Γ → σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
⊢ halt ∈ stmts₁ halt
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝¹ : Primcodable α
inst✝ : Inhabited α
p : Set α
⊢ ManyOneEquiv (toNat p) p

Tactic:
by simp [ManyOneEquiv]

Goal state after:
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
by simp [ManyOneEquiv]

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ rmatch 0 [] = false

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 0 tail✝ = false
⊢ rmatch 0 (head✝ :: tail✝) = false

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ rmatch 0 [] = false

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 0 tail✝ = false
⊢ rmatch 0 (head✝ :: tail✝) = false
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ rmatch 1 [] = true ↔ [] = []

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 1 tail✝ = true ↔ tail✝ = []
⊢ rmatch 1 (head✝ :: tail✝) = true ↔ head✝ :: tail✝ = []

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ rmatch 1 [] = true ↔ [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : rmatch 1 tail✝ = true ↔ tail✝ = []
⊢ rmatch 1 (head✝ :: tail✝) = true ↔ head✝ :: tail✝ = []
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ head✝ = a

pp: case cons.nil.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ head✝ = a

Tactic:
<;>

Goal state after:
case cons.nil.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : a = head✝
⊢ rmatch 1 [] = true ↔ head✝ = a

case cons.nil.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
h✝ : ¬a = head✝
⊢ rmatch 0 [] = true ↔ head✝ = a
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

pp: case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
<;>

Goal state after:
case neg.mp
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case neg.mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true) →
    ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q

pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[n✝ + 1] q) = SupportsStmt S q

Tactic:
<;>

Goal state after:
case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q

case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[n✝ + 1] q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (write [] q) = SupportsStmt S q

pp: case cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
head✝ : Bool
tail✝ : List Bool
tail_ih✝ : SupportsStmt S (write tail✝ q) = SupportsStmt S q
⊢ SupportsStmt S (write (head✝ :: tail✝) q) = SupportsStmt S q

Tactic:
<;>

Goal state after:
case nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (write [] q) = SupportsStmt S q

case cons
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
head✝ : Bool
tail✝ : List Bool
tail_ih✝ : SupportsStmt S (write tail✝ q) = SupportsStmt S q
⊢ SupportsStmt S (write (head✝ :: tail✝) q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
⊢ push k✝ a✝¹ a✝ ∈ stmts₁ (push k✝ a✝¹ a✝)

pp: case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ peek k✝ a✝¹ a✝ ∈ stmts₁ (peek k✝ a✝¹ a✝)

pp: case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ pop k✝ a✝¹ a✝ ∈ stmts₁ (pop k✝ a✝¹ a✝)

pp: case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝² : σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

pp: case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝ : σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

pp: case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
⊢ halt ∈ stmts₁ halt

Tactic:
<;>

Goal state after:
case push
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Γ k✝
a✝ : Stmt Γ Λ σ
⊢ push k✝ a✝¹ a✝ ∈ stmts₁ (push k✝ a✝¹ a✝)

case peek
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ peek k✝ a✝¹ a✝ ∈ stmts₁ (peek k✝ a✝¹ a✝)

case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
⊢ pop k✝ a✝¹ a✝ ∈ stmts₁ (pop k✝ a✝¹ a✝)

case load
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝¹ : σ → σ
a✝ : Stmt Γ Λ σ
⊢ load a✝¹ a✝ ∈ stmts₁ (load a✝¹ a✝)

case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝² : σ → Bool
a✝¹ a✝ : Stmt Γ Λ σ
⊢ branch a✝² a✝¹ a✝ ∈ stmts₁ (branch a✝² a✝¹ a✝)

case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
a✝ : σ → Λ
⊢ goto a✝ ∈ stmts₁ (goto a✝)

case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
⊢ halt ∈ stmts₁ halt
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (true ::ᵥ v)))

pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (false ::ᵥ v)))

Tactic:
<;>

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (true ::ᵥ v)))

case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun v ↦ f (false ::ᵥ v)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))

pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))

Tactic:
<;>

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))

case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
⊢ ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (true ::ᵥ v✝))

pp: case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (false ::ᵥ v✝))

Tactic:
<;>

Goal state after:
case succ.left
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (true ::ᵥ v✝))

case succ.right
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v✝ : List.Vector Bool i
⊢ SupportsStmt S (f (false ::ᵥ v✝))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case refine_1
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList.reverse = List.replicate n default

pp: case refine_2
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList = List.replicate n default

Tactic:
<;>

Goal state after:
case refine_1
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList.reverse = List.replicate n default

case refine_2
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList = List.replicate n default