Supporting results for pointwise provable equality.

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

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

The is Eq Nat construction in Nat.

Equations

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

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

The is Lt Nat construction in Nat.

Equations

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

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

The is Le Nat construction in Nat.

Equations

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

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

The is Dvd Nat construction in Nat.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def PointwiseComposition.Nat.inv (n : ℕ) : ℕ

The inv construction in Nat.

Equations

• PointwiseComposition.Nat.inv n = PointwiseComposition.Nat.isEqNat n 0

def PointwiseComposition.Nat.pos (n : ℕ) : ℕ

The pos construction in Nat.

Equations

• PointwiseComposition.Nat.pos n = PointwiseComposition.Nat.isLtNat 0 n

@[simp]

theorem PointwiseComposition.Nat.inv_zero : inv 0 = 1

@[simp]

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

@[simp]

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

@[simp]

theorem PointwiseComposition.Nat.pos_zero : pos 0 = 0

@[simp]

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

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

The and construction in Nat.

Equations

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

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

The or construction in Nat.

Equations

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def PointwiseComposition.Nat.ball (n : ℕ) (φ : ℕ → ℕ) : ℕ

The ball construction in Nat.

Equations

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

@[simp]

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

@[simp]

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

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

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

Data and laws for Arith Part₁ in Nat.

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

def PointwiseComposition.Nat.Arithmetic₁ {n : ℕ} (f : List.Vector ℕ n → ℕ) : Prop

The Arithmetic₁ construction in Nat.

Equations

• PointwiseComposition.Nat.Arithmetic₁ f = PointwiseComposition.Nat.ArithPart₁ ↑f

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

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

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

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

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

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

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

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

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

theorem PointwiseComposition.Nat.Arithmetic₁.zero {n : ℕ} : Arithmetic₁ fun (x : List.Vector ℕ n) => 0

theorem PointwiseComposition.Nat.Arithmetic₁.one {n : ℕ} : Arithmetic₁ fun (x : List.Vector ℕ n) => 1

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

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

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

theorem PointwiseComposition.Nat.Arithmetic₁.head {n : ℕ} : Arithmetic₁ fun (v : List.Vector ℕ (n + 1)) => v.head

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

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

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

def PointwiseComposition.Nat.Arithmetic₁.Vec {n m : ℕ} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop

The Vec construction in Nat.Arithmetic₁.

Equations

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

theorem PointwiseComposition.Nat.Arithmetic₁.nil {n : ℕ} : Vec fun (x : List.Vector ℕ n) => List.Vector.nil

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

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

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

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

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

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

theorem PointwiseComposition.Nat.Arithmetic₁.const {n : ℕ} (m : ℕ) : Arithmetic₁ fun (x : List.Vector ℕ n) => m

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem PointwiseComposition.Nat.Arithmetic₁.ball {n : ℕ} {φ : List.Vector ℕ n → ℕ → ℕ} (hp : Arithmetic₁ fun (v : List.Vector ℕ (n + 1)) => φ v.tail v.head) (i : Fin n) : Arithmetic₁ fun (v : List.Vector ℕ n) => Nat.ball (v.get i) (φ v)

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

The rec Sequence construction in Nat.Arithmetic₁.

Equations

• PointwiseComposition.Nat.Arithmetic₁.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 PointwiseComposition.Nat.Arithmetic₁.beta_unbeta_recSequence_eq {n : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) (z : ℕ) (v : List.Vector ℕ n) (m : ℕ) (hm : m < z + 1) : (Nat.unbeta (recSequence f g z v)).beta m = Nat.rec (f v) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v)) m

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

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

theorem PointwiseComposition.Nat.Arithmetic₁.beta_eq_rec {n m : ℕ} (f : List.Vector ℕ n → ℕ) (g : List.Vector ℕ (n + 2) → ℕ) {z : ℕ} {v : List.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 PointwiseComposition.Nat.Arithmetic₁.prec {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} (hf : Arithmetic₁ f) (hg : Arithmetic₁ g) : Arithmetic₁ fun (v : List.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head

theorem PointwiseComposition.Nat.Arithmetic₁.of_primrec {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Nat.Primrec' f) : Arithmetic₁ f

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

inductive PointwiseComposition.Nat.ArithPart₁.Code : ℕ → Type

Data and laws for Code in Nat.ArithPart₁.

• zero (n : ℕ) : Code n
• one (n : ℕ) : Code n
• add {n : ℕ} (i j : Fin n) : Code n
• mul {n : ℕ} (i j : Fin n) : Code n
• proj {n : ℕ} (i : Fin n) : Code n
• equal {n : ℕ} (i j : Fin n) : Code n
• lt {n : ℕ} (i j : Fin n) : Code n
• comp {m n : ℕ} : Code n → (Fin n → Code m) → Code m
• rfind {n : ℕ} : Code (n + 1) → Code n

@[instance_reducible]

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

Equations

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

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

Data and laws for eval in Nat.ArithPart₁.Code.

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

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