Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.clear
p✝¹ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (move p✝¹ k₁✝ k₂✝ q✝¹ = clear p✝ k✝ q✝)

pp: case move.copy
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = q✝.copy)

pp: case move.push
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = push k✝ s✝ q✝)

pp: case move.read
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = read f✝)

pp: case move.succ
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = q✝.succ)

pp: case move.pred
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = q₁✝.pred q₂✝)

pp: case move.ret
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = ret k✝)

pp: case clear.move
p✝¹ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (clear p✝¹ k✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝)

pp: case clear.copy
p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝¹ = q✝.copy)

pp: case clear.push
p✝ : Γ' → Bool
k✝¹ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (clear p✝ k✝¹ q✝¹ = push k✝ s✝ q✝)

pp: case clear.read
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (clear p✝ k✝ q✝ = read f✝)

pp: case clear.succ
p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝¹ = q✝.succ)

pp: case clear.pred
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝ = q₁✝.pred q₂✝)

pp: case clear.ret
p✝ : Γ' → Bool
k✝¹ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (clear p✝ k✝¹ q✝ = ret k✝)

pp: case copy.move
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = move p✝ k₁✝ k₂✝ q✝)

pp: case copy.clear
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = clear p✝ k✝ q✝)

pp: case copy.push
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = push k✝ s✝ q✝)

pp: case copy.read
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q✝.copy = read f✝)

pp: case copy.succ
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.copy = q✝.succ)

pp: case copy.pred
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q✝.copy = q₁✝.pred q₂✝)

pp: case copy.ret
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (q✝.copy = ret k✝)

pp: case push.move
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝)

pp: case push.clear
k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (push k✝¹ s✝ q✝¹ = clear p✝ k✝ q✝)

pp: case push.copy
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = q✝.copy)

pp: case push.read
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (push k✝ s✝ q✝ = read f✝)

pp: case push.succ
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = q✝.succ)

pp: case push.pred
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝ = q₁✝.pred q₂✝)

pp: case push.ret
k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (push k✝¹ s✝ q✝ = ret k✝)

pp: case read.move
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✝)

pp: case read.clear
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (read f✝ = clear p✝ k✝ q✝)

pp: case read.copy
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.copy)

pp: case read.push
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (read f✝ = push k✝ s✝ q✝)

pp: case read.succ
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.succ)

pp: case read.pred
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (read f✝ = q₁✝.pred q₂✝)

pp: case read.ret
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : Cont'
⊢ Decidable (read f✝ = ret k✝)

pp: case succ.move
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = move p✝ k₁✝ k₂✝ q✝)

pp: case succ.clear
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = clear p✝ k✝ q✝)

pp: case succ.copy
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.succ = q✝.copy)

pp: case succ.push
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = push k✝ s✝ q✝)

pp: case succ.read
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q✝.succ = read f✝)

pp: case succ.pred
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q✝.succ = q₁✝.pred q₂✝)

pp: case succ.ret
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (q✝.succ = ret k✝)

pp: case pred.move
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✝)

pp: case pred.clear
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✝)

pp: case pred.copy
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.copy)

pp: case pred.push
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✝)

pp: case pred.read
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q₁✝.pred q₂✝ = read f✝)

pp: case pred.succ
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.succ)

pp: case pred.ret
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : Cont'
⊢ Decidable (q₁✝.pred q₂✝ = ret k✝)

pp: case ret.move
k✝ : Cont'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝ = move p✝ k₁✝ k₂✝ q✝)

pp: case ret.clear
k✝¹ : Cont'
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝¹ = clear p✝ k✝ q✝)

pp: case ret.copy
k✝ : Cont'
q✝ : Λ'
⊢ Decidable (ret k✝ = q✝.copy)

pp: case ret.push
k✝¹ : Cont'
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (ret k✝¹ = push k✝ s✝ q✝)

pp: case ret.read
k✝ : Cont'
f✝ : Option Γ' → Λ'
⊢ Decidable (ret k✝ = read f✝)

pp: case ret.succ
k✝ : Cont'
q✝ : Λ'
⊢ Decidable (ret k✝ = q✝.succ)

pp: case ret.pred
k✝ : Cont'
q₁✝ q₂✝ : Λ'
⊢ Decidable (ret k✝ = q₁✝.pred q₂✝)

Tactic:
all_goals exact .isFalse (by rintro ⟨⟨⟩⟩)

Goal state after: