noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqBvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (z : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqBvar z = ⟪0, z⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqFvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqFvar x = ⟪1, x⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (k f v : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc k f v = ⟪2, ⟪k, ⟪f, v⟫⟫⟫ + 1

def LO.FirstOrder.Arithmetic.Bootstrapping.qqFuncN (k f v : ℕ) : ℕ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqFuncN k f v = Nat.pair 2 (Nat.pair k (Nat.pair f v)) + 1

def LO.FirstOrder.Arithmetic.Bootstrapping.«term^#_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.«term^&_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.«term^func_» : Lean.ParserDescr

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqFuncN_eq_qqFunc (k f v : ℕ) : qqFuncN k f v = qqFunc k f v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.var_lt_qqBvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (z : V) : z < qqBvar z

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.var_lt_qqFvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : x < qqFvar x

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.arity_lt_qqFunc {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (k f v : V) : k < qqFunc k f v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.func_lt_qqFunc {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (k f v : V) : f < qqFunc k f v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.terms_lt_qqFunc {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (k f v : V) : v < qqFunc k f v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_lt_qqFunc_of_lt {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {i k f v : V} (hi : i < len v) : nth v i < qqFunc k f v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqBvar_inj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {z z' : V} : qqBvar z = qqBvar z' ↔ z = z'

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqFvar_inj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {x x' : V} : qqFvar x = qqFvar x' ↔ x = x'

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc_inj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k f v k' f' w : V} : qqFunc k f v = qqFunc k' f' w ↔ k = k' ∧ f = f' ∧ v = w

def LO.FirstOrder.Arithmetic.qqBvarDef : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqBvar_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₁ qqBvar via qqBvarDef

def LO.FirstOrder.Arithmetic.qqFvarDef : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqFvar_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₁ qqFvar via qqFvarDef

def LO.FirstOrder.Arithmetic.qqFuncDef : 𝚺₀.Semisentence 4

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqFunc_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₃ qqFunc via qqFuncDef

def LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.Phi {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (C : Set V) (t : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : Fixpoint.Blueprint 0

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : Fixpoint.Construction V (blueprint L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.construction L = { Φ := fun (x : Fin 0 → V) => LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.Phi L, defined := ⋯, monotone := ⋯ }

instance LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.instStrongFiniteConstruction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : Fixpoint.Construction.StrongFinite V (construction L)

def LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : V → Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm L = (LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.construction L).Fixpoint ![]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isUTerm (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 1

Note: noncomputable attribute to prohibit compilation of a large term. This is necessary for Zoo and integration with Verso.

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.isUTerm L = (LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedTerm.blueprint L).fixpointDefΔ₁

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Predicate IsUTerm L via isUTerm L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Predicate IsUTerm L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Predicate IsUTerm L

def LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (n w : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec L n w = (n = LO.FirstOrder.Arithmetic.len w ∧ ∀ i < n, LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm L (LO.FirstOrder.Arithmetic.nth w i))

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isUTermVec (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 2

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.lh {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n w : V} (h : IsUTermVec L n w) : n = len w

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.nth {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n w : V} (h : IsUTermVec L n w) {i : V} : i < n → IsUTerm L (Arithmetic.nth w i)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : IsUTermVec L 0 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.empty_iff {L : Language} [L.Encodable] [L.LORDefinable] {v : ℕ} : IsUTermVec L 0 v ↔ v = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.two_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {v : V} : IsUTermVec L 2 v ↔ ∃ (t₁ : V) (t₂ : V), IsUTerm L t₁ ∧ IsUTerm L t₂ ∧ v = ?[t₁, t₂]

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.adjoin {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n w t : V} (h : IsUTermVec L n w) (ht : IsUTerm L t) : IsUTermVec L (n + 1) (Adjoin.adjoin t w)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.adjoin₁_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} : IsUTermVec L 1 ?[t] ↔ IsUTerm L t

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.mkSeq₂_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t₁ t₂ : V} : IsUTermVec L 2 ?[t₁, t₂] ↔ IsUTerm L t₁ ∧ IsUTerm L t₂

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation IsUTermVec L via isUTermVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation IsUTermVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} (Γ : SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Relation IsUTermVec L

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.case_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} : IsUTerm L t ↔ (∃ (z : V), t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsUTermVec L k v ∧ t = qqFunc k f v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.case {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} : IsUTerm L t → (∃ (z : V), t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsUTermVec L k v ∧ t = qqFunc k f v

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.case_iff.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.mk {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} : ((∃ (z : V), t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsUTermVec L k v ∧ t = qqFunc k f v) → IsUTerm L t

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.case_iff.

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {z : V} : IsUTerm L (qqBvar z)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (x : V) : IsUTerm L (qqFvar x)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.func_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k f v : V} : IsUTerm L (qqFunc k f v) ↔ L.IsFunc k f ∧ IsUTermVec L k v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) : IsUTerm L (qqFunc k f v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.induction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hbvar : ∀ (z : V), P (qqBvar z)) (hfvar : ∀ (x : V), P (qqFvar x)) (hfunc : ∀ (k f v : V), L.IsFunc k f → IsUTermVec L k v → (∀ i < k, P (nth v i)) → P (qqFunc k f v)) (t : V) : IsUTerm L t → P t

structure LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint (arity : ℕ) : Type

• bvar : 𝚺₁.Semisentence (arity + 2)
• fvar : 𝚺₁.Semisentence (arity + 2)
• func : 𝚺₁.Semisentence (arity + 5)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.blueprint {arity : ℕ} (L : Language) [L.Encodable] [L.LORDefinable] (β : Blueprint arity) : Fixpoint.Blueprint arity

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.graph {arity : ℕ} (L : Language) [L.Encodable] [L.LORDefinable] (β : Blueprint arity) : 𝚺₁.Semisentence (arity + 2)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.result {arity : ℕ} (L : Language) [L.Encodable] [L.LORDefinable] (β : Blueprint arity) : 𝚺₁.Semisentence (arity + 2)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.resultVec {arity : ℕ} (L : Language) [L.Encodable] [L.LORDefinable] (β : Blueprint arity) : 𝚺₁.Semisentence (arity + 3)

Equations

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

structure LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction (V : Type u_1) [ORingStructure V] {k : ℕ} (φ : Blueprint k) : Type u_1

• bvar : (Fin k → V) → V → V
• fvar : (Fin k → V) → V → V
• func : (Fin k → V) → V → V → V → V → V
• bvar_defined : HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => self.bvar (fun (x : Fin k) => v x.succ) (v 0)) φ.bvar
• fvar_defined : HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => self.fvar (fun (x : Fin k) => v x.succ) (v 0)) φ.fvar
• func_defined : HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1 + 1 + 1 + 1) → V) => self.func (fun (x : Fin k) => v x.succ.succ.succ.succ) (v 0) (v 1) (v 2) (v 3)) φ.func

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.Phi {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (C : Set V) (pr : V) : Prop

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.seq_bound {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k s m : V} (Ss : Seq s) (hk : k = lh s) (hs : ∀ (i z : V), ⟪i, z⟫ ∈ s → z < m) : s < Exp.exp ((k + m + 1) ^ 2)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.cons_app_9 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 9 = s 8

TODO: move

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.cons_app_10 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 10 = s 9

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.cons_app_11 {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 11 = s 10

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction V (Blueprint.blueprint L β)

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.instFiniteConstruction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : Fixpoint.Construction.Finite V (construction L c)

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.Graph {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (x y : V) : Prop

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.Graph.case_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} {t y : V} : Graph L c param t y ↔ IsUTerm L t ∧ ((∃ (z : V), t = qqBvar z ∧ y = c.bvar param z) ∨ (∃ (x : V), t = qqFvar x ∧ y = c.fvar param x) ∨ ∃ (k : V) (f : V) (v : V) (w : V), (k = len w ∧ ∀ i < k, Graph L c param (nth v i) (nth w i)) ∧ t = qqFunc k f v ∧ y = c.func param k f v w)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : HierarchySymbol.Defined (fun (v : Fin (arity + 1 + 1) → V) => Graph L c (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)) (Blueprint.graph L β)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.eval_graphDef {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2) → V) : V ⊧/v ↑(Blueprint.graph L β) ↔ Graph L c (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)

instance LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : 𝚺₁.Definable fun (v : Fin (arity + 1 + 1) → V) => Graph L c (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)

instance LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_definable₂ {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : { Γ := 𝚺, rank := 0 + 1 }-Relation Graph L c param

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_dom_isUTerm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {t y : V} : Graph L c param t y → IsUTerm L t

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_bvar_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {y z : V} : Graph L c param (qqBvar z) y ↔ y = c.bvar param z

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_fvar_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {y : V} (x : V) : Graph L c param (qqFvar x) y ↔ y = c.fvar param x

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {k f v w : V} (hkr : L.IsFunc k f) (hv : IsUTermVec L k v) (hkw : k = len w) (hw : ∀ i < k, Graph L c param (nth v i) (nth w i)) : Graph L c param (qqFunc k f v) (c.func param k f v w)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_func_inv {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {k f v y : V} : Graph L c param (qqFunc k f v) y → ∃ (w : V), (k = len w ∧ ∀ i < k, Graph L c param (nth v i) (nth w i)) ∧ y = c.func param k f v w

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_exists {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} (param : Fin arity → V) {t : V} : IsUTerm L t → ∃ (y : V), Graph L c param t y

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_unique {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} (param : Fin arity → V) {t y₁ y₂ : V} : Graph L c param t y₁ → Graph L c param t y₂ → y₁ = y₂

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_existsUnique {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {t : V} (ht : IsUTerm L t) : ∃! y : V, Graph L c param t y

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_existsUnique_total {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (t : V) : ∃! y : V, (IsUTerm L t → Graph L c param t y) ∧ (¬IsUTerm L t → y = 0)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (t : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result L c param t = Classical.choose! ⋯

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_prop {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {t : V} (ht : IsUTerm L t) : Graph L c param t (result L c param t)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_prop_not {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {t : V} (ht : ¬IsUTerm L t) : result L c param t = 0

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_eq_of_graph {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} {t y : V} (ht : IsUTerm L t) (h : Graph L c param t y) : result L c param t = y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} (z : V) : result L c param (qqBvar z) = c.bvar param z

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} (x : V) : result L c param (qqFvar x) = c.fvar param x

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} {k f v w : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) (hkw : k = len w) (hw : ∀ i < k, result L c param (nth v i) = nth w i) : result L c param (qqFunc k f v) = c.func param k f v w

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_existsUnique_vec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} {c : Construction V β} {param : Fin arity → V} {k w : V} (hw : IsUTermVec L k w) : ∃! w' : V, k = len w' ∧ ∀ i < k, Graph L c param (nth w i) (nth w' i)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_existsUnique_vec_total {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (k w : V) : ∃! w' : V, (IsUTermVec L k w → k = len w' ∧ ∀ i < k, Graph L c param (nth w i) (nth w' i)) ∧ (¬IsUTermVec L k w → w' = 0)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) (k w : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec L c param k w = Classical.choose! ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec_lh {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {k w : V} (hw : IsUTermVec L k w) : len (resultVec L c param k w) = k

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.graph_of_mem_resultVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {k w : V} (hw : IsUTermVec L k w) {i : V} (hi : i < k) : Graph L c param (nth w i) (nth (resultVec L c param k w) i)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.nth_resultVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {k w i : V} (hw : IsUTermVec L k w) (hi : i < k) : nth (resultVec L c param k w) i = result L c param (nth w i)

@[simp]

def LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec_of_not {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {k w : V} (hw : ¬IsUTermVec L k w) : resultVec L c param k w = 0

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec_nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) : resultVec L c param 0 0 = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec_cons {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (param : Fin arity → V) {k w t : V} (hw : IsUTermVec L k w) (ht : IsUTerm L t) : resultVec L c param (k + 1) (adjoin t w) = adjoin (result L c param t) (resultVec L c param k w)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_func' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) {param : Fin arity → V} {k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) : result L c param (qqFunc k f v) = c.func param k f v (resultVec L c param k v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1) → V) => result L c (fun (x : Fin arity) => v x.succ) (v 0)) (Blueprint.result L β)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.result_graphDef {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 2) → V) : V ⊧/v ↑(Blueprint.result L β) ↔ v 0 = result L c (fun (x : Fin arity) => v x.succ.succ) (v 1)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.resultVec_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) : HierarchySymbol.DefinedFunction (fun (v : Fin (arity + 1 + 1) → V) => resultVec L c (fun (x : Fin arity) => v x.succ.succ) (v 0) (v 1)) (Blueprint.resultVec L β)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Construction.eval_resultVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {arity : ℕ} {β : Blueprint arity} (c : Construction V β) (v : Fin (arity + 3) → V) : V ⊧/v ↑(Blueprint.resultVec L β) ↔ v 0 = resultVec L c (fun (x : Fin arity) => v x.succ.succ.succ) (v 1) (v 2)

def LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.BV.blueprint : Language.TermRec.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.BV.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : Language.TermRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBV {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBVGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.termBVGraph L = LO.FirstOrder.Arithmetic.Bootstrapping.Language.TermRec.Blueprint.result L LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.BV.blueprint

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.termBVVecGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBV_bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (z : V) : termBV L (qqBvar z) = z + 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBV_fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (x : V) : termBV L (qqFvar x) = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBV_func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k f v : V} (hkf : L.IsFunc k f) (hv : IsUTermVec L k v) : termBV L (qqFunc k f v) = listMax (termBVVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_termBVVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) : len (termBVVec L k v) = k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_termBVVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (hv : IsUTermVec L k v) {i : V} (hi : i < k) : nth (termBVVec L k v) i = termBV L (nth v i)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec_nil {L : Language} [L.Encodable] [L.LORDefinable] : termBVVec L 0 0 = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec_cons {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k t ts : V} (ht : IsUTerm L t) (hts : IsUTermVec L k ts) : termBVVec L (k + 1) (adjoin t ts) = adjoin (termBV L t) (termBVVec L k ts)

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBV.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termBV L via termBVGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBV.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ termBV L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBV.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {k : ℕ} : { Γ := Γ, rank := k + 1 }-Function₁ termBV L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termBVVec L via termBVVecGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ termBVVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.termBVVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {i : ℕ} : { Γ := Γ, rank := i + 1 }-Function₂ termBVVec L

class LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (n t : V) : Prop

• isUTerm : IsUTerm L t
• bv : termBV L t ≤ n

class LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k n v : V) : Prop

• isUTermVec : IsUTermVec L k v
• bv {i : V} : i < k → termBV L (Arithmetic.nth v i) ≤ n

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isSemiterm (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 2

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isSemitermVec (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 3

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.Bootstrapping.IsTerm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (t : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsTerm L t = LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm L 0 t

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.Bootstrapping.IsTermVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (k v : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsTermVec L k v = LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec L k 0 v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.def {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} : IsSemiterm L n t ↔ IsUTerm L t ∧ termBV L t ≤ n

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.def {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} : IsSemitermVec L k n v ↔ IsUTermVec L k v ∧ ∀ i < k, termBV L (Arithmetic.nth v i) ≤ n

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.isUTerm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} (h : IsSemitermVec L k n v) : IsUTermVec L k v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.lh {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} (h : IsSemitermVec L k n v) : len v = k

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.nth {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} (h : IsSemitermVec L k n v) {i : V} (hi : i < k) : IsSemiterm L n (Arithmetic.nth v i)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTerm.isSemiterm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {t : V} (h : IsUTerm L t) : IsSemiterm L (termBV L t) t

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUTermVec.isSemitermVec {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k v : V} (h : IsUTermVec L k v) : IsSemitermVec L k (listMax (termBVVec L k v)) v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n v : V} : IsSemitermVec L k n v ↔ len v = k ∧ ∀ i < k, IsSemiterm L n (Arithmetic.nth v i)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.bvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n z : V} : IsSemiterm L n (qqBvar z) ↔ z < n

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.fvar {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (n x : V) : IsSemiterm L n (qqFvar x)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.func {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k f v : V} : IsSemiterm L n (qqFunc k f v) ↔ L.IsFunc k f ∧ IsSemitermVec L k n v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (n : V) : IsSemitermVec L 0 n 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.empty_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {v n : V} : IsSemitermVec L 0 n v ↔ v = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.cons_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n w t : V} : IsSemitermVec L (k + 1) n (Adjoin.adjoin t w) ↔ IsSemiterm L n t ∧ IsSemitermVec L k n w

theorem LO.FirstOrder.Arithmetic.Bootstrapping.SemitermVec.adjoin {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m w t : V} (h : IsSemitermVec L n m w) (ht : IsSemiterm L m t) : IsSemitermVec L (n + 1) m (Adjoin.adjoin t w)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.singleton {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} : IsSemitermVec L 1 n ?[t] ↔ IsSemiterm L n t

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.doubleton {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t₁ t₂ : V} : IsSemitermVec L 2 n ?[t₁, t₂] ↔ IsSemiterm L n t₁ ∧ IsSemiterm L n t₂

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation IsSemiterm L via isSemiterm L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation IsSemiterm L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation IsSemiterm L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation₃ IsSemitermVec L via isSemitermVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Relation₃ IsSemitermVec L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Relation₃ IsSemitermVec L

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.case_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} : IsSemiterm L n t ↔ (∃ z < n, t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsSemitermVec L k n v ∧ t = qqFunc k f v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.case {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} : IsSemiterm L n t → (∃ z < n, t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsSemitermVec L k n v ∧ t = qqFunc k f v

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.case_iff.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.mk' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t : V} : ((∃ z < n, t = qqBvar z) ∨ (∃ (x : V), t = qqFvar x) ∨ ∃ (k : V) (f : V) (v : V), L.IsFunc k f ∧ IsSemitermVec L k n v ∧ t = qqFunc k f v) → IsSemiterm L n t

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.case_iff.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.induction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hbvar : ∀ z < n, P (qqBvar z)) (hfvar : ∀ (x : V), P (qqFvar x)) (hfunc : ∀ (k f v : V), L.IsFunc k f → IsSemitermVec L k n v → (∀ i < k, P (nth v i)) → P (qqFunc k f v)) (t : V) : IsSemiterm L n t → P t

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.nil {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (k : V) : IsSemitermVec L 0 k 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemitermVec.adjoin {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k n w t : V} (h : IsSemitermVec L n k w) (ht : IsSemiterm L k t) : IsSemitermVec L (n + 1) k (Adjoin.adjoin t w)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.sigma1_induction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} {P : V → Prop} (hP : 𝚺₁-Predicate P) (hbvar : ∀ z < n, P (qqBvar z)) (hfvar : ∀ (x : V), P (qqFvar x)) (hfunc : ∀ (k f v : V), L.IsFunc k f → IsSemitermVec L k n v → (∀ i < k, P (nth v i)) → P (qqFunc k f v)) (t : V) : IsSemiterm L n t → P t