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

Goal state before:
pp: case pos
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : i = (S k).length
⊢ some (f v) = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

pp: case neg
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : ¬i = (S k).length
⊢ L.nth i k = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
·

Goal state after:
case pos
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h : i = (S k).length
⊢ some (f v) = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n

pp: case pos
n : ℕ
a✝ : PosNum
⊢ ↑(pos (a✝ <<< n)) = ↑(pos a✝) <<< n

Tactic:
·

Goal state after:
case zero
n : ℕ
⊢ ↑0 = ↑zero <<< n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n

pp: case pos
n : ℕ
m : PosNum
⊢ ↑(m >>> n) = ↑(pos m) >>> n

Tactic:
·

Goal state after:
case zero
n : ℕ
⊢ ↑0 = ↑zero >>> n
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) >>> (n + 1)

pp: case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)

pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
·

Goal state after:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
⊢ ↑0 = ↑(pos one) >>> (n + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write.inl
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ 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')
a : Γ
⊢ SupportsStmt (trSupp M S) (tr enc dec M (Λ'.write a q))

pp: case write.inr
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ 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')
q' : Λ' Γ Λ σ
hq : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
·

Goal state after:
case write.inl
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ 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')
a : Γ
⊢ SupportsStmt (trSupp M S) (tr enc dec M (Λ'.write a q))
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)

pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
·

Goal state after:
case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)
Module: Mathlib.Data.Num.Lemmas

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

pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.126 = ↑(pos m.bit1) >>> (n + 1)

pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ

Tactic:
·

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

Goal state before:
pp: case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)

Tactic:
·

Goal state after:
case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case write.inr
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ 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')
q' : Λ' Γ Λ σ
hq : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
·

Goal state after:
case write.inr
Γ : 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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ a, Λ'.write a q = q') ∨ 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')
q' : Λ' Γ Λ σ
hq : 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
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ↑(m.shiftr n) = ?m.171

pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ?m.171 = ↑(pos m.bit0) >>> (n + 1)

pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
hdiv2 : ∀ (m : ℕ), (m + m).div2 = m
m : PosNum
⊢ ℕ

Tactic:
·

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

Goal state before:
pp: case pos.zero.one
⊢ true = (↑one).testBit 0

pp: case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

pp: case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
·

Goal state after:
case pos.zero.one
⊢ true = (↑one).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

pp: case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
·

Goal state after:
case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
·

Goal state after:
case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)

pp: case pos.succ.bit1
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit1).testBit (n✝ + 1)

pp: case pos.succ.bit0
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
m : PosNum
⊢ m.testBit n✝ = (↑m.bit0).testBit (n✝ + 1)

Tactic:
·

Goal state after:
case pos.succ.one
n✝ : ℕ
a✝ : ∀ (m : PosNum), m.testBit n✝ = (↑m).testBit n✝
⊢ false = (↑one).testBit (n✝ + 1)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inl
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

pp: case neg.inr
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : (S k).length < i
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
·

Goal state after:
case neg.inl
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : i < (S k).length
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
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) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

pp: case some
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
val : Λ × TM0.Stmt Γ
e : M q T.head = some val
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

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) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.inr
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : (S k).length < i
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i

Tactic:
·

Goal state after:
case neg.inr
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
i : ℕ
h✝ : ¬i = (S k).length
h : (S k).length < i
⊢ (List.map some (S k)).reverse.getI i = ((List.map some (S k)).reverse ++ [some (f v)]).getI i
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

Tactic:
·

Goal state after:
case neg
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
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case rfind.mp
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ (∃
      a ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v),
      x = [a.headI.pred]) →
    ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x

pp: case rfind.mpr
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ (∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x) →
    ∃
      a ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v),
      x = [a.headI.pred]

Tactic:
·

Goal state after:
case rfind.mp
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
x : List ℕ
⊢ (∃
      a ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v),
      x = [a.headI.pred]) →
    ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case right.e_a.e_a.nil
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
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k = [].head?

pp: case right.e_a.e_a.cons
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
f : σ → Option (Γ k) → σ
head✝ : Γ k
tail✝ : List (Γ k)
e : S k = head✝ :: tail✝
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[(head✝ :: tail✝).length] (Tape.mk' ∅ (addBottom L)))).head.2 k =
    (head✝ :: tail✝).head?

Tactic:
·

Goal state after:
case right.e_a.e_a.nil
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
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (Tape.move Dir.left ((Tape.move Dir.right)^[[].length] (Tape.mk' ∅ (addBottom L)))).head.2 k = [].head?
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case pop.cons
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
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (hd :: tl).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (hd :: tl).head?)
          ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom L')))

Tactic:
·

Goal state after:
case pop.cons
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
f : σ → Option (Γ k) → σ
hd : Γ k
tl : List (Γ k)
e : S k = hd :: tl
⊢ ∃ L',
    (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (hd :: tl).tail k_1)).reverse) ∧
      (bif ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L))).head.1 then
          TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))
        else
          TM1.stepAux q
            (f v ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k))
            (Tape.write
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.1,
                update
                  (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))).head.2 k
                  none)
              (Tape.move Dir.left ((Tape.move Dir.right)^[(hd :: tl).length] (Tape.mk' ∅ (addBottom L)))))) =
        TM1.stepAux q (f v (hd :: tl).head?)
          ((Tape.move Dir.right)^[(hd :: tl).tail.length] (Tape.mk' ∅ (addBottom L')))