awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
⊢ Decidable (Λ'.read f = b)
have read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
⊢ Decidable (Λ'.read f = b)
have read₄ : (f_1 : Option Γ' → Λ') → Decidable (Λ'.read f = Λ'.read f_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
read₄ : (f_1 : Option Γ' → Λ') → Decidable (Λ'.read f = Λ'.read f_1)
⊢ Decidable (Λ'.read f = b)
have read₅ : (q : Λ') → Decidable (Λ'.read f = q.succ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
read₄ : (f_1 : Option Γ' → Λ') → Decidable (Λ'.read f = Λ'.read f_1)
read₅ : (q : Λ') → Decidable (Λ'.read f = q.succ)
⊢ Decidable (Λ'.read f = b)
have read₆ : (q₁ q₂ : Λ') → Decidable (Λ'.read f = q₁.pred q₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
read₄ : (f_1 : Option Γ' → Λ') → Decidable (Λ'.read f = Λ'.read f_1)
read₅ : (q : Λ') → Decidable (Λ'.read f = q.succ)
read₆ : (q₁ q₂ : Λ') → Decidable (Λ'.read f = q₁.pred q₂)
⊢ Decidable (Λ'.read f = b)
have read₇ : (k : Cont') → Decidable (Λ'.read f = ret k)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
⊢ Decidable (q.succ = b)
have succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
⊢ Decidable (q.succ = b)
have succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
⊢ Decidable (q.succ = b)
have succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
⊢ Decidable (q.succ = b)
have succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
⊢ Decidable (q.succ = b)
have succ₄ : (f : Option Γ' → Λ') → Decidable (q.succ = read f)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
succ₄ : (f : Option Γ' → Λ') → Decidable (q.succ = read f)
⊢ Decidable (q.succ = b)
have succ₅ : (q_1 : Λ') → Decidable (q.succ = q_1.succ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
succ₄ : (f : Option Γ' → Λ') → Decidable (q.succ = read f)
succ₅ : (q_1 : Λ') → Decidable (q.succ = q_1.succ)
⊢ Decidable (q.succ = b)
have succ₆ : (q₁ q₂ : Λ') → Decidable (q.succ = q₁.pred q₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
succ₄ : (f : Option Γ' → Λ') → Decidable (q.succ = read f)
succ₅ : (q_1 : Λ') → Decidable (q.succ = q_1.succ)
succ₆ : (q₁ q₂ : Λ') → Decidable (q.succ = q₁.pred q₂)
⊢ Decidable (q.succ = b)
have succ₇ : (k : Cont') → Decidable (q.succ = ret k)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
⊢ Decidable (q₁.pred q₂ = b)
have pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
⊢ Decidable (q₁.pred q₂ = b)
have pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
⊢ Decidable (q₁.pred q₂ = b)
have pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
⊢ Decidable (q₁.pred q₂ = b)
have pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
⊢ Decidable (q₁.pred q₂ = b)
have pred₄ : (f : Option Γ' → Λ') → Decidable (q₁.pred q₂ = read f)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
pred₄ : (f : Option Γ' → Λ') → Decidable (q₁.pred q₂ = read f)
⊢ Decidable (q₁.pred q₂ = b)
have pred₅ : (q : Λ') → Decidable (q₁.pred q₂ = q.succ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
pred₄ : (f : Option Γ' → Λ') → Decidable (q₁.pred q₂ = read f)
pred₅ : (q : Λ') → Decidable (q₁.pred q₂ = q.succ)
⊢ Decidable (q₁.pred q₂ = b)
have pred₆ : (q₁_1 q₂_1 : Λ') → Decidable (q₁.pred q₂ = q₁_1.pred q₂_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
pred₄ : (f : Option Γ' → Λ') → Decidable (q₁.pred q₂ = read f)
pred₅ : (q : Λ') → Decidable (q₁.pred q₂ = q.succ)
pred₆ : (q₁_1 q₂_1 : Λ') → Decidable (q₁.pred q₂ = q₁_1.pred q₂_1)
⊢ Decidable (q₁.pred q₂ = b)
have pred₇ : (k : Cont') → Decidable (q₁.pred q₂ = ret k)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
⊢ Decidable (ret k = b)
have ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (ret k = move p k₁ k₂ q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
⊢ Decidable (Λ'.ret k = b)
have ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
⊢ Decidable (Λ'.ret k = b)
have ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
⊢ Decidable (Λ'.ret k = b)
have ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
⊢ Decidable (Λ'.ret k = b)
have ret₄ : (f : Option Γ' → Λ') → Decidable (Λ'.ret k = read f)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
ret₄ : (f : Option Γ' → Λ') → Decidable (Λ'.ret k = read f)
⊢ Decidable (Λ'.ret k = b)
have ret₅ : (q : Λ') → Decidable (Λ'.ret k = q.succ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
ret₄ : (f : Option Γ' → Λ') → Decidable (Λ'.ret k = read f)
ret₅ : (q : Λ') → Decidable (Λ'.ret k = q.succ)
⊢ Decidable (Λ'.ret k = b)
have ret₆ : (q₁ q₂ : Λ') → Decidable (Λ'.ret k = q₁.pred q₂)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
ret₄ : (f : Option Γ' → Λ') → Decidable (Λ'.ret k = read f)
ret₅ : (q : Λ') → Decidable (Λ'.ret k = q.succ)
ret₆ : (q₁ q₂ : Λ') → Decidable (Λ'.ret k = q₁.pred q₂)
⊢ Decidable (Λ'.ret k = b)
have ret₇ : (k_1 : Cont') → Decidable (Λ'.ret k = Λ'.ret k_1)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d a' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' = elim a' b c d
have h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d a' : List Γ'
x : K'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
have h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' main = elim a' b c d main
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
have h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' rev = elim a' b c d rev
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
have h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' aux = elim a' b c d aux
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' x = elim a' b c d x
have h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) main a' stack = elim a' b c d stack
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d b' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' = elim a b' c d
have h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d b' : List Γ'
x : K'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
have h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' main = elim a b' c d main
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
have h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' rev = elim a b' c d rev
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
have h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' aux = elim a b' c d aux
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' x = elim a b' c d x
have h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) rev b' stack = elim a b' c d stack
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d c' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' = elim a b c' d
have h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d c' : List Γ'
x : K'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
have h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' main = elim a b c' d main
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
have h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' rev = elim a b c' d rev
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
have h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' aux = elim a b c' d aux
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' x = elim a b c' d x
have h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) aux c' stack = elim a b c' d stack
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d d' : List Γ'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' = elim a b c d'
have h : ∀ (x : K'), update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d d' : List Γ'
x : K'
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
have h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' main = elim a b c d' main
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
have h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' rev = elim a b c d' rev
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
have h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' aux = elim a b c d' aux
Tactic: cases x
Cleared hypotheses: x