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

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: case branch
Γ : 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 p T.head v then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S

Tactic:
;

Goal state after:
case branch
Γ : 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 p T.head v then stepAux q₁' v T else stepAux q₂' v T).l ∈ Finset.insertNone S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T })
    (TM1.step M { l := none, var := v, Tape := T })

pp: case some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := some l₁, var := v, Tape := T })
    (TM1.step M { l := some l₁, var := v, Tape := T })

Tactic:
;

Goal state after:
case none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T })
    (TM1.step M { l := none, var := v, Tape := T })

case some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := some l₁, var := v, Tape := T })
    (TM1.step M { l := some l₁, var := v, Tape := T })
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.branch
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }

Tactic:
;

Goal state after:
case some.branch
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.branch p a✝¹ a✝), v), Tape := T }
    {
      q :=
        (match (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).l with
          | some x => some (M x)
          | none => none,
          (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).var),
      Tape := (bif p T.head v then TM1.stepAux a✝¹ v T else TM1.stepAux a✝ v T).Tape }
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif false then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝ v))

Tactic:
;

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = false
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif false then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝ v))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(bif g true true then 1 else 0) = Nat.bit (g true true) 0

Tactic:
;

Goal state after:
case pos.pos.one.one
f : Num → Num → Num
g : Bool → Bool → Bool
p : PosNum → PosNum → Num
gff : g false false = false
f00 : f 0 0 = 0
f0n : ∀ (n : PosNum), f 0 (pos n) = bif g false true then pos n else 0
fn0 : ∀ (n : PosNum), f (pos n) 0 = bif g true false then pos n else 0
fnn : ∀ (m n : PosNum), f (pos m) (pos n) = p m n
p11 : p 1 1 = bif g true true then 1 else 0
p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = bit (g true b) (bif g false true then pos n else 0)
pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = bit (g a true) (bif g true false then pos m else 0)
pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = bit (g a b) (p m n)
this : ∀ (b : Bool) (n : PosNum), (bif b then ↑n else 0) = ↑(bif b then pos n else 0)
this' : ∀ (b : Bool) (n : PosNum), ↑(pos (PosNum.bit b n)) = Nat.bit b ↑n
⊢ ↑(bif g true true then 1 else 0) = Nat.bit (g true true) 0
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif true then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝¹ v))

Tactic:
;

Goal state after:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
x✝ : TM1.Cfg Γ Λ σ
l₁ : Λ
p : Γ → σ → Bool
a✝¹ a✝ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝¹, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝¹ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝¹ v T).var),
        Tape := (TM1.stepAux a✝¹ v T).Tape }
IH₂ :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a✝, v), Tape := T }
      {
        q :=
          (match (TM1.stepAux a✝ v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a✝ v T).var),
        Tape := (TM1.stepAux a✝ v T).Tape }
v : σ
T : Tape Γ
e : p T.head v = true
⊢ Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (bif true then trAux M T.head a✝¹ v else trAux M T.head a✝ v)) =
    Option.map
      (fun x ↦
        { q := x.1,
          Tape :=
            match x.2 with
            | move d => Tape.move d T
            | write a => Tape.write a T })
      (some (trAux M T.head a✝¹ v))
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P * Q).matchEpsilon = true ↔ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
;

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
P Q : RegularExpression α
⊢ (P * Q).matchEpsilon = true ↔ ∃ t u, [] = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons
α : 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 α
⊢ ((P * Q).deriv a).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
;

Goal state after:
case cons
α : 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 α
⊢ ((P * Q).deriv a).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
v : σ
h₁ : (q', s) ∈ tr M (none, v) a
h₂ : (none, v) ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)

pp: case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
h₁ : (q', s) ∈ tr M (some q, v) a
h₂ : (some q, v) ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)

Tactic:
;

Goal state after:
case right.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
v : σ
h₁ : (q', s) ∈ tr M (none, v) a
h₂ : (none, v) ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)

case right.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
h₁ : (q', s) ∈ tr M (some q, v) a
h₂ : (some q, v) ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
h₁ : ((none, v'), s) ∈ tr M (some q, v) a
⊢ none ∈ TM1.stmts M S

pp: case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
;

Goal state after:
case right.some.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
h₁ : ((none, v'), s) ∈ tr M (some q, v) a
⊢ none ∈ TM1.stmts M S

case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : ((some val✝, v'), s) ∈ tr M (some q, v) a
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S

Tactic:
;

Goal state after:
case right.some.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
;

Goal state after:
case right.some.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
;

Goal state after:
case right.some.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

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

Tactic:
;

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
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 q) = SupportsStmt S q

Tactic:
;

Goal state after:
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 q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
v✝ : List.Vector Bool n
⊢ SupportsStmt S (move n Dir.left (f✝ (dec v✝)))

Tactic:
;

Goal state after:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f✝ : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f✝ a)
v✝ : List.Vector Bool n
⊢ SupportsStmt S (move n Dir.left (f✝ (dec v✝)))
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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ {goto l}

Tactic:
subst h₁₂

Goal state after:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}
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
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}

Tactic:
;

Goal state after:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {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
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}

Tactic:
subst h₁₂

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}