Theorems · Theorem · logic and foundations

Primrec.nat_omega_rec

∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (f : α → β → σ) {m : α → β → ℕ} {l : α → β → List β} {g : α → β × List σ → Option σ},
  Primrec₂ m →
    Primrec₂ l →
      Primrec₂ g →
        (∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b) →
          (∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)) → Primrec₂ f

Defined in

Mathlib.Computability.Primrec.List

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PrimcodablePrimcodablePrimcodable