Lax Lean Archive

Proof of `First-order model checking on monadically dependent graph classes`

groundedproofs/Lax185574Proofs/ModelChecking.lean · lax-185574

What this proof establishes

thm✓Lax185574.ModelChecking

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

In the paper

  • page 15 of this submission's paper

Description

The proof of the main theorem. The algorithm converts the word of the graph into its compressed sparse row form and runs the program of existsprogrammodelCheckingcsrexists_program_modelChecking_csr on it. The conversion takes time linear in the length of the input, which is O(n2)O(n²).