Prove2Me

Boolean-to-symbol encoding distributes over conjunction

Proved
boolSym_and

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

The boolean-to-symbol encoding distributes over conjunction: encoding the AND of two booleans equals the conditional encoding based on the first boolean.

Formal statement
import Definitions.Def_CookLevin_Cost

open CookLevin

theorem boolSym_and (b1 b2 : Bool) :
    boolSym (b1 && b2) = if b1 then boolSym b2 else zeroSymbol := by sorry

View graph