mathlib documentation

computability.partrec_code

theorem nat.partrec.rfind' {f : →. } (hf : nat.partrec f) :
nat.partrec (nat.unpaired (λ (a m : ), part.map (λ (_x : ), _x + m) (nat.rfind (λ (n : ), (λ (m : ), to_bool (m = 0)) <$> f (nat.mkpair a (n + m))))))
theorem nat.partrec.code.const_inj {n₁ n₂ : } :
Equations
@[protected, instance]
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 × σ → σ} (hrf : 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σ → σ} (hrf : 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 × σ → σ} (hrf : 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
@[protected, instance]
Equations
@[simp]
theorem nat.partrec.code.eval_curry (c : nat.partrec.code) (n x : ) :
(c.curry n).eval x = c.eval (nat.mkpair n x)
theorem nat.partrec.code.curry_inj {c₁ c₂ : nat.partrec.code} {n₁ n₂ : } (h : 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 (nat.mkpair n 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 : } :