The partial recursive functions

The partial recursive functions are defined similarly to the primitive recursive functions, but now all functions are partial, implemented using the Part monad, and there is an additional operation, called μ-recursion, which performs unbounded minimization.

References

• [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]

def Nat.rfindX (p : ℕ →. Bool) (H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom) : { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }

Equations

• One or more equations did not get rendered due to their size.

def Nat.rfind (p : ℕ →. Bool) : Part ℕ

Equations

• Nat.rfind p = { Dom := ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom, get := fun (h : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom) => ↑(Nat.rfindX p h) }

theorem Nat.rfind_spec {p : ℕ →. Bool} {n : ℕ} (h : n ∈ Nat.rfind p) : true ∈ p n

theorem Nat.rfind_min {p : ℕ →. Bool} {n : ℕ} (h : n ∈ Nat.rfind p) {m : ℕ} : m < n → false ∈ p m

@[simp]

theorem Nat.rfind_dom {p : ℕ →. Bool} : (Nat.rfind p).Dom ↔ ∃ (n : ℕ), true ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).Dom

theorem Nat.rfind_dom' {p : ℕ →. Bool} : (Nat.rfind p).Dom ↔ ∃ (n : ℕ), true ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).Dom

@[simp]

theorem Nat.mem_rfind {p : ℕ →. Bool} {n : ℕ} : n ∈ Nat.rfind p ↔ true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m

theorem Nat.rfind_min' {p : ℕ → Bool} {m : ℕ} (pm : p m = true) : ∃ n ∈ Nat.rfind ↑p, n ≤ m

theorem Nat.rfind_zero_none (p : ℕ →. Bool) (p0 : p 0 = Part.none) : Nat.rfind p = Part.none

def Nat.rfindOpt {α : Type u_1} (f : ℕ → Option α) : Part α

Equations

• Nat.rfindOpt f = Part.bind (Nat.rfind fun (n : ℕ) => ↑(some (Option.isSome (f n)))) fun (n : ℕ) => ↑(f n)

theorem Nat.rfindOpt_spec {α : Type u_1} {f : ℕ → Option α} {a : α} (h : a ∈ Nat.rfindOpt f) : ∃ (n : ℕ), a ∈ f n

theorem Nat.rfindOpt_dom {α : Type u_1} {f : ℕ → Option α} : (Nat.rfindOpt f).Dom ↔ ∃ (n : ℕ) (a : α), a ∈ f n

theorem Nat.rfindOpt_mono {α : Type u_1} {f : ℕ → Option α} (H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n) {a : α} : a ∈ Nat.rfindOpt f ↔ ∃ (n : ℕ), a ∈ f n

inductive Nat.Partrec : (ℕ →. ℕ) → Prop

• zero: Nat.Partrec (pure 0)
• succ: Nat.Partrec ↑Nat.succ
• left: Nat.Partrec ↑fun (n : ℕ) => (Nat.unpair n).1
• right: Nat.Partrec ↑fun (n : ℕ) => (Nat.unpair n).2
• pair: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun (n : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => g n
• comp: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun (n : ℕ) => g n >>= f
• prec: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec (Nat.unpaired fun (a n : ℕ) => Nat.rec (f a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH g (Nat.pair a (Nat.pair y i))) n)
• rfind: ∀ {f : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)

theorem Nat.Partrec.of_eq {f : ℕ →. ℕ} {g : ℕ →. ℕ} (hf : Nat.Partrec f) (H : ∀ (n : ℕ), f n = g n) : Nat.Partrec g

theorem Nat.Partrec.of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Nat.Partrec f) (H : ∀ (n : ℕ), g n ∈ f n) : Nat.Partrec ↑g

theorem Nat.Partrec.of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Nat.Partrec ↑f

theorem Nat.Partrec.some : Nat.Partrec Part.some

theorem Nat.Partrec.none : Nat.Partrec fun (x : ℕ) => Part.none

theorem Nat.Partrec.prec' {f : ℕ →. ℕ} {g : ℕ →. ℕ} {h : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (hh : Nat.Partrec h) : Nat.Partrec fun (a : ℕ) => Part.bind (f a) fun (n : ℕ) => Nat.rec (g a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH h (Nat.pair a (Nat.pair y i))) n

theorem Nat.Partrec.ppred : Nat.Partrec fun (n : ℕ) => ↑(Nat.ppred n)

def Partrec {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α →. σ) : Prop

Equations

• Partrec f = Nat.Partrec fun (n : ℕ) => Part.bind ↑(Encodable.decode n) fun (a : α) => Part.map Encodable.encode (f a)

def Partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : α → β →. σ) : Prop

Equations

• Partrec₂ f = Partrec fun (p : α × β) => f p.1 p.2

def Computable {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α → σ) : Prop

Equations

• Computable f = Partrec ↑f

def Computable₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : α → β → σ) : Prop

Equations

• Computable₂ f = Computable fun (p : α × β) => f p.1 p.2

theorem Primrec.to_comp {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Primrec f) : Computable f

theorem Primrec₂.to_comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Primrec₂ f) : Computable₂ f

theorem Computable.partrec {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Computable f) : Partrec ↑f

theorem Computable₂.partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Computable₂ f) : Partrec₂ fun (a : α) => ↑(f a)

theorem Computable.of_eq {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → σ} {g : α → σ} (hf : Computable f) (H : ∀ (n : α), f n = g n) : Computable g

theorem Computable.const {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : σ) : Computable fun (x : α) => s

theorem Computable.ofOption {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → Option β} (hf : Computable f) : Partrec fun (a : α) => ↑(f a)

theorem Computable.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β → σ} (hf : Computable f) : Computable₂ fun (a : α) (b : β) => f (a, b)

theorem Computable.id {α : Type u_1} [Primcodable α] : Computable id

theorem Computable.fst {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable Prod.fst

theorem Computable.snd {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable Prod.snd

theorem Computable.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β} {g : α → γ} (hf : Computable f) (hg : Computable g) : Computable fun (a : α) => (f a, g a)

theorem Computable.unpair : Computable Nat.unpair

theorem Computable.succ : Computable Nat.succ

theorem Computable.pred : Computable Nat.pred

theorem Computable.nat_bodd : Computable Nat.bodd

theorem Computable.nat_div2 : Computable Nat.div2

theorem Computable.sum_inl {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable Sum.inl

theorem Computable.sum_inr {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable Sum.inr

theorem Computable.list_cons {α : Type u_1} [Primcodable α] : Computable₂ List.cons

theorem Computable.list_reverse {α : Type u_1} [Primcodable α] : Computable List.reverse

theorem Computable.list_get? {α : Type u_1} [Primcodable α] : Computable₂ List.get?

theorem Computable.list_append {α : Type u_1} [Primcodable α] : Computable₂ fun (x x_1 : List α) => x ++ x_1

theorem Computable.list_concat {α : Type u_1} [Primcodable α] : Computable₂ fun (l : List α) (a : α) => l ++ [a]

theorem Computable.list_length {α : Type u_1} [Primcodable α] : Computable List.length

theorem Computable.vector_cons {α : Type u_1} [Primcodable α] {n : ℕ} : Computable₂ Vector.cons

theorem Computable.vector_toList {α : Type u_1} [Primcodable α] {n : ℕ} : Computable Vector.toList

theorem Computable.vector_length {α : Type u_1} [Primcodable α] {n : ℕ} : Computable Vector.length

theorem Computable.vector_head {α : Type u_1} [Primcodable α] {n : ℕ} : Computable Vector.head

theorem Computable.vector_tail {α : Type u_1} [Primcodable α] {n : ℕ} : Computable Vector.tail

theorem Computable.vector_get {α : Type u_1} [Primcodable α] {n : ℕ} : Computable₂ Vector.get

theorem Computable.vector_ofFn' {α : Type u_1} [Primcodable α] {n : ℕ} : Computable Vector.ofFn

theorem Computable.fin_app {σ : Type u_4} [Primcodable σ] {n : ℕ} : Computable₂ id

theorem Computable.encode {α : Type u_1} [Primcodable α] : Computable Encodable.encode

theorem Computable.decode {α : Type u_1} [Primcodable α] : Computable Encodable.decode

theorem Computable.ofNat (α : Type u_5) [Denumerable α] : Computable (Denumerable.ofNat α)

theorem Computable.encode_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → σ} : (Computable fun (a : α) => Encodable.encode (f a)) ↔ Computable f

theorem Computable.option_some {α : Type u_1} [Primcodable α] : Computable some

theorem Partrec.of_eq {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (H : ∀ (n : α), f n = g n) : Partrec g

theorem Partrec.of_eq_tot {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α → σ} (hf : Partrec f) (H : ∀ (n : α), g n ∈ f n) : Computable g

theorem Partrec.none {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] : Partrec fun (x : α) => Part.none

theorem Partrec.some {α : Type u_1} [Primcodable α] : Partrec Part.some

theorem Decidable.Partrec.const' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : Part σ) [Decidable s.Dom] : Partrec fun (x : α) => s

theorem Partrec.const' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : Part σ) : Partrec fun (x : α) => s

theorem Partrec.bind {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α →. β} {g : α → β →. σ} (hf : Partrec f) (hg : Partrec₂ g) : Partrec fun (a : α) => Part.bind (f a) (g a)

theorem Partrec.map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α →. β} {g : α → β → σ} (hf : Partrec f) (hg : Computable₂ g) : Partrec fun (a : α) => Part.map (g a) (f a)

theorem Partrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β →. σ} (hf : Partrec f) : Partrec₂ fun (a : α) (b : β) => f (a, b)

theorem Partrec.nat_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g) (hh : Partrec₂ h) : Partrec fun (a : α) => Nat.rec (g a) (fun (y : ℕ) (IH : Part σ) => Part.bind IH fun (i : σ) => h a (y, i)) (f a)

theorem Partrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : β →. σ} {g : α → β} (hf : Partrec f) (hg : Computable g) : Partrec fun (a : α) => f (g a)

theorem Partrec.nat_iff {f : ℕ →. ℕ} : Partrec f ↔ Nat.Partrec f

theorem Partrec.map_encode_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} : (Partrec fun (a : α) => Part.map Encodable.encode (f a)) ↔ Partrec f

theorem Partrec₂.unpaired {α : Type u_1} [Primcodable α] {f : ℕ → ℕ →. α} : Partrec (Nat.unpaired f) ↔ Partrec₂ f

theorem Partrec₂.unpaired' {f : ℕ → ℕ →. ℕ} : Nat.Partrec (Nat.unpaired f) ↔ Partrec₂ f

theorem Partrec₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : β → γ →. σ} {g : α → β} {h : α → γ} (hf : Partrec₂ f) (hg : Computable g) (hh : Computable h) : Partrec fun (a : α) => f (g a) (h a)

theorem Partrec₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γ → δ →. σ} {g : α → β → γ} {h : α → β → δ} (hf : Partrec₂ f) (hg : Computable₂ g) (hh : Computable₂ h) : Partrec₂ fun (a : α) (b : β) => f (g a b) (h a b)

theorem Computable.comp {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : β → σ} {g : α → β} (hf : Computable f) (hg : Computable g) : Computable fun (a : α) => f (g a)

theorem Computable.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : γ → σ} {g : α → β → γ} (hf : Computable f) (hg : Computable₂ g) : Computable₂ fun (a : α) (b : β) => f (g a b)

theorem Computable₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : β → γ → σ} {g : α → β} {h : α → γ} (hf : Computable₂ f) (hg : Computable g) (hh : Computable h) : Computable fun (a : α) => f (g a) (h a)

theorem Computable₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ} (hf : Computable₂ f) (hg : Computable₂ g) (hh : Computable₂ h) : Computable₂ fun (a : α) (b : β) => f (g a b) (h a b)

theorem Partrec.rfind {α : Type u_1} [Primcodable α] {p : α → ℕ →. Bool} (hp : Partrec₂ p) : Partrec fun (a : α) => Nat.rfind (p a)

theorem Partrec.rfindOpt {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → ℕ → Option σ} (hf : Computable₂ f) : Partrec fun (a : α) => Nat.rfindOpt (f a)

theorem Partrec.nat_casesOn_right {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ} (hf : Computable f) (hg : Computable g) (hh : Partrec₂ h) : Partrec fun (a : α) => Nat.casesOn (f a) (Part.some (g a)) (h a)

theorem Partrec.bind_decode₂_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} : Partrec f ↔ Nat.Partrec fun (n : ℕ) => Part.bind ↑(Encodable.decode₂ α n) fun (a : α) => Part.map Encodable.encode (f a)

theorem Partrec.vector_mOfFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α →. σ} : (∀ (i : Fin n), Partrec (f i)) → Partrec fun (a : α) => Vector.mOfFn fun (i : Fin n) => f i a

@[simp]

theorem Vector.mOfFn_part_some {α : Type u_1} {n : ℕ} (f : Fin n → α) : (Vector.mOfFn fun (i : Fin n) => Part.some (f i)) = Part.some (Vector.ofFn f)

theorem Computable.option_some_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → σ} : (Computable fun (a : α) => some (f a)) ↔ Computable f

theorem Computable.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → Option σ} : (Computable₂ fun (a : α) (n : ℕ) => Option.bind (Encodable.decode n) (f a)) ↔ Computable₂ f

theorem Computable.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Computable₂ fun (a : α) (n : ℕ) => Option.map (f a) (Encodable.decode n)) ↔ Computable₂ f

theorem Computable.nat_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ} (hf : Computable f) (hg : Computable g) (hh : Computable₂ h) : Computable fun (a : α) => Nat.rec (g a) (fun (y : ℕ) (IH : (fun (x : ℕ) => σ) y) => h a (y, IH)) (f a)

theorem Computable.nat_casesOn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ} (hf : Computable f) (hg : Computable g) (hh : Computable₂ h) : Computable fun (a : α) => Nat.casesOn (f a) (g a) (h a)

theorem Computable.cond {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Computable c) (hf : Computable f) (hg : Computable g) : Computable fun (a : α) => bif c a then f a else g a

theorem Computable.option_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Computable o) (hf : Computable f) (hg : Computable₂ g) : Computable fun (a : α) => Option.casesOn (o a) (f a) (g a)

theorem Computable.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → Option β} {g : α → β → Option σ} (hf : Computable f) (hg : Computable₂ g) : Computable fun (a : α) => Option.bind (f a) (g a)

theorem Computable.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → Option β} {g : α → β → σ} (hf : Computable f) (hg : Computable₂ g) : Computable fun (a : α) => Option.map (g a) (f a)

theorem Computable.option_getD {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → Option β} {g : α → β} (hf : Computable f) (hg : Computable g) : Computable fun (a : α) => Option.getD (f a) (g a)

theorem Computable.subtype_mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} {p : β → Prop} [DecidablePred p] {h : ∀ (a : α), p (f a)} (hp : PrimrecPred p) (hf : Computable f) : Computable fun (a : α) => { val := f a, property := (_ : p (f a)) }

theorem Computable.sum_casesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Computable f) (hg : Computable₂ g) (hh : Computable₂ h) : Computable fun (a : α) => Sum.casesOn (f a) (g a) (h a)

theorem Computable.nat_strong_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Computable₂ g) (H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)) : Computable₂ f

theorem Computable.list_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} : (∀ (i : Fin n), Computable (f i)) → Computable fun (a : α) => List.ofFn fun (i : Fin n) => f i a

theorem Computable.vector_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} (hf : ∀ (i : Fin n), Computable (f i)) : Computable fun (a : α) => Vector.ofFn fun (i : Fin n) => f i a

theorem Partrec.option_some_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} : (Partrec fun (a : α) => Part.map some (f a)) ↔ Partrec f

theorem Partrec.option_casesOn_right {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {o : α → Option β} {f : α → σ} {g : α → β →. σ} (ho : Computable o) (hf : Computable f) (hg : Partrec₂ g) : Partrec fun (a : α) => Option.casesOn (o a) (Part.some (f a)) (g a)

theorem Partrec.sum_casesOn_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ} (hf : Computable f) (hg : Computable₂ g) (hh : Partrec₂ h) : Partrec fun (a : α) => Sum.casesOn (f a) (fun (b : β) => Part.some (g a b)) (h a)

theorem Partrec.sum_casesOn_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ} (hf : Computable f) (hg : Partrec₂ g) (hh : Computable₂ h) : Partrec fun (a : α) => Sum.casesOn (f a) (g a) fun (c : γ) => Part.some (h a c)

theorem Partrec.fix_aux {α : Type u_5} {σ : Type u_6} (f : α →. σ ⊕ α) (a : α) (b : σ) : let F := fun (a : α) (n : ℕ) => Nat.rec (Part.some (Sum.inr a)) (fun (x : ℕ) (IH : Part (σ ⊕ α)) => Part.bind IH fun (s : σ ⊕ α) => Sum.casesOn s (fun (x : σ) => Part.some s) f) n; (∃ (n : ℕ), ((∃ (b' : σ), Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ (b : α), Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ PFun.fix f a

theorem Partrec.fix {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ ⊕ α} (hf : Partrec f) : Partrec (PFun.fix f)