def List.incBoolList' (xs : List Bool) (c : Bool) : List Bool

Equations

• [].incBoolList' c = []
• (x :: xs_2).incBoolList' c = (!x == c) :: xs_2.incBoolList' (x && c)

def List.incBoolList (xs : List Bool) : List Bool

Equations

• xs.incBoolList = xs.incBoolList' true

def List.decideBoolList' (p : List Bool → Bool) (xs : List Bool) (n : ℕ) : Bool

Equations

• List.decideBoolList' p xs 0 = bif !p xs then false else true
• List.decideBoolList' p xs n_2.succ = bif !p xs then false else List.decideBoolList' p xs.incBoolList n_2

def List.decideBoolList (p : List Bool → Bool) (n : ℕ) : Bool

Equations

• List.decideBoolList p n = List.decideBoolList' p (List.replicate n false) (2 ^ n)

def List.BoolListFinset' (xs : List Bool) (n : ℕ) : Finset (List Bool)

Equations

• xs.BoolListFinset' 0 = insert xs ∅
• xs.BoolListFinset' n_2.succ = insert xs (xs.incBoolList.BoolListFinset' n_2)

def List.BoolListFinset (n : ℕ) : Finset (List Bool)

Equations

• List.BoolListFinset n = (List.replicate n false).BoolListFinset' (2 ^ n)

@[simp]

theorem List.length_incBoolList' {xs : List Bool} {c : Bool} : (xs.incBoolList' c).length = xs.length

@[simp]

theorem List.length_incBoolList {xs : List Bool} : xs.incBoolList.length = xs.length

theorem List.decideBoolList_of {p : List Bool → Prop} [hp : DecidablePred p] {n : ℕ} (h : ∀ (xs : List Bool), xs.length = n → p xs) : decideBoolList (fun (b : List Bool) => decide (p b)) n = true

@[simp]

theorem List.incBoolList_nil : [].incBoolList = []

@[simp]

theorem List.decideBoolList_zero {p : List Bool → Prop} [hp : DecidablePred p] : decideBoolList (fun (b : List Bool) => decide (p b)) 0 = decide (p [])

@[simp]

theorem List.BoolListFinset_zero : BoolListFinset 0 = {[]}

theorem List.of_mem_BoolListFinset {xs : List Bool} {n : ℕ} (h : xs ∈ BoolListFinset n) : xs.length = n

theorem List.self_mem_BoolListFinset' {xs : List Bool} {n : ℕ} : xs ∈ xs.BoolListFinset' n

theorem List.BoolListFinset'_add {xs : List Bool} {n k : ℕ} : xs.BoolListFinset' (n + k) = xs.BoolListFinset' n ∪ (incBoolList^[n] xs).BoolListFinset' k

theorem List.mem_BoolListFinset'_iff_exi_iter {zs xs : List Bool} {n : ℕ} : xs ∈ zs.BoolListFinset' n ↔ ∃ k ≤ n, xs = incBoolList^[k] zs

theorem List.incBoolList'_prefix_of_prefix {xs ys : List Bool} {c : Bool} (h : xs <+: ys) : xs.incBoolList' c <+: ys.incBoolList' c

theorem List.incBoolList_prefix_of_prefix {xs ys : List Bool} (h : xs <+: ys) : xs.incBoolList <+: ys.incBoolList

theorem List.iter_incBoolList_prefix_of_prefix {xs ys : List Bool} {k : ℕ} (h : xs <+: ys) : incBoolList^[k] xs <+: incBoolList^[k] ys

@[simp]

theorem List.incBoolList'_false {xs : List Bool} : xs.incBoolList' false = xs

@[simp]

theorem List.incBoolList_false_cons {xs : List Bool} : (false :: xs).incBoolList = true :: xs

@[simp]

theorem List.incBoolList_true_cons {xs : List Bool} : (true :: xs).incBoolList = false :: xs.incBoolList

@[simp]

theorem List.incBoolList_incBoolList_cons {x : Bool} {xs : List Bool} : (x :: xs).incBoolList.incBoolList = x :: xs.incBoolList

@[simp]

theorem List.iter_incBoolList_cons_mul_two {x : Bool} {xs : List Bool} {k : ℕ} : incBoolList^[k * 2] (x :: xs) = x :: incBoolList^[k] xs

@[simp]

theorem List.iter_incBoolList_nil {k : ℕ} : incBoolList^[k] [] = []

@[simp]

theorem List.iter_incBoolList_two_pow {xs : List Bool} {k : ℕ} : incBoolList^[2 ^ k] xs = take k xs ++ (drop k xs).incBoolList

theorem List.mem_BoolListFinset_of {xs : List Bool} {n : ℕ} (h : xs.length = n) : xs ∈ BoolListFinset n

theorem List.mem_BoolListFinset_iff_length_eq {xs : List Bool} {n : ℕ} : xs ∈ BoolListFinset n ↔ xs.length = n

theorem List.mem_BoolListFinset_iff_exi_iter {xs : List Bool} {n : ℕ} : xs ∈ BoolListFinset n ↔ ∃ k ≤ 2 ^ n, xs = incBoolList^[k] (replicate n false)

theorem List.decideBoolList_iff_forall_mem_BoolListFinset {p : List Bool → Prop} [hp : DecidablePred p] {n : ℕ} : decideBoolList (fun (b : List Bool) => decide (p b)) n = true ↔ ∀ xs ∈ BoolListFinset n, p xs

theorem List.of_decideBoolList {p : List Bool → Prop} [hp : DecidablePred p] {xs : List Bool} {n : ℕ} (hn : xs.length = n) (h : decideBoolList (fun (b : List Bool) => decide (p b)) n = true) : p xs

theorem List.decideBoolList_iff {p : List Bool → Prop} [hp : DecidablePred p] {n : ℕ} : decideBoolList (fun (b : List Bool) => decide (p b)) n = true ↔ ∀ (xs : List Bool), xs.length = n → p xs

@[instance_reducible]

instance List.instDecidableForallForallEqNatLengthBoolOfDecidablePred_projects {p : List Bool → Prop} [hp : DecidablePred p] {n : ℕ} : Decidable (∀ (xs : List Bool), xs.length = n → p xs)

Equations

• List.instDecidableForallForallEqNatLengthBoolOfDecidablePred_projects = decidable_of_bool (List.decideBoolList (fun (b : List Bool) => decide (p b)) n) ⋯