@[simp]

theorem ite_pos_iff {p : Prop} [Decidable p] : (0 < if p then 1 else 0) ↔ p

@[simp]

theorem ite_zero_iff {p : Prop} [Decidable p] : (0 = if p then 1 else 0) ↔ ¬p

@[simp]

theorem Nat.mul_pos_iff {a b : ℕ} : 0 < a * b ↔ 0 < a ∧ 0 < b

inductive Primrec : ℕ → Type

• const {n : ℕ} : ℕ → Primrec n
• succ : Primrec 1
• proj {n : ℕ} : Fin n → Primrec n
• comp {n m : ℕ} : Primrec n → (Fin n → Primrec m) → Primrec m
• prec {n : ℕ} : Primrec n → Primrec (n + 2) → Primrec (n + 1)

@[reducible, inline]

abbrev Primrec.comp₀ {n : ℕ} (f : Primrec 0) : Primrec n

Equations

• f.comp₀ = f.comp []ᵥ

@[reducible, inline]

abbrev Primrec.comp₁ {n : ℕ} (f : Primrec 1) (g : Primrec n) : Primrec n

Equations

• f.comp₁ g = f.comp [g]ᵥ

@[reducible, inline]

abbrev Primrec.comp₂ {n : ℕ} (f : Primrec 2) (g₁ g₂ : Primrec n) : Primrec n

Equations

• f.comp₂ g₁ g₂ = f.comp [g₁, g₂]ᵥ

@[reducible, inline]

abbrev Primrec.comp₃ {n : ℕ} (f : Primrec 3) (g₁ g₂ g₃ : Primrec n) : Primrec n

Equations

• f.comp₃ g₁ g₂ g₃ = f.comp [g₁, g₂, g₃]ᵥ

@[reducible, inline]

abbrev Primrec.comp₄ {n : ℕ} (f : Primrec 4) (g₁ g₂ g₃ g₄ : Primrec n) : Primrec n

Equations

• f.comp₄ g₁ g₂ g₃ g₄ = f.comp [g₁, g₂, g₃, g₄]ᵥ

@[reducible, inline]

abbrev Primrec.comp₅ {n : ℕ} (f : Primrec 5) (g₁ g₂ g₃ g₄ g₅ : Primrec n) : Primrec n

Equations

• f.comp₅ g₁ g₂ g₃ g₄ g₅ = f.comp [g₁, g₂, g₃, g₄, g₅]ᵥ

@[reducible, inline]

abbrev Primrec.comp₆ {n : ℕ} (f : Primrec 6) (g₁ g₂ g₃ g₄ g₅ g₆ : Primrec n) : Primrec n

Equations

• f.comp₆ g₁ g₂ g₃ g₄ g₅ g₆ = f.comp [g₁, g₂, g₃, g₄, g₅, g₆]ᵥ

@[reducible, inline]

abbrev Primrec.zero {n : ℕ} : Primrec n

Equations

• Primrec.zero = Primrec.const 0

def Primrec.eval {n : ℕ} : Primrec n → Vec ℕ n → ℕ

Equations

• (Primrec.const n_3).eval x✝ = n_3
• Primrec.succ.eval v = v.head.succ
• (Primrec.proj i).eval x✝ = x✝ i
• (f.comp g).eval x✝ = f.eval fun (i : Fin n_3) => (g i).eval x✝
• (f.prec g).eval v = Nat.recOn v.head (f.eval v.tail) fun (n ih : ℕ) => g.eval (n ∷ᵥ ih ∷ᵥ v.tail)

instance Primrec.instCoeFunForallVecNat {n : ℕ} : CoeFun (Primrec n) fun (x : Primrec n) => Vec ℕ n → ℕ

Equations

• Primrec.instCoeFunForallVecNat = { coe := Primrec.eval }

@[simp]

theorem Primrec.const_eval {n n✝ : ℕ} {v : Vec ℕ n✝} : (const n).eval v = n

@[simp]

theorem Primrec.succ_eval {v : Vec ℕ 1} : succ.eval v = v.head.succ

@[simp]

theorem Primrec.proj_eval {n✝ : ℕ} {i : Fin n✝} {v : Vec ℕ n✝} : (proj i).eval v = v i

@[simp]

theorem Primrec.comp_eval {a✝ : ℕ} {f : Primrec a✝} {a✝¹ : ℕ} {g : Fin a✝ → Primrec a✝¹} {v : Vec ℕ a✝¹} : (f.comp g).eval v = f.eval fun (i : Fin a✝) => (g i).eval v

@[simp]

theorem Primrec.comp₀_eval {f : Primrec 0} {n✝ : ℕ} {v : Vec ℕ n✝} : f.comp₀.eval v = f.eval []ᵥ

@[simp]

theorem Primrec.comp₁_eval {f : Primrec 1} {a✝ : ℕ} {g : Primrec a✝} {v : Vec ℕ a✝} : (f.comp₁ g).eval v = f.eval [g.eval v]ᵥ

@[simp]

theorem Primrec.comp₂_eval {f : Primrec 2} {a✝ : ℕ} {g₁ g₂ : Primrec a✝} {v : Vec ℕ a✝} : (f.comp₂ g₁ g₂).eval v = f.eval [g₁.eval v, g₂.eval v]ᵥ

@[simp]

theorem Primrec.comp₃_eval {f : Primrec 3} {a✝ : ℕ} {g₁ g₂ g₃ : Primrec a✝} {v : Vec ℕ a✝} : (f.comp₃ g₁ g₂ g₃).eval v = f.eval [g₁.eval v, g₂.eval v, g₃.eval v]ᵥ

@[simp]

theorem Primrec.comp₄_eval {f : Primrec 4} {a✝ : ℕ} {g₁ g₂ g₃ g₄ : Primrec a✝} {v : Vec ℕ a✝} : (f.comp₄ g₁ g₂ g₃ g₄).eval v = f.eval [g₁.eval v, g₂.eval v, g₃.eval v, g₄.eval v]ᵥ

theorem Primrec.prec_eval {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 2)} {v : Vec ℕ (a✝ + 1)} : (f.prec g).eval v = Nat.recOn v.head (f.eval v.tail) fun (n ih : ℕ) => g.eval (n ∷ᵥ ih ∷ᵥ v.tail)

theorem Primrec.prec_eval_zero {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 2)} {v : Vec ℕ a✝} : (f.prec g).eval (0 ∷ᵥ v) = f.eval v

theorem Primrec.prec_eval_succ {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 2)} {n : ℕ} {v : Vec ℕ a✝} : (f.prec g).eval ((n + 1) ∷ᵥ v) = g.eval (n ∷ᵥ (f.prec g).eval (n ∷ᵥ v) ∷ᵥ v)

def Primrec.id : Primrec 1

Equations

• Primrec.id = Primrec.proj 0

@[simp]

theorem Primrec.id_eval {v : Vec ℕ 1} : id.eval v = v 0

def Primrec.swap {n : ℕ} (f : Primrec (n + 2)) : Primrec (n + 2)

Equations

• f.swap = f.comp (Primrec.proj 1 ∷ᵥ Primrec.proj 0 ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ.succ)

@[simp]

theorem Primrec.swap_eval {a✝ : ℕ} {f : Primrec (a✝ + 2)} {v : Vec ℕ (a✝ + 2)} : f.swap.eval v = f.eval (v 1 ∷ᵥ v 0 ∷ᵥ v.tail.tail)

def Primrec.cases {n : ℕ} (f : Primrec n) (g : Primrec (n + 1)) : Primrec (n + 1)

Equations

• f.cases g = f.prec (g.comp (Primrec.proj 0 ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ.succ))

theorem Primrec.cases_eval {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ (a✝ + 1)} : (f.cases g).eval v = Nat.casesOn v.head (f.eval v.tail) fun (n : ℕ) => g.eval (n ∷ᵥ v.tail)

theorem Primrec.cases_eval_zero {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ a✝} : (f.cases g).eval (0 ∷ᵥ v) = f.eval v

theorem Primrec.cases_eval_succ {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {n : ℕ} {v : Vec ℕ a✝} : (f.cases g).eval ((n + 1) ∷ᵥ v) = g.eval (n ∷ᵥ v)

def Primrec.add : Primrec 2

Equations

• Primrec.add = (Primrec.proj 0).prec (Primrec.succ.comp₁ (Primrec.proj 1))

@[simp]

theorem Primrec.add_eval {v : Vec ℕ 2} : add.eval v = v 0 + v 1

def Primrec.mul : Primrec 2

Equations

• Primrec.mul = Primrec.zero.prec (Primrec.add.comp₂ (Primrec.proj 1) (Primrec.proj 2))

@[simp]

theorem Primrec.mul_eval {v : Vec ℕ 2} : mul.eval v = v 0 * v 1

def Primrec.exp : Primrec 2

Equations

• Primrec.exp = ((Primrec.const 1).prec (Primrec.mul.comp₂ (Primrec.proj 1) (Primrec.proj 2))).swap

@[simp]

theorem Primrec.exp_eval {v : Vec ℕ 2} : exp.eval v = v 0 ^ v 1

def Primrec.pred : Primrec 1

Equations

• Primrec.pred = Primrec.zero.prec (Primrec.proj 0)

@[simp]

theorem Primrec.pred_eval {v : Vec ℕ 1} : pred.eval v = (v 0).pred

def Primrec.sub : Primrec 2

Equations

• Primrec.sub = ((Primrec.proj 0).prec (Primrec.pred.comp₁ (Primrec.proj 1))).swap

@[simp]

theorem Primrec.sub_eval {v : Vec ℕ 2} : sub.eval v = v 0 - v 1

def Primrec.sign : Primrec 1

Equations

• Primrec.sign = Primrec.zero.cases (Primrec.const 1)

@[simp]

theorem Primrec.sign_eval {v : Vec ℕ 1} : sign.eval v = if 0 < v 0 then 1 else 0

def Primrec.nsign : Primrec 1

Equations

• Primrec.nsign = (Primrec.const 1).cases (Primrec.const 0)

@[simp]

theorem Primrec.nsign_eval {v : Vec ℕ 1} : nsign.eval v = if v 0 = 0 then 1 else 0

def Primrec.not {n : ℕ} (f : Primrec n) : Primrec n

Equations

• f.not = Primrec.nsign.comp₁ f

@[simp]

theorem Primrec.not_eval_pos_iff {a✝ : ℕ} {f : Primrec a✝} {v : Vec ℕ a✝} : 0 < f.not.eval v ↔ f.eval v = 0

@[simp]

theorem Primrec.not_eval_zero_iff {a✝ : ℕ} {f : Primrec a✝} {v : Vec ℕ a✝} : f.not.eval v = 0 ↔ 0 < f.eval v

def Primrec.and {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.and g = Primrec.mul.comp₂ f g

@[simp]

theorem Primrec.and_eval_pos_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : 0 < (f.and g).eval v ↔ 0 < f.eval v ∧ 0 < g.eval v

@[simp]

theorem Primrec.and_eval_zero_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : (f.and g).eval v = 0 ↔ f.eval v = 0 ∨ g.eval v = 0

def Primrec.andv {n m : ℕ} (f : Vec (Primrec n) m) : Primrec n

Equations

• Primrec.andv f_2 = Primrec.const 1
• Primrec.andv f_2 = f_2.head.and (Primrec.andv f_2.tail)

@[simp]

theorem Primrec.andv_eval_pos_iff {n m : ℕ} {v : Vec ℕ n} {f : Vec (Primrec n) m} : 0 < (andv f).eval v ↔ ∀ (i : Fin m), 0 < (f i).eval v

@[simp]

theorem Primrec.andv_eval_zero_iff {n m : ℕ} {v : Vec ℕ n} {f : Vec (Primrec n) m} : (andv f).eval v = 0 ↔ ∃ (i : Fin m), (f i).eval v = 0

def Primrec.or {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.or g = Primrec.add.comp₂ f g

@[simp]

theorem Primrec.or_eval_pos_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : 0 < (f.or g).eval v ↔ 0 < f.eval v ∨ 0 < g.eval v

@[simp]

theorem Primrec.or_eval_zero_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : (f.or g).eval v = 0 ↔ f.eval v = 0 ∧ g.eval v = 0

def Primrec.orv {n m : ℕ} (f : Vec (Primrec n) m) : Primrec n

Equations

• Primrec.orv f_2 = Primrec.const 0
• Primrec.orv f_2 = f_2.head.or (Primrec.orv f_2.tail)

@[simp]

theorem Primrec.orv_eval_pos_iff {n m : ℕ} {v : Vec ℕ n} {f : Vec (Primrec n) m} : 0 < (orv f).eval v ↔ ∃ (i : Fin m), 0 < (f i).eval v

@[simp]

theorem Primrec.orv_eval_zero_iff {n m : ℕ} {v : Vec ℕ n} {f : Vec (Primrec n) m} : (orv f).eval v = 0 ↔ ∀ (i : Fin m), (f i).eval v = 0

def Primrec.lt {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.lt g = Primrec.sub.comp₂ g f

@[simp]

theorem Primrec.lt_eval_pos_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : 0 < (f.lt g).eval v ↔ f.eval v < g.eval v

@[simp]

theorem Primrec.lt_eval_zero_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : (f.lt g).eval v = 0 ↔ g.eval v ≤ f.eval v

@[reducible, inline]

abbrev Primrec.gt {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.gt g = g.lt f

def Primrec.le {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.le g = Primrec.nsign.comp₁ (g.lt f)

@[simp]

theorem Primrec.le_eval_pos_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : 0 < (f.le g).eval v ↔ f.eval v ≤ g.eval v

@[simp]

theorem Primrec.le_eval_zero_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : (f.le g).eval v = 0 ↔ g.eval v < f.eval v

@[reducible, inline]

abbrev Primrec.ge {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.ge g = g.le f

def Primrec.eq {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.eq g = (f.le g).and (f.ge g)

@[simp]

theorem Primrec.eq_eval_pos_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : 0 < (f.eq g).eval v ↔ f.eval v = g.eval v

@[simp]

theorem Primrec.eq_eval_zero_iff {a✝ : ℕ} {f g : Primrec a✝} {v : Vec ℕ a✝} : (f.eq g).eval v = 0 ↔ f.eval v ≠ g.eval v

@[reducible, inline]

abbrev Primrec.ne {n : ℕ} (f g : Primrec n) : Primrec n

Equations

• f.ne g = (f.eq g).not

def Primrec.cond : Primrec 3

Equations

• Primrec.cond = (Primrec.proj 1).cases (Primrec.proj 1)

@[simp]

theorem Primrec.cond_eval {v : Vec ℕ 3} : cond.eval v = if 0 < v 0 then v 1 else v 2

def Primrec.ite {n : ℕ} (f g h : Primrec n) : Primrec n

Equations

• f.ite g h = Primrec.cond.comp₃ f g h

@[simp]

theorem Primrec.ite_eval {a✝ : ℕ} {f g h : Primrec a✝} {v : Vec ℕ a✝} : (f.ite g h).eval v = if 0 < f.eval v then g.eval v else h.eval v

def Primrec.odd : Primrec 1

Equations

• Primrec.odd = Primrec.zero.prec (Primrec.nsign.comp₁ (Primrec.proj 1))

@[simp]

theorem Primrec.odd_eval {v : Vec ℕ 1} : odd.eval v = if (v 0).bodd = true then 1 else 0

def Primrec.div2 : Primrec 1

Equations

• Primrec.div2 = Primrec.zero.prec ((Primrec.odd.comp₁ (Primrec.proj 0)).ite (Primrec.succ.comp₁ (Primrec.proj 1)) (Primrec.proj 1))

@[simp]

theorem Primrec.div2_eval {v : Vec ℕ 1} : div2.eval v = (v 0).div2

def Primrec.mod : Primrec 2

Equations

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

@[simp]

theorem Primrec.mod_eval {v : Vec ℕ 2} : mod.eval v = v 0 % v 1

def Primrec.max : Primrec 2

Equations

• Primrec.max = ((Primrec.proj 0).le (Primrec.proj 1)).ite (Primrec.proj 1) (Primrec.proj 0)

@[simp]

theorem Primrec.max_eval {v : Vec ℕ 2} : max.eval v = (v 0).max (v 1)

def Primrec.pair : Primrec 2

Equations

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

@[simp]

theorem Primrec.pair_eval {v : Vec ℕ 2} : pair.eval v = Nat.pair (v 0) (v 1)

def Primrec.sqrt : Primrec 1

Equations

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

@[simp]

theorem Primrec.sqrt_eval {v : Vec ℕ 1} : sqrt.eval v = (v 0).sqrt

def Primrec.fst : Primrec 1

Equations

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

@[simp]

theorem Primrec.fst_eval {v : Vec ℕ 1} : fst.eval v = (Nat.unpair (v 0)).1

def Primrec.snd : Primrec 1

Equations

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

@[simp]

theorem Primrec.snd_eval {v : Vec ℕ 1} : snd.eval v = (Nat.unpair (v 0)).2

def Primrec.paired {n : ℕ} (f : Primrec (n + 1)) : Primrec (n + 2)

Equations

• f.paired = f.comp (Primrec.pair.comp₂ (Primrec.proj 0) (Primrec.proj 1) ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ.succ)

@[simp]

theorem Primrec.paired_eval {a✝ : ℕ} {f : Primrec (a✝ + 1)} {v : Vec ℕ (a✝ + 2)} : f.paired.eval v = f.eval (Nat.pair (v 0) (v 1) ∷ᵥ v.tail.tail)

def Primrec.unpaired {n : ℕ} (f : Primrec (n + 2)) : Primrec (n + 1)

Equations

• f.unpaired = f.comp (Primrec.fst.comp₁ (Primrec.proj 0) ∷ᵥ Primrec.snd.comp₁ (Primrec.proj 0) ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ)

@[simp]

theorem Primrec.unpaired_eval {a✝ : ℕ} {f : Primrec (a✝ + 2)} {v : Vec ℕ (a✝ + 1)} : f.unpaired.eval v = f.eval ((Nat.unpair (v 0)).1 ∷ᵥ (Nat.unpair (v 0)).2 ∷ᵥ v.tail)

def Primrec.iterate {n : ℕ} (f : Primrec (n + 1)) : Primrec (n + 2)

Equations

• f.iterate = (Primrec.proj 0).prec (f.comp (Primrec.proj 1 ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ.succ.succ))

theorem Primrec.iterate_eval {a✝ : ℕ} {f : Primrec (a✝ + 1)} {n x : ℕ} {v : Vec ℕ a✝} : f.iterate.eval (n ∷ᵥ x ∷ᵥ v) = (fun (x : ℕ) => f.eval (x ∷ᵥ v))^[n] x

def Primrec.vget : Primrec 2

Equations

• Primrec.vget = Primrec.fst.comp₁ Primrec.snd.iterate.swap

theorem Primrec.vget_eval {n : ℕ} {v : Vec ℕ n} {i : Fin n} : vget.eval [v.paired, ↑i]ᵥ = v i

theorem Primrec.vget_eval' {n i : ℕ} {v : Vec ℕ n} (h : i < n) : vget.eval [v.paired, i]ᵥ = v ⟨i, h⟩

def Primrec.isvec : Primrec 2

Equations

• Primrec.isvec = Primrec.snd.iterate.not

theorem Primrec.isvec_eval_pos_iff {n k : ℕ} : 0 < isvec.eval [n, k]ᵥ ↔ ∃ (v : Vec ℕ n), k = v.paired

def Primrec.vmk {n : ℕ} (f : Primrec (n + 1)) : Primrec (n + 1)

Equations

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

theorem Primrec.vmk_eval {a✝ : ℕ} {f : Primrec (a✝ + 1)} {n : ℕ} {v : Vec ℕ a✝} : f.vmk.eval (n ∷ᵥ v) = Vec.paired fun (i : Fin n) => f.eval (↑i ∷ᵥ v)

def Primrec.vmap {n : ℕ} (f : Primrec (n + 1)) : Primrec (n + 2)

Equations

• f.vmap = (f.comp (Primrec.vget.comp₂ (Primrec.proj 1) (Primrec.proj 0) ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ.succ)).vmk

theorem Primrec.vmap_eval {n a✝ : ℕ} {f : Primrec (a✝ + 1)} {w : Vec ℕ a✝} {v : Vec ℕ n} : f.vmap.eval (n ∷ᵥ v.paired ∷ᵥ w) = Vec.paired fun (i : Fin n) => f.eval (v i ∷ᵥ w)

def Primrec.rcons : Primrec 3

Equations

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

theorem Primrec.rcons_eval {n x : ℕ} {v : Vec ℕ n} : rcons.eval [n, v.paired, x]ᵥ = (v.rcons x).paired

def Primrec.cov {n : ℕ} (f : Primrec (n + 2)) : Primrec (n + 1)

Equations

• f.cov = Primrec.zero.prec (Primrec.rcons.comp₃ (Primrec.proj 0) (Primrec.proj 1) f)

theorem Primrec.cov_eval {n m : ℕ} {v : Vec ℕ n} {f : Primrec (n + 2)} : f.cov.eval (m ∷ᵥ v) = Vec.paired fun (i : Fin m) => f.eval (↑i ∷ᵥ f.cov.eval (↑i ∷ᵥ v) ∷ᵥ v)

def Primrec.covrec {n : ℕ} (f : Primrec (n + 2)) : Primrec (n + 1)

Equations

• f.covrec = Primrec.vget.comp₂ (f.cov.comp (Primrec.succ.comp₁ (Primrec.proj 0) ∷ᵥ fun (x : Fin n) => Primrec.proj x.succ)) (Primrec.proj 0)

theorem Primrec.covrec_eval {n m : ℕ} {v : Vec ℕ n} {f : Primrec (n + 2)} : f.covrec.eval (m ∷ᵥ v) = f.eval (m ∷ᵥ (Vec.paired fun (i : Fin m) => f.covrec.eval (↑i ∷ᵥ v)) ∷ᵥ v)

def Primrec.div : Primrec 2

Equations

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

@[simp]

theorem Primrec.div_eval {v : Vec ℕ 2} : div.eval v = v 0 / v 1

def Primrec.vmap' : Primrec 3

Equations

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

theorem Primrec.vmap'_eval {n m : ℕ} {v : Vec ℕ n} {f : Vec ℕ m} (h : ∀ (i : Fin n), v i < m) : vmap'.eval [n, v.paired, f.paired]ᵥ = Vec.paired fun (i : Fin n) => f ⟨v i, ⋯⟩

def Primrec.vmax : Primrec 2

Equations

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

theorem Primrec.vmax_eval {n : ℕ} {v : Vec ℕ n} : vmax.eval [n, v.paired]ᵥ = v.max

def Primrec.vand : Primrec 2

Equations

• Primrec.vand = (Primrec.vmax.comp₂ (Primrec.proj 0) (Primrec.nsign.vmap.comp₂ (Primrec.proj 0) (Primrec.proj 1))).not

theorem Primrec.vand_eval_pos_iff {n : ℕ} {v : Vec ℕ n} : 0 < vand.eval [n, v.paired]ᵥ ↔ ∀ (i : Fin n), v i > 0

def Primrec.bdMu {n : ℕ} (f : Primrec (n + 1)) : Primrec (n + 1)

Equations

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

theorem Primrec.bdMu_eval_le_self {a✝ : ℕ} {f : Primrec (a✝ + 1)} {m : ℕ} {v : Vec ℕ a✝} : f.bdMu.eval (m ∷ᵥ v) ≤ m

theorem Primrec.bdMu_eval_gt {k a✝ : ℕ} {f : Primrec (a✝ + 1)} {m : ℕ} {v : Vec ℕ a✝} : k < f.bdMu.eval (m ∷ᵥ v) → f.eval (k ∷ᵥ v) = 0

theorem Primrec.bdMu_eval_lt_self {a✝ : ℕ} {f : Primrec (a✝ + 1)} {m : ℕ} {v : Vec ℕ a✝} : f.bdMu.eval (m ∷ᵥ v) < m → f.eval (f.bdMu.eval (m ∷ᵥ v) ∷ᵥ v) > 0

theorem Primrec.bdMu_eval_lt_self_iff {a✝ : ℕ} {f : Primrec (a✝ + 1)} {m : ℕ} {v : Vec ℕ a✝} : f.bdMu.eval (m ∷ᵥ v) < m ↔ ∃ k < m, f.eval (k ∷ᵥ v) > 0

theorem Primrec.bdMu_eval_eq {n m n✝ : ℕ} {v : Vec ℕ n✝} {f : Primrec (n✝ + 1)} : n ≤ m → (∀ k < n, f.eval (k ∷ᵥ v) = 0) → f.eval (n ∷ᵥ v) > 0 → f.bdMu.eval (m ∷ᵥ v) = n

def Primrec.bdExists {n : ℕ} (f : Primrec n) (g : Primrec (n + 1)) : Primrec n

Equations

• f.bdExists g = (g.bdMu.comp (f ∷ᵥ Primrec.proj)).lt f

@[simp]

theorem Primrec.bdExists_eval_pos_iff {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ a✝} : 0 < (f.bdExists g).eval v ↔ ∃ k < f.eval v, 0 < g.eval (k ∷ᵥ v)

@[simp]

theorem Primrec.bdExists_eval_zero_iff {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ a✝} : (f.bdExists g).eval v = 0 ↔ ∀ k < f.eval v, g.eval (k ∷ᵥ v) = 0

def Primrec.bdForall {n : ℕ} (f : Primrec n) (g : Primrec (n + 1)) : Primrec n

Equations

• f.bdForall g = (f.bdExists g.not).not

@[simp]

theorem Primrec.bdForall_eval_pos_iff {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ a✝} : 0 < (f.bdForall g).eval v ↔ ∀ k < f.eval v, 0 < g.eval (k ∷ᵥ v)

@[simp]

theorem Primrec.bdForall_eval_zero_iff {a✝ : ℕ} {f : Primrec a✝} {g : Primrec (a✝ + 1)} {v : Vec ℕ a✝} : (f.bdForall g).eval v = 0 ↔ ∃ k < f.eval v, g.eval (k ∷ᵥ v) = 0

def Primrec.repr {n : ℕ} : Primrec n → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• (Primrec.const n_3).repr x✝ = Std.Format.text "const " ++ Std.Format.text n_3.repr
• Primrec.succ.repr x✝ = Std.Format.text "succ"
• (Primrec.proj i).repr x✝ = Repr.addAppParen (Std.Format.text "proj " ++ reprPrec i Lean.Parser.maxPrec) x✝
• (f.prec g).repr x✝ = Repr.addAppParen (Std.Format.text "prec " ++ f.repr Lean.Parser.maxPrec ++ Std.Format.text " " ++ g.repr Lean.Parser.maxPrec) x✝

instance Primrec.instRepr {n : ℕ} : Repr (Primrec n)

Equations

• Primrec.instRepr = { reprPrec := Primrec.repr }