Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Nice Tree Decompositions of Small Width Are Found in Fixed-Parameter Time`

groundedproofs/Lax117284Proofs/BodlaenderProved.lean · lax-117284

What this proof establishes

no assumptions

def✓Lax117284.Bodlaender

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Bodlaender's theorem with Kloks' niceness for the overall conflict graph of an instance, on a word RAM: the case of Lax117284.BodlaenderGeneral.niceDecompositioncomputableLax117284.BodlaenderGeneral.niceDecomposition_computable, proved there by running the exact Bodlaender–Kloks algorithm on a verified virtual machine, for the graph overallGraphIoverallGraph I on the I.clientsI.clients vertices.