Documentation

Mathlib.Computability.Partrec

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 : ℕ), k < n → (p k).Dom) :

{ n // true ∈ p n ∧ ∀ (m : ℕ), m < n → false ∈ p m }

Instances For

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

Instances For

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

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, 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 α) :

Instances For

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).fst
right: Nat.Partrec ↑fun n => (Nat.unpair n).snd
pair: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => Seq.seq (Nat.pair <$> f n) fun x => 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 => 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)

Instances For

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

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 => 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 : α →. σ) :

Instances For

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

Instances For

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

Instances For

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

Instances For

theorem Primrec.to_comp {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Primrec 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) :

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) :

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 α] :

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 => x ++ x_1

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

Computable₂ fun l 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) :

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

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.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 => f i a

@[simp]

theorem Vector.mOfFn_part_some {α : Type u_1} {n : ℕ} (f : Fin n → α) :

(Vector.mOfFn fun i => 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 => 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 := h 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 => 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 => 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.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)