def slow {n : ℕ} {q : ℕ} (h : Mathlib.Vector (Fin q) n.succ) : Prop

Equations

• slow h = (↑(h.get 0) = 0 ∧ ∀ (j : Fin q), ∃ (i : Fin q), ↑i < (↑j).succ ∧ ↑(h.get ↑(↑j).succ) ≤ ↑(h.get ↑↑i).succ)

instance instDecidableSlow {n : ℕ} (q : ℕ) (h : Mathlib.Vector (Fin q) n.succ) : Decidable (slow h)

Equations

• instDecidableSlow q h = instDecidableAnd

def is_witness {n : ℕ} {b : ℕ} (x : Mathlib.Vector (Fin b) n) (q : ℕ) (h : Mathlib.Vector (Fin q) n.succ) : Prop

Equations

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

instance instDecidableIs_witness {n : ℕ} {b : ℕ} (x : Mathlib.Vector (Fin b) n) (q : ℕ) (h : Mathlib.Vector (Fin q) n.succ) : Decidable (is_witness x q h)

Equations

• instDecidableIs_witness x q h = Fintype.decidableForallFintype

def A_N_bounded_by {n : ℕ} {b : ℕ} (x : Mathlib.Vector (Fin b) n) (q : ℕ) : Prop

Equations

• A_N_bounded_by x q = ∃ (h : Mathlib.Vector (Fin q) n.succ), is_witness x q h

instance instDecidableA_N_bounded_by {n : ℕ} {b : ℕ} {q : ℕ} (x : Mathlib.Vector (Fin b) n) : Decidable (A_N_bounded_by x q)

Equations

• instDecidableA_N_bounded_by x = Fintype.decidableExistsFintype

def complexity_equals {n : ℕ} (x : Mathlib.Vector (Fin 2) n) (k : ℕ) : Prop

Equations

• complexity_equals x k = (A_N_bounded_by x k ∧ ¬A_N_bounded_by x (k - 1))

instance instDecidableComplexity_equals {n : ℕ} (x : Mathlib.Vector (Fin 2) n) (k : ℕ) : Decidable (complexity_equals x k)

Equations

• instDecidableComplexity_equals x k = instDecidableAnd