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

Equations

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

@[implicit_reducible]

instance instDecidableIs_witness {n b : ℕ} (x : List.Vector (Fin b) n) (q : ℕ) (h : List.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 : List.Vector (Fin b) n) (q : ℕ) : Prop

Equations

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

@[implicit_reducible]

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

Equations

• instDecidableA_N_bounded_by x = Fintype.decidableExistsFintype

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

Equations

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

@[implicit_reducible]

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

Equations

• instDecidableComplexity_equals x k = instDecidableAnd