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

Goal state before:
pp: case refl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = none
⊢ none = none

pp: case refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
d₁ : σ₁
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none

Tactic:
·

Goal state after:
case refl.none
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = none
⊢ none = none
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

pp: case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
·

Goal state after:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
·

Goal state after:
case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = T.nth (i + 1)

Tactic:
by
  conv => rhs; rw [← T.move_right_left]
  rw [Tape.move_left_nth, add_sub_cancel_right]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0

pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)

Tactic:
·

Goal state after:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)

Tactic:
·

Goal state after:
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.move
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
d : Dir
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.move d))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.move d)))

pp: case some.write
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Γ
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.write a))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.write a)))

Tactic:
·

Goal state after:
case some.move
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
d : Dir
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.move d))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.move d)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Γ
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.write a))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.write a)))

Tactic:
·

Goal state after:
case some.write
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Γ
⊢ Option.map (fun x ↦ { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x ↦
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        (some (q', Stmt.write a))) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) (some (q', Stmt.write a)))
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

pp: case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ match some val✝ with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
·

Goal state after:
case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
e : step M c = none
⊢ match none with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ match some val✝ with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none

Tactic:
·

Goal state after:
case some
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : PointedMap Λ Λ'
g₂ : Λ' → Λ
S : Set Λ
ss : Supports M S
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁.f q) = q
c : Cfg Γ Λ
a₂✝ : Cfg Γ' Λ'
cs : c.q ∈ S
val✝ : Cfg Γ Λ
e : step M c = some val✝
⊢ match some val✝ with
  | some b₁ =>
    ∃ b₂,
      (fun a b ↦ a.q ∈ S ∧ Cfg.map f₁ g₁.f a = b) b₁ b₂ ∧ Reaches₁ (step (M.map f₁ f₂ g₁.f g₂)) (Cfg.map f₁ g₁.f c) b₂
  | none => step (M.map f₁ f₂ g₁.f g₂) (Cfg.map f₁ g₁.f c) = none
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
·

Goal state after:
case branch.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

pp: case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
·

Goal state after:
case branch.inr.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
·

Goal state after:
case branch.inr.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p

Tactic:
show p = fun a => q (f a) from Set.ext hf

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a ↦ q (f a)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (move a✝ q)
IH : move a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)

pp: case move.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case move.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Dir
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (move a✝ q)
IH : move a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case move.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case move.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv p₁ p₂

pp: case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)

Tactic:
·

Goal state after:
case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv p₁ p₂
Module: Mathlib.Computability.Reduce

Goal state before:
pp: case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)

Tactic:
·

Goal state after:
case h.a
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
φ : Sort ?u.20
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p✝ : Set ℕ
⊢ ManyOneEquiv (toNat p✝) (toNat p✝)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (write a✝ q)
IH : write a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)

pp: case write.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case write.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (write a✝ q)
IH : write a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case write.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case load.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

pp: case load.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case load.inl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₀ : Stmt Γ Λ σ
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case load.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

Tactic:
·

Goal state after:
case load.inr
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

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

Tactic:
·

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