awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : K'
s : Option Γ' → Option Γ'
q_1 : Λ'
⊢ Decidable (move p k₁ k₂ q = push k s q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
f : Option Γ' → Λ'
⊢ Decidable (move p k₁ k₂ q = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (move p k₁ k₂ q = q_1.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q₁ q₂ : Λ'
⊢ Decidable (move p k₁ k₂ q = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : Cont'
⊢ Decidable (move p k₁ k₂ q = ret k)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p_1 : Γ' → Bool
k₁ k₂ : K'
q_1 : Λ'
⊢ Decidable (clear p k q = move p_1 k₁ k₂ q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (clear p k q = q_1.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k_1 : K'
s : Option Γ' → Option Γ'
q_1 : Λ'
⊢ Decidable (clear p k q = push k_1 s q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
f : Option Γ' → Λ'
⊢ Decidable (clear p k q = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (clear p k q = q_1.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q₁ q₂ : Λ'
⊢ Decidable (clear p k q = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k_1 : Cont'
⊢ Decidable (clear p k q = ret k_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k₁ k₂ : K'
q_1 : Λ'
⊢ Decidable (q.copy = move p k₁ k₂ q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k : K'
q_1 : Λ'
⊢ Decidable (q.copy = clear p k q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : K'
s : Option Γ' → Option Γ'
q_1 : Λ'
⊢ Decidable (q.copy = push k s q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
f : Option Γ' → Λ'
⊢ Decidable (q.copy = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (q.copy = q_1.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q₁ q₂ : Λ'
⊢ Decidable (q.copy = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : Cont'
⊢ Decidable (q.copy = ret k)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k₁ k₂ : K'
q_1 : Λ'
⊢ Decidable (push k s q = move p k₁ k₂ q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k_1 : K'
q_1 : Λ'
⊢ Decidable (push k s q = clear p k_1 q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (push k s q = q_1.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
f : Option Γ' → Λ'
⊢ Decidable (push k s q = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (push k s q = q_1.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q₁ q₂ : Λ'
⊢ Decidable (push k s q = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k_1 : Cont'
⊢ Decidable (push k s q = ret k_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
⊢ Decidable (read f = move p k₁ k₂ q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
p : Γ' → Bool
k : K'
q : Λ'
⊢ Decidable (read f = clear p k q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
q : Λ'
⊢ Decidable (read f = q.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
k : K'
s : Option Γ' → Option Γ'
q : Λ'
⊢ Decidable (read f = push k s q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
q : Λ'
⊢ Decidable (read f = q.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
q₁ q₂ : Λ'
⊢ Decidable (read f = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
k : Cont'
⊢ Decidable (read f = ret k)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k₁ k₂ : K'
q_1 : Λ'
⊢ Decidable (q.succ = move p k₁ k₂ q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p : Γ' → Bool
k : K'
q_1 : Λ'
⊢ Decidable (q.succ = clear p k q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (q.succ = q_1.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : K'
s : Option Γ' → Option Γ'
q_1 : Λ'
⊢ Decidable (q.succ = push k s q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
f : Option Γ' → Λ'
⊢ Decidable (q.succ = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q₁ q₂ : Λ'
⊢ Decidable (q.succ = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k : Cont'
⊢ Decidable (q.succ = ret k)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
⊢ Decidable (q₁.pred q₂ = move p k₁ k₂ q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
p : Γ' → Bool
k : K'
q : Λ'
⊢ Decidable (q₁.pred q₂ = clear p k q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
q : Λ'
⊢ Decidable (q₁.pred q₂ = q.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
k : K'
s : Option Γ' → Option Γ'
q : Λ'
⊢ Decidable (q₁.pred q₂ = push k s q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
f : Option Γ' → Λ'
⊢ Decidable (q₁.pred q₂ = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
q : Λ'
⊢ Decidable (q₁.pred q₂ = q.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
k : Cont'
⊢ Decidable (q₁.pred q₂ = ret k)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
⊢ Decidable (ret k = move p k₁ k₂ q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
p : Γ' → Bool
k_1 : K'
q : Λ'
⊢ Decidable (ret k = clear p k_1 q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
q : Λ'
⊢ Decidable (ret k = q.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
k_1 : K'
s : Option Γ' → Option Γ'
q : Λ'
⊢ Decidable (ret k = push k_1 s q)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
f : Option Γ' → Λ'
⊢ Decidable (ret k = read f)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
q : Λ'
⊢ Decidable (ret k = q.succ)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
q₁ q₂ : Λ'
⊢ Decidable (ret k = q₁.pred q₂)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
⊢ tr (Λ'.move p k₁ k₂ q) =
    pop' k₁
      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ s.elim true p)
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)
        (push' k₂ (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.move p k₁ k₂ q)))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
f : Option Γ' → Option Γ'
q : Λ'
⊢ tr (Λ'.push k f q) =
    branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ (f s).isSome)
      (push (Γ := fun (x : K') ↦ Γ') k (fun (s : Option Γ') ↦ (f s).getD default)
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q))
      (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Option Γ' → Λ'
⊢ tr (Λ'.read q) = goto (Γ := fun (x : K') ↦ Γ') q

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
⊢ tr (Λ'.clear p k q) =
    pop' k
      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ s.elim true p)
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.clear p k q))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
⊢ tr q.copy =
    pop' rev
      (branch (Γ := fun (x : K') ↦ Γ') Option.isSome
        (push' main (push' stack (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.copy)))
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
⊢ tr q.succ =
    pop' main
      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit1))
        (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.succ))
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.cons))
          (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.cons)
            (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q)))
          (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q))))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
⊢ tr (q₁.pred q₂) =
    pop' main
      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit0))
        (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit1)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁.pred q₂))
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁)
          (peek' main
            (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
              (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
k : Cont'
⊢ tr (Λ'.ret (Cont'.cons₁ fs k)) =
    goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦
      move₂ (fun (x : Γ') ↦ false) main aux
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs k.cons₂)))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
⊢ tr (Λ'.ret k.cons₂) = goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ head stack (Λ'.ret k)

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont'
⊢ tr (Λ'.ret (Cont'.comp f k)) = goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ trNormal f k

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Code
k : Cont'
⊢ tr (Λ'.ret (Cont'.fix f k)) =
    pop' main
      (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
        bif natEnd (s.getD default) then Λ'.ret k else Λ'.clear natEnd main (trNormal f (Cont'.fix f k)))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
⊢ tr (Λ'.ret Cont'.halt) = load (Γ := fun (x : K') ↦ Γ') (fun (x : Option Γ') ↦ none) (halt (Γ := fun (x : K') ↦ Γ'))

Tactic:
rfl

Premises used: Turing.PartrecToTM2.tr, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
⊢ trNum 0 = []

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
⊢ trNat default = []

Tactic:
trNat_zero

Premises used: Turing.PartrecToTM2.trNat_zero
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d : List Γ'
⊢ elim a b c d main = a

Tactic:
rfl

Premises used: Turing.PartrecToTM2.K'.elim, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d : List Γ'
⊢ elim a b c d rev = b

Tactic:
rfl

Premises used: Turing.PartrecToTM2.K'.elim, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d : List Γ'
⊢ elim a b c d aux = c

Tactic:
rfl

Premises used: Turing.PartrecToTM2.K'.elim, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d : List Γ'
⊢ elim a b c d stack = d

Tactic:
rfl

Premises used: Turing.PartrecToTM2.K'.elim, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' = elim a' b c d

Tactic:
funext x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
x : K'
h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' main = elim a' b c d main
h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' rev = elim a' b c d rev
h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' aux = elim a' b c d aux
h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' stack = elim a' b c d stack
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x

Tactic:
cases x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' main = elim a' b c d main

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' rev = elim a' b c d rev

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' aux = elim a' b c d aux

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d a' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' stack = elim a' b c d stack

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' = elim a b' c d

Tactic:
funext x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
x : K'
h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' main = elim a b' c d main
h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' rev = elim a b' c d rev
h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' aux = elim a b' c d aux
h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' stack = elim a b' c d stack
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x

Tactic:
cases x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' main = elim a b' c d main

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' rev = elim a b' c d rev

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' aux = elim a b' c d aux

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d b' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' stack = elim a b' c d stack

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' = elim a b c' d

Tactic:
funext x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
x : K'
h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' main = elim a b c' d main
h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' rev = elim a b c' d rev
h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' aux = elim a b c' d aux
h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' stack = elim a b c' d stack
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x

Tactic:
cases x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' main = elim a b c' d main

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' rev = elim a b c' d rev

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' aux = elim a b c' d aux

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d c' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' stack = elim a b c' d stack

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' = elim a b c d'

Tactic:
funext x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
x : K'
h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' main = elim a b c d' main
h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' rev = elim a b c d' rev
h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' aux = elim a b c d' aux
h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' stack = elim a b c d' stack
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x

Tactic:
cases x
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' main = elim a b c d' main

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' rev = elim a b c d' rev

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' aux = elim a b c d' aux

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
a b c d d' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' stack = elim a b c d' stack

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
l₁ : List α
o : α
l₂ : List α
h : ∀ x ∈ l₁, p x = false
left : p o = true
h₃ : [] = l₁ ++ o :: l₂
⊢ splitAtPred p [] = (l₁, some o, l₂)

Tactic:
simp at h₃