Sequence

def LO.Arith.Seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : Prop

Equations

• LO.Arith.Seq s = (LO.Arith.IsMapping s ∧ ∃ (l : V), LO.Arith.domain s = LO.Arith.under l)

Instances For

• LO.Arith.seq_definable
• LO.Arith.seq_definable'

def LO.Arith.Seq.isMapping {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) : LO.Arith.IsMapping s

Equations

• ⋯ = ⋯

def LO.FirstOrder.Arith.seqDef : 𝚺₀.Semisentence 1

Equations

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

theorem LO.Arith.seq_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Predicate LO.Arith.Seq via LO.FirstOrder.Arith.seqDef

@[simp]

theorem LO.Arith.seq_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 1 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.seqDef) ↔ LO.Arith.Seq (v 0)

instance LO.Arith.seq_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Predicate LO.Arith.Seq

Equations

• ⋯ = ⋯

instance LO.Arith.seq_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Predicate LO.Arith.Seq

Equations

• ⋯ = ⋯

def LO.Arith.«first_order_formula:Seq_» : Lean.ParserDescr

Equations

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

theorem LO.Arith.lh_exists_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∃! l : V, (LO.Arith.Seq s → LO.Arith.domain s = LO.Arith.under l) ∧ (¬LO.Arith.Seq s → l = 0)

def LO.Arith.lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• LO.Arith.lh s = Classical.choose! ⋯

Instances For

• LO.Arith.instBounded₁Lh
• LO.Arith.lh_definable
• LO.Arith.lh_definable'

theorem LO.Arith.lh_prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : (LO.Arith.Seq s → LO.Arith.domain s = LO.Arith.under (LO.Arith.lh s)) ∧ (¬LO.Arith.Seq s → LO.Arith.lh s = 0)

theorem LO.Arith.lh_prop_of_not_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : ¬LO.Arith.Seq s) : LO.Arith.lh s = 0

theorem LO.Arith.Seq.domain_eq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) : LO.Arith.domain s = LO.Arith.under (LO.Arith.lh s)

@[simp]

theorem LO.Arith.lh_bound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : LO.Arith.lh s ≤ 2 * s

def LO.FirstOrder.Arith.lhDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.lh_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.lh via LO.FirstOrder.Arith.lhDef

@[simp]

theorem LO.Arith.lh_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.lhDef) ↔ v 0 = LO.Arith.lh (v 1)

instance LO.Arith.lh_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.lh

Equations

• ⋯ = ⋯

instance LO.Arith.lh_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ LO.Arith.lh

Equations

• ⋯ = ⋯

instance LO.Arith.instBounded₁Lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.FirstOrder.Arith.Bounded₁ LO.Arith.lh

Equations

• ⋯ = ⋯

theorem LO.Arith.Seq.exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) : ∃ (y : V), ⟪x, y⟫ ∈ s

theorem LO.Arith.Seq.nth_exists_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) : ∃! y : V, ⟪x, y⟫ ∈ s

def LO.Arith.Seq.nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) : V

Equations

• h.nth hx = Classical.choose! ⋯

@[simp]

theorem LO.Arith.Seq.nth_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) : ⟪x, h.nth hx⟫ ∈ s

theorem LO.Arith.Seq.nth_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} {y : V} (hx : x < LO.Arith.lh s) (hy : ⟪x, y⟫ ∈ s) : y = h.nth hx

@[simp]

theorem LO.Arith.Seq.nth_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {x : V} (hx : x < LO.Arith.lh s) : h.nth hx < s

theorem LO.Arith.Seq.lh_eq_of {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : LO.Arith.Seq s) {l : V} (h : LO.Arith.domain s = LO.Arith.under l) : LO.Arith.lh s = l

theorem LO.Arith.Seq.lt_lh_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {i : V} : i < LO.Arith.lh s ↔ i ∈ LO.Arith.domain s

theorem LO.Arith.Seq.lt_lh_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) {i : V} {x : V} (hix : ⟪i, x⟫ ∈ s) : i < LO.Arith.lh s

def LO.Arith.seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) : V

Equations

• s ⁀' x = insert ⟪LO.Arith.lh s, x⟫ s

Instances For

• LO.Arith.seqCons_definable
• LO.Arith.seqCons_definable'

def LO.Arith.znth_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (i : V) : ∃! x : V, (LO.Arith.Seq s ∧ i < LO.Arith.lh s → ⟪i, x⟫ ∈ s) ∧ (¬(LO.Arith.Seq s ∧ i < LO.Arith.lh s) → x = 0)

Equations

• ⋯ = ⋯

def LO.Arith.znth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (i : V) : V

Equations

• LO.Arith.znth s i = Classical.choose! ⋯

Instances For

• LO.Arith.znth_definable
• LO.Arith.znth_definable'

theorem LO.Arith.Seq.znth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {i : V} (h : LO.Arith.Seq s) (hi : i < LO.Arith.lh s) : ⟪i, LO.Arith.znth s i⟫ ∈ s

theorem LO.Arith.Seq.znth_eq_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {s : V} {i : V} (h : LO.Arith.Seq s) (hi : ⟪i, x⟫ ∈ s) : LO.Arith.znth s i = x

theorem LO.Arith.znth_prop_not {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {i : V} (h : ¬LO.Arith.Seq s ∨ LO.Arith.lh s ≤ i) : LO.Arith.znth s i = 0

def LO.FirstOrder.Arith.znthDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.znth_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.znth via LO.FirstOrder.Arith.znthDef

@[simp]

theorem LO.Arith.eval_znthDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.znthDef) ↔ v 0 = LO.Arith.znth (v 1) (v 2)

instance LO.Arith.znth_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.znth

Equations

• ⋯ = ⋯

instance LO.Arith.znth_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ LO.Arith.znth

Equations

• ⋯ = ⋯

def LO.Arith.«term_⁀'_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_⁀'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_⁀'_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁀' ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem LO.Arith.seq_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.Seq ∅

@[simp]

theorem LO.Arith.lh_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.lh ∅ = 0

theorem LO.Arith.Seq.isempty_of_lh_eq_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (Hs : LO.Arith.Seq s) (h : LO.Arith.lh s = 0) : s = ∅

@[simp]

theorem LO.Arith.Seq.subset_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) : s ⊆ s ⁀' x

theorem LO.Arith.Seq.lt_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (hs : LO.Arith.Seq s) (x : V) : s < s ⁀' x

@[simp]

theorem LO.Arith.Seq.mem_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (x : V) : ⟪LO.Arith.lh s, x⟫ ∈ s ⁀' x

theorem LO.Arith.Seq.seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (h : LO.Arith.Seq s) (x : V) : LO.Arith.Seq (s ⁀' x)

@[simp]

theorem LO.Arith.Seq.lh_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) {s : V} (h : LO.Arith.Seq s) : LO.Arith.lh (s ⁀' x) = LO.Arith.lh s + 1

theorem LO.Arith.mem_seqCons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {x : V} {z : V} {s : V} : ⟪i, x⟫ ∈ s ⁀' z ↔ i = LO.Arith.lh s ∧ x = z ∨ ⟪i, x⟫ ∈ s

@[simp]

theorem LO.Arith.lh_mem_seqCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (z : V) : ⟪LO.Arith.lh s, z⟫ ∈ s ⁀' z

@[simp]

theorem LO.Arith.lh_mem_seqCons_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {x : V} {z : V} (H : LO.Arith.Seq s) : ⟪LO.Arith.lh s, x⟫ ∈ s ⁀' z ↔ x = z

theorem LO.Arith.Seq.mem_seqCons_iff_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {s : V} {x : V} {z : V} (hi : i < LO.Arith.lh s) : ⟪i, x⟫ ∈ s ⁀' z ↔ ⟪i, x⟫ ∈ s

@[simp]

theorem LO.Arith.lh_not_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (Ss : LO.Arith.Seq s) (x : V) : ⟪LO.Arith.lh s, x⟫ ∉ s

theorem LO.Arith.seqCons_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (t : V) (x : V) (s : V) : t = s ⁀' x ↔ ∃ l ≤ 2 * s, l = LO.Arith.lh s ∧ ∃ p ≤ (2 * s + x + 1) ^ 2, p = ⟪l, x⟫ ∧ t = insert p s

def LO.FirstOrder.Arith.seqConsDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.seqCons_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.seqCons via LO.FirstOrder.Arith.seqConsDef

@[simp]

theorem LO.Arith.seqCons_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.seqConsDef) ↔ v 0 = v 1 ⁀' v 2

instance LO.Arith.seqCons_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.seqCons

Equations

• ⋯ = ⋯

instance LO.Arith.seqCons_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ LO.Arith.seqCons

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.natCast_empty {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ↑∅ = ∅

theorem LO.Arith.seqCons_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : ℕ) (a : ℕ) : ↑(s ⁀' a) = ↑s ⁀' ↑a

theorem LO.Arith.Seq.restr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : LO.Arith.Seq s) {i : V} (hi : i ≤ LO.Arith.lh s) : LO.Arith.Seq (LO.Arith.restr s (LO.Arith.under i))

theorem LO.Arith.Seq.restr_lh {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} (H : LO.Arith.Seq s) {i : V} (hi : i ≤ LO.Arith.lh s) : LO.Arith.lh (LO.Arith.restr s (LO.Arith.under i)) = i

theorem LO.Arith.domain_bitRemove_of_isMapping_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {s : V} (hs : LO.Arith.IsMapping s) (hxy : ⟪x, y⟫ ∈ s) : LO.Arith.domain (LO.Arith.bitRemove ⟪x, y⟫ s) = LO.Arith.bitRemove x (LO.Arith.domain s)

theorem LO.Arith.Seq.eq_of_eq_of_subset {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) (hl : LO.Arith.lh s₁ = LO.Arith.lh s₂) (h : s₁ ⊆ s₂) : s₁ = s₂

theorem LO.Arith.subset_pair {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} {t : V} (h : ∀ (i x : V), ⟪i, x⟫ ∈ s → ⟪i, x⟫ ∈ t) : s ⊆ t

theorem LO.Arith.Seq.lh_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) (h : LO.Arith.lh s₁ = LO.Arith.lh s₂) (H : ∀ (i x₁ x₂ : V), ⟪i, x₁⟫ ∈ s₁ → ⟪i, x₂⟫ ∈ s₂ → x₁ = x₂) : s₁ = s₂

@[simp]

theorem LO.Arith.Seq.seqCons_ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a₁ : V} {a₂ : V} {s₁ : V} {s₂ : V} (H₁ : LO.Arith.Seq s₁) (H₂ : LO.Arith.Seq s₂) : s₁ ⁀' a₁ = s₂ ⁀' a₂ ↔ a₁ = a₂ ∧ s₁ = s₂

theorem LO.Arith.ne_zero_iff_one_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} : a ≠ 0 ↔ 1 ≤ a

TODO: move to Lemmata.lean

theorem LO.Arith.Seq.cases_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : LO.Arith.Seq s ↔ s = ∅ ∨ ∃ (x : V) (s' : V), LO.Arith.Seq s' ∧ s = s' ⁀' x

theorem LO.Arith.Seq.cases {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : LO.Arith.Seq s → s = ∅ ∨ ∃ (x : V) (s' : V), LO.Arith.Seq s' ∧ s = s' ⁀' x

Alias of the forward direction of LO.Arith.Seq.cases_iff.

theorem LO.Arith.seq_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hnil : P ∅) (hcons : ∀ (s x : V), LO.Arith.Seq s → P s → P (s ⁀' x)) {s : V} : LO.Arith.Seq s → P s

def LO.Arith.«term!⟦_⟧» : Lean.ParserDescr

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

Equations

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

def LO.Arith.vecConsUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem LO.Arith.singleton_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : LO.Arith.Seq !⟦x⟧

@[simp]

theorem LO.Arith.doubleton_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : LO.Arith.Seq !⟦x, y⟧

@[simp]

theorem LO.Arith.mem_singleton_seq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) (y : V) : ⟪0, x⟫ ∈ !⟦y⟧ ↔ x = y

def LO.FirstOrder.Arith.mkSeq₁Def : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.mkSeq₁_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => !⟦x⟧ via LO.FirstOrder.Arith.mkSeq₁Def

@[simp]

theorem LO.Arith.eval_mkSeq₁Def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.mkSeq₁Def) ↔ v 0 = !⟦v 1⟧

instance LO.Arith.mkSeq₁_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ fun (x : V) => !⟦x⟧

Equations

• ⋯ = ⋯

instance LO.Arith.mkSeq₁_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Function₁ fun (x : V) => !⟦x⟧

Equations

• ⋯ = ⋯

def LO.FirstOrder.Arith.mkSeq₂Def : 𝚺₁.Semisentence 3

Equations

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

theorem LO.Arith.mkSeq₂_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧ via LO.FirstOrder.Arith.mkSeq₂Def

@[simp]

theorem LO.Arith.eval_mkSeq₂Def {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.mkSeq₂Def) ↔ v 0 = !⟦v 1, v 2⟧

instance LO.Arith.mkSeq₂_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ fun (x y : V) => !⟦x, y⟧

Equations

• ⋯ = ⋯

instance LO.Arith.mkSeq₂_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => !⟦x, y⟧

Equations

• ⋯ = ⋯

theorem LO.Arith.sigmaOne_skolem_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {l : V} (H : ∀ x < l, ∃ (y : V), R x y) : ∃ (s : V), LO.Arith.Seq s ∧ LO.Arith.lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x

theorem LO.Arith.sigmaOne_skolem_seq! {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {R : V → V → Prop} (hP : 𝚺₁-Relation R) {l : V} (H : ∀ x < l, ∃! y : V, R x y) : ∃! s : V, LO.Arith.Seq s ∧ LO.Arith.lh s = l ∧ ∀ (i x : V), ⟪i, x⟫ ∈ s → R i x

def LO.Arith.vecToSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} : (Fin n → V) → V

Equations

• LO.Arith.vecToSeq x_2 = ∅
• LO.Arith.vecToSeq v = (LO.Arith.vecToSeq fun (x : Fin n) => v x.castSucc) ⁀' v (Fin.last n)

@[simp]

theorem LO.Arith.vecToSeq_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.vecToSeq ![] = ∅

@[simp]

theorem LO.Arith.vecToSeq_vecCons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) (a : V) : LO.Arith.vecToSeq (v <: a) = LO.Arith.vecToSeq v ⁀' a

@[simp]

theorem LO.Arith.vecToSeq_seq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) : LO.Arith.Seq (LO.Arith.vecToSeq v)

@[simp]

theorem LO.Arith.lh_vecToSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) : LO.Arith.lh (LO.Arith.vecToSeq v) = ↑n

theorem LO.Arith.mem_vectoSeq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : ℕ} (v : Fin n → V) (i : Fin n) : ⟪↑↑i, v i⟫ ∈ LO.Arith.vecToSeq v

theorem LO.Arith.order_ball_induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : V → V → V} (hf : 𝚺₁-Function₂ f) {P : V → V → Prop} (hP : 𝚺₁-Relation P) (ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f x y, P x' y') → P x y) (x : V) (y : V) : P x y

theorem LO.Arith.order_ball_induction_sigma1' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {f : V → V} (hf : 𝚺₁-Function₁ f) {P : V → V → Prop} (hP : 𝚺₁-Relation P) (ind : ∀ (x y : V), (∀ x' < x, ∀ y' ≤ f y, P x' y') → P x y) (x : V) (y : V) : P x y

theorem LO.Arith.order_ball_induction₂_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {fy : V → V → V → V} {fz : V → V → V → V} (hfy : 𝚺₁-Function₃ fy) (hfz : 𝚺₁-Function₃ fz) {P : V → V → V → Prop} (hP : 𝚺₁-Relation₃ P) (ind : ∀ (x y z : V), (∀ x' < x, ∀ y' ≤ fy x y z, ∀ z' ≤ fz x y z, P x' y' z') → P x y z) (x : V) (y : V) (z : V) : P x y z

theorem LO.Arith.order_ball_induction₃_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {fy : V → V → V → V → V} {fz : V → V → V → V → V} {fw : V → V → V → V → V} (hfy : 𝚺₁-Function₄ fy) (hfz : 𝚺₁-Function₄ fz) (hfw : 𝚺₁-Function₄ fw) {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P) (ind : ∀ (x y z w : V), (∀ x' < x, ∀ y' ≤ fy x y z w, ∀ z' ≤ fz x y z w, ∀ w' ≤ fw x y z w, P x' y' z' w') → P x y z w) (x : V) (y : V) (z : V) (w : V) : P x y z w