theorem Nat.pos_of_eq_one {n : ℕ} (h : n = 1) : 0 < n

def Nat.isEqNat (n : ℕ) (m : ℕ) : ℕ

Equations

• n.isEqNat m = if n = m then 1 else 0

def Nat.isLtNat (n : ℕ) (m : ℕ) : ℕ

Equations

• n.isLtNat m = if n < m then 1 else 0

def Nat.isLeNat (n : ℕ) (m : ℕ) : ℕ

Equations

• n.isLeNat m = if n ≤ m then 1 else 0

def Nat.isDvdNat (n : ℕ) (m : ℕ) : ℕ

Equations

• n.isDvdNat m = if n ∣ m then 1 else 0

@[simp]

theorem Nat.isEqNat_pos_iff {n : ℕ} {m : ℕ} : 0 < n.isEqNat m ↔ n = m

@[simp]

theorem Nat.isLtNat_pos_iff {n : ℕ} {m : ℕ} : 0 < n.isLtNat m ↔ n < m

@[simp]

theorem Nat.isLeNat_pos_iff {n : ℕ} {m : ℕ} : 0 < n.isLeNat m ↔ n ≤ m

@[simp]

theorem Nat.isDvdNat_pos_iff {n : ℕ} {m : ℕ} : 0 < n.isDvdNat m ↔ n ∣ m

def Nat.inv (n : ℕ) : ℕ

Equations

• n.inv = n.isEqNat 0

def Nat.pos (n : ℕ) : ℕ

Equations

• n.pos = Nat.isLtNat 0 n

@[simp]

theorem Nat.inv_zero : Nat.inv 0 = 1

@[simp]

theorem Nat.inv_iff_ne_zero {n : ℕ} : n.inv = 0 ↔ 0 < n

@[simp]

theorem Nat.inv_ne_zero {n : ℕ} (h : n ≠ 0) : n.inv = 0

@[simp]

theorem Nat.pos_zero : Nat.pos 0 = 0

@[simp]

theorem Nat.pos_ne_zero {n : ℕ} (h : n ≠ 0) : n.pos = 1

def Nat.and (n : ℕ) (m : ℕ) : ℕ

Equations

• n.and m = Nat.isLtNat 0 (n * m)

def Nat.or (n : ℕ) (m : ℕ) : ℕ

Equations

• n.or m = Nat.isLtNat 0 (n + m)

theorem Nat.and_eq (n : ℕ) (m : ℕ) : n.and m = if 0 < n ∧ 0 < m then 1 else 0

theorem Nat.and_eq_one (n : ℕ) (m : ℕ) : n.and m = 1 ↔ 0 < n ∧ 0 < m

theorem Nat.or_eq (n : ℕ) (m : ℕ) : n.or m = if 0 < n ∨ 0 < m then 1 else 0

@[simp]

theorem Nat.and_pos_iff (n : ℕ) (m : ℕ) : 0 < n.and m ↔ 0 < n ∧ 0 < m

@[simp]

theorem Nat.or_pos_iff (n : ℕ) (m : ℕ) : 0 < n.or m ↔ 0 < n ∨ 0 < m

@[simp]

theorem Nat.inv_pos_iff (n : ℕ) : 0 < n.inv ↔ ¬0 < n

@[simp]

theorem Nat.pos_pos_iff (n : ℕ) : 0 < n.pos ↔ 0 < n

def Nat.ball (n : ℕ) (p : ℕ → ℕ) : ℕ

Equations

• n.ball p = Nat.rec 1 (fun (n ih : ℕ) => (p n).pos.and ih) n

@[simp]

theorem Nat.ball_pos_iff {p : ℕ → ℕ} {n : ℕ} : 0 < n.ball p ↔ ∀ m < n, 0 < p m

@[simp]

theorem Nat.ball_eq_zero_iff {p : ℕ → ℕ} {n : ℕ} : n.ball p = 0 ↔ ∃ m < n, p m = 0

theorem Nat.ball_pos_iff_eq_one {p : ℕ → ℕ} {n : ℕ} : n.ball p = 1 ↔ 0 < n.ball p

inductive Nat.ArithPart₁ {n : ℕ} : (Mathlib.Vector ℕ n →. ℕ) → Prop

• zero: ∀ {n : ℕ}, Nat.ArithPart₁ fun (x : Mathlib.Vector ℕ n) => 0
• one: ∀ {n : ℕ}, Nat.ArithPart₁ fun (x : Mathlib.Vector ℕ n) => 1
• add: ∀ {n : ℕ} (i j : Fin n), Nat.ArithPart₁ ↑fun (v : Mathlib.Vector ℕ n) => v.get i + v.get j
• mul: ∀ {n : ℕ} (i j : Fin n), Nat.ArithPart₁ ↑fun (v : Mathlib.Vector ℕ n) => v.get i * v.get j
• proj: ∀ {n : ℕ} (i : Fin n), Nat.ArithPart₁ ↑fun (v : Mathlib.Vector ℕ n) => v.get i
• equal: ∀ {n : ℕ} (i j : Fin n), Nat.ArithPart₁ ↑fun (v : Mathlib.Vector ℕ n) => (v.get i).isEqNat (v.get j)
• lt: ∀ {n : ℕ} (i j : Fin n), Nat.ArithPart₁ ↑fun (v : Mathlib.Vector ℕ n) => (v.get i).isLtNat (v.get j)
• comp: ∀ {m n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (g : Fin n → Mathlib.Vector ℕ m →. ℕ), Nat.ArithPart₁ f → (∀ (i : Fin n), Nat.ArithPart₁ (g i)) → Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ m) => (Mathlib.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind: ∀ {n : ℕ} {f : Mathlib.Vector ℕ (n + 1) → ℕ}, Nat.ArithPart₁ ↑f → Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

def Nat.Arith₁ {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ) : Prop

Equations

• Nat.Arith₁ f = Nat.ArithPart₁ ↑f

theorem Nat.ArithPart₁.to_partrec' {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (hf : Nat.ArithPart₁ f) : Nat.Partrec' f

theorem Nat.ArithPart₁.of_eq {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Mathlib.Vector ℕ n →. ℕ} (hf : Nat.ArithPart₁ f) (H : ∀ (i : Mathlib.Vector ℕ n), f i = g i) : Nat.ArithPart₁ g

theorem Nat.ArithPart₁.bind {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ →. ℕ) (hf : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ (n + 1)) => f v.tail v.head) {g : Mathlib.Vector ℕ n →. ℕ} (hg : Nat.ArithPart₁ g) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => (g v).bind (f v)

theorem Nat.ArithPart₁.map {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ → ℕ) (hf : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => f v.tail v.head) {g : Mathlib.Vector ℕ n →. ℕ} (hg : Nat.ArithPart₁ g) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Part.map (f v) (g v)

theorem Nat.ArithPart₁.comp₁ (f : ℕ →. ℕ) (hf : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ 1) => f (v.get 0)) {n : ℕ} {g : Mathlib.Vector ℕ n → ℕ} (hg : Nat.Arith₁ g) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => f (g v)

theorem Nat.ArithPart₁.comp₂ (f : ℕ → ℕ →. ℕ) (hf : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ 2) => f (v.get 0) (v.get 1)) {n : ℕ} {g : Mathlib.Vector ℕ n → ℕ} {h : Mathlib.Vector ℕ n → ℕ} (hg : Nat.Arith₁ g) (hh : Nat.Arith₁ h) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => f (g v) (h v)

theorem Nat.ArithPart₁.rfind' {n : ℕ} {f : ℕ → Mathlib.Vector ℕ n → ℕ} (h : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => f v.head v.tail) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n : ℕ) => Part.some (decide (f n v = 0))

theorem Nat.ArithPart₁.rfind'₁ {n : ℕ} (i : Fin n) {f : ℕ → ℕ → ℕ} (h : Nat.Arith₁ fun (v : Mathlib.Vector ℕ 2) => f (v.get 0) (v.get 1)) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f n_1 (v.get i) = 0))

theorem Nat.Arith₁.of_eq {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ n → ℕ} (hf : Nat.Arith₁ f) (H : ∀ (i : Mathlib.Vector ℕ n), f i = g i) : Nat.Arith₁ g

theorem Nat.Arith₁.zero {n : ℕ} : Nat.Arith₁ fun (x : Mathlib.Vector ℕ n) => 0

theorem Nat.Arith₁.one {n : ℕ} : Nat.Arith₁ fun (x : Mathlib.Vector ℕ n) => 1

theorem Nat.Arith₁.add {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i + v.get j

theorem Nat.Arith₁.mul {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i * v.get j

theorem Nat.Arith₁.proj {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i

theorem Nat.Arith₁.head {n : ℕ} : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => v.head

theorem Nat.Arith₁.equal {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).isEqNat (v.get j)

theorem Nat.Arith₁.lt {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).isLtNat (v.get j)

theorem Nat.Arith₁.comp {m : ℕ} {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (g : Fin n → Mathlib.Vector ℕ m → ℕ) (hf : Nat.Arith₁ f) (hg : ∀ (i : Fin n), Nat.Arith₁ (g i)) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ m) => f (Mathlib.Vector.ofFn fun (i : Fin n) => g i v)

def Nat.Arith₁.Vec {n : ℕ} {m : ℕ} (f : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m) : Prop

Equations

• Nat.Arith₁.Vec f = ∀ (i : Fin m), Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (f v).get i

theorem Nat.Arith₁.nil {n : ℕ} : Nat.Arith₁.Vec fun (x : Mathlib.Vector ℕ n) => Mathlib.Vector.nil

theorem Nat.Arith₁.cons {n : ℕ} {m : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m} (hf : Nat.Arith₁ f) (hg : Nat.Arith₁.Vec g) : Nat.Arith₁.Vec fun (v : Mathlib.Vector ℕ n) => f v ::ᵥ g v

theorem Nat.Arith₁.tail {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (hf : Nat.Arith₁ f) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n.succ) => f v.tail

theorem Nat.Arith₁.comp' {n : ℕ} {m : ℕ} {f : Mathlib.Vector ℕ m → ℕ} {g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m} (hf : Nat.Arith₁ f) (hg : Nat.Arith₁.Vec g) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => f (g v)

theorem Nat.Arith₁.comp₁ (f : ℕ → ℕ) (hf : Nat.Arith₁ fun (v : Mathlib.Vector ℕ 1) => f (v.get 0)) {n : ℕ} {g : Mathlib.Vector ℕ n → ℕ} (hg : Nat.Arith₁ g) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => f (g v)

theorem Nat.Arith₁.comp₂ (f : ℕ → ℕ → ℕ) (hf : Nat.Arith₁ fun (v : Mathlib.Vector ℕ 2) => f (v.get 0) (v.get 1)) {n : ℕ} {g : Mathlib.Vector ℕ n → ℕ} {h : Mathlib.Vector ℕ n → ℕ} (hg : Nat.Arith₁ g) (hh : Nat.Arith₁ h) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => f (g v) (h v)

theorem Nat.Arith₁.succ {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i + 1

theorem Nat.Arith₁.const {n : ℕ} (m : ℕ) : Nat.Arith₁ fun (x : Mathlib.Vector ℕ n) => m

theorem Nat.Arith₁.inv {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).inv

theorem Nat.Arith₁.pos {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).pos

theorem Nat.Arith₁.and {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).and (v.get j)

theorem Nat.Arith₁.or {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).or (v.get j)

theorem Nat.Arith₁.le {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).isLeNat (v.get j)

theorem Nat.Arith₁.if_pos {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ n → ℕ} {h : Mathlib.Vector ℕ n → ℕ} (hf : Nat.Arith₁ f) (hg : Nat.Arith₁ g) (hh : Nat.Arith₁ h) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => if 0 < f v then g v else h v

theorem Nat.Arith₁.to_arith₁ {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (h : Nat.Arith₁ f) : Nat.ArithPart₁ fun (x : Mathlib.Vector ℕ n) => ↑(some (f x))

theorem Nat.ArithPart₁.rfindPos {n : ℕ} {f : Mathlib.Vector ℕ (n + 1) → ℕ} (h : Nat.Arith₁ f) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (0 < f (n_1 ::ᵥ v)))

theorem Nat.ArithPart₁.rfindPos₁ {n : ℕ} (i : Fin n) {f : ℕ → ℕ → ℕ} (h : Nat.Arith₁ fun (v : Mathlib.Vector ℕ 2) => f (v.get 0) (v.get 1)) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (0 < f n_1 (v.get i)))

theorem Nat.ArithPart₁.inv_fun {n : ℕ} (i : Fin n) (f : ℕ → ℕ) (hf : Nat.Arith₁ fun (v : Mathlib.Vector ℕ 1) => f (v.get 0)) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (x : ℕ) => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))

theorem Nat.ArithPart₁.implicit_fun {n : ℕ} (i : Fin n) (f : Mathlib.Vector ℕ n → ℕ → ℕ) (hf : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => f v.tail v.head) : Nat.ArithPart₁ fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (x : ℕ) => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))

theorem Nat.Arith₁.sqrt {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).sqrt

theorem Nat.Arith₁.sub {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i - v.get j

theorem Nat.Arith₁.pair {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => Nat.pair (v.get i) (v.get j)

theorem Nat.Arith₁.unpair₁ {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (Nat.unpair (v.get i)).1

theorem Nat.Arith₁.unpair₂ {n : ℕ} (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (Nat.unpair (v.get i)).2

theorem Nat.Arith₁.dvd {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).isDvdNat (v.get j)

theorem Nat.Arith₁.rem {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => v.get i % v.get j

theorem Nat.Arith₁.beta {n : ℕ} (i : Fin n) (j : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).beta (v.get j)

theorem Nat.Arith₁.ball {n : ℕ} {p : Mathlib.Vector ℕ n → ℕ → ℕ} (hp : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => p v.tail v.head) (i : Fin n) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ n) => (v.get i).ball (p v)

def Nat.Arith₁.recSequence {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) : List ℕ

Equations

• Nat.Arith₁.recSequence f g z v = List.ofFn fun (i : Fin (z + 1)) => Nat.recOn (↑i) (f v) fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)

theorem Nat.Arith₁.beta_unbeta_recSequence_eq {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) (m : ℕ) (hm : m < z + 1) : (Nat.unbeta (Nat.Arith₁.recSequence f g z v)).beta m = Nat.rec (f v) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)) m

theorem Nat.Arith₁.beta_unbeta_recSequence_zero {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) : (Nat.unbeta (Nat.Arith₁.recSequence f g z v)).beta 0 = f v

theorem Nat.Arith₁.beta_unbeta_recSequence_succ {n : ℕ} (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : Mathlib.Vector ℕ n) {m : ℕ} (hm : m < z) : (Nat.unbeta (Nat.Arith₁.recSequence f g z v)).beta (m + 1) = g (m ::ᵥ (Nat.unbeta (Nat.Arith₁.recSequence f g z v)).beta m ::ᵥ v)

theorem Nat.Arith₁.beta_eq_rec {n : ℕ} {m : ℕ} (f : Mathlib.Vector ℕ n → ℕ) (g : Mathlib.Vector ℕ (n + 2) → ℕ) {z : ℕ} {v : Mathlib.Vector ℕ n} (h0 : z.beta 0 = f v) (hs : ∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) : z.beta m = Nat.rec (f v) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)) m

theorem Nat.Arith₁.prec {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ (n + 2) → ℕ} (hf : Nat.Arith₁ f) (hg : Nat.Arith₁ g) : Nat.Arith₁ fun (v : Mathlib.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head

theorem Nat.Arith₁.of_primrec {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (hf : Nat.Primrec' f) : Nat.Arith₁ f

theorem Nat.ArithPart₁.of_partrec {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : Nat.ArithPart₁ f

inductive Nat.ArithPart₁.Code : ℕ → Type

• zero: (n : ℕ) → Nat.ArithPart₁.Code n
• one: (n : ℕ) → Nat.ArithPart₁.Code n
• add: {n : ℕ} → Fin n → Fin n → Nat.ArithPart₁.Code n
• mul: {n : ℕ} → Fin n → Fin n → Nat.ArithPart₁.Code n
• proj: {n : ℕ} → Fin n → Nat.ArithPart₁.Code n
• equal: {n : ℕ} → Fin n → Fin n → Nat.ArithPart₁.Code n
• lt: {n : ℕ} → Fin n → Fin n → Nat.ArithPart₁.Code n
• comp: {m n : ℕ} → Nat.ArithPart₁.Code n → (Fin n → Nat.ArithPart₁.Code m) → Nat.ArithPart₁.Code m
• rfind: {n : ℕ} → Nat.ArithPart₁.Code (n + 1) → Nat.ArithPart₁.Code n

instance Nat.ArithPart₁.instInhabitedCode (k : ℕ) : Inhabited (Nat.ArithPart₁.Code k)

Equations

• Nat.ArithPart₁.instInhabitedCode k = { default := Nat.ArithPart₁.Code.zero k }

inductive Nat.ArithPart₁.Code.eval {n : ℕ} : Nat.ArithPart₁.Code n → (Mathlib.Vector ℕ n →. ℕ) → Prop

• zero: ∀ {n : ℕ}, (Nat.ArithPart₁.Code.zero n).eval fun (x : Mathlib.Vector ℕ n) => 0
• one: ∀ {n : ℕ}, (Nat.ArithPart₁.Code.one n).eval fun (x : Mathlib.Vector ℕ n) => 1
• add: ∀ {n : ℕ} (i j : Fin n), (Nat.ArithPart₁.Code.add i j).eval fun (v : Mathlib.Vector ℕ n) => ↑(some (v.get i + v.get j))
• mul: ∀ {n : ℕ} (i j : Fin n), (Nat.ArithPart₁.Code.mul i j).eval fun (v : Mathlib.Vector ℕ n) => ↑(some (v.get i * v.get j))
• proj: ∀ {n : ℕ} (i : Fin n), (Nat.ArithPart₁.Code.proj i).eval fun (v : Mathlib.Vector ℕ n) => ↑(some (v.get i))
• equal: ∀ {n : ℕ} (i j : Fin n), (Nat.ArithPart₁.Code.equal i j).eval fun (v : Mathlib.Vector ℕ n) => ↑(some ((v.get i).isEqNat (v.get j)))
• lt: ∀ {n : ℕ} (i j : Fin n), (Nat.ArithPart₁.Code.lt i j).eval fun (v : Mathlib.Vector ℕ n) => ↑(some ((v.get i).isLtNat (v.get j)))
• comp: ∀ {m n : ℕ} (c : Nat.ArithPart₁.Code n) (d : Fin n → Nat.ArithPart₁.Code m) (f : Mathlib.Vector ℕ n →. ℕ) (g : Fin n → Mathlib.Vector ℕ m →. ℕ), c.eval f → (∀ (i : Fin n), (d i).eval (g i)) → (c.comp d).eval fun (v : Mathlib.Vector ℕ m) => (Mathlib.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind: ∀ {n : ℕ} (c : Nat.ArithPart₁.Code (n + 1)) (f : Mathlib.Vector ℕ (n + 1) → ℕ), c.eval ↑f → c.rfind.eval fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

theorem Nat.ArithPart₁.exists_code {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} : Nat.ArithPart₁ f → ∃ (c : Nat.ArithPart₁.Code n), c.eval f