Supporting results for pointwise provable equality.

Sequence

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

The Seq construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.isMapping {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) : IsMapping s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.seqDef : Σ₀.Semisentence 1

The seq Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.seq_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₀-Predicate Seq via seqDef

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

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«firstOrderFormula:Seq_» : Lean.ParserDescr

The «first order formula:Seq » construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_exists_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s : V) : ∃! l : V, (Seq s → domain s = under l) ∧ (¬Seq s → l = 0)

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

The lh construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.lh s = PointwiseComposition.Classical.chooseUnique ⋯

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_prop {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s : V) : (Seq s → domain s = under (lh s)) ∧ (¬Seq s → lh s = 0)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_prop_of_not_seq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : ¬Seq s) : lh s = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.domain_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) : domain s = under (lh s)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_bound {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s : V) : lh s ≤ 2 * s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.lhDef : Σ₀.Semisentence 2

The lh Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded₁Lh {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Bounded₁ lh

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) : ∃ (y : V), ⟪x, y⟫ ∈ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.nth_exists_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) : ∃! y : V, ⟪x, y⟫ ∈ s

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.nth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) : V

The nth construction in FFL.FirstOrder.Arithmetic.Seq.

Equations

• h.nth hx = PointwiseComposition.Classical.chooseUnique ⋯

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.nth_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) : ⟪x, h.nth hx⟫ ∈ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.nth_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x y : V} (hx : x < lh s) (hy : ⟪x, y⟫ ∈ s) : y = h.nth hx

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.nth_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {x : V} (hx : x < lh s) : h.nth hx < s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lh_eq_of {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (H : Seq s) {l : V} (h : domain s = under l) : lh s = l

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lt_lh_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {i : V} : i < lh s ↔ i ∈ domain s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lt_lh_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) {i x : V} (hix : ⟪i, x⟫ ∈ s) : i < lh s

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

The seq Cons construction in FFL.FirstOrder.Arithmetic.

Equations

• s ⁀' x = insert ⟪PointwiseComposition.FFL.FirstOrder.Arithmetic.lh s, x⟫ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.znth_existsUnique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s i : V) : ∃! x : V, (Seq s ∧ i < lh s → ⟪i, x⟫ ∈ s) ∧ (¬(Seq s ∧ i < lh s) → x = 0)

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

The znth construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.znth s i = PointwiseComposition.Classical.chooseUnique ⋯

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.znth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s i : V} (h : Seq s) (hi : i < lh s) : ⟪i, znth s i⟫ ∈ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.znth_eq_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x s i : V} (h : Seq s) (hi : ⟪i, x⟫ ∈ s) : znth s i = x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.znth_prop_not {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s i : V} (h : ¬Seq s ∨ lh s ≤ i) : znth s i = 0

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

The znth Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

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

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.seq_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Seq ∅

@[simp]

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.isempty_of_lh_eq_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (Hs : Seq s) (h : lh s = 0) : s = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.subset_seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s x : V) : s ⊆ s ⁀' x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lt_seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (hs : Seq s) (x : V) : s < s ⁀' x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.mem_seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s x : V) : ⟪lh s, x⟫ ∈ s ⁀' x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (h : Seq s) (x : V) : Seq (s ⁀' x)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lh_seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) {s : V} (h : Seq s) : lh (s ⁀' x) = lh s + 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_seqCons_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {i x z s : V} : ⟪i, x⟫ ∈ s ⁀' z ↔ i = lh s ∧ x = z ∨ ⟪i, x⟫ ∈ s

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_mem_seqCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s z : V) : ⟪lh s, z⟫ ∈ s ⁀' z

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_mem_seqCons_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s x z : V} (H : Seq s) : ⟪lh s, x⟫ ∈ s ⁀' z ↔ x = z

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.mem_seqCons_iff_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {i s x z : V} (hi : i < lh s) : ⟪i, x⟫ ∈ s ⁀' z ↔ ⟪i, x⟫ ∈ s

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_not_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (Ss : Seq s) (x : V) : ⟪lh s, x⟫ ∉ s

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.seqCons_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (t x s : V) : t = s ⁀' x ↔ ∃ l ≤ 2 * s, l = lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ t = insert p s

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

The seq Cons Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

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

@[simp]

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.restr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (H : Seq s) {i : V} (hi : i ≤ lh s) : Seq (Arithmetic.restr s (under i))

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.restr_lh {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} (H : Seq s) {i : V} (hi : i ≤ lh s) : lh (Arithmetic.restr s (under i)) = i

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.domain_bitRemove_of_isMapping_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x y s : V} (hs : IsMapping s) (hxy : ⟪x, y⟫ ∈ s) : domain (bitRemove ⟪x, y⟫ s) = bitRemove x (domain s)

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.eq_of_eq_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) (hl : lh s₁ = lh s₂) (h : s₁ ⊆ s₂) : s₁ = s₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.subset_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s t : V} (h : ∀ (i x : V), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t) : s ⊆ t

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.lh_ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) (h : lh s₁ = lh s₂) (H : ∀ (i x₁ x₂ : V), ⟪i, x₁⟫ ∈ s₁ → ⟪i, x₂⟫ ∈ s₂ → x₁ = x₂) : s₁ = s₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.seqCons_ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {a₁ a₂ s₁ s₂ : V} (H₁ : Seq s₁) (H₂ : Seq s₂) : s₁ ⁀' a₁ = s₂ ⁀' a₂ ↔ a₁ = a₂ ∧ s₁ = s₂

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.ne_zero_iff_one_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {a : V} : a ≠ 0 ↔ 1 ≤ a

TODO: move to Lemmata.lean

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.cases_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} : Seq s ↔ s = ∅ ∨ ∃ (x : V) (s' : V), Seq s' ∧ s = s' ⁀' x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.cases {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {s : V} : Seq s → s = ∅ ∨ ∃ (x : V) (s' : V), Seq s' ∧ s = s' ⁀' x

Alias of the forward direction of PointwiseComposition.FFL.FirstOrder.Arithmetic.Seq.cases_iff.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.seq_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hnil : P ∅) (hcons : ∀ (s x : V), Seq s → P s → P (s ⁀' x)) {s : V} : Seq s → P s

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term!⟦_⟧» : Lean.ParserDescr

!⟦x, y, z, ...⟧ notation for Seq

Equations

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

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

The vec Cons Unexpander construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.singleton_seq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) : Seq !⟦x⟧

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.doubleton_seq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : Seq !⟦x, y⟧

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_singleton_seq_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : ⟪0, x⟫ ∈ !⟦y⟧ ↔ x = y

def PointwiseComposition.FFL.FirstOrder.Arithmetic.binaryGraphAtZero (φ : Σ₀.Semisentence 3) : Σ₀.Semisentence 2

Fix the first input of a binary graph to zero, retaining its output variable.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eval_binaryGraphAtZero {V : Type u_1} [ORingStructure V] (φ : Σ₀.Semisentence 3) (v : Fin 2 → V) : (Semiformula.Evalb v) ↑(binaryGraphAtZero φ) ↔ (Semiformula.Evalb ![v 0, 0, v 1]) ↑φ

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

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

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.mkSeq₁Def = PointwiseComposition.FFL.FirstOrder.Arithmetic.binaryGraphAtZero PointwiseComposition.FFL.FirstOrder.Arithmetic.seqConsDef

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

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

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

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

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

Equations

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

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

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigmaOne_skolem_seq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {R : V → V → Prop} (hP : Σ₁-Relation R) {l : V} (H : ∀ x < l, ∃ (y : V), R x y) : ∃ (s : V), Seq s ∧ lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigmaOne_skolem_seqProof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {R : V → V → Prop} (hP : Σ₁-Relation R) {l : V} (H : ∀ x < l, ∃! y : V, R x y) : ∃! s : V, Seq s ∧ lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : ℕ} : (Fin n → V) → V

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

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq x_2 = ∅
• PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq v = (PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq fun (x : Fin n) => v x.castSucc) ⁀' v (Fin.last n)

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq_vecCons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : ℕ} (v : Fin n → V) (a : V) : vecToSeq (v <: a) = vecToSeq v ⁀' a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.vecToSeq_seq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : ℕ} (v : Fin n → V) : Seq (vecToSeq v)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lh_vecToSeq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : ℕ} (v : Fin n → V) : lh (vecToSeq v) = ↑n

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_vectoSeq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {n : ℕ} (v : Fin n → V) (i : Fin n) : ⟪↑↑i, v i⟫ ∈ vecToSeq v