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

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 = (Nat.rfind fun (n : ℕ) => ↑(some (f n).isSome)).bind 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

PartRec f means that the partial function f : ℕ → ℕ is partially recursive.

• 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 : ℕ) => Nat.pair <$> f n <*> 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 : ℕ) => (f a).bind 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 : ℕ) => ↑n.ppred

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

Partially recursive partial functions α → σ between Primcodable types

Equations

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

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

Partially recursive partial functions α → β → σ between Primcodable types

Equations

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

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

Computable functions α → σ between Primcodable types: a function is computable if and only if it is partially recursive (as a partial function)

Equations

• Computable f = Partrec ↑f

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

Computable functions α → β → σ between Primcodable types

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 (x1 x2 : List α) => x1 ++ x2

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₂ List.Vector.cons

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

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

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

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

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

theorem Computable.vector_ofFn' {α : Type u_1} [Primcodable α] {n : ℕ} : Computable List.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_3} [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_3} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α → σ} (hf : Partrec f) (H : ∀ (n : α), g n ∈ f n) : Computable g

theorem Partrec.none {α : Type u_1} {σ : Type u_3} [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_3} [Primcodable α] [Primcodable σ] (s : Part σ) [Decidable s.Dom] : Partrec fun (x : α) => s

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

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

theorem Partrec.map {α : Type u_1} {β : Type u_2} {σ : Type u_3} [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_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β →. σ} (hf : Partrec f) : Partrec₂ fun (a : α) (b : β) => f (a, b)

theorem Partrec.nat_rec {α : Type u_1} {σ : Type u_3} [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 σ) => IH.bind fun (i : σ) => h a (y, i)) (f a)

theorem Partrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [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_3} [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₂.mk {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Computable fun (p : α × β) => f p.1 p.2) : Computable₂ f

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_2} [Primcodable α] [Primcodable σ] {f : α → ℕ → Option σ} (hf : Computable₂ f) : Partrec fun (a : α) => Nat.rfindOpt (f a)

theorem Partrec.nat_casesOn_right {α : Type u_1} {σ : Type u_2} [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_2} [Primcodable α] [Primcodable σ] {f : α →. σ} : Partrec f ↔ Nat.Partrec fun (n : ℕ) => (↑(Encodable.decode₂ α n)).bind fun (a : α) => Part.map Encodable.encode (f a)

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

@[simp]

theorem Vector.mOfFn_part_some {α : Type u_1} {n : ℕ} (f : Fin n → α) : (List.Vector.mOfFn fun (i : Fin n) => Part.some (f i)) = Part.some (List.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 : ℕ) => (Encodable.decode n).bind (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 : α) => (f a).bind (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 : α) => (f a).getD (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 : α) => ⟨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 : α) => List.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 (σ ⊕ α)) => IH.bind 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 ∈ f.fix a

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