Encoding formula concatenation splices terminal delimiters

Proved

CookLevin.encodeFormula_append

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

cnf-encodingcook-levinlist-identity

For any two CNF formulas $\varphi$ and $\psi$ , encoding their concatenation is obtained by removing the unique terminal delimiter from the encoding of $\varphi$ and appending the encoding of $\psi$ .

This identity isolates the exact stream-splicing invariant needed to assemble separately emitted Cook-Levin clause families.

Formal statement

import Definitions.Def_CookLevin_Satisfiability
open CookLevin

theorem CookLevin.encodeFormula_append (φ ψ : Formula) :
    encodeFormula (φ ++ ψ) =
      (encodeFormula φ).dropLast ++ encodeFormula ψ := by sorry

Source

Exact encoding definitions in CookLevin_Satisfiability and decomposition of https://prove2.me/theorems/52bfe0b2-676b-48d9-a6ee-9a495cd865fb

View graph