Every Boolean function has a circuit

The formula of a Boolean function on N bits from its truth table (Fml.table): a mux tree on the bits, of size at most 7 · 2^N. Its circuit is well-formed (Fml.toCircuit_wellFormed) and computes the function (Fml.eval_table). This is how the check circuit of the Cook–Levin tableau of the interpreter machine is obtained: from the truth table of the local check predicate, as in the paper's lem:pack-check-size (planning/succinct-cook-levin.md, S3).

def MIPRE.SAT.Fml.table (N : ℕ) : ((Fin N → Bool) → Bool) → Fml

The formula of a Boolean function on N bits: a mux tree on the bits, the leaves being the entries of the truth table.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.SAT.Fml.table 0 f = MIPRE.SAT.Fml.const (f Fin.elim0)

theorem MIPRE.SAT.Fml.eval_table (N : ℕ) (f : (Fin N → Bool) → Bool) (x : ℕ → Bool) : eval x (table N f) = f fun (i : Fin N) => x ↑i

theorem MIPRE.SAT.Fml.table_inputsLt (N : ℕ) (f : (Fin N → Bool) → Bool) : InputsLt N (table N f)

theorem MIPRE.SAT.Fml.size_table (N : ℕ) (f : (Fin N → Bool) → Bool) : (table N f).size + 6 ≤ 7 * 2 ^ N

theorem MIPRE.SAT.Fml.exists_circuit (N : ℕ) (f : (Fin N → Bool) → Bool) : ∃ (C : Circuit), C.WellFormed ∧ C.inputs = N ∧ C.size ≤ 7 * 2 ^ N ∧ ∀ (x : Fin N → Bool), C.evalBits (List.ofFn x) = f x

Every Boolean function on N bits is computed by a well-formed circuit on N inputs of at most 7 · 2^N gates.