Theorems · Theorem · logic and foundations

Nat.Partrec.Code.computable_recOn

∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
  Computable c →
    ∀ {z : α → σ},
      Computable z →
        ∀ {s : α → σ},
          Computable s →
            ∀ {l : α → σ},
              Computable l →
                ∀ {r : α → σ},
                  Computable r →
                    ∀ {pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                      Computable₂ pr →
                        ∀ {co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                          Computable₂ co →
                            ∀ {pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                              Computable₂ pc →
                                ∀ {rf : α → Nat.Partrec.Code × σ → σ},
                                  Computable₂ rf →
                                    have PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
                                    have CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
                                    have PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
                                    have RF := fun a cf hf => rf a (cf, hf);
                                    have F := fun a c =>
                                      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
                                    Computable fun a => F a (c a)

Recursion on Nat.Partrec.Code is computable.

Defined in

Mathlib.Computability.PartrecCode

Cited by

0 results in Mathlib

Foundations

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

Assumes

PrimcodablePrimcodable