theorem Part.eq_of_get_eq_get {σ : Type u_1} {a b : Part σ} (ha : a.Dom) (hb : b.Dom) (hab : a.get ha = b.get hb) : a = b

theorem Part.eq_iff_of_dom {σ : Type u_1} {a b : Part σ} (ha : a.Dom) (hb : b.Dom) : a.get ha = b.get hb ↔ a = b

theorem Part.get_eq_get {σ : Type u_1} {a b : Part σ} (ha : a.Dom) (hb : a.get ha ∈ b) : a = b

theorem Turing.dom_of_apply_eq_none {σ : Type u_1} {f : σ → Option σ} {s : σ} (hf : f s = none) : s ∈ eval f s

@[simp]

theorem Turing.apply_get_eval {σ : Type u_1} {f : σ → Option σ} {s : σ} (H : (eval f s).Dom) : f ((eval f s).get H) = none

theorem Turing.eval_get_eval {σ : Type u_1} {f : σ → Option σ} {s : σ} (H : (eval f s).Dom) : eval f ((eval f s).get H) = eval f s

theorem Turing.eval_eq_eval {σ : Type u_1} {f : σ → Option σ} {a a' : σ} (H : f a = some a') : eval f a = eval f a'

theorem Turing.eval_dom_iff {σ : Type u_1} {f : σ → Option σ} {s : σ} : (∃ (n : ℕ), (fun (x : Option σ) => x.bind f)^[n + 1] (some s) = none) ↔ (eval f s).Dom