@[simp]

theorem LO.Arith.Nuon.llen_lt_len_hash_len {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (K : V) : ‖‖K‖‖ < ‖K # ‖K‖‖

theorem LO.Arith.Nuon.mul_len_lt_len_hash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {i I L : V} (hi : i ≤ ‖I‖) : i * ‖L‖ < ‖I # L‖

theorem LO.Arith.Nuon.mul_len_lt_len_hash' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {i K z : V} (hi : i ≤ ‖z‖) : i * ‖‖K‖‖ < ‖z # ‖K‖‖

def LO.Arith.Nuon.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L S i : V) : V

Equations

• LO.Arith.Nuon.ext L S i = S / LO.Arith.bexp S (i * ‖L‖) % L # 1

Instances For

• LO.Arith.Nuon.ext_Definable
• LO.Arith.Nuon.instBounded₃Ext
• LO.Arith.Nuon.instBounded₃Ext_1

theorem LO.Arith.Nuon.ext_eq_zero_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L S i : V} (h : ‖S‖ ≤ i * ‖L‖) : ext L S i = 0

@[simp]

theorem LO.Arith.Nuon.ext_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L S i : V) : ext L S i ≤ S

theorem LO.Arith.Nuon.ext_graph_aux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (z S L i : V) : z = ext L S i ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)

theorem LO.Arith.Nuon.ext_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (z S L i : V) : z = ext L S i ↔ ∃ lS ≤ S, lS = ‖S‖ ∧ ∃ lL ≤ L, lL = ‖L‖ ∧ (lS ≤ i * lL → z = 0) ∧ (i * lL < lS → ∃ b ≤ S, Exponential (i * lL) b ∧ ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

def LO.Arith.Nuon.extDef : 𝚺₀.Semisentence 4

Equations

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

@[simp]

theorem LO.Arith.Nuon.cons_app_seven {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 7 = s 6

@[simp]

theorem LO.Arith.Nuon.cons_app_eight {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 8 = s 7

@[simp]

theorem LO.Arith.Nuon.cons_app_nine {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 9 = s 8

theorem LO.Arith.Nuon.ext_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₃ ext via extDef

instance LO.Arith.Nuon.ext_Definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₃ ext

instance LO.Arith.Nuon.instBounded₃Ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.Bounded₃ ext

@[simp]

theorem LO.Arith.Nuon.ext_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L i : V) : ext L 0 i = 0

theorem LO.Arith.Nuon.ext_zero_eq_self_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L S : V} (h : ‖S‖ ≤ ‖L‖) : ext L S 0 = S

theorem LO.Arith.Nuon.ext_eq_of_ge {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L S S' i : V} (h : S ≤ S') : S / bexp S' (i * ‖L‖) % L # 1 = ext L S i

theorem LO.Arith.Nuon.ext_eq_of_gt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L S S' i : V} (h : i * ‖L‖ < ‖S'‖) : S / bexp S' (i * ‖L‖) % L # 1 = ext L S i

theorem LO.Arith.Nuon.ext_eq_hash_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {I L S i : V} (h : i ≤ ‖I‖) : S / bexp (I # L) (i * ‖L‖) % L # 1 = ext L S i

theorem LO.Arith.Nuon.ext_add₁_pow2 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L i S₁ S₂ p : V} (pp : Pow2 p) (h : (i + 1) * ‖L‖ < ‖p‖) : ext L (S₁ + S₂ * p) i = ext L S₁ i

theorem LO.Arith.Nuon.ext_add₁_bexp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {I L i j S₁ S₂ : V} (hi : i ≤ ‖I‖) (hij : j < i) : ext L (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) j = ext L S₁ j

theorem LO.Arith.Nuon.ext_add₂_bexp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L I i j S₁ S₂ : V} (hij : i + j ≤ ‖I‖) (hS₁ : ‖S₁‖ ≤ i * ‖L‖) : ext L (S₁ + S₂ * bexp (I # L) (i * ‖L‖)) (i + j) = ext L S₂ j

def LO.Arith.Nuon.append {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S i X : V) : V

Equations

• LO.Arith.Nuon.append I L S i X = S % LO.Arith.bexp (I # L) (i * ‖L‖) + X * LO.Arith.bexp (I # L) (i * ‖L‖)

theorem LO.Arith.Nuon.append_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S i : V) : append I L S i 0 = S % bexp (I # L) (i * ‖L‖)

theorem LO.Arith.Nuon.len_append {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S : V) {i X : V} (hi : i ≤ ‖I‖) (hX : 0 < X) : ‖append I L S i X‖ = ‖X‖ + i * ‖L‖

theorem LO.Arith.Nuon.append_lt_hash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S : V) {i X : V} (hi : i < ‖I‖) (hX : ‖X‖ ≤ ‖L‖) : append I L S i X < I # L

theorem LO.Arith.Nuon.append_lt_sq_hash {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S : V) {i X : V} (hi : i ≤ ‖I‖) (hX : ‖X‖ ≤ ‖L‖) (Ipos : 0 < I) : append I L S i X < (I # L) ^ 2

theorem LO.Arith.Nuon.ext_append_last {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S : V) {i X : V} (hi : i ≤ ‖I‖) (hX : ‖X‖ ≤ ‖L‖) : ext L (append I L S i X) i = X

theorem LO.Arith.Nuon.ext_append_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I L S : V) {i j X : V} (hi : i ≤ ‖I‖) (hij : j < i) : ext L (append I L S i X) j = ext L S j

def LO.Arith.Nuon.IsSegment {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L A start intv S : V) : Prop

Equations

• LO.Arith.Nuon.IsSegment L A start intv S = ∀ i < intv, LO.Arith.Nuon.ext L S (i + 1) = LO.Arith.Nuon.ext L S i + LO.Arith.fbit A (start + i)

def LO.Arith.Nuon.Segment {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U L A start intv nₛ nₑ : V) : Prop

Equations

• LO.Arith.Nuon.Segment U L A start intv nₛ nₑ = ∃ S < U, LO.Arith.Nuon.IsSegment L A start intv S ∧ LO.Arith.Nuon.ext L S 0 = nₛ ∧ LO.Arith.Nuon.ext L S intv = nₑ

def LO.Arith.Nuon.IsSeries {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U I L A iter T : V) : Prop

Equations

• LO.Arith.Nuon.IsSeries U I L A iter T = ∀ l < iter, LO.Arith.Nuon.Segment U L A (‖I‖ * l) ‖I‖ (LO.Arith.Nuon.ext L T l) (LO.Arith.Nuon.ext L T (l + 1))

def LO.Arith.Nuon.Series {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U I L A iter n : V) : Prop

Equations

• LO.Arith.Nuon.Series U I L A iter n = ∃ T < U, LO.Arith.Nuon.IsSeries U I L A iter T ∧ LO.Arith.Nuon.ext L T 0 = 0 ∧ LO.Arith.Nuon.ext L T iter = n

def LO.Arith.Nuon.SeriesSegment {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U I L A k n : V) : Prop

Equations

• LO.Arith.Nuon.SeriesSegment U I L A k n = ∃ nₖ ≤ n, LO.Arith.Nuon.Series U I L A (k / ‖I‖) nₖ ∧ LO.Arith.Nuon.Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₖ n

theorem LO.Arith.Nuon.SeriesSegment.series {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A k n : V} (H : SeriesSegment U I L A k n) : ∃ (T : V) (S : V), IsSeries U I L A (k / ‖I‖) T ∧ IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S ∧ ext L T 0 = 0 ∧ ext L T (k / ‖I‖) = ext L S 0 ∧ ext L S (k % ‖I‖) = n

theorem LO.Arith.Nuon.IsSegment.le_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L A start intv S : V} (H : IsSegment L A start intv S) (i : V) : i ≤ intv → ext L S i ≤ ext L S 0 + i

theorem LO.Arith.Nuon.Segment.refl {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U L A start n : V) (hL : L # 1 ≤ U) (hn : ‖n‖ ≤ ‖L‖) : Segment U L A start 0 n n

theorem LO.Arith.Nuon.Segment.le_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U L A start intv nₛ nₑ : V} (H : Segment U L A start intv nₛ nₑ) : nₑ ≤ nₛ + intv

theorem LO.Arith.Nuon.Segment.uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U L A start intv nₛ nₑ₁ nₑ₂ : V} (H₁ : Segment U L A start intv nₛ nₑ₁) (H₂ : Segment U L A start intv nₛ nₑ₂) : nₑ₁ = nₑ₂

theorem LO.Arith.Nuon.IsSeries.le_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A iter T : V} (H : IsSeries U I L A iter T) (l : V) : l ≤ iter → ext L T l ≤ ext L T 0 + ‖I‖ * l

theorem LO.Arith.Nuon.Series.le_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A iter n : V} (H : Series U I L A iter n) : n ≤ ‖I‖ * iter

theorem LO.Arith.Nuon.Series.uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A iter n₁ n₂ : V} (H₁ : Series U I L A iter n₁) (H₂ : Series U I L A iter n₂) : n₁ = n₂

theorem LO.Arith.Nuon.SeriesSegment.le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A k n : V} (H : SeriesSegment U I L A k n) : n ≤ k

theorem LO.Arith.Nuon.SeriesSegment.initial {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A : V} (Upos : 0 < U) : SeriesSegment U I L A 0 0

theorem LO.Arith.Nuon.SeriesSegment.zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L k : V} (Upos : 0 < U) : SeriesSegment U I L 0 k 0

theorem LO.Arith.Nuon.SeriesSegment.uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A k n₁ n₂ : V} (H₁ : SeriesSegment U I L A k n₁) (H₂ : SeriesSegment U I L A k n₂) : n₁ = n₂

theorem LO.Arith.Nuon.Segment.succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A : V} (hU : (I # L) ^ 2 ≤ U) {start intv nₛ nₑ : V} (H : Segment U L A start intv nₛ nₑ) (hintv : intv < ‖I‖) (hnₛ : ‖nₛ + ‖I‖‖ ≤ ‖L‖) : Segment U L A start (intv + 1) nₛ (nₑ + fbit A (start + intv))

theorem LO.Arith.Nuon.Series.succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A : V} (hU : (I # L) ^ 2 ≤ U) (hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖) {iter n n' : V} (HT : Series U I L A iter n) (HS : Segment U L A (‖I‖ * iter) ‖I‖ n n') (hiter : iter < ‖I‖) : Series U I L A (iter + 1) n'

theorem LO.Arith.Nuon.div_mod_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a b : V) : (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1

theorem LO.Arith.Nuon.SeriesSegment.succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U I L A : V} (hU : (I # L) ^ 2 ≤ U) (hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖) {k n : V} (hk : k < ‖I‖ ^ 2) (H : SeriesSegment U I L A k n) : SeriesSegment U I L A (k + 1) (n + fbit A k)

def LO.Arith.Nuon.polyI {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Define $I$, $L$, $U$ to satisfy the following:

1. $I$, $L$, $U$ are polynomial of $A$.
2. $(I\mathrm{\#}L{)}^2\le U$
3. $\Vert \Vert I{\Vert }^2\Vert \le \Vert L\Vert$
4. $\Vert A\Vert <\Vert I{\Vert }^2$

Equations

• LO.Arith.Nuon.polyI A = LO.Arith.bexp (2 * A) (√‖A‖)

def LO.Arith.Nuon.polyL {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Equations

• LO.Arith.Nuon.polyL A = ‖LO.Arith.Nuon.polyI A‖ ^ 2

def LO.Arith.Nuon.polyU {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Equations

• LO.Arith.Nuon.polyU A = (2 * A + 1) ^ 128

theorem LO.Arith.Nuon.len_polyI {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : ‖polyI A‖ = √‖A‖ + 1

theorem LO.Arith.Nuon.polyI_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : ‖A‖ < ‖polyI A‖ ^ 2

theorem LO.Arith.Nuon.two_add_two_eq_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 2 + 2 = 4

theorem LO.Arith.Nuon.four_mul_eq_two_mul_two_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : 4 * a = 2 * (2 * a)

@[simp]

theorem LO.Arith.Nuon.two_mul_sqrt_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : 2 * √a ≤ a + 1

theorem LO.Arith.Nuon.four_mul_hash_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : (4 * a) # (4 * a) ≤ (a # a) ^ 16

@[simp]

theorem LO.Arith.Nuon.pos_sq_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} : 0 < √a ↔ 0 < a

@[simp]

theorem LO.Arith.Nuon.pow_four_le_pow_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b : V} : a ^ 4 ≤ b ^ 4 ↔ a ≤ b

theorem LO.Arith.Nuon.bexp_four_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a a' x : V} (hx : 4 * x < ‖a‖) (hx' : x < ‖a'‖) : bexp a (4 * x) = bexp a' x ^ 4

theorem LO.Arith.Nuon.polyI_hash_self_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : polyI A # polyI A ≤ (2 * A + 1) ^ 4

theorem LO.Arith.Nuon.polyI_hash_polyL_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : polyI A # polyL A ≤ (2 * A + 1) ^ 64

theorem LO.Arith.Nuon.sq_polyI_hash_polyL_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : (polyI A # polyL A) ^ 2 ≤ polyU A

def LO.Arith.Nuon.NuonAux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A k n : V) : Prop

Equations

• LO.Arith.Nuon.NuonAux A k n = LO.Arith.Nuon.SeriesSegment (LO.Arith.Nuon.polyU A) (LO.Arith.Nuon.polyI A) (LO.Arith.Nuon.polyL A) A k n

Instances For

• LO.Arith.Nuon.nuonAux_definable

def LO.Arith.Nuon.isSegmentDef : 𝚺₀.Semisentence 5

Equations

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

theorem LO.Arith.Nuon.isSegmentDef_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 5 → V) => IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) isSegmentDef

def LO.Arith.Nuon.segmentDef : 𝚺₀.Semisentence 7

Equations

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

theorem LO.Arith.Nuon.segmentDef_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 7 → V) => Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) segmentDef

def LO.Arith.Nuon.isSeriesDef : 𝚺₀.Semisentence 6

Equations

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

theorem LO.Arith.Nuon.bex_eq_le_iff {V : Type u_1} [ORingStruc V] {z : V} {p : V → Prop} {b : V} : (∃ a ≤ z, a = b ∧ p a) ↔ b ≤ z ∧ p b

theorem LO.Arith.Nuon.bex_eq_lt_iff {V : Type u_1} [ORingStruc V] {z : V} {p : V → Prop} {b : V} : (∃ a < z, a = b ∧ p a) ↔ b < z ∧ p b

theorem LO.Arith.Nuon.isSerieDef_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => IsSeries (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) isSeriesDef

def LO.Arith.Nuon.seriesDef : 𝚺₀.Semisentence 6

Equations

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

theorem LO.Arith.Nuon.seriesDef_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => Series (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) seriesDef

def LO.Arith.Nuon.seriesSegmentDef : 𝚺₀.Semisentence 6

Equations

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

theorem LO.Arith.Nuon.seriesSegmentDef_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => SeriesSegment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) seriesSegmentDef

def LO.Arith.Nuon.nuonAuxDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.Nuon.nuonAux_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Relation₃ NuonAux via nuonAuxDef

instance LO.Arith.Nuon.nuonAux_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Relation₃ NuonAux

instance LO.Arith.Nuon.instBounded₃Ext_1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : FirstOrder.Arith.Bounded₃ ext

@[simp]

theorem LO.Arith.Nuon.NuonAux.initial {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : NuonAux A 0 0

@[simp]

theorem LO.Arith.Nuon.NuonAux.initial_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A n : V) : NuonAux A 0 n ↔ n = 0

@[simp]

theorem LO.Arith.Nuon.NuonAux.zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (k : V) : NuonAux 0 k 0

theorem LO.Arith.Nuon.NuonAux.le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A k n : V} (H : NuonAux A k n) : n ≤ k

theorem LO.Arith.Nuon.NuonAux.uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A k n₁ n₂ : V} (H₁ : NuonAux A k n₁) (H₂ : NuonAux A k n₂) : n₁ = n₂

theorem LO.Arith.Nuon.NuonAux.succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n A k : V} (H : NuonAux A k n) (hk : k ≤ ‖A‖) : NuonAux A (k + 1) (n + fbit A k)

theorem LO.Arith.Nuon.NuonAux.exists {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A k : V} (hk : k ≤ ‖A‖) : ∃ (n : V), NuonAux A k n

theorem LO.Arith.Nuon.NuonAux.succ_elim {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n A k : V} (hk : k ≤ ‖A‖) (H : NuonAux A (k + 1) n) : ∃ (n' : V), n = n' + fbit A k ∧ NuonAux A k n'

theorem LO.Arith.Nuon.NuonAux.succ_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n A k : V} (hk : k ≤ ‖A‖) : NuonAux A (k + 1) (n + fbit A k) ↔ NuonAux A k n

theorem LO.Arith.Nuon.NuonAux.two_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A k n : V} (hk : k ≤ ‖A‖) : NuonAux A k n → NuonAux (2 * A) (k + 1) n

theorem LO.Arith.Nuon.NuonAux.two_mul_add_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A k n : V} (hk : k ≤ ‖A‖) : NuonAux A k n → NuonAux (2 * A + 1) (k + 1) (n + 1)

def LO.Arith.Nuon {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A n : V) : Prop

Equations

• LO.Arith.Nuon A n = LO.Arith.Nuon.NuonAux A ‖A‖ n

theorem LO.Arith.Nuon.exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : ∃! n : V, Nuon A n

def LO.Arith.nuon {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : V

Equations

• LO.Arith.nuon a = Classical.choose! ⋯

Instances For

• LO.Arith.nuon_definable

@[simp]

theorem LO.Arith.nuon_nuon {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : Nuon a (nuon a)

theorem LO.Arith.Nuon.nuon_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b : V} (h : Nuon a b) : nuon a = b

theorem LO.Arith.Nuon.nuon_eq_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a b : V} : b = nuon a ↔ Nuon a b

theorem LO.Arith.nuon_bit0 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : nuon (2 * a) = nuon a

theorem LO.Arith.nuon_bit1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : nuon (2 * a + 1) = nuon a + 1

@[simp]

theorem LO.Arith.nuon_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : nuon 0 = 0

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

Equations

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

theorem LO.Arith.nuon_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₁ nuon via FirstOrder.Arith.nuonDef

@[simp]

theorem LO.Arith.eval_nuon_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.nuonDef) ↔ v 0 = nuon (v 1)

instance LO.Arith.nuon_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₁ nuon