Supporting results for pointwise provable equality.

theorem PointwiseComposition.Nat.Partrec.projection {f : ℕ →. ℕ} (hf : Nat.Partrec f) (unif : ∀ {m n₁ n₂ a₁ a₂ : ℕ}, a₁ ∈ f (Nat.pair m n₁) → a₂ ∈ f (Nat.pair m n₂) → a₁ = a₂) : ∃ (g : ℕ →. ℕ), Nat.Partrec g ∧ ∀ (a m : ℕ), a ∈ g m ↔ ∃ (z : ℕ), a ∈ f (Nat.pair m z)

theorem PointwiseComposition.Partrec.projection {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β →. γ} (hf : Partrec₂ f) (unif : ∀ {a : α} {b₁ b₂ : β} {c₁ c₂ : γ}, c₁ ∈ f a b₁ → c₂ ∈ f a b₂ → c₁ = c₂) : ∃ (g : α →. γ), Partrec g ∧ ∀ (c : γ) (a : α), c ∈ g a ↔ ∃ (b : β), c ∈ f a b

@[simp]

theorem PointwiseComposition.REPred.const {α : Type u_1} [Primcodable α] (p : Prop) : REPred fun (x : α) => p

theorem PointwiseComposition.REPred.iff {α : Type u_1} [Primcodable α] {p : α → Prop} : REPred p ↔ ∃ (f : α →. Unit), Partrec f ∧ p = fun (x : α) => (f x).Dom

theorem PointwiseComposition.REPred.iff' {α : Type u_1} [Primcodable α] {p : α → Prop} : REPred p ↔ ∃ (f : α →. Unit), Partrec f ∧ ∀ (x : α), p x ↔ (f x).Dom

theorem PointwiseComposition.REPred.and {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred fun (x : α) => p x ∧ q x

theorem PointwiseComposition.REPred.or {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred fun (x : α) => p x ∨ q x

theorem PointwiseComposition.REPred.projection {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α × β → Prop} (hp : REPred p) : REPred fun (x : α) => ∃ (y : β), p (x, y)

theorem PointwiseComposition.REPred.comp {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} (hf : Computable f) {p : β → Prop} (hp : REPred p) : REPred fun (x : α) => p (f x)

@[simp]

theorem PointwiseComposition.ComputablePred.const {α : Type u_1} [Primcodable α] (p : Prop) : ComputablePred fun (x : α) => p

theorem PointwiseComposition.ComputablePred.and {α : Type u_1} [Primcodable α] {p q : α → Prop} : ComputablePred p → ComputablePred q → ComputablePred fun (x : α) => p x ∧ q x

theorem PointwiseComposition.ComputablePred.or {α : Type u_1} [Primcodable α] {p q : α → Prop} : ComputablePred p → ComputablePred q → ComputablePred fun (x : α) => p x ∨ q x

theorem PointwiseComposition.ComputablePred.of_graph_rePred {α : Type u_1} [Primcodable α] {g : α → ℕ} (h : REPred fun (p : α × ℕ) => p.2 = g p.1) : Computable g

def PointwiseComposition.Nat.boundedMax (f : ℕ → ℕ) (n : ℕ) : ℕ

The bounded Max construction in Nat.

Equations

• PointwiseComposition.Nat.boundedMax f n = Nat.rec (f 0) (fun (k ih : ℕ) => max ih (f (k + 1))) n

theorem PointwiseComposition.Nat.computable_boundedMax {f : ℕ → ℕ} (hf : Computable f) : Computable (boundedMax f)

theorem PointwiseComposition.Nat.le_boundedMax {f : ℕ → ℕ} {k n : ℕ} (h : k ≤ n) : f k ≤ boundedMax f n

theorem PointwiseComposition.Primrec.nat_natToList : Primrec Nat.natToList