Supporting results for pointwise provable equality.

Vec

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instAdjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Adjoin V V

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.instAdjoin = { adjoin := fun (x1 x2 : V) => ⟪x1, x2⟫ + 1 }

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term_∷_» : Lean.TrailingParserDescr

The «term ∷ » construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term?[_]» : Lean.ParserDescr

The «term?[ ]» construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoinUnexpander : Lean.PrettyPrinter.Unexpander

The adjoin Unexpander construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : adjoin x v = ⟪x, v⟫ + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.fstIdx_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : fstIdx (adjoin x v) = x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sndIdx_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : sndIdx (adjoin x v) = v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_eq_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : x + 1 = adjoin (π₁ x) (π₂ x)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : x < adjoin x v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_adjoin' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : v < adjoin x v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_lt_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : 0 < adjoin x v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_ne_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : adjoin x v ≠ 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_ne_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : 0 ≠ adjoin x v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nil_or_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (z : V) : z = 0 ∨ ∃ (x : V) (v : V), z = adjoin x v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x₁ x₂ v₁ v₂ : V) : adjoin x₁ v₁ = adjoin x₂ v₂ ↔ x₁ = x₂ ∧ v₁ = v₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_le_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x₁ x₂ v₁ v₂ : V} (hx : x₁ ≤ x₂) (hv : v₁ ≤ v₂) : adjoin x₁ v₁ ≤ adjoin x₂ v₂

def PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoinDef : Σ₀.Semisentence 3

The adjoin Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₀-Function₂ adjoin via adjoinDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₀-Function₂ adjoin

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (ℌ : HierarchySymbol) : ℌ-Function₂ adjoin

def PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₁Def : Σ₀.Semisentence 2

The mk Vec₁Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₁_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₀-Function₁ fun (x : V) => ?[x] via mkVec₁Def

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₁_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₀-Function₁ fun (x : V) => ?[x]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₁_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (ℌ : HierarchySymbol) : ℌ-Function₁ fun (x : V) => ?[x]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₂Def : Σ₁.Semisentence 3

The mk Vec₂Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₂_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ fun (x y : V) => ?[x, y] via mkVec₂Def

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₂_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ fun (x y : V) => ?[x, y]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mkVec₂_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => ?[x, y]

N-th element of List

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.Phi {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (C : Set V) (pr : V) : Prop

The Phi construction in FFL.FirstOrder.Arithmetic.Nth.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.blueprint : Fixpoint.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Nth.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Fixpoint.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.Nth.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.adjointruction = { Φ := fun (x : Fin 0 → V) => PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.Phi, defined := ⋯, monotone := ⋯ }

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.instFiniteAdjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Fixpoint.Construction.Finite V adjointruction

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.Graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : V → Prop

The Graph construction in FFL.FirstOrder.Arithmetic.Nth.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.Graph = PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.adjointruction.IsFixedPoint ![]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graphDef : Σ₁.Semisentence 1

The graph Def construction in FFL.FirstOrder.Arithmetic.Nth.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graphDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.blueprint.fixpointDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Predicate Graph via graphDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Predicate Graph

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : { Γ := Σ, rank := 0 + 1 }-Predicate Graph

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.zero_ne_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : 0 ≠ x + 1

TODO: move

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_case {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {pr : V} : Graph pr ↔ (∃ (v : V), pr = ⟪v, ⟪0, fstIdx v⟫⟫) ∨ ∃ (v : V) (i : V) (x : V), pr = ⟪v, ⟪i + 1, x⟫⟫ ∧ Graph ⟪sndIdx v, ⟪i, x⟫⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v x : V} : Graph ⟪v, ⟪0, x⟫⟫ ↔ x = fstIdx v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i x : V} : Graph ⟪v, ⟪i + 1, x⟫⟫ ↔ Graph ⟪sndIdx v, ⟪i, x⟫⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : ∃ (x : V), Graph ⟪v, ⟪i, x⟫⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i x₁ x₂ : V} : Graph ⟪v, ⟪i, x₁⟫⟫ → Graph ⟪v, ⟪i, x₂⟫⟫ → x₁ = x₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Nth.graph_existsUnique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : ∃! x : V, Graph ⟪v, ⟪i, x⟫⟫

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.nth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : V

The nth construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.nth v i = PointwiseComposition.Classical.chooseUnique ⋯

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term_.[_]» : Lean.TrailingParserDescr

The [ ]» construction in FFL.FirstOrder.Arithmetic.«term_.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : Nth.Graph ⟪v, ⟪i, nth v i⟫⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_eq_of_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i x : V} (h : Nth.Graph ⟪v, ⟪i, x⟫⟫) : nth v i = x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : nth v 0 = fstIdx v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : nth v (i + 1) = nth (sndIdx v) i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_adjoin_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : nth (adjoin x v) 0 = x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_adjoin_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v i : V) : nth (adjoin x v) (i + 1) = nth v i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_adjoin_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : nth (adjoin x v) 1 = nth v 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_adjoin_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : nth (adjoin x v) 2 = nth v 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_cases {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : x = 0 ∨ ∃ (y : V) (v : V), x = adjoin y v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (nil : P 0) (adjoin : ∀ (x v : V), P v → P (adjoin x v)) (v : V) : P v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_ISigma1.sigma1_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {P : V → Prop} (hP : Σ₁-Predicate P) (nil : P 0) (adjoin : ∀ (x v : V), P v → P (adjoin x v)) (v : V) : P v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_ISigma1.pi1_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {P : V → Prop} (hP : Π₁-Predicate P) (nil : P 0) (adjoin : ∀ (x v : V), P v → P (adjoin x v)) (v : V) : P v

def PointwiseComposition.FFL.FirstOrder.Arithmetic.nthDef : Σ₁.Semisentence 3

The nth Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ nth via nthDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ nth

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ nth

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.adjoin_absolute {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (a v : ℕ) : ↑(adjoin a v) = adjoin ↑a ↑v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : π₁ 0 = 0

TODO: move

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : π₂ 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_zero_idx {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (i : V) : nth 0 i = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_lt_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v : V} (hv : 0 < v) (i : V) : nth v i < v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v i : V) : nth v i ≤ v

Inductivly Construction of Function on List

structure PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Blueprint (arity : ℕ) : Type

Data specifying the encoded construction in FFL.FirstOrder.Arithmetic.VecRec.

• nil : Σ₁.Semisentence (arity + 1)

  The nil construction in FFL.FirstOrder.Arithmetic.VecRec.Blueprint.

• adjoin : Σ₁.Semisentence (arity + 4)

  The adjoin construction in FFL.FirstOrder.Arithmetic.VecRec.Blueprint.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Blueprint.blueprint {arity : ℕ} (β : Blueprint arity) : Fixpoint.Blueprint arity

The blueprint construction in FFL.FirstOrder.Arithmetic.VecRec.Blueprint.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Blueprint.graphDef {arity : ℕ} (β : Blueprint arity) : Σ₁.Semisentence (arity + 1)

The graph Def construction in FFL.FirstOrder.Arithmetic.VecRec.Blueprint.

Equations

• β.graphDef = β.blueprint.fixpointDef

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Blueprint.resultDef {arity : ℕ} (β : Blueprint arity) : Σ₁.Semisentence (arity + 2)

The result Def construction in FFL.FirstOrder.Arithmetic.VecRec.Blueprint.

Equations

• One or more equations did not get rendered due to their size.

structure PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction (V : Type u_1) [ORingStructure V] {arity : ℕ} (β : Blueprint arity) : Type u_1

Data and laws for Construction in FFL.FirstOrder.Arithmetic.VecRec.

• nil (param : Fin arity → V) : V

  The nil construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

• adjoin (param : Fin arity → V) (x xs ih : V) : V

  The adjoin construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

• nil_defined : HierarchySymbol.DefinedFunction self.nil β.nil
• adjoin_defined : HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1 + 1 + 1) → V) => self.adjoin (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2)) β.adjoin

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.Phi {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (C : Set V) (pr : V) : Prop

The Phi construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

Equations

• c.Phi param C pr = (pr = ⟪0, c.nil param⟫ ∨ ∃ (x : V) (xs : V) (ih : V), pr = ⟪PointwiseComposition.adjoin x xs, c.adjoin param x xs ih⟫ ∧ ⟪xs, ih⟫ ∈ C)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction V β.blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

Equations

• c.adjointruction = { Φ := c.Phi, defined := ⋯, monotone := ⋯ }

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.instFiniteAdjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction.Finite V c.adjointruction

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.Graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : V → Prop

The Graph construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

Equations

• c.Graph param = c.adjointruction.IsFixedPoint param

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : HierarchySymbol.Defined (fun (v : Fin (arity + 1) → V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Σ₁.Definable fun (v : Fin (arity + 1) → V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : Σ₁-Predicate c.Graph param

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_definable'' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : { Γ := Σ, rank := 0 + 1 }-Predicate c.Graph param

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_case {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {pr : V} : c.Graph param pr ↔ pr = ⟪0, c.nil param⟫ ∨ ∃ (x : V) (xs : V) (ih : V), pr = ⟪PointwiseComposition.adjoin x xs, c.adjoin param x xs ih⟫ ∧ c.Graph param ⟪xs, ih⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {l : V} : c.Graph param ⟪0, l⟫ ↔ l = c.nil param

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {x xs y : V} : c.Graph param ⟪PointwiseComposition.adjoin x xs, y⟫ ↔ ∃ (y' : V), y = c.adjoin param x xs y' ∧ c.Graph param ⟪xs, y'⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (xs : V) : ∃ (y : V), c.Graph param ⟪xs, y⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {xs y₁ y₂ : V} : c.Graph param ⟪xs, y₁⟫ → c.Graph param ⟪xs, y₂⟫ → y₁ = y₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.graph_existsUnique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (xs : V) : ∃! y : V, c.Graph param ⟪xs, y⟫

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (xs : V) : V

The result construction in FFL.FirstOrder.Arithmetic.VecRec.Construction.

Equations

• c.result param xs = PointwiseComposition.Classical.chooseUnique ⋯

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (xs : V) : c.Graph param ⟪xs, c.result param xs⟫

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_eq_of_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {xs y : V} (h : c.Graph param ⟪xs, y⟫) : c.result param xs = y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : c.result param 0 = c.nil param

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (x xs : V) : c.result param (PointwiseComposition.adjoin x xs) = c.adjoin param x xs (c.result param xs)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1) → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.resultDef

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.eval_resultDef {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2) → V) : (Semiformula.Evalb v) ↑β.resultDef ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Σ₁.DefinableFunction fun (v : Fin (arity + 1) → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.VecRec.Construction.result_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }.DefinableFunction fun (v : Fin (arity + 1) → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)

Length of List

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Len.blueprint : VecRec.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.Len.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Len.adjointruction {V : Type u_1} [ORingStructure V] : VecRec.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.Len.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.len {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : V

The len construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.len v = PointwiseComposition.FFL.FirstOrder.Arithmetic.Len.adjointruction.result ![] v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : len 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : len (adjoin x v) = len v + 1

def PointwiseComposition.FFL.FirstOrder.Arithmetic.lenDef : Σ₁.Semisentence 2

The len Def construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.lenDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.Len.blueprint.resultDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.len_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ len via lenDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.len_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ len

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.len_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₁ len

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_zero_iff_eq_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v : V} : len v = 0 ↔ v = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_lt_len {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i : V} (hl : len v ≤ i) : nth v i = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : len v ≤ v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : ∀ i < len v₁, nth v₁ i = nth v₂ i) : v₁ = v₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_ext' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (l : V) {v₁ v₂ : V} (hl₁ : len v₁ = l) (hl₂ : len v₂ = l) (H : ∀ i < l, nth v₁ i = nth v₂ i) : v₁ = v₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_of_nth_le_nth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v₁ v₂ : V} (hl : len v₁ = len v₂) (H : ∀ i < len v₁, nth v₁ i ≤ nth v₂ i) : v₁ ≤ v₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_lt_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i : V} (hi : i < len v) : nth v i < v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigmaOne_skolem_vec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {R : V → V → Prop} (hP : Σ₁-Relation R) {l : V} (H : ∀ x < l, ∃ (y : V), R x y) : ∃ (v : V), len v = l ∧ ∀ i < l, R i (nth v i)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_singleton_iff_len_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v : V} : len v = 1 ↔ ∃ (x : V), v = ?[x]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_doubleton_of_len_eq_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v : V} : len v = 2 ↔ ∃ (x : V) (y : V), v = ?[x, y]

Maximum of List

def PointwiseComposition.FFL.FirstOrder.Arithmetic.ListMax.blueprint : VecRec.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.ListMax.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.ListMax.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : VecRec.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.ListMax.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : V

The list Max construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax v = PointwiseComposition.FFL.FirstOrder.Arithmetic.ListMax.adjointruction.result ![] v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : listMax 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : listMax (adjoin x v) = x ⊔ listMax v

def PointwiseComposition.FFL.FirstOrder.Arithmetic.listMaxDef : Σ₁.Semisentence 2

The list Max Def construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.listMaxDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.ListMax.blueprint.resultDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ listMax via listMaxDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ listMax

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.listMax_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₁ listMax

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_le_listMax {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {i v : V} (h : i < len v) : nth v i ≤ listMax v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.listMaxss_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v z : V} (h : ∀ i < len v, nth v i ≤ z) : listMax v ≤ z

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.listMaxss_le_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v z : V} : listMax v ≤ z ↔ ∀ i < len v, nth v i ≤ z

Take Last k-Element

def PointwiseComposition.FFL.FirstOrder.Arithmetic.TakeLast.blueprint : VecRec.Blueprint 1

The blueprint construction in FFL.FirstOrder.Arithmetic.TakeLast.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.TakeLast.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : VecRec.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.TakeLast.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v k : V) : V

The take Last construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast v k = PointwiseComposition.FFL.FirstOrder.Arithmetic.TakeLast.adjointruction.result ![k] v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {k : V} : takeLast 0 k = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {k : V} (x v : V) : takeLast (adjoin x v) k = if len v < k then adjoin x v else takeLast v k

def PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLastDef : Σ₁.Semisentence 3

The take Last Def construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLastDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.TakeLast.blueprint.resultDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ takeLast via takeLastDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ takeLast

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ takeLast

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_takeLast {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v k : V} (h : k ≤ len v) : len (takeLast v k) = k

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_len_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : takeLast v (len v) = v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_sub_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (a b c : V) : a + c - (b + c) = a - b

TODO: move

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : takeLast v 0 = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.takeLast_succ_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {i v : V} (h : i < len v) : takeLast v (i + 1) = adjoin (nth v (len v - (i + 1))) (takeLast v i)

Concatation

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Concat.blueprint : VecRec.Blueprint 1

The blueprint construction in FFL.FirstOrder.Arithmetic.Concat.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Concat.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : VecRec.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.Concat.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.concat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v z : V) : V

The concat construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.concat v z = PointwiseComposition.FFL.FirstOrder.Arithmetic.Concat.adjointruction.result ![z] v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (z : V) : concat 0 z = ?[z]

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v z : V) : concat (adjoin x v) z = adjoin x (concat v z)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.concatDef : Σ₁.Semisentence 3

The concat Def construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.concatDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.Concat.blueprint.resultDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ concat via concatDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ concat

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ concat

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_concat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v z : V) : len (concat v z) = len v + 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_nth_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v z : V) {i : V} (hi : i < len v) : nth (concat v z) i = nth v i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_nth_len {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v z : V) : nth (concat v z) (len v) = z

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.concat_nth_len' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v z : V) {i : V} (hi : len v = i) : nth (concat v z) i = z

Membership

def PointwiseComposition.FFL.FirstOrder.Arithmetic.MemVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : Prop

The Mem Vec construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.MemVec x v = ∃ i < PointwiseComposition.FFL.FirstOrder.Arithmetic.len v, x = PointwiseComposition.FFL.FirstOrder.Arithmetic.nth v i

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term_∈ᵥ_» : Lean.TrailingParserDescr

The «term ∈ᵥ » construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.not_memVec_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : ¬MemVec x 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_mem_memVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {i v : V} (h : i < len v) : MemVec (nth v i) v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.memVec_insert_fst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x v : V} : MemVec x (adjoin x v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.memVec_adjoin_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x y v : V} : MemVec x (adjoin y v) ↔ x = y ∨ MemVec x v

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_of_memVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x v : V} (h : MemVec x v) : x ≤ v

def PointwiseComposition.FFL.FirstOrder.Arithmetic.memVecDef : ∆₁.Semisentence 2

The mem Vec Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.memVec_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ∆₁-Relation MemVec via memVecDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.memVec_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ∆₁-Relation MemVec

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.memVec_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation MemVec

Subset

def PointwiseComposition.FFL.FirstOrder.Arithmetic.SubsetVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v w : V) : Prop

The Subset Vec construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term_⊆ᵥ_» : Lean.TrailingParserDescr

The «term ⊆ᵥ » construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.SubsetVec.refl {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : SubsetVec v v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.subsetVec_insert_tail {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : SubsetVec v (adjoin x v)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.subsetVecDef : ∆₁.Semisentence 2

The subset Vec Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.subsetVec_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ∆₁-Relation SubsetVec via subsetVecDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.subsetVec_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : ∆₁-Relation SubsetVec

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.subsetVec_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation SubsetVec

Repeat

def PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec.blueprint : PR.Blueprint 1

The blueprint construction in FFL.FirstOrder.Arithmetic.repeatVec.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : PR.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.repeatVec.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x k : V) : V

repeatVec x k = x ∷ x ∷ x ∷ ... k times ... ∷ 0

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec x k = PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec.adjointruction.result ![x] k

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : repeatVec x 0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x k : V) : repeatVec x (k + 1) = adjoin x (repeatVec x k)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVecDef : Σ₁.Semisentence 3

The repeat Vec Def construction in FFL.FirstOrder.Arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ repeatVec via repeatVecDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ repeatVec

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.repeatVec_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₂ repeatVec

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_repeatVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x k : V) : len (repeatVec x k) = k

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_repaetVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x k : V) : k ≤ repeatVec x k

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_repeatVec {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x k : V) {i : V} (h : i < k) : nth (repeatVec x k) i = x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.len_repeatVec_of_nth_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v m : V} (H : ∀ i < len v, nth v i ≤ m) : v ≤ repeatVec m (len v)

Convert to Set

def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecToSet.blueprint : VecRec.Blueprint 0

The blueprint construction in FFL.FirstOrder.Arithmetic.VecToSet.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.VecToSet.adjointruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : VecRec.Construction V blueprint

The adjointruction construction in FFL.FirstOrder.Arithmetic.VecToSet.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : V) : V

The vec To Set construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet v = PointwiseComposition.FFL.FirstOrder.Arithmetic.VecToSet.adjointruction.result ![] v

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : vecToSet 0 = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet_adjoin {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x v : V) : vecToSet (adjoin x v) = insert x (vecToSet v)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSetDef : Σ₁.Semisentence 2

The vec To Set Def construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSetDef = PointwiseComposition.FFL.FirstOrder.Arithmetic.VecToSet.blueprint.resultDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ vecToSet via vecToSetDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₁ vecToSet

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSet_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₁ vecToSet

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_vecToSet_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v x : V} : x ∈ vecToSet v ↔ ∃ i < len v, x = nth v i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nth_mem_vecToSet {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v i : V} (h : i < len v) : nth v i ∈ vecToSet v