mathlib documentation

computability.partrec_code

theorem nat.partrec.rfind' {f : →. } :
nat.partrec fnat.partrec (nat.unpaired (λ (a m : ), roption.map (λ (_x : ), _x + m) (nat.rfind (λ (n : ), (λ (m : ), to_bool (m = 0)) <$> f (a.mkpair (n + m))))))

theorem nat.partrec.code.const_inj {n₁ n₂ : } :

Equations
theorem nat.partrec.code.rec_prim' {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable «σ»] {c : α → nat.partrec.code} (hc : primrec c) {z : α → «σ»} (hz : primrec z) {s : α → «σ»} (hs : primrec s) {l : α → «σ»} (hl : primrec l) {r : α → «σ»} (hr : primrec r) {pr : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hpr : primrec₂ pr) {co : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hco : primrec₂ co) {pc : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hpc : primrec₂ pc) {rf : α → nat.partrec.code × «σ» → «σ»} :
primrec₂ rf(let PR : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), pr a (cf, cg, hf, hg), CO : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), co a (cf, cg, hf, hg), PC : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code«σ» → «σ» := λ (a : α) (cf : nat.partrec.code) (hf : «σ»), rf a (cf, hf), F : α → nat.partrec.code → «σ» := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in primrec (λ (a : α), F a (c a)))

theorem nat.partrec.code.rec_prim {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable «σ»] {c : α → nat.partrec.code} (hc : primrec c) {z : α → «σ»} (hz : primrec z) {s : α → «σ»} (hs : primrec s) {l : α → «σ»} (hl : primrec l) {r : α → «σ»} (hr : primrec r) {pr : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ»} (hpr : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × «σ» × «σ»), pr a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {co : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ»} (hco : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × «σ» × «σ»), co a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {pc : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ»} (hpc : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × «σ» × «σ»), pc a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {rf : α → nat.partrec.code«σ» → «σ»} :
primrec (λ (a : α × nat.partrec.code × «σ»), rf a.fst a.snd.fst a.snd.snd)(let F : α → nat.partrec.code → «σ» := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a) in primrec (λ (a : α), F a (c a)))

theorem nat.partrec.code.rec_computable {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable «σ»] {c : α → nat.partrec.code} (hc : computable c) {z : α → «σ»} (hz : computable z) {s : α → «σ»} (hs : computable s) {l : α → «σ»} (hl : computable l) {r : α → «σ»} (hr : computable r) {pr : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hpr : computable₂ pr) {co : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hco : computable₂ co) {pc : α → nat.partrec.code × nat.partrec.code × «σ» × «σ» → «σ»} (hpc : computable₂ pc) {rf : α → nat.partrec.code × «σ» → «σ»} :
computable₂ rf(let PR : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), pr a (cf, cg, hf, hg), CO : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), co a (cf, cg, hf, hg), PC : α → nat.partrec.codenat.partrec.code«σ» → «σ» → «σ» := λ (a : α) (cf cg : nat.partrec.code) (hf hg : «σ»), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code«σ» → «σ» := λ (a : α) (cf : nat.partrec.code) (hf : «σ»), rf a (cf, hf), F : α → nat.partrec.code → «σ» := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in computable (λ (a : α), F a (c a)))

Equations
@[simp]
theorem nat.partrec.code.eval_curry (c : nat.partrec.code) (n x : ) :
(c.curry n).eval x = c.eval (n.mkpair x)

theorem nat.partrec.code.curry_inj {c₁ c₂ : nat.partrec.code} {n₁ n₂ : } :
c₁.curry n₁ = c₂.curry n₂c₁ = c₂ n₁ = n₂

theorem nat.partrec.code.smn  :
∃ (f : nat.partrec.codenat.partrec.code), computable₂ f ∀ (c : nat.partrec.code) (n x : ), (f c n).eval x = c.eval (n.mkpair x)

Equations
theorem nat.partrec.code.evaln_bound {k : } {c : nat.partrec.code} {n x : } :
x nat.partrec.code.evaln k c nn < k

theorem nat.partrec.code.evaln_mono {k₁ k₂ : } {c : nat.partrec.code} {n x : } :
k₁ k₂x nat.partrec.code.evaln k₁ c nx nat.partrec.code.evaln k₂ c n

theorem nat.partrec.code.evaln_sound {k : } {c : nat.partrec.code} {n x : } :