Supporting results for pointwise provable equality.

class PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) : Prop

Data and laws for Bounded in FFL.FirstOrder.Arithmetic.

• bounded : ∃ (t : ArithmeticSemiterm V k), ∀ (v : Fin k → V), f v ≤ Semiterm.val v id t

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₁ {V : Type u_2} [ORingStructure V] (f : V → V) : Prop

The Bounded₁ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₁ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded fun (v : Fin 1 → V) => f (v 0)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂ {V : Type u_2} [ORingStructure V] (f : V → V → V) : Prop

The Bounded₂ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded fun (v : Fin 2 → V) => f (v 0) (v 1)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₃ {V : Type u_2} [ORingStructure V] (f : V → V → V → V) : Prop

The Bounded₃ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₃ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [h : Bounded f] : Bounded f

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.var {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (i : Fin k) : Bounded fun (v : Fin k → V) => v i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.const {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (c : V) : Bounded fun (x : Fin k → V) => c

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.term_retraction {n : ℕ} {V : Type u_2} [ORingStructure V] {k : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] (t : ArithmeticSemiterm V n) (e : Fin n → Fin k) : Bounded fun (v : Fin k → V) => Semiterm.val (fun (x : Fin n) => v (e x)) id t

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.term {V : Type u_2} [ORingStructure V] {k : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] (t : ArithmeticSemiterm V k) : Bounded fun (v : Fin k → V) => Semiterm.val v id t

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.retraction {n : ℕ} {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} (hf : Bounded f) (e : Fin k → Fin n) : Bounded fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded.comp {V : Type u_2} [ORingStructure V] {l : ℕ} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {f : (Fin l → V) → V} {g : Fin l → (Fin k → V) → V} (hf : Bounded f) (hg : ∀ (i : Fin l), Bounded (g i)) : Bounded fun (v : Fin k → V) => f fun (x : Fin l) => g x v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₁.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {f : V → V} {k : ℕ} {g : (Fin k → V) → V} (hf : Bounded₁ f) (hg : Bounded g) : Bounded fun (v : Fin k → V) => f (g v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {f : V → V → V} {k : ℕ} {g₁ g₂ : (Fin k → V) → V} (hf : Bounded₂ f) (hg₁ : Bounded g₁) (hg₂ : Bounded g₂) : Bounded fun (v : Fin k → V) => f (g₁ v) (g₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₃.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {f : V → V → V → V} {k : ℕ} {g₁ g₂ g₃ : (Fin k → V) → V} (hf : Bounded₃ f) (hg₁ : Bounded g₁) (hg₂ : Bounded g₂) (hg₃ : Bounded g₃) : Bounded fun (v : Fin k → V) => f (g₁ v) (g₂ v) (g₃ v)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂.add {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] : Bounded₂ fun (x1 x2 : V) => x1 + x2

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂.mul {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] : Bounded₂ fun (x1 x2 : V) => x1 * x2

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂.hAdd {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] : Bounded₂ HAdd.hAdd

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded₂.hMul {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] : Bounded₂ HMul.hMul

def PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) : Prop

The Definable Bounded Function construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction f = (PointwiseComposition.FFL.FirstOrder.Arithmetic.Bounded f ∧ Σ₀.DefinableFunction f)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₁ {V : Type u_2} [ORingStructure V] (f : V → V) : Prop

The Definable Bounded Function₁ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₁ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction fun (v : Fin 1 → V) => f (v 0)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₂ {V : Type u_2} [ORingStructure V] (f : V → V → V) : Prop

The Definable Bounded Function₂ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₂ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction fun (v : Fin 2 → V) => f (v 0) (v 1)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₃ {V : Type u_2} [ORingStructure V] (f : V → V → V → V) : Prop

The Definable Bounded Function₃ construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₃ f = PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.bounded {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} (h : DefinableBoundedFunction f) : Bounded f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₁.bounded {V : Type u_2} [ORingStructure V] {f : V → V} (h : DefinableBoundedFunction₁ f) : Bounded₁ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₂.bounded {V : Type u_2} [ORingStructure V] {f : V → V → V} (h : DefinableBoundedFunction₂ f) : Bounded₂ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₃.bounded {V : Type u_2} [ORingStructure V] {f : V → V → V → V} (h : DefinableBoundedFunction₃ f) : Bounded₃ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.definable {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {k : ℕ} {f : (Fin k → V) → V} (h : DefinableBoundedFunction f) : ℌ.DefinableFunction f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₁.definable {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V} (h : DefinableBoundedFunction₁ f) : ℌ-Function₁ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₂.definable {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V → V} (h : DefinableBoundedFunction₂ f) : ℌ-Function₂ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₃.definable {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} {f : V → V → V → V} (h : DefinableBoundedFunction₃ f) : ℌ-Function₃ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.of_polybounded_of_definable {V : Type u_2} [ORingStructure V] {k : ℕ} (f : (Fin k → V) → V) [hb : Bounded f] [hf : Σ₀.DefinableFunction f] : DefinableBoundedFunction f

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.of_polybounded_of_definable₁ {V : Type u_2} [ORingStructure V] (f : V → V) [hb : Bounded₁ f] [hf : Σ₀-Function₁ f] : DefinableBoundedFunction₁ f

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.of_polybounded_of_definable₂ {V : Type u_2} [ORingStructure V] (f : V → V → V) [hb : Bounded₂ f] [hf : Σ₀-Function₂ f] : DefinableBoundedFunction₂ f

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.of_polybounded_of_definable₃ {V : Type u_2} [ORingStructure V] (f : V → V → V → V) [hb : Bounded₃ f] [hf : Σ₀-Function₃ f] : DefinableBoundedFunction₃ f

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.retraction {n : ℕ} {V : Type u_2} [ORingStructure V] {k : ℕ} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (e : Fin k → Fin n) : DefinableBoundedFunction fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_blt {k : ℕ} {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : ℌ.Definable fun (v : Fin k → V) => ∀ x < f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_blt {k : ℕ} {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : ℌ.Definable fun (v : Fin k → V) => ∃ x < f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_ble {k : ℕ} {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : ℌ.Definable fun (v : Fin k → V) => ∀ x ≤ f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_ble {k : ℕ} {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : ℌ.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : ℌ.Definable fun (v : Fin k → V) => ∃ x ≤ f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_blt_zero {k : ℕ} {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => ∀ x < f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_blt_zero {k : ℕ} {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => ∃ x < f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_ble_zero {k : ℕ} {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => ∀ x ≤ f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_ble_zero {k : ℕ} {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : DefinableBoundedFunction f) (h : { Γ := Γ, rank := 0 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => ∃ x ≤ f v, P v x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_vec_le_boldfaceBoundedFunction {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {l k : ℕ} {φ : Fin l → (Fin k → V) → V} {P : (Fin k → V) → (Fin l → V) → Prop} (pp : ∀ (i : Fin l), DefinableBoundedFunction (φ i)) (hP : ℌ.Definable fun (w : Fin (k + l) → V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) : ℌ.Definable fun (v : Fin k → V) => ∃ w ≤ fun (x : Fin l) => φ x v, P v w

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.substitution_boldfaceBoundedFunction {k : ℕ} {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {P : (Fin k → V) → Prop} {l : ℕ} {f : Fin k → (Fin l → V) → V} (hP : ℌ.Definable P) (hf : ∀ (i : Fin k), DefinableBoundedFunction (f i)) : ℌ.Definable fun (z : Fin l → V) => P fun (x : Fin k) => f x z

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.of_iff {V : Type u_2} [ORingStructure V] {k : ℕ} {f g : (Fin k → V) → V} (H : DefinableBoundedFunction f) (h : ∀ (v : Fin k → V), f v = g v) : DefinableBoundedFunction g

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.var {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (i : Fin k) : DefinableBoundedFunction fun (v : Fin k → V) => v i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.const {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (c : V) : DefinableBoundedFunction fun (x : Fin k → V) => c

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.term_retraction {n : ℕ} {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (t : ArithmeticSemiterm V n) (e : Fin n → Fin k) : DefinableBoundedFunction fun (v : Fin k → V) => Semiterm.val (fun (x : Fin n) => v (e x)) id t

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.term {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} (t : ArithmeticSemiterm V k) : DefinableBoundedFunction fun (v : Fin k → V) => Semiterm.val v id t

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₁ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {P : V → Prop} {f : (Fin k → V) → V} [hP : ℌ-Predicate P] (hf : DefinableBoundedFunction f) : ℌ.Definable fun (v : Fin k → V) => P (f v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₂ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → Prop} {f₁ f₂ : (Fin k → V) → V} [hR : ℌ-Relation R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) : ℌ.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₃ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → V → Prop} {f₁ f₂ f₃ : (Fin k → V) → V} [hR : ℌ-Relation₃ R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) : ℌ.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₄ {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → V → V → Prop} {f₁ f₂ f₃ f₄ : (Fin k → V) → V} [hR : ℌ-Relation₄ R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) (hf₄ : DefinableBoundedFunction f₄) : ℌ.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₁_zero {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {P : V → Prop} {f : (Fin k → V) → V} [hP : { Γ := Γ, rank := 0 }-Predicate P] (hf : DefinableBoundedFunction f) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => P (f v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₂_zero {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → Prop} {f₁ f₂ : (Fin k → V) → V} [hR : { Γ := Γ, rank := 0 }-Relation R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₃_zero {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → V → Prop} {f₁ f₂ f₃ : (Fin k → V) → V} [hR : { Γ := Γ, rank := 0 }-Relation₃ R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bcomp₄_zero {V : Type u_2} [ORingStructure V] {Γ : SigmaPiDelta} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {R : V → V → V → V → Prop} {f₁ f₂ f₃ f₄ : (Fin k → V) → V} [hR : { Γ := Γ, rank := 0 }-Relation₄ R] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) (hf₄ : DefinableBoundedFunction f₄) : { Γ := Γ, rank := 0 }.Definable fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction.bcomp {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {l k : ℕ} {F : (Fin l → V) → V} {f : Fin l → (Fin k → V) → V} (hF : ℌ.DefinableFunction F) (hf : ∀ (i : Fin l), DefinableBoundedFunction (f i)) : ℌ.DefinableFunction fun (v : Fin k → V) => F fun (x : Fin l) => f x v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₁.bcomp {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V} {f : (Fin k → V) → V} (hF : ℌ-Function₁ F) (hf : DefinableBoundedFunction f) : ℌ.DefinableFunction fun (v : Fin k → V) => F (f v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₂.bcomp {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V} {f₁ f₂ : (Fin k → V) → V} (hF : ℌ-Function₂ F) (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) : ℌ.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.DefinableFunction₃.bcomp {V : Type u_2} [ORingStructure V] {ℌ : HierarchySymbol} [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V → V} {f₁ f₂ f₃ : (Fin k → V) → V} (hF : ℌ-Function₃ F) (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) : ℌ.DefinableFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₁.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V} {f : (Fin k → V) → V} (hF : DefinableBoundedFunction₁ F) (hf : DefinableBoundedFunction f) : DefinableBoundedFunction fun (v : Fin k → V) => F (f v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₂.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V} {f₁ f₂ : (Fin k → V) → V} (hF : DefinableBoundedFunction₂ F) (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) : DefinableBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction₃.comp {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V → V} {f₁ f₂ f₃ : (Fin k → V) → V} (hF : DefinableBoundedFunction₃ F) (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) : DefinableBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.comp₁ {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V} {f : (Fin k → V) → V} [hFb : Bounded₁ F] [hFd : Σ₀-Function₁ F] (hf : DefinableBoundedFunction f) : DefinableBoundedFunction fun (v : Fin k → V) => F (f v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.comp₂ {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V} {f₁ f₂ : (Fin k → V) → V} [hFb : Bounded₂ F] [hFd : Σ₀-Function₂ F] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) : DefinableBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.DefinableBoundedFunction.comp₃ {V : Type u_2} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {k : ℕ} {F : V → V → V → V} {f₁ f₂ f₃ : (Fin k → V) → V} [hFb : Bounded₃ F] [hFd : Σ₀-Function₃ F] (hf₁ : DefinableBoundedFunction f₁) (hf₂ : DefinableBoundedFunction f₂) (hf₃ : DefinableBoundedFunction f₃) : DefinableBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)