Vec #
Equations
- LO.Arith.«term_∷_» = Lean.ParserDescr.trailingNode `LO.Arith.term_∷_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ ") (Lean.ParserDescr.cat `term 67))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Arith.fstIdx_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.fstIdx (cons x v) = x
@[simp]
theorem
LO.Arith.sndIdx_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.sndIdx (cons x v) = v
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Arith.eval_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.consDef) ↔ v 0 = cons (v 1) (v 2)
Equations
- ⋯ = ⋯
instance
LO.Arith.cons_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ cons
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.mkVec₁_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ fun (x : V) => ?[x] via LO.FirstOrder.Arith.mkVec₁Def
@[simp]
instance
LO.Arith.mkVec₁_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ fun (x : V) => ?[x]
Equations
- ⋯ = ⋯
instance
LO.Arith.mkVec₁_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₁ fun (x : V) => ?[x]
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.mkVec₂_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ fun (x y : V) => ?[x, y] via LO.FirstOrder.Arith.mkVec₂Def
@[simp]
theorem
LO.Arith.eval_mkVec₂Def
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.mkVec₂Def) ↔ v 0 = ?[v 1, v 2]
instance
LO.Arith.mkVec₂_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ fun (x y : V) => ?[x, y]
Equations
- ⋯ = ⋯
instance
LO.Arith.mkVec₂_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ fun (x y : V) => ?[x, y]
Equations
- ⋯ = ⋯
N-th element of List #
Equations
- LO.Arith.Nth.Phi C pr = ((∃ (v : V), pr = ⟪v, ⟪0, LO.Arith.fstIdx v⟫⟫) ∨ ∃ (v : V) (i : V) (x : V), pr = ⟪v, ⟪i + 1, x⟫⟫ ∧ ⟪LO.Arith.sndIdx v, ⟪i, x⟫⟫ ∈ C)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.Arith.Nth.instFiniteConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
LO.Arith.Fixpoint.Construction.Finite V LO.Arith.Nth.construction
Equations
- LO.Arith.Nth.instFiniteConstruction = { finite := ⋯ }
Equations
- LO.Arith.Nth.Graph = LO.Arith.Nth.construction.Fixpoint ![]
Instances For
Equations
- LO.Arith.Nth.graphDef = LO.Arith.Nth.blueprint.fixpointDef
Instances For
theorem
LO.Arith.Nth.graph_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Predicate LO.Arith.Nth.Graph via LO.Arith.Nth.graphDef
instance
LO.Arith.Nth.graph_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Predicate LO.Arith.Nth.Graph
Equations
- ⋯ = ⋯
instance
LO.Arith.Nth.graph_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
{ Γ := 𝚺, rank := 0 + 1 }-Predicate LO.Arith.Nth.Graph
Equations
- ⋯ = ⋯
@[simp]
TODO: move
theorem
LO.Arith.Nth.graph_case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{pr : V}
:
LO.Arith.Nth.Graph pr ↔ (∃ (v : V), pr = ⟪v, ⟪0, LO.Arith.fstIdx v⟫⟫) ∨ ∃ (v : V) (i : V) (x : V), pr = ⟪v, ⟪i + 1, x⟫⟫ ∧ LO.Arith.Nth.Graph ⟪LO.Arith.sndIdx v, ⟪i, x⟫⟫
theorem
LO.Arith.Nth.graph_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{x : V}
:
LO.Arith.Nth.Graph ⟪v, ⟪0, x⟫⟫ ↔ x = LO.Arith.fstIdx v
theorem
LO.Arith.Nth.graph_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
{x : V}
:
LO.Arith.Nth.Graph ⟪v, ⟪i + 1, x⟫⟫ ↔ LO.Arith.Nth.Graph ⟪LO.Arith.sndIdx v, ⟪i, x⟫⟫
theorem
LO.Arith.Nth.graph_exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(i : V)
:
∃ (x : V), LO.Arith.Nth.Graph ⟪v, ⟪i, x⟫⟫
theorem
LO.Arith.Nth.graph_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
{x₁ : V}
{x₂ : V}
:
LO.Arith.Nth.Graph ⟪v, ⟪i, x₁⟫⟫ → LO.Arith.Nth.Graph ⟪v, ⟪i, x₂⟫⟫ → x₁ = x₂
theorem
LO.Arith.Nth.graph_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(i : V)
:
∃! x : V, LO.Arith.Nth.Graph ⟪v, ⟪i, x⟫⟫
Equations
- LO.Arith.nth v i = Classical.choose! ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.nth_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(i : V)
:
LO.Arith.Nth.Graph ⟪v, ⟪i, LO.Arith.nth v i⟫⟫
theorem
LO.Arith.nth_eq_of_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
{x : V}
(h : LO.Arith.Nth.Graph ⟪v, ⟪i, x⟫⟫)
:
LO.Arith.nth v i = x
theorem
LO.Arith.nth_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
:
LO.Arith.nth v 0 = LO.Arith.fstIdx v
theorem
LO.Arith.nth_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(i : V)
:
LO.Arith.nth v (i + 1) = LO.Arith.nth (LO.Arith.sndIdx v) i
@[simp]
theorem
LO.Arith.nth_cons_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.nth (cons x v) 0 = x
@[simp]
theorem
LO.Arith.nth_cons_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
(i : V)
:
LO.Arith.nth (cons x v) (i + 1) = LO.Arith.nth v i
@[simp]
theorem
LO.Arith.nth_cons_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.nth (cons x v) 1 = LO.Arith.nth v 0
@[simp]
theorem
LO.Arith.nth_cons_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.nth (cons x v) 2 = LO.Arith.nth v 1
theorem
LO.Arith.cons_induction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (Cons.cons x v))
(v : V)
:
P v
theorem
LO.Arith.cons_induction_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{P : V → Prop}
(hP : 𝚺₁-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (Cons.cons x v))
(v : V)
:
P v
theorem
LO.Arith.cons_induction_pi1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{P : V → Prop}
(hP : 𝚷₁-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (Cons.cons x v))
(v : V)
:
P v
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.nth_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.nth via LO.FirstOrder.Arith.nthDef
@[simp]
theorem
LO.Arith.eval_nthDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.nthDef) ↔ v 0 = LO.Arith.nth (v 1) (v 2)
instance
LO.Arith.nth_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.nth
Equations
- ⋯ = ⋯
instance
LO.Arith.nth_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.nth
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.nth_zero_idx
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(i : V)
:
LO.Arith.nth 0 i = 0
theorem
LO.Arith.nth_lt_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
(hv : 0 < v)
(i : V)
:
LO.Arith.nth v i < v
@[simp]
theorem
LO.Arith.nth_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(i : V)
:
LO.Arith.nth v i ≤ v
Inductivly Construction of Function on List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- β.graphDef = β.blueprint.fixpointDef
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
LO.Arith.VecRec.Construction
(V : Type u_1)
[LO.ORingStruc V]
{arity : ℕ}
(β : LO.Arith.VecRec.Blueprint arity)
:
Type u_1
- nil : (Fin arity → V) → V
- cons : (Fin arity → V) → V → V → V → V
- nil_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.nil β.nil
- cons_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin arity.succ.succ.succ → V) => self.cons (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2)) β.cons
Instances For
theorem
LO.Arith.VecRec.Construction.nil_defined
{V : Type u_1}
[LO.ORingStruc V]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(self : LO.Arith.VecRec.Construction V β)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.nil β.nil
theorem
LO.Arith.VecRec.Construction.cons_defined
{V : Type u_1}
[LO.ORingStruc V]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(self : LO.Arith.VecRec.Construction V β)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin arity.succ.succ.succ → V) => self.cons (fun (x : Fin arity) => v x.succ.succ.succ) (v 0) (v 1) (v 2))
β.cons
def
LO.Arith.VecRec.Construction.Phi
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(C : Set V)
(pr : V)
:
Equations
Instances For
def
LO.Arith.VecRec.Construction.construction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
LO.Arith.Fixpoint.Construction V β.blueprint
Equations
- c.construction = { Φ := c.Phi, defined := ⋯, monotone := ⋯ }
Instances For
instance
LO.Arith.VecRec.Construction.instFiniteConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
LO.Arith.Fixpoint.Construction.Finite V c.construction
Equations
- c.instFiniteConstruction = { finite := ⋯ }
def
LO.Arith.VecRec.Construction.Graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
:
V → Prop
Equations
- c.Graph param = c.construction.Fixpoint param
Instances For
theorem
LO.Arith.VecRec.Construction.graph_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
LO.FirstOrder.Arith.HierarchySymbol.Defined
(fun (v : Fin arity.succ → V) => c.Graph (fun (x : Fin arity) => v x.succ) (v 0)) β.graphDef
instance
LO.Arith.VecRec.Construction.graph_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
Equations
- ⋯ = ⋯
instance
LO.Arith.VecRec.Construction.graph_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
:
𝚺₁-Predicate c.Graph param
Equations
- ⋯ = ⋯
instance
LO.Arith.VecRec.Construction.graph_definable''
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
:
{ Γ := 𝚺, rank := 0 + 1 }-Predicate c.Graph param
Equations
- ⋯ = ⋯
theorem
LO.Arith.VecRec.Construction.graph_case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
{param : Fin arity → V}
{pr : V}
:
theorem
LO.Arith.VecRec.Construction.graph_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
{param : Fin arity → V}
{l : V}
:
theorem
LO.Arith.VecRec.Construction.graph_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
{param : Fin arity → V}
{x : V}
{xs : V}
{y : V}
:
theorem
LO.Arith.VecRec.Construction.graph_exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(xs : V)
:
∃ (y : V), c.Graph param ⟪xs, y⟫
theorem
LO.Arith.VecRec.Construction.graph_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
{param : Fin arity → V}
{xs : V}
{y₁ : V}
{y₂ : V}
:
c.Graph param ⟪xs, y₁⟫ → c.Graph param ⟪xs, y₂⟫ → y₁ = y₂
theorem
LO.Arith.VecRec.Construction.graph_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(xs : V)
:
∃! y : V, c.Graph param ⟪xs, y⟫
def
LO.Arith.VecRec.Construction.result
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(xs : V)
:
V
Equations
- c.result param xs = Classical.choose! ⋯
Instances For
theorem
LO.Arith.VecRec.Construction.result_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(xs : V)
:
c.Graph param ⟪xs, c.result param xs⟫
theorem
LO.Arith.VecRec.Construction.result_eq_of_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
{xs : V}
{y : V}
(h : c.Graph param ⟪xs, y⟫)
:
c.result param xs = y
@[simp]
theorem
LO.Arith.VecRec.Construction.result_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
:
c.result param 0 = c.nil param
@[simp]
theorem
LO.Arith.VecRec.Construction.result_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(param : Fin arity → V)
(x : V)
(xs : V)
:
theorem
LO.Arith.VecRec.Construction.result_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin arity.succ → V) => c.result (fun (x : Fin arity) => v x.succ) (v 0)) β.resultDef
@[simp]
theorem
LO.Arith.VecRec.Construction.eval_resultDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(v : Fin (arity + 2) → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.resultDef) ↔ v 0 = c.result (fun (x : Fin arity) => v x.succ.succ) (v 1)
instance
LO.Arith.VecRec.Construction.result_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
:
Equations
- ⋯ = ⋯
instance
LO.Arith.VecRec.Construction.result_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : LO.Arith.VecRec.Blueprint arity}
(c : LO.Arith.VecRec.Construction V β)
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
Equations
- ⋯ = ⋯
Length of List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Arith.len v = LO.Arith.Len.construction.result ![] v
Instances For
@[simp]
@[simp]
theorem
LO.Arith.len_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.len (cons x v) = LO.Arith.len v + 1
Equations
Instances For
theorem
LO.Arith.len_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.len via LO.FirstOrder.Arith.lenDef
@[simp]
instance
LO.Arith.len_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.len
Equations
- ⋯ = ⋯
instance
LO.Arith.len_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.len
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.len_zero_iff_eq_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
:
LO.Arith.len v = 0 ↔ v = 0
theorem
LO.Arith.nth_lt_len
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
(hl : LO.Arith.len v ≤ i)
:
LO.Arith.nth v i = 0
@[simp]
theorem
LO.Arith.nth_ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v₁ : V}
{v₂ : V}
(hl : LO.Arith.len v₁ = LO.Arith.len v₂)
(H : ∀ i < LO.Arith.len v₁, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i)
:
v₁ = v₂
theorem
LO.Arith.nth_ext'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(l : V)
{v₁ : V}
{v₂ : V}
(hl₁ : LO.Arith.len v₁ = l)
(hl₂ : LO.Arith.len v₂ = l)
(H : ∀ i < l, LO.Arith.nth v₁ i = LO.Arith.nth v₂ i)
:
v₁ = v₂
theorem
LO.Arith.le_of_nth_le_nth
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v₁ : V}
{v₂ : V}
(hl : LO.Arith.len v₁ = LO.Arith.len v₂)
(H : ∀ i < LO.Arith.len v₁, LO.Arith.nth v₁ i ≤ LO.Arith.nth v₂ i)
:
v₁ ≤ v₂
theorem
LO.Arith.nth_lt_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
(hi : i < LO.Arith.len v)
:
LO.Arith.nth v i < v
theorem
LO.Arith.sigmaOne_skolem_vec
{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)
:
∃ (v : V), LO.Arith.len v = l ∧ ∀ i < l, R i (LO.Arith.nth v i)
theorem
LO.Arith.eq_singleton_iff_len_eq_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
:
LO.Arith.len v = 1 ↔ ∃ (x : V), v = ?[x]
theorem
LO.Arith.eq_doubleton_of_len_eq_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
:
LO.Arith.len v = 2 ↔ ∃ (x : V) (y : V), v = ?[x, y]
Maximum of List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- LO.Arith.listMax v = LO.Arith.ListMax.construction.result ![] v
Instances For
@[simp]
@[simp]
theorem
LO.Arith.listMax_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.listMax (cons x v) = max x (LO.Arith.listMax v)
Equations
Instances For
theorem
LO.Arith.listMax_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.listMax via LO.FirstOrder.Arith.listMaxDef
@[simp]
instance
LO.Arith.listMax_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.listMax
Equations
- ⋯ = ⋯
instance
LO.Arith.listMax_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.listMax
Equations
- ⋯ = ⋯
theorem
LO.Arith.nth_le_listMax
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{v : V}
(h : i < LO.Arith.len v)
:
LO.Arith.nth v i ≤ LO.Arith.listMax v
theorem
LO.Arith.listMaxss_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{z : V}
(h : ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ z)
:
LO.Arith.listMax v ≤ z
theorem
LO.Arith.listMaxss_le_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{z : V}
:
LO.Arith.listMax v ≤ z ↔ ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ z
Take Last k-Element #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Arith.takeLast v k = LO.Arith.TakeLast.construction.result ![k] v
Instances For
@[simp]
theorem
LO.Arith.takeLast_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : V}
:
LO.Arith.takeLast 0 k = 0
theorem
LO.Arith.takeLast_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{k : V}
(x : V)
(v : V)
:
LO.Arith.takeLast (cons x v) k = if LO.Arith.len v < k then cons x v else LO.Arith.takeLast v k
Equations
Instances For
theorem
LO.Arith.takeLast_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.takeLast via LO.FirstOrder.Arith.takeLastDef
@[simp]
theorem
LO.Arith.eval_takeLastDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.takeLastDef) ↔ v 0 = LO.Arith.takeLast (v 1) (v 2)
instance
LO.Arith.takeLast_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.takeLast
Equations
- ⋯ = ⋯
instance
LO.Arith.takeLast_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.takeLast
Equations
- ⋯ = ⋯
theorem
LO.Arith.len_takeLast
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{k : V}
(h : k ≤ LO.Arith.len v)
:
LO.Arith.len (LO.Arith.takeLast v k) = k
@[simp]
theorem
LO.Arith.takeLast_len_self
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
:
LO.Arith.takeLast v (LO.Arith.len v) = v
@[simp]
theorem
LO.Arith.takeLast_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
:
LO.Arith.takeLast v 0 = 0
theorem
LO.Arith.takeLast_succ_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{v : V}
(h : i < LO.Arith.len v)
:
LO.Arith.takeLast v (i + 1) = cons (LO.Arith.nth v (LO.Arith.len v - (i + 1))) (LO.Arith.takeLast v i)
Concatation #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- LO.Arith.concat v z = LO.Arith.Concat.construction.result ![z] v
Instances For
@[simp]
theorem
LO.Arith.concat_nil
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(z : V)
:
LO.Arith.concat 0 z = ?[z]
@[simp]
theorem
LO.Arith.concat_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
(z : V)
:
LO.Arith.concat (cons x v) z = cons x (LO.Arith.concat v z)
Equations
Instances For
theorem
LO.Arith.concat_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.concat via LO.FirstOrder.Arith.concatDef
@[simp]
theorem
LO.Arith.eval_concatDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.concatDef) ↔ v 0 = LO.Arith.concat (v 1) (v 2)
instance
LO.Arith.concat_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.concat
Equations
- ⋯ = ⋯
instance
LO.Arith.concat_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.concat
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.len_concat
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(z : V)
:
LO.Arith.len (LO.Arith.concat v z) = LO.Arith.len v + 1
theorem
LO.Arith.concat_nth_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(z : V)
{i : V}
(hi : i < LO.Arith.len v)
:
LO.Arith.nth (LO.Arith.concat v z) i = LO.Arith.nth v i
@[simp]
theorem
LO.Arith.concat_nth_len
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(z : V)
:
LO.Arith.nth (LO.Arith.concat v z) (LO.Arith.len v) = z
theorem
LO.Arith.concat_nth_len'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : V)
(z : V)
{i : V}
(hi : LO.Arith.len v = i)
:
LO.Arith.nth (LO.Arith.concat v z) i = z
Membership #
Equations
- LO.Arith.MemVec x v = ∃ i < LO.Arith.len v, x = LO.Arith.nth v i
Instances For
Equations
- LO.Arith.«term_∈ᵥ_» = Lean.ParserDescr.trailingNode `LO.Arith.term_∈ᵥ_ 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᵥ ") (Lean.ParserDescr.cat `term 41))
Instances For
@[simp]
theorem
LO.Arith.not_memVec_empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
:
¬LO.Arith.MemVec x 0
theorem
LO.Arith.nth_mem_memVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{v : V}
(h : i < LO.Arith.len v)
:
LO.Arith.MemVec (LO.Arith.nth v i) v
@[simp]
theorem
LO.Arith.memVec_insert_fst
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{v : V}
:
LO.Arith.MemVec x (cons x v)
@[simp]
theorem
LO.Arith.memVec_cons_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{y : V}
{v : V}
:
LO.Arith.MemVec x (cons y v) ↔ x = y ∨ LO.Arith.MemVec x v
theorem
LO.Arith.le_of_memVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x : V}
{v : V}
(h : LO.Arith.MemVec x v)
:
x ≤ v
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.memVec_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚫₁-Relation LO.Arith.MemVec via LO.FirstOrder.Arith.memVecDef
@[simp]
Equations
- ⋯ = ⋯
instance
LO.Arith.memVec_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
Equations
- ⋯ = ⋯
Subset #
Equations
- LO.Arith.SubsetVec v w = ∀ (x : V), LO.Arith.MemVec x v → LO.Arith.MemVec x w
Instances For
Equations
- LO.Arith.«term_⊆ᵥ_» = Lean.ParserDescr.trailingNode `LO.Arith.term_⊆ᵥ_ 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ᵥ ") (Lean.ParserDescr.cat `term 31))
Instances For
@[simp]
@[simp]
theorem
LO.Arith.subsetVec_insert_tail
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.SubsetVec v (cons x v)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.subsetVec_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚫₁-Relation LO.Arith.SubsetVec via LO.FirstOrder.Arith.subsetVecDef
@[simp]
Equations
- ⋯ = ⋯
instance
LO.Arith.subsetVec_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
Equations
- ⋯ = ⋯
Repeat #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
repeatVec x k = x ∷ x ∷ x ∷ ... k times ... ∷ 0
Equations
- LO.Arith.repeatVec x k = LO.Arith.repeatVec.construction.result ![x] k
Instances For
@[simp]
theorem
LO.Arith.repeatVec_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
:
LO.Arith.repeatVec x 0 = 0
@[simp]
theorem
LO.Arith.repeatVec_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(k : V)
:
LO.Arith.repeatVec x (k + 1) = cons x (LO.Arith.repeatVec x k)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.repeatVec_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.repeatVec via LO.FirstOrder.Arith.repeatVecDef
@[simp]
instance
LO.Arith.repeatVec_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.repeatVec
Equations
- ⋯ = ⋯
instance
LO.Arith.repeatVec_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{m : ℕ}
(Γ : LO.SigmaPiDelta)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.repeatVec
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.len_repeatVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(k : V)
:
LO.Arith.len (LO.Arith.repeatVec x k) = k
@[simp]
theorem
LO.Arith.le_repaetVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(k : V)
:
k ≤ LO.Arith.repeatVec x k
theorem
LO.Arith.nth_repeatVec
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(k : V)
{i : V}
(h : i < k)
:
LO.Arith.nth (LO.Arith.repeatVec x k) i = x
theorem
LO.Arith.len_repeatVec_of_nth_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{m : V}
(H : ∀ i < LO.Arith.len v, LO.Arith.nth v i ≤ m)
:
v ≤ LO.Arith.repeatVec m (LO.Arith.len v)
Convert to Set #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- LO.Arith.vecToSet v = LO.Arith.VecToSet.construction.result ![] v
Instances For
@[simp]
@[simp]
theorem
LO.Arith.vecToSet_cons
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(v : V)
:
LO.Arith.vecToSet (cons x v) = insert x (LO.Arith.vecToSet v)
Equations
Instances For
theorem
LO.Arith.vecToSet_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.vecToSet via LO.FirstOrder.Arith.vecToSetDef
@[simp]
instance
LO.Arith.vecToSet_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₁ LO.Arith.vecToSet
Equations
- ⋯ = ⋯
instance
LO.Arith.vecToSet_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{m : ℕ}
(Γ : LO.SigmaPiDelta)
:
{ Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.vecToSet
Equations
- ⋯ = ⋯
theorem
LO.Arith.mem_vecToSet_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{x : V}
:
x ∈ LO.Arith.vecToSet v ↔ ∃ i < LO.Arith.len v, x = LO.Arith.nth v i
@[simp]
theorem
LO.Arith.nth_mem_vecToSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
{i : V}
(h : i < LO.Arith.len v)
:
LO.Arith.nth v i ∈ LO.Arith.vecToSet v